LeanPool.AsymptoticTrianglePacking.Internal — the Efron–Stein (bounded-differences) variance

inequality on a finite Bernoulli cube

This file is elementary and self-contained: no measure theory, only Finset sums. For a finite index type ι and p ∈ [0,1] the Bernoulli cube is the finite set ι → Bool weighted by

wt p ω = ∏ i, (if ω i then p else 1 − p),

with expectation Exp p f = ∑ ω, wt p ω · f ω. The main result is

LeanPool.AsymptoticTrianglePacking.Internal.Cube.variance_le_sum_sq_diff : Exp p f² − (Exp p f)² ≤ ∑ i, p(1−p)·Exp p ((D i f)²),

where D i f ω = f (ω[i ↦ true]) − f (ω[i ↦ false]) is the discrete derivative in coordinate i. This is the Efron–Stein / tensorization-of-variance inequality; Mathlib has no form of it.

The proof is the usual one-coordinate-at-a-time argument, organised through the averaging operator avgOne p i f ω = p·f (ω[i ↦ true]) + (1−p)·f (ω[i ↦ false]), which satisfies

• Exp p (avgOne p i f) = Exp p f,
• Exp p f² − Exp p (avgOne p i f)² = p(1−p)·Exp p ((D i f)²) (the exact one-coordinate variance decomposition), and hence Exp p (avgOne p i f)² ≤ Exp p f²,
• D i (avgOne p j f) = avgOne p j (D i f) for i ≠ j.

Averaging over a duplicate-free list exhausting ι turns f into the constant Exp p f, and the telescoping sum of the second bullet is exactly the statement.

The weighted cube

def LeanPool.AsymptoticTrianglePacking.Internal.Cube.wt {ι : Type u_1} [Fintype ι] (p : ℝ) (ω : ι → Bool) : ℝ

The Bernoulli(p) weight of a configuration of the cube ι → Bool.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.Cube.wt p ω = ∏ i : ι, if ω i = true then p else 1 - p

def LeanPool.AsymptoticTrianglePacking.Internal.Cube.wtc {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (p : ℝ) (ω : ι → Bool) : ℝ

The Bernoulli(p) weight with coordinate i omitted.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.Cube.wtc i p ω = ∏ j ∈ Finset.univ.erase i, if ω j = true then p else 1 - p

def LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (f : (ι → Bool) → ℝ) : ℝ

The expectation of f on the Bernoulli(p) cube.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp p f = ∑ ω : ι → Bool, LeanPool.AsymptoticTrianglePacking.Internal.Cube.wt p ω * f ω

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.wt_nonneg {ι : Type u_1} [Fintype ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (ω : ι → Bool) : 0 ≤ wt p ω

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.wtc_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (i : ι) (ω : ι → Bool) : 0 ≤ wtc i p ω

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.sum_wt {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} : ∑ ω : ι → Bool, wt p ω = 1

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.wt_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (p : ℝ) (ω : ι → Bool) : wt p ω = (if ω i = true then p else 1 - p) * wtc i p ω

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.wtc_update {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (p : ℝ) (ω : ι → Bool) (b : Bool) : wtc i p (Function.update ω i b) = wtc i p ω

The one-coordinate averaging operator

def LeanPool.AsymptoticTrianglePacking.Internal.Cube.D {ι : Type u_1} [DecidableEq ι] (i : ι) (f : (ι → Bool) → ℝ) (ω : ι → Bool) : ℝ

The discrete derivative of f in coordinate i.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.Cube.D i f ω = f (Function.update ω i true) - f (Function.update ω i false)

def LeanPool.AsymptoticTrianglePacking.Internal.Cube.avgOne {ι : Type u_1} [DecidableEq ι] (p : ℝ) (i : ι) (f : (ι → Bool) → ℝ) (ω : ι → Bool) : ℝ

Averaging f over coordinate i.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.Cube.avgOne p i f ω = p * f (Function.update ω i true) + (1 - p) * f (Function.update ω i false)

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.avgOne_update {ι : Type u_1} [DecidableEq ι] (p : ℝ) (i : ι) (f : (ι → Bool) → ℝ) (ω : ι → Bool) (b : Bool) : avgOne p i f (Function.update ω i b) = avgOne p i f ω

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.D_update {ι : Type u_1} [DecidableEq ι] (i : ι) (f : (ι → Bool) → ℝ) (ω : ι → Bool) (b : Bool) : D i f (Function.update ω i b) = D i f ω

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.sum_split {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (g : (ι → Bool) → ℝ) : ∑ ω : ι → Bool, g ω = ∑ ω : ι → Bool with ω i = false, (g ω + g (Function.update ω i true))

The basic splitting of a cube sum along one coordinate.

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_split {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (i : ι) (f : (ι → Bool) → ℝ) : Exp p f = ∑ ω : ι → Bool with ω i = false, wtc i p ω * ((1 - p) * f ω + p * f (Function.update ω i true))

The expectation, split along one coordinate.

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_avgOne {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (i : ι) (f : (ι → Bool) → ℝ) : Exp p (avgOne p i f) = Exp p f

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_sq_sub_avgOne {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (i : ι) (f : (ι → Bool) → ℝ) : ((Exp p fun (ω : ι → Bool) => f ω ^ 2) - Exp p fun (ω : ι → Bool) => avgOne p i f ω ^ 2) = p * (1 - p) * Exp p fun (ω : ι → Bool) => D i f ω ^ 2

The exact one-coordinate variance decomposition.

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_sq_avgOne_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (i : ι) (f : (ι → Bool) → ℝ) : (Exp p fun (ω : ι → Bool) => avgOne p i f ω ^ 2) ≤ Exp p fun (ω : ι → Bool) => f ω ^ 2

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.D_avgOne_comm {ι : Type u_1} [DecidableEq ι] {i j : ι} (hij : i ≠ j) (p : ℝ) (f : (ι → Bool) → ℝ) : D i (avgOne p j f) = avgOne p j (D i f)

Averaging over a list of coordinates

def LeanPool.AsymptoticTrianglePacking.Internal.Cube.avgL {ι : Type u_1} [DecidableEq ι] (p : ℝ) : List ι → ((ι → Bool) → ℝ) → (ι → Bool) → ℝ

Averaging over every coordinate in a list.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.Cube.avgL p [] x✝ = x✝
• LeanPool.AsymptoticTrianglePacking.Internal.Cube.avgL p (i :: t) x✝ = LeanPool.AsymptoticTrianglePacking.Internal.Cube.avgOne p i (LeanPool.AsymptoticTrianglePacking.Internal.Cube.avgL p t x✝)

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_avgL {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (l : List ι) (f : (ι → Bool) → ℝ) : Exp p (avgL p l f) = Exp p f

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_sq_avgL_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (l : List ι) (f : (ι → Bool) → ℝ) : (Exp p fun (ω : ι → Bool) => avgL p l f ω ^ 2) ≤ Exp p fun (ω : ι → Bool) => f ω ^ 2

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.D_avgL_comm {ι : Type u_1} [DecidableEq ι] {i : ι} {l : List ι} (hi : i ∉ l) (p : ℝ) (f : (ι → Bool) → ℝ) : D i (avgL p l f) = avgL p l (D i f)

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.avgL_congr {ι : Type u_1} [DecidableEq ι] (p : ℝ) (l : List ι) (f : (ι → Bool) → ℝ) {ω ω' : ι → Bool} (h : ∀ j ∉ l, ω j = ω' j) : avgL p l f ω = avgL p l f ω'

If ω and ω' agree off l, then avgL p l f takes the same value at both.

The Efron–Stein inequality

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_const {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p c : ℝ) : (Exp p fun (x : ι → Bool) => c) = c

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.variance_le_of_list {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (l : List ι) (hl : l.Nodup) (f : (ι → Bool) → ℝ) : ((Exp p fun (ω : ι → Bool) => f ω ^ 2) - Exp p fun (ω : ι → Bool) => avgL p l f ω ^ 2) ≤ (List.map (fun (i : ι) => p * (1 - p) * Exp p fun (ω : ι → Bool) => D i f ω ^ 2) l).sum

Telescoping the one-coordinate decomposition along a duplicate-free list.

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.variance_le_sum_sq_diff {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (f : (ι → Bool) → ℝ) : (Exp p fun (ω : ι → Bool) => f ω ^ 2) - Exp p f ^ 2 ≤ ∑ i : ι, p * (1 - p) * Exp p fun (ω : ι → Bool) => D i f ω ^ 2

Efron–Stein on the Bernoulli cube. The variance of f is at most p(1−p) times the sum over coordinates of the mean square discrete derivative.

Linearity, products and the variance identity

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_prod {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (g : ι → Bool → ℝ) : (Exp p fun (ω : ι → Bool) => ∏ i : ι, g i (ω i)) = ∏ i : ι, (p * g i true + (1 - p) * g i false)

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_centred_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (f : (ι → Bool) → ℝ) : (Exp p fun (ω : ι → Bool) => (f ω - Exp p f) ^ 2) = (Exp p fun (ω : ι → Bool) => f ω ^ 2) - Exp p f ^ 2

The centred second moment of f is Exp f² − (Exp f)².

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.centred_sq_le_sum_sq_diff {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (f : (ι → Bool) → ℝ) : (Exp p fun (ω : ι → Bool) => (f ω - Exp p f) ^ 2) ≤ ∑ i : ι, p * (1 - p) * Exp p fun (ω : ι → Bool) => D i f ω ^ 2

Efron–Stein, in centred form.

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_mono {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {f g : (ι → Bool) → ℝ} (h : ∀ (ω : ι → Bool), f ω ≤ g ω) : Exp p f ≤ Exp p g

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {f : (ι → Bool) → ℝ} (h : ∀ (ω : ι → Bool), 0 ≤ f ω) : 0 ≤ Exp p f

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_add {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (f g : (ι → Bool) → ℝ) : (Exp p fun (ω : ι → Bool) => f ω + g ω) = Exp p f + Exp p g

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_smul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p c : ℝ) (f : (ι → Bool) → ℝ) : (Exp p fun (ω : ι → Bool) => c * f ω) = c * Exp p f

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_finset_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} (p : ℝ) (s : Finset α) (g : α → (ι → Bool) → ℝ) : (Exp p fun (ω : ι → Bool) => ∑ a ∈ s, g a ω) = ∑ a ∈ s, Exp p (g a)

Second moments of weighted sums of coordinates

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_coord_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (f g : ι) : (Exp p fun (ω : ι → Bool) => (if ω f = true then 1 else 0) * if ω g = true then 1 else 0) = if f = g then p else p ^ 2

The pair correlation of two coordinate indicators: p on the diagonal, p² off it.

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_weighted_sum_sq_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (M : Finset ι) (w : ι → ℝ) : (Exp p fun (ω : ι → Bool) => (∑ f ∈ M, if ω f = true then w f else 0) ^ 2) ≤ p * ∑ f ∈ M, w f ^ 2 + p ^ 2 * (∑ f ∈ M, w f) ^ 2

The second moment of a nonnegatively weighted sum of coordinate indicators.

LeanPool.AsymptoticTrianglePacking.Internal — stability of the covered set under a single-edge

flip

The one remaining analytic input of the tight-band nibble (see LeanPool.AsymptoticTrianglePacking.Internal.Tight.SharpRound) is the SHARP per-vertex safe-degree variance bound

Var(safeDeg(v)) ≤ C(r)·(γΔ + κγΔ),

i.e. a bound with NO term of the shape c·γ^a·Δ². The Bonferroni route of LeanPool.AsymptoticTrianglePacking.Internal.Tight.SafeDegreeVariance leaves a residue Θ(γ³Δ²), which is a constant factor (depending on the target β) too large to iterate.

This file provides the key COMBINATORIAL input of the bounded-differences (Efron–Stein) route to that bound: the round's covered set is locally stable — flipping the retention status of a single edge e only moves vertices that lie on e itself or on a retained edge meeting e.

Concretely, with

flipInfluence R e = insert e (R.filter (fun f => ¬ Disjoint f e)),

LeanPool.AsymptoticTrianglePacking.Internal.mem_roundMatching_insert_iff_erase says that every edge outside flipInfluence R e belongs to roundMatching (insert e R) exactly when it belongs to roundMatching (R.erase e), and hence LeanPool.AsymptoticTrianglePacking.Internal.covered_insert_sdiff_subset / LeanPool.AsymptoticTrianglePacking.Internal.covered_erase_sdiff_subset bound the symmetric difference of the two covered sets by ⋃ (flipInfluence R e). For an r-uniform hypergraph this has at most r·(1 + #{f ∈ R : f meets e}) vertices (LeanPool.AsymptoticTrianglePacking.Internal.card_biUnion_flipInfluence_le), so the safe degree at v moves by at most ∑_{u} codeg(v,u) over that set (LeanPool.AsymptoticTrianglePacking.Internal.abs_safeDegree_sub_le_codegree_sum).

Summing p·𝔼[(ΔsafeDeg)²] over the edges e and using ∑_{u ≠ v} codeg(v,u)² ≤ κ(r−1)deg(v) gives exactly O_r(γΔ(1 + κ)), the sharp bound — the arithmetic is recorded in the header of LeanPool.AsymptoticTrianglePacking.Internal.Tight.SharpRound.

placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

The influence set of a single edge

def LeanPool.AsymptoticTrianglePacking.Internal.flipInfluence {V : Type u_1} [DecidableEq V] (R : Finset (Finset V)) (e : Finset V) : Finset (Finset V)

The edges whose membership in the round matching can be affected by flipping the retention status of e: the edge e itself, and the retained edges meeting e.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.flipInfluence R e = insert e ({f ∈ R | ¬Disjoint f e})

theorem LeanPool.AsymptoticTrianglePacking.Internal.notMem_flipInfluence_ne {V : Type u_1} [DecidableEq V] {R : Finset (Finset V)} {e f : Finset V} (hf : f ∉ flipInfluence R e) : f ≠ e

theorem LeanPool.AsymptoticTrianglePacking.Internal.notMem_flipInfluence_disjoint {V : Type u_1} [DecidableEq V] {R : Finset (Finset V)} {e f : Finset V} (hf : f ∉ flipInfluence R e) (hfR : f ∈ R) : Disjoint f e

theorem LeanPool.AsymptoticTrianglePacking.Internal.mem_roundMatching_insert_iff_erase {V : Type u_1} [DecidableEq V] {R : Finset (Finset V)} {e f : Finset V} (hf : f ∉ flipInfluence R e) : f ∈ Hypergraph.roundMatching (insert e R) ↔ f ∈ Hypergraph.roundMatching (R.erase e)

Local stability of the round matching. An edge outside the influence set of e is in the round matching of insert e R exactly when it is in the round matching of R.erase e.

Stability of the covered set

theorem LeanPool.AsymptoticTrianglePacking.Internal.covered_insert_sdiff_subset {V : Type u_1} [DecidableEq V] (R : Finset (Finset V)) (e : Finset V) : Hypergraph.covered (insert e R) \ Hypergraph.covered (R.erase e) ⊆ (flipInfluence R e).biUnion id

theorem LeanPool.AsymptoticTrianglePacking.Internal.covered_erase_sdiff_subset {V : Type u_1} [DecidableEq V] (R : Finset (Finset V)) (e : Finset V) : Hypergraph.covered (R.erase e) \ Hypergraph.covered (insert e R) ⊆ (flipInfluence R e).biUnion id

theorem LeanPool.AsymptoticTrianglePacking.Internal.card_biUnion_flipInfluence_le {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {r : ℕ} (hunif : Hypergraph.IsUniform H r) {R : Finset (Finset V)} (hRH : R ⊆ H) {e : Finset V} (he : e ∈ H) : ((flipInfluence R e).biUnion id).card ≤ r * (1 + {f ∈ R | ¬Disjoint f e}.card)

The flip only moves few vertices. For an r-uniform hypergraph the influence set of e spans at most r·(1 + #{f ∈ R : f meets e}) vertices.

The safe degree moves by at most a codegree sum

theorem LeanPool.AsymptoticTrianglePacking.Internal.abs_safeDegree_sub_le_card_meeting {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {C C' D : Finset V} {v : V} (hCC' : C \ C' ⊆ D) (hC'C : C' \ C ⊆ D) : (↑(safeDegree H C v) - ↑(safeDegree H C' v)).natAbs ≤ {e ∈ H | v ∈ e ∧ ¬Disjoint (e.erase v) D}.card

If two covered sets differ only inside D, the safe degrees at v differ by at most the number of edges at v meeting D away from v.

theorem LeanPool.AsymptoticTrianglePacking.Internal.card_meeting_le_codegree_sum {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {D : Finset V} {v : V} : {e ∈ H | v ∈ e ∧ ¬Disjoint (e.erase v) D}.card ≤ ∑ u ∈ D.erase v, Hypergraph.codegree H v u

The number of edges at v meeting a set D away from v is at most ∑_{u ∈ D} codeg(v,u).

theorem LeanPool.AsymptoticTrianglePacking.Internal.abs_safeDegree_sub_le_codegree_sum {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {C C' D : Finset V} {v : V} (hCC' : C \ C' ⊆ D) (hC'C : C' \ C ⊆ D) : (↑(safeDegree H C v) - ↑(safeDegree H C' v)).natAbs ≤ ∑ u ∈ D.erase v, Hypergraph.codegree H v u

The bounded-differences estimate for the safe degree. If the covered sets C, C' differ only inside D, then the safe degrees at v differ by at most ∑_{u ∈ D \ {v}} codeg(v,u).

theorem LeanPool.AsymptoticTrianglePacking.Internal.abs_safeDegree_flip_le {V : Type u_1} [DecidableEq V] (H R : Finset (Finset V)) (e : Finset V) (v : V) : (↑(safeDegree H (Hypergraph.covered (insert e R)) v) - ↑(safeDegree H (Hypergraph.covered (R.erase e)) v)).natAbs ≤ ∑ u ∈ ((flipInfluence R e).biUnion id).erase v, Hypergraph.codegree H v u

The safe degree is stable under a single-edge flip. Flipping the retention status of e changes the safe degree at v by at most the codegree sum over the vertices spanned by the influence set of e.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sum_sq_codegree_le {V : Type u_1} [DecidableEq V] [Fintype V] {H : Finset (Finset V)} {r : ℕ} (hr : Hypergraph.IsUniform H r) {κ : ℝ} (v : V) (hκ : ∀ (u : V), u ≠ v → ↑(Hypergraph.codegree H v u) ≤ κ) : ∑ u ∈ Finset.univ.erase v, ↑(Hypergraph.codegree H v u) ^ 2 ≤ κ * ↑((r - 1) * Hypergraph.degree H v)

The squared codegree sum. With all codegrees at v bounded by κ, ∑_{u ≠ v} codeg(v,u)² ≤ κ·(r−1)·deg(v) — the weight that drives the Efron–Stein estimate.

LeanPool.AsymptoticTrianglePacking.Internal — the SHARP per-vertex safe-degree variance

This is the one analytic input the iterable nibble round was missing. The Bonferroni route of LeanPool.AsymptoticTrianglePacking.Internal.Tight.SafeDegreeVariance bounds the variance of safeDeg(v) by Δ²((r−1)²ε₂ + 2(r−1)³q_hi(q_hi²+ε₂)) + q_hi κ(r−1)Δ ≈ 2γ³Δ²; the Θ(γ³Δ²) residue is a constant factor too large to iterate. Here we prove the sharp bound

Var(safeDeg(v)) ≤ 2p·r²κΔ²·(1 + prΔ + (prΔ)²),

i.e. ≈ 2rγκΔ at the nibble retention p = γ/(rΔ) — with NO Δ² term.

The route is bounded differences (Efron–Stein). Everything happens on the explicit Bernoulli cube Finset V → Bool of LeanPool.AsymptoticTrianglePacking.Internal.Tight.CubeVariance, where the Efron–Stein inequality LeanPool.AsymptoticTrianglePacking.Internal.Cube.centred_sq_le_sum_sq_diff is available. The combinatorial input is LeanPool.AsymptoticTrianglePacking.Internal.Tight.FlipStability: flipping the retention of a single edge k moves the covered set only inside k ∪ ⋃ {f ∈ R : f meets k}, so the safe degree at v moves by at most

edgeWeight k + ∑_{f ∈ R, f meets k} edgeWeight f, edgeWeight f = ∑_{u ∈ f∖v} codeg(v,u).

Squaring, taking expectations and summing over k produces exactly the three terms above.

The cube picture of a round

def LeanPool.AsymptoticTrianglePacking.Internal.retSet {V : Type u_1} (H : Finset (Finset V)) (ω : Finset V → Bool) : Finset (Finset V)

The retained set at a configuration of the cube.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.retSet H ω = {e ∈ H | ω e = true}

def LeanPool.AsymptoticTrianglePacking.Internal.safeDegCube {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (v : V) (ω : Finset V → Bool) : ℝ

The safe degree at v as a function on the cube.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.AsymptoticTrianglePacking.Internal.edgeWeight {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (v : V) (f : Finset V) : ℝ

The codegree weight of an edge as seen from v: ∑_{u ∈ f∖v} codeg(v,u).

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.edgeWeight H v f = ∑ u ∈ f.erase v, ↑(Hypergraph.codegree H v u)

def LeanPool.AsymptoticTrianglePacking.Internal.meets {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (k : Finset V) : Finset (Finset V)

The edges of H meeting k.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.meets H k = {f ∈ H | ¬Disjoint f k}

def LeanPool.AsymptoticTrianglePacking.Internal.flipWeight {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (v : V) (k : Finset V) (ω : Finset V → Bool) : ℝ

The random part of the flip bound: the total codegree weight of the retained edges meeting k.

Equations

• One or more equations did not get rendered due to their size.

Elementary bounds on the codegree weight

theorem LeanPool.AsymptoticTrianglePacking.Internal.edgeWeight_nonneg {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (v : V) (f : Finset V) : 0 ≤ edgeWeight H v f

theorem LeanPool.AsymptoticTrianglePacking.Internal.edgeWeight_le_of_mem {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {r κ : ℕ} (hr : Hypergraph.IsUniform H r) (hκ : ∀ (y z : V), y ≠ z → Hypergraph.codegree H y z ≤ κ) (v : V) {f : Finset V} (hf : f ∈ H) : edgeWeight H v f ≤ ↑r * ↑κ

theorem LeanPool.AsymptoticTrianglePacking.Internal.sum_edgeWeight_eq {V : Type u_1} [Fintype V] [DecidableEq V] (H : Finset (Finset V)) (v : V) : ∑ f ∈ H, edgeWeight H v f = ∑ u ∈ Finset.univ.erase v, ↑(Hypergraph.codegree H v u) * ↑(Hypergraph.degree H u)

Double counting: ∑_{f ∈ H} edgeWeight f = ∑_{u ≠ v} codeg(v,u)·deg(u).

theorem LeanPool.AsymptoticTrianglePacking.Internal.sum_edgeWeight_le {V : Type u_1} [DecidableEq V] [Finite V] {H : Finset (Finset V)} {r Δ : ℕ} (hr : Hypergraph.IsUniform H r) (hΔ : ∀ (y : V), Hypergraph.degree H y ≤ Δ) (v : V) : ∑ f ∈ H, edgeWeight H v f ≤ ↑r * ↑Δ ^ 2

theorem LeanPool.AsymptoticTrianglePacking.Internal.sum_edgeWeight_sq_le {V : Type u_1} [DecidableEq V] [Finite V] {H : Finset (Finset V)} {r Δ κ : ℕ} (hr : Hypergraph.IsUniform H r) (hΔ : ∀ (y : V), Hypergraph.degree H y ≤ Δ) (hκ : ∀ (y z : V), y ≠ z → Hypergraph.codegree H y z ≤ κ) (v : V) : ∑ f ∈ H, edgeWeight H v f ^ 2 ≤ ↑r ^ 2 * ↑κ * ↑Δ ^ 2

theorem LeanPool.AsymptoticTrianglePacking.Internal.card_meets_le {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {r Δ : ℕ} (hr : Hypergraph.IsUniform H r) (hΔ : ∀ (y : V), Hypergraph.degree H y ≤ Δ) {k : Finset V} (hk : k ∈ H) : ↑(meets H k).card ≤ ↑r * ↑Δ

At most rΔ edges meet a given edge.

theorem LeanPool.AsymptoticTrianglePacking.Internal.meets_comm {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (f : Finset V) : meets H f = {k ∈ H | ¬Disjoint f k}

theorem LeanPool.AsymptoticTrianglePacking.Internal.sum_biUnion_le_of_nonneg {α : Type u_2} {β : Type u_3} [DecidableEq α] (B : Finset β) (t : β → Finset α) (g : α → ℝ) (hg : ∀ (a : α), 0 ≤ g a) : ∑ u ∈ B.biUnion t, g u ≤ ∑ f ∈ B, ∑ u ∈ t f, g u

A sum over a biUnion is at most the sum of the sums, for a nonnegative summand.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sum_meets_swap {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (g : Finset V → ℝ) : ∑ k ∈ H, ∑ f ∈ meets H k, g f = ∑ f ∈ H, ↑(meets H f).card * g f

Double counting the incidences k ∈ H, f ∈ meets H k.

The flip bound

theorem LeanPool.AsymptoticTrianglePacking.Internal.retSet_update_true {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {k : Finset V} (hk : k ∈ H) (ω : Finset V → Bool) : retSet H (Function.update ω k true) = insert k (retSet H ω)

theorem LeanPool.AsymptoticTrianglePacking.Internal.retSet_update_false {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (k : Finset V) (ω : Finset V → Bool) : retSet H (Function.update ω k false) = (retSet H ω).erase k

theorem LeanPool.AsymptoticTrianglePacking.Internal.retSet_update_of_notMem {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {k : Finset V} (hk : k ∉ H) (ω : Finset V → Bool) (b : Bool) : retSet H (Function.update ω k b) = retSet H ω

theorem LeanPool.AsymptoticTrianglePacking.Internal.sum_codegree_biUnion_le {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (v : V) (B : Finset (Finset V)) : ∑ u ∈ (B.biUnion id).erase v, ↑(Hypergraph.codegree H v u) ≤ ∑ f ∈ B, edgeWeight H v f

The codegree weight of the vertices spanned by a family of edges is at most the total codegree weight of the family.

theorem LeanPool.AsymptoticTrianglePacking.Internal.flipWeight_nonneg {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (v : V) (k : Finset V) (ω : Finset V → Bool) : 0 ≤ flipWeight H v k ω

theorem LeanPool.AsymptoticTrianglePacking.Internal.D_safeDegCube_of_notMem {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {k : Finset V} (hk : k ∉ H) (v : V) (ω : Finset V → Bool) : Cube.D k (safeDegCube H v) ω = 0

The bounded-differences bound. Flipping the retention of k moves the safe degree at v by at most edgeWeight k + flipWeight k.

theorem LeanPool.AsymptoticTrianglePacking.Internal.abs_D_safeDegCube_le {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (v : V) (k : Finset V) (ω : Finset V → Bool) : |Cube.D k (safeDegCube H v) ω| ≤ edgeWeight H v k + flipWeight H v k ω

The second moment of the flip weight

theorem LeanPool.AsymptoticTrianglePacking.Internal.Exp_flipWeight_sq_le {V : Type u_1} [Fintype V] [DecidableEq V] {H : Finset (Finset V)} {p : ℝ} (v : V) (k : Finset V) : (Cube.Exp p fun (ω : Finset V → Bool) => flipWeight H v k ω ^ 2) ≤ p * ∑ f ∈ meets H k, edgeWeight H v f ^ 2 + p ^ 2 * (∑ f ∈ meets H k, edgeWeight H v f) ^ 2

The variance bound

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeDegCube_variance_le {V : Type u_1} [Fintype V] [DecidableEq V] {H : Finset (Finset V)} {r Δ κ : ℕ} {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hr : Hypergraph.IsUniform H r) (hΔ : ∀ (y : V), Hypergraph.degree H y ≤ Δ) (hκ : ∀ (y z : V), y ≠ z → Hypergraph.codegree H y z ≤ κ) (v : V) : (Cube.Exp p fun (ω : Finset V → Bool) => (safeDegCube H v ω - Cube.Exp p (safeDegCube H v)) ^ 2) ≤ 2 * p * (↑r ^ 2 * ↑κ * ↑Δ ^ 2) * (1 + p * ↑r * ↑Δ + (p * ↑r * ↑Δ) ^ 2)

The sharp per-vertex safe-degree variance bound.

LeanPool.AsymptoticTrianglePacking.Internal — the VARIANCE of the safe degree

The tight round of LeanPool.AsymptoticTrianglePacking.Internal.Tight.TightRound controls the safe degree through the LOSS WEIGHT ∑_{u} codeg(v,u)·1[u covered] and the PAIR COUNT correction. The pair count has mean ≍ Δγ² and is handled by Markov, which forces the upper tolerance s ≳ Δγ²/θ — first order in γ once the exceptional fraction θ is pushed down to the ≍ γ demanded by a γ^{-1}log(1/β)-round schedule, and therefore not summable over the schedule.

This file removes that bottleneck by treating the safe degree DIRECTLY:

safeDeg(v) = ∑_{e ∋ v} X_e, X_e = 1[(e∖v) ∩ covered = ∅],

and bounding its variance. The covariance of two edge indicators is exactly

Cov(X_e, X_{e'}) = ℙ(S_e ∩ S_{e'}) − ℙ(S_e)·ℙ(S_{e'}), S_e = ⋃_{u ∈ e∖v} {u covered},

(safeIndicator_covariance_eq) and the two-sided second-order estimates give

Cov(X_e, X_{e'}) ≤ (r−1)²ε₂ + Q_e·B_{e'} + Q_{e'}·B_e + |(e ∩ e')∖v|·q_hi

(safeIndicator_covariance_le), with Q_e = ∑_{u ∈ e∖v} q_u ≤ (r−1)q_hi the first-order weight, B_e ≤ (r−1)²(q_hi² + ε₂) the Bonferroni correction and ε₂ the pair excess. The crucial point is that the Θ(γ²) terms CANCEL: ∑_{u,u'} ℙ(u,u' covered) ≤ Q_eQ_{e'} + (r−1)²ε₂ is matched by the Bonferroni lower bound ℙ(S_e)ℙ(S_{e'}) ≥ Q_eQ_{e'} − Q_eB_{e'} − Q_{e'}B_e.

Summing over the deg(v)² pairs and using ∑_{u≠v} codeg(v,u)² ≤ κ(r−1)deg(v):

Var(safeDeg(v)) ≤ Δ²((r−1)²ε₂ + 2(r−1)³q_hi(q_hi² + ε₂)) + q_hi·κ·(r−1)·Δ

(safeDegree_variance_le). In the nibble regime q_hi = γ/r, ε₂ ≤ 2κγ/(rΔ), κ ≤ γΔ/(2048r) this is ≈ 2γ³Δ², so Chebyshev at a deviation t = ε·γΔ — a factor ε below the first-order per-round degree gain — has failure probability ≈ 2γ/ε². This is a decisive improvement on the pairCount route (whose tolerance is first order in γ), but see the caveat on safeDegree_variance_le_codegree: the residual Θ(γ³Δ²) term is still a constant factor too large for the round to be iterated, and removing it requires a third-order Bonferroni estimate.

placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

The covariance of two edge indicators

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeIndicator_mul_eq {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (v : V) (e e' : Finset V) (ω : Ω) : safeIndicator ρ v e ω * safeIndicator ρ v e' ω = if ω ∈ {ω : Ω | Disjoint (e.erase v) (Hypergraph.covered (retainedSet H ρ ω))} ∩ {ω : Ω | Disjoint (e'.erase v) (Hypergraph.covered (retainedSet H ρ ω))} then 1 else 0

The product of two safe indicators is the indicator of the intersection of the safe events.

theorem LeanPool.AsymptoticTrianglePacking.Internal.integrable_safeIndicator_mul {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (v : V) (e e' : Finset V) : MeasureTheory.Integrable (fun (ω : Ω) => safeIndicator ρ v e ω * safeIndicator ρ v e' ω) MeasureTheory.volume

theorem LeanPool.AsymptoticTrianglePacking.Internal.integral_safeIndicator_mul {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (v : V) (e e' : Finset V) : ∫ (ω : Ω), safeIndicator ρ v e ω * safeIndicator ρ v e' ω = 1 - MeasureTheory.volume.real (⋃ u ∈ e.erase v, {ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)}) - MeasureTheory.volume.real (⋃ u ∈ e'.erase v, {ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)}) + MeasureTheory.volume.real ((⋃ u ∈ e.erase v, {ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)}) ∩ ⋃ u ∈ e'.erase v, {ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)})

The covariance of two edge indicators. 𝔼[X_e X_{e'}] = 1 − ℙ(S_e) − ℙ(S_{e'}) + ℙ(S_e ∩ S_{e'}).

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeIndicator_covariance_eq {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (v : V) (e e' : Finset V) : (∫ (ω : Ω), safeIndicator ρ v e ω * safeIndicator ρ v e' ω) - (∫ (ω : Ω), safeIndicator ρ v e ω) * ∫ (ω : Ω), safeIndicator ρ v e' ω = MeasureTheory.volume.real ((⋃ u ∈ e.erase v, {ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)}) ∩ ⋃ u ∈ e'.erase v, {ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)}) - MeasureTheory.volume.real (⋃ u ∈ e.erase v, {ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)}) * MeasureTheory.volume.real (⋃ u ∈ e'.erase v, {ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)})

The covariance of two edge indicators. Cov(X_e, X_{e'}) = ℙ(S_e ∩ S_{e'}) − ℙ(S_e)·ℙ(S_{e'}).

A union bound for the intersection of two unions

theorem LeanPool.AsymptoticTrianglePacking.Internal.measureReal_inter_biUnion_le {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {ι : Type u_3} {ι' : Type u_4} (s : Finset ι) (t : Finset ι') (f : ι → Set Ω) (g : ι' → Set Ω) : MeasureTheory.volume.real ((⋃ i ∈ s, f i) ∩ ⋃ j ∈ t, g j) ≤ ∑ i ∈ s, ∑ j ∈ t, MeasureTheory.volume.real (f i ∩ g j)

ℙ((⋃_{i∈s} f i) ∩ (⋃_{j∈t} g j)) ≤ ∑_i ∑_j ℙ(f i ∩ g j).

The quantitative covariance bound

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeIndicator_covariance_le {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (v : V) (e e' : Finset V) {n : ℕ} {qhi ε₂ : ℝ} (hq : ∀ (u : V), coverRate H p u ≤ qhi) (hε0 : 0 ≤ ε₂) (hpair : ∀ (u u' : V), u ≠ u' → MeasureTheory.volume.real ({ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)} ∩ {ω : Ω | u' ∈ Hypergraph.covered (retainedSet H ρ ω)}) - coverRate H p u * coverRate H p u' ≤ ε₂) (hn : (e.erase v).card ≤ n) (hn' : (e'.erase v).card ≤ n) : (∫ (ω : Ω), safeIndicator ρ v e ω * safeIndicator ρ v e' ω) - (∫ (ω : Ω), safeIndicator ρ v e ω) * ∫ (ω : Ω), safeIndicator ρ v e' ω ≤ ↑n ^ 2 * ε₂ + ↑((e ∩ e').erase v).card * qhi + 2 * (↑n * qhi) * (↑n ^ 2 * (qhi ^ 2 + ε₂))

The covariance bound for two edge indicators. With covering rates at most qhi, pair excesses at most ε₂ and at most n non-v vertices per edge,

Cov(X_e, X_{e'}) ≤ n²ε₂ + |(e ∩ e')∖v|·qhi + 2·(n·qhi)·(n²(qhi² + ε₂)).

The crucial point is that the first-order Θ(n²qhi²) terms CANCEL between the pairwise union bound for ℙ(S_e ∩ S_{e'}) and the second-order Bonferroni lower bound for ℙ(S_e)·ℙ(S_{e'}).

The variance of the safe degree

noncomputable def LeanPool.AsymptoticTrianglePacking.Internal.safeDegMean {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (v : V) : ℝ

The mean of the safe degree, written as the sum of the edge-indicator means.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.safeDegMean ρ v = ∑ e ∈ H with v ∈ e, ∫ (ω : Ω), LeanPool.AsymptoticTrianglePacking.Internal.safeIndicator ρ v e ω

theorem LeanPool.AsymptoticTrianglePacking.Internal.integral_safeDegree_eq {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (v : V) : ∫ (ω : Ω), ↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v) = safeDegMean ρ v

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeDegree_sub_mean_eq {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (v : V) (ω : Ω) : ↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v) - safeDegMean ρ v = ∑ e ∈ H with v ∈ e, (safeIndicator ρ v e ω - ∫ (ω' : Ω), safeIndicator ρ v e ω')

theorem LeanPool.AsymptoticTrianglePacking.Internal.integrable_sq_centered_safeDegree {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (v : V) : MeasureTheory.Integrable (fun (ω : Ω) => (↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v) - safeDegMean ρ v) ^ 2) MeasureTheory.volume

The centred safe degree has an integrable square (it is a bounded random variable).

theorem LeanPool.AsymptoticTrianglePacking.Internal.integral_sq_centered_safeDegree {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (v : V) : ∫ (ω : Ω), (↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v) - safeDegMean ρ v) ^ 2 = ∑ e ∈ H with v ∈ e, ∑ e' ∈ H with v ∈ e', ((∫ (ω : Ω), safeIndicator ρ v e ω * safeIndicator ρ v e' ω) - (∫ (ω : Ω), safeIndicator ρ v e ω) * ∫ (ω : Ω), safeIndicator ρ v e' ω)

The centred second moment of the safe degree as a double sum of covariances.

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeDegree_variance_le {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (v : V) {Δ n : ℕ} {qhi ε₂ Ksum : ℝ} (hq : ∀ (u : V), coverRate H p u ≤ qhi) (hε0 : 0 ≤ ε₂) (hpair : ∀ (u u' : V), u ≠ u' → MeasureTheory.volume.real ({ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)} ∩ {ω : Ω | u' ∈ Hypergraph.covered (retainedSet H ρ ω)}) - coverRate H p u * coverRate H p u' ≤ ε₂) (hdeg : {e ∈ H | v ∈ e}.card ≤ Δ) (hcard : ∀ e ∈ {e ∈ H | v ∈ e}, (e.erase v).card ≤ n) (hK : ∑ e ∈ H with v ∈ e, ∑ e' ∈ H with v ∈ e', ↑((e ∩ e').erase v).card ≤ Ksum) : ∫ (ω : Ω), (↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v) - safeDegMean ρ v) ^ 2 ≤ ↑Δ ^ 2 * (↑n ^ 2 * ε₂ + 2 * (↑n * qhi) * (↑n ^ 2 * (qhi ^ 2 + ε₂))) + Ksum * qhi

The variance bound for the safe degree. With deg(v) ≤ Δ edges at v, at most n other vertices per edge, covering rates at most qhi, pair excesses at most ε₂, and the codegree-controlled overlap budget ∑_{e,e'∈H_v} |(e ∩ e')∖v| ≤ Ksum,

Var(safeDeg v) ≤ Δ²·(n²ε₂ + 2n³qhi(qhi² + ε₂)) + Ksum·qhi.

The codegree budget for the overlap sum

theorem LeanPool.AsymptoticTrianglePacking.Internal.sum_pair_overlap_le_codegree {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} (v : V) {n κ : ℕ} (hcard : ∀ e ∈ {e ∈ H | v ∈ e}, (e.erase v).card ≤ n) (hκ : ∀ (u : V), u ≠ v → Hypergraph.codegree H v u ≤ κ) : ∑ e ∈ H with v ∈ e, ∑ e' ∈ H with v ∈ e', ↑((e ∩ e').erase v).card ≤ ↑{e ∈ H | v ∈ e}.card * ↑n * ↑κ

∑_{e,e' ∋ v} |(e ∩ e')∖v| = ∑_{e ∋ v} ∑_{u ∈ e∖v} codeg(v,u) ≤ deg(v)·n·κ: the overlap budget in safeDegree_variance_le is controlled by the codegree, NOT by Δ².

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeDegree_variance_le_codegree {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (v : V) {Δ n κ : ℕ} {qhi ε₂ : ℝ} (hq : ∀ (u : V), coverRate H p u ≤ qhi) (hε0 : 0 ≤ ε₂) (hpair : ∀ (u u' : V), u ≠ u' → MeasureTheory.volume.real ({ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)} ∩ {ω : Ω | u' ∈ Hypergraph.covered (retainedSet H ρ ω)}) - coverRate H p u * coverRate H p u' ≤ ε₂) (hdeg : {e ∈ H | v ∈ e}.card ≤ Δ) (hcard : ∀ e ∈ {e ∈ H | v ∈ e}, (e.erase v).card ≤ n) (hκ : ∀ (u : V), u ≠ v → Hypergraph.codegree H v u ≤ κ) : ∫ (ω : Ω), (↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v) - safeDegMean ρ v) ^ 2 ≤ ↑Δ ^ 2 * (↑n ^ 2 * ε₂ + 2 * (↑n * qhi) * (↑n ^ 2 * (qhi ^ 2 + ε₂))) + ↑Δ * ↑n * ↑κ * qhi

The codegree-tightened variance of the safe degree. Combining safeDegree_variance_le with the codegree budget sum_pair_overlap_le_codegree:

Var(safeDeg v) ≤ Δ²(n²ε₂ + 2n³qhi(qhi²+ε₂)) + Δ·n·κ·qhi.

In the nibble regime n = r−1, qhi = γ/r, ε₂ ≤ 2κγ/(rΔ), κ ≤ γΔ/(2048r) the right-hand side is ≈ 2γ³Δ², i.e. o(γ²Δ²): the standard deviation ≃ √2·γ^{3/2}Δ is a factor √γ below the first-order per-round degree gain ≃ γΔ/8, so Chebyshev at deviation t = ε·γΔ gives a bad fraction ≈ 2γ/ε² per round.

Caveat for the iteration: a schedule that covers a c ≃ γ/(8r) fraction per round needs the bad fraction to be ≪ c, i.e. 2γ/ε² ≪ γ/(8r) — a condition on CONSTANTS that no choice of γ can satisfy (ε ≤ 1). The obstruction is the 2·Q_e·B_{e'} term, which comes from combining a first-order union bound for ℙ(S_e ∩ S_{e'}) with a SECOND-order Bonferroni lower bound for ℙ(S_e)·ℙ(S_{e'}); the two errors add rather than cancel. A third-order Bonferroni would replace Θ(γ³Δ²) by Θ(γ⁴Δ²), making the bad fraction ≈ Cγ²/ε² ≪ γ/(8r) for all small enough γ. That refinement is NOT part of this file.

LeanPool.AsymptoticTrianglePacking.Internal — the round with a DIRECT safe-degree Chebyshev band

LeanPool.AsymptoticTrianglePacking.Internal.exists_tight_round_cheb controls the safe degree indirectly, through the loss weight (second moment, tolerance t) and the pair count (first moment, tolerance s). The pair count has mean ≍ Δγ² and can only be handled by Markov, forcing s ≳ Δγ²/θ; combined with the junk budget that the round schedule can afford, this is not summable over the ≍ γ^{-1}log(1/β) rounds.

Here the safe degree is controlled DIRECTLY by its own variance (LeanPool.AsymptoticTrianglePacking.Internal.safeDegree_variance_le_codegree), so a single symmetric tolerance t replaces the pair (t, s) and no first-moment (Markov) term survives:

#{v : |safeDeg(v) − 𝔼safeDeg(v)| ≥ t} ≤ ∑_v (safeDeg(v) − 𝔼)²/t²,

whose mean is N·Vs/t². Combined with the Chebyshev coverage bound (LeanPool.AsymptoticTrianglePacking.Internal.prob_coverage_deviation_le) one obtains exists_safe_round_cheb: an outcome with

• fewer than a exceptional vertices, every other vertex having its safe degree within t of its mean, and
• at least Q/2 covered vertices,

as soon as N·Vs/(t²a) + Cvar/(Q/2)² < 1. With the codegree-tightened variance Vs ≈ 2γ³Δ² (LeanPool.AsymptoticTrianglePacking.Internal.safeDegree_variance_le_codegree) the tolerance t ≍ γ^{3/2}Δ already suffices, which is a factor √γ below the first-order per-round gain ≍ γΔ/8.

This removes the pairCount bottleneck, but it is NOT yet enough to iterate: a schedule covering a c ≍ γ/(8r) fraction per round needs the exceptional fraction a/N ≈ Vs/(εγΔ)² ≈ 2γ/ε² to be ≪ c, a constant-factor condition that no choice of γ satisfies. See the caveat on LeanPool.AsymptoticTrianglePacking.Internal.safeDegree_variance_le_codegree: closing that gap needs a third-order Bonferroni estimate, which would turn Vs ≈ 2γ³Δ² into Vs = O(γ⁴Δ²).

placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

The aggregated safe-degree badness

noncomputable def LeanPool.AsymptoticTrianglePacking.Internal.safeBad {V : Type u_1} [DecidableEq V] [Fintype V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (t : ℝ) (ω : Ω) : ℝ

The aggregated safe-degree badness of an outcome: ∑_v (safeDeg_v − 𝔼safeDeg_v)²/t². It dominates the number of vertices whose safe degree deviates by t or more.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeBad_nonneg {V : Type u_1} [DecidableEq V] [Fintype V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (t : ℝ) (ω : Ω) : 0 ≤ safeBad ρ t ω

theorem LeanPool.AsymptoticTrianglePacking.Internal.integrable_safeBad {V : Type u_1} [DecidableEq V] [Fintype V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (t : ℝ) : MeasureTheory.Integrable (safeBad ρ t) MeasureTheory.volume

theorem LeanPool.AsymptoticTrianglePacking.Internal.card_safeBadSet_le {V : Type u_1} [DecidableEq V] [Fintype V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) {t : ℝ} (ht : 0 < t) (ω : Ω) : ↑{v : V | t ≤ |↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v) - safeDegMean ρ v|}.card ≤ safeBad ρ t ω

The number of vertices whose safe degree deviates by at least t is at most the aggregated safe-degree badness.

theorem LeanPool.AsymptoticTrianglePacking.Internal.integral_safeBad_le {V : Type u_1} [DecidableEq V] [Fintype V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) {t Vs : ℝ} (ht : 0 < t) (hVs : ∀ (v : V), ∫ (ω : Ω), (↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v) - safeDegMean ρ v) ^ 2 ≤ Vs) : ∫ (ω : Ω), safeBad ρ t ω ≤ ↑(Fintype.card V) * (Vs / t ^ 2)

The mean of the aggregated safe-degree badness, from the per-vertex variance bound.

The round

theorem LeanPool.AsymptoticTrianglePacking.Internal.exists_safe_round_cheb {V : Type u_1} [DecidableEq V] [Fintype V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) {t a Q Vs Cvar : ℝ} (ht : 0 < t) (ha : 0 < a) (hQ : 0 < Q) (hVs : ∀ (v : V), ∫ (ω : Ω), (↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v) - safeDegMean ρ v) ^ 2 ≤ Vs) (hmean : Q ≤ ∑ v : V, coverRate H p v) (hvar : ∫ (ω : Ω), (↑(Hypergraph.covered (retainedSet H ρ ω)).card - ∑ v : V, coverRate H p v) ^ 2 ≤ Cvar) (hsmall : ↑(Fintype.card V) * (Vs / t ^ 2) / a + Cvar / (Q / 2) ^ 2 < 1) : ∃ (ω : Ω) (B : Finset V), ↑B.card < a ∧ (∀ v ∉ B, |↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v) - safeDegMean ρ v| < t) ∧ Q / 2 < ↑(Hypergraph.covered (retainedSet H ρ ω)).card

The round with a direct safe-degree band. If the per-vertex safe-degree variance is at most Vs, the covered-count variance at most Cvar, the expected coverage at least Q > 0, and

N·(Vs/t²)/a + Cvar/(Q/2)² < 1,

then there is an outcome with fewer than a exceptional vertices, all remaining vertices having their safe degree within t of its mean, and at least Q/2 covered vertices.

LeanPool.AsymptoticTrianglePacking.Internal — the Bernoulli retention carried by the finite cube

LeanPool.AsymptoticTrianglePacking.Internal.exists_bernoulliRetention produces some probability space carrying a Bernoulli retention. For the sharp variance bound of LeanPool.AsymptoticTrianglePacking.Internal.Tight.SharpVariance we need a space on which the Efron–Stein inequality of LeanPool.AsymptoticTrianglePacking.Internal.Tight.CubeVariance is available, i.e. an honest product of independent coordinates. This file provides it: the cube ι → Bool with the explicit weighted counting measure

cubeMeasure p = ∑_ω ofReal (wt p ω) · δ_ω,

for which

• integrals are the elementary sums LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp (LeanPool.AsymptoticTrianglePacking.Internal.integral_cubeMeasure),
• the coordinate events are independent with probability p (LeanPool.AsymptoticTrianglePacking.Internal.iIndepSet_cubeCoord), hence the cube carries a LeanPool.AsymptoticTrianglePacking.Internal.BernoulliRetention (LeanPool.AsymptoticTrianglePacking.Internal.cubeRetention), and
• the Efron–Stein bound holds in integral form (LeanPool.AsymptoticTrianglePacking.Internal.cube_centred_sq_le).

noncomputable def LeanPool.AsymptoticTrianglePacking.Internal.Cube.cubeMeasure {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) : MeasureTheory.Measure (ι → Bool)

The Bernoulli(p) measure on the finite cube ι → Bool.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.Cube.cubeMeasure p = ∑ ω : ι → Bool, ENNReal.ofReal (LeanPool.AsymptoticTrianglePacking.Internal.Cube.wt p ω) • MeasureTheory.Measure.dirac ω

@[instance_reducible]

noncomputable def LeanPool.AsymptoticTrianglePacking.Internal.Cube.cubeSpace {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) : MeasureTheory.MeasureSpace (ι → Bool)

The finite cube as a measure space.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.Cube.cubeSpace p = { toMeasurableSpace := MeasurableSpace.pi, volume := LeanPool.AsymptoticTrianglePacking.Internal.Cube.cubeMeasure p }

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.cubeMeasure_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (A : Set (ι → Bool)) : (cubeMeasure p) A = ENNReal.ofReal (∑ ω : ι → Bool, wt p ω * A.indicator 1 ω)

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.isProbabilityMeasure_cubeMeasure {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : MeasureTheory.IsProbabilityMeasure (cubeMeasure p)

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.integral_cubeMeasure {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (f : (ι → Bool) → ℝ) : ∫ (ω : ι → Bool), f ω ∂cubeMeasure p = Exp p f

Integrals against the cube measure are the elementary sums Exp.

Independence of the coordinates

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.indicator_biInter_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) (ω : ι → Bool) : (⋂ e ∈ S, {ω : ι → Bool | ω e = true}).indicator 1 ω = ∏ i : ι, if i ∈ S then if ω i = true then 1 else 0 else 1

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.Exp_indicator_biInter {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (S : Finset ι) : (Exp p fun (ω : ι → Bool) => (⋂ e ∈ S, {ω : ι → Bool | ω e = true}).indicator 1 ω) = p ^ S.card

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.cubeMeasure_biInter {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (S : Finset ι) : (cubeMeasure p) (⋂ e ∈ S, {ω : ι → Bool | ω e = true}) = ENNReal.ofReal (p ^ S.card)

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.cubeMeasure_coord {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (e : ι) : (cubeMeasure p) {ω : ι → Bool | ω e = true} = ENNReal.ofReal p

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.iIndepSet_cubeCoord {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : ProbabilityTheory.iIndepSet (fun (e : ι) => {ω : ι → Bool | ω e = true}) (cubeMeasure p)

Efron–Stein in integral form

theorem LeanPool.AsymptoticTrianglePacking.Internal.Cube.cube_centred_sq_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (f : (ι → Bool) → ℝ) : ∫ (ω : ι → Bool), (f ω - ∫ (ω' : ι → Bool), f ω' ∂cubeMeasure p) ^ 2 ∂cubeMeasure p ≤ ∑ i : ι, p * (1 - p) * ∫ (ω : ι → Bool), (f (Function.update ω i true) - f (Function.update ω i false)) ^ 2 ∂cubeMeasure p

The retention carried by the cube

noncomputable def LeanPool.AsymptoticTrianglePacking.Internal.cubeRetention {V : Type u_1} [Fintype V] [DecidableEq V] (H : Finset (Finset V)) {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : BernoulliRetention H p

The Bernoulli retention on the finite cube. The coordinate events of the cube Finset V → Bool form an independent family of events of probability p.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.cubeRetention H hp0 hp1 = { A := fun (e : Finset V) => {ω : Finset V → Bool | ω e = true}, meas := ⋯, indep := ⋯, prob := ⋯ }

theorem LeanPool.AsymptoticTrianglePacking.Internal.retainedSet_cubeRetention {V : Type u_1} [Fintype V] [DecidableEq V] (H : Finset (Finset V)) {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (ω : Finset V → Bool) : retainedSet H (cubeRetention H hp0 hp1) ω = {e ∈ H | ω e = true}

LeanPool.AsymptoticTrianglePacking.Internal — the sharp round: transporting the Efron–Stein

variance to the cube retention

LeanPool.AsymptoticTrianglePacking.Internal.safeDegCube_variance_le (LeanPool.AsymptoticTrianglePacking.Internal.Tight.SharpVariance) is the sharp per-vertex safe-degree variance bound on the elementary Bernoulli cube. Here it is transported to the LeanPool.AsymptoticTrianglePacking.Internal.BernoulliRetention carried by that cube (LeanPool.AsymptoticTrianglePacking.Internal.cubeRetention), which is the form the Chebyshev round LeanPool.AsymptoticTrianglePacking.Internal.exists_safe_round_cheb consumes.

theorem LeanPool.AsymptoticTrianglePacking.Internal.integral_centered_safeDegree_cube_le {V : Type u_1} [Fintype V] [DecidableEq V] (K : Finset (Finset V)) {r Δ κ : ℕ} {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hr : Hypergraph.IsUniform K r) (hΔ : ∀ (y : V), Hypergraph.degree K y ≤ Δ) (hκ : ∀ (y z : V), y ≠ z → Hypergraph.codegree K y z ≤ κ) (v : V) : ∫ (ω : Finset V → Bool), (↑(safeDegree K (Hypergraph.covered (retainedSet K (cubeRetention K hp0 hp1) ω)) v) - safeDegMean (cubeRetention K hp0 hp1) v) ^ 2 ∂Cube.cubeMeasure p ≤ 2 * p * (↑r ^ 2 * ↑κ * ↑Δ ^ 2) * (1 + p * ↑r * ↑Δ + (p * ↑r * ↑Δ) ^ 2)

The sharp per-vertex safe-degree variance, in integral form.

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeDegMean_cubeRetention {V : Type u_1} [Fintype V] [DecidableEq V] (K : Finset (Finset V)) {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (v : V) : safeDegMean (cubeRetention K hp0 hp1) v = Cube.Exp p (safeDegCube K v)

The sharp round on an active set

The whole probabilistic content of the sharp round. Everything that is not a deterministic estimate of the MEAN safe degree Cube.Exp p (safeDegCube K v) is discharged here: the safe degree is pinned to within t of its mean off an exceptional set of size < a, and the round covers more than Q/2 vertices, where Q = |A|·δp(1−p)^{rΔ} uses the degree floor only on the active set.

theorem LeanPool.AsymptoticTrianglePacking.Internal.exists_sharp_round_band {V : Type u_1} [Fintype V] [DecidableEq V] {K : Finset (Finset V)} (A : Finset V) {r Δ δ κ : ℕ} {p t a mlo : ℝ} {mhi : V → ℝ} (hp0 : 0 < p) (hp1 : p < 1) (hr1 : 1 ≤ r) (hr : Hypergraph.IsUniform K r) (hΔ : ∀ (y : V), Hypergraph.degree K y ≤ Δ) (hδA : ∀ y ∈ A, δ ≤ Hypergraph.degree K y) (hκ : ∀ (y z : V), y ≠ z → Hypergraph.codegree K y z ≤ κ) (ht : 0 < t) (ha : 0 < a) (hδ0 : 0 < δ) (hA : 0 < A.card) (hlo : ∀ v ∈ A, mlo ≤ Cube.Exp p (safeDegCube K v)) (hhi : ∀ v ∈ A, Cube.Exp p (safeDegCube K v) ≤ mhi v) (hsmall : ↑(Fintype.card V) * (2 * p * (↑r ^ 2 * ↑κ * ↑Δ ^ 2) * (1 + p * ↑r * ↑Δ + (p * ↑r * ↑Δ) ^ 2) / t ^ 2) / a + (↑(Fintype.card V) * (↑Δ * p) + ↑(Fintype.card V) ^ 2 * (↑κ * p + 4 * ↑r ^ 2 * ↑κ * ↑Δ ^ 2 * p ^ 3)) / (↑A.card * (↑δ * (p * (1 - p) ^ (r * Δ))) / 2) ^ 2 < 1) : ∃ R' ⊆ K, ∃ (B : Finset V), ↑B.card < a ∧ (∀ v ∈ A, v ∉ B → v ∉ Hypergraph.covered R' → mlo - t ≤ ↑(Hypergraph.degree (Hypergraph.residual K R') v) ∧ ↑(Hypergraph.degree (Hypergraph.residual K R') v) ≤ mhi v + t) ∧ ↑A.card * (↑δ * (p * (1 - p) ^ (r * Δ))) / 2 < ↑(Hypergraph.covered R').card

The sharp Chebyshev round on an active set. Given ANY two-sided estimate mlo ≤ mean ≤ mhi for the mean safe degree on A, and the smallness condition, one round leaves every active, uncovered vertex outside an exceptional set of size < a with residual degree in [mlo − t, mhi + t], and covers more than Q/2 vertices.

The variance input is the SHARP Efron–Stein bound LeanPool.AsymptoticTrianglePacking.Internal.safeDegCube_variance_le: Vs = 2p·r²κΔ²(1 + prΔ + (prΔ)²), which carries NO Δ² term at p = γ/(rΔ).

The deterministic mean estimates

theorem LeanPool.AsymptoticTrianglePacking.Internal.Exp_safeDegCube_ge {V : Type u_1} [Fintype V] [DecidableEq V] {K : Finset (Finset V)} {r Δ : ℕ} {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hr1 : 1 ≤ r) (hr : Hypergraph.IsUniform K r) (hΔ : ∀ (y : V), Hypergraph.degree K y ≤ Δ) (v : V) : ↑(Hypergraph.degree K v) * (1 - (↑r - 1) * (↑Δ * p)) ≤ Cube.Exp p (safeDegCube K v)

Floor for the mean safe degree (union bound on the covering events).

theorem LeanPool.AsymptoticTrianglePacking.Internal.Exp_safeDegCube_le {V : Type u_1} [Fintype V] [DecidableEq V] {K : Finset (Finset V)} (A : Finset V) {r Δ δ κ : ℕ} {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hr2 : 2 ≤ r) (hr : Hypergraph.IsUniform K r) (hΔ : ∀ (y : V), Hypergraph.degree K y ≤ Δ) (hδA : ∀ y ∈ A, δ ≤ Hypergraph.degree K y) (hκ : ∀ (y z : V), y ≠ z → Hypergraph.codegree K y z ≤ κ) (v : V) : Cube.Exp p (safeDegCube K v) ≤ ↑(Hypergraph.degree K v) - (↑(Hypergraph.degree K v) - ↑(lostDegree K Aᶜ v)) * ((↑r - 1) * ↑δ * (p * (1 - p) ^ (r * Δ))) + ↑(Hypergraph.degree K v) * ((↑r - 1) * (↑r - 2)) * (↑Δ ^ 2 * p ^ 2 + ↑κ * p)

Ceiling for the mean safe degree (second Bonferroni inequality), with the degree floor used only on the active set A: the drop is carried by the deg(v) − lostDegree K Aᶜ v edges at v that stay inside A.

LeanPool.AsymptoticTrianglePacking.Internal — assembling the sharp round

LeanPool.AsymptoticTrianglePacking.Internal.SharpRoundFor (LeanPool.AsymptoticTrianglePacking.Internal.Tight.SharpRound) is proved here in the regime 2γ ≤ ε, from

• LeanPool.AsymptoticTrianglePacking.Internal.exists_sharp_round_band — the probabilistic content (sharp Efron–Stein variance + Chebyshev on the safe degree, cover variance on the active set), and
• LeanPool.AsymptoticTrianglePacking.Internal.Exp_safeDegCube_ge / LeanPool.AsymptoticTrianglePacking.Internal.Exp_safeDegCube_le — the two deterministic estimates of the MEAN safe degree (union bound and second Bonferroni inequality).

The retention is p = γ/(r⌊Δ⌋₊), the tolerance t = εγ⌊Δ⌋₊/16, the exceptional budget a = θ|V|, the degree threshold D₀ = 256r/(α²γ) + 96/ε + 4 and the codegree factor c₀ = θε²γα²/(16384r).

The hypothesis 2γ ≤ ε is what pays for the SECOND-ORDER error of the mean safe degree: the Bonferroni residue is Θ(γ²Δ) per vertex, while SharpRoundFor allows only εγΔ, so a hypothesis of the shape γ = O(ε) is unavoidable for a round built from the uniform retention p = γ/(rΔ). The CONSTANT, however, is not: the exact requirement is that the residue

Δ⌊·⌋(r−1)(r−2)(Δ²p² + κp) ≤ γ²Δ (mean ceiling, Bonferroni)

together with the Chebyshev tolerance t, the codegree term rκγ, and the rounding/(1−p)^{rΔ} discrepancy γ³Δ + O(1) fit inside εγΔ. Charging γ²Δ ≤ εγΔ/2, γ³Δ ≤ εγΔ/4, t ≤ εγΔ/16 and the two O(1)-terms εγΔ/32 each leaves 28/32 of the budget used, so 2γ ≤ ε suffices. This is exactly the regime the tight-band schedule uses: LeanPool.AsymptoticTrianglePacking.Internal.exists_tightParams sets ε = 4aγ with a = (r−1)/r ≥ 1/2, hence ε ≥ 2γ.

The discrepancy γ³Δ + O(1) (rather than the γ²Δ + O(1) of the earlier bookkeeping) comes from the sharp upper bound (1−p)^{rΔ} ≤ 1 − γ + γ²/2 (LeanPool.AsymptoticTrianglePacking.Internal.one_sub_pow_le_quadratic), which cancels the (1−γ) factor carried by the ceiling drop that SharpRoundFor requests.

theorem LeanPool.AsymptoticTrianglePacking.Internal.lostDegree_le_degree {V : Type u_1} [DecidableEq V] (K : Finset (Finset V)) (B : Finset V) (v : V) : lostDegree K B v ≤ Hypergraph.degree K v

theorem LeanPool.AsymptoticTrianglePacking.Internal.one_sub_pow_le_quadratic {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (m : ℕ) : (1 - p) ^ m ≤ 1 - ↑m * p + (↑m * p) ^ 2 / 2

Second-order upper bound for (1 − p)^m. For 0 ≤ p ≤ 1, (1 − p)^m ≤ 1 − mp + (mp)²/2; at mp = γ this is 1 − γ + γ²/2, the bound that cancels the (1 − γ) factor of the requested ceiling drop.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sharp_drop_ratio_le (γ δ Δ Dn dn L : ℝ) (hγ0 : 0 < γ) (hγ1 : γ ≤ 1 / 2) (hδ2 : 2 ≤ δ) (hδΔ : δ ≤ Δ) (hDn3 : 3 ≤ Dn) (hΔDn : Δ < Dn + 1) (hδdn : δ ≤ dn) (hdnδ : dn < δ + 1) (hL0 : 0 < L) (hLu : L ≤ 1 - γ + γ ^ 2 / 2) : Δ * (dn * L / Dn) ≤ δ * (1 - γ) + γ ^ 2 * Δ + 3

The rounding/(1−p)^{rΔ} discrepancy of the ceiling drop. With dn = ⌈δ⌉₊, Dn = ⌊Δ⌋₊ and L = (1−p)^{rDn} ≤ 1 − γ + γ²/2, the achieved relative drop dn·L/Dn exceeds the requested one δ(1−γ)/Δ by at most γ² + 3/Δ in relative terms — i.e. Δ·(dn L/Dn) ≤ δ(1−γ) + γ²Δ + 3.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sharp_survival_bounds {p γ : ℝ} {m : ℕ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hpγ : ↑m * p = γ) : 1 - γ ≤ (1 - p) ^ m ∧ (1 - p) ^ m ≤ 1 - γ + γ ^ 2 / 2

The survival factor of one round. For m·p = γ with 0 ≤ p ≤ 1, Bernoulli and LeanPool.AsymptoticTrianglePacking.Internal.one_sub_pow_le_quadratic pin (1 − p)^m between 1 − γ and 1 − γ + γ²/2.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sharp_mean_ceiling_arith {D Dn dn l W C X : ℝ} (hW : 0 ≤ W) (hC : 0 ≤ C) (hX : 0 ≤ X) (h1 : D ≤ Dn) (h2 : dn ≤ D) : D - (D - l) * W + D * C * X ≤ Dn - (dn - l) * W + Dn * C * X

The mean ceiling is monotone in the degree. Replacing the degree D of a vertex by the global ceiling Dn and its floor by dn can only increase the mean safe degree estimate.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sharp_cover_rate_le {rr γ Dn dn p L : ℝ} (hR0 : 0 < rr) (hDn0 : 0 < Dn) (hdnhalf : Dn / 2 ≤ dn) (hLhalf : 1 / 2 ≤ L) (hp0 : 0 < p) (hpγ : rr * Dn * p = γ) : γ / (8 * rr) ≤ dn * (p * L) / 2

The cover rate of one round. With p = γ/(rD), a floor dn ≥ D/2 and a survival factor L ≥ 1/2, each active vertex is matched with probability at least γ/(8r).

theorem LeanPool.AsymptoticTrianglePacking.Internal.sharp_bonferroni_error_le {rr γ Δ Dn kn p Err : ℝ} (hR2 : 2 ≤ rr) (hDn0 : 0 ≤ Dn) (hkn0 : 0 ≤ kn) (hp0 : 0 < p) (hpγ : rr * Dn * p = γ) (hDn_le : Dn ≤ Δ) (hErrdef : Err = Dn * ((rr - 1) * (rr - 2)) * (Dn ^ 2 * p ^ 2 + kn * p)) : Err ≤ Δ * γ ^ 2 + rr * kn * γ

The second-order (Bonferroni) error of the mean safe degree. With p = γ/(rD) the residue D(r−1)(r−2)(D²p² + κp) is at most Δγ² + rκγ.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sharp_codegree_tolerance_le {rr γ ε θ α Δ Dn kn : ℝ} (hR0 : 0 < rr) (hγ0 : 0 < γ) (hγ1 : γ ≤ 1 / 2) (hε0 : 0 < ε) (hε1 : ε ≤ 1) (hθ0 : 0 < θ) (hθ1 : θ ≤ 1) (hα0 : 0 < α) (hα1 : α ≤ 1) (hDn0 : 0 ≤ Dn) (hDn_le : Dn ≤ Δ) (hkn3 : kn ≤ θ * ε ^ 2 * γ * α ^ 2 * Dn / (8192 * rr)) : rr * kn * γ ≤ ε * γ * Δ / 32

The codegree share of the tolerance budget. At κ ≤ θε²γα²D/(8192r) the codegree term rκγ of the ceiling drop uses at most a 1/32 of the budget εγΔ.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sharp_ceiling_clause_arith {S γ ε δ dn Δ Dn l c d Err t x e : ℝ} (hSnn : 0 ≤ S) (hS1 : S ≤ 1) (hγ0 : 0 < γ) (hΔ0 : 0 < Δ) (hδ2 : 2 ≤ δ) (hδdn : δ ≤ dn) (hlΔ : l ≤ Δ) (hcd : c ≤ d) (hd0 : 0 ≤ d) (hΔc : Δ * c = δ * (1 - γ)) (hΔd : Δ * d ≤ δ * (1 - γ) + γ ^ 2 * Δ + 3) (hDn_le : Dn ≤ Δ) (hb2 : x ≤ Dn - S * γ * ((dn - l) * d) + Err + t) (hErrle : Err ≤ Δ * γ ^ 2 + e) (ht2 : t ≤ ε * γ * Δ / 16) (hg2 : Δ * γ ^ 2 ≤ ε * γ * Δ / 2) (hg3 : γ * (γ ^ 2 * Δ) ≤ ε * γ * Δ / 4) (hg4 : 3 * γ ≤ ε * γ * Δ / 32) (he : e ≤ ε * γ * Δ / 32) (hεγΔ : 0 ≤ ε * γ * Δ) : x ≤ Δ - S * γ * ((δ - l) * c) + ε * γ * Δ

The ceiling clause of the round, in arithmetic form. The mean ceiling Dn − Sγ(dn−l)d + Err produced by the Chebyshev band, plus the tolerance t, still fits below the requested ceiling Δ − Sγ(δ−l)c + εγΔ, where c = δ(1−γ)/Δ is the requested relative drop and d = dn·L/Dn the achieved one: the five error terms use 1/2 + 1/4 + 1/16 + 1/32 + 1/32 < 1 of the budget.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sharp_smallness_numeric (r : ℕ) (hr2 : 2 ≤ r) (γ ε θ α N Dn dn kn Ac p L t : ℝ) (hγ0 : 0 < γ) (hγ1 : γ ≤ 1 / 2) (hε0 : 0 < ε) (hε1 : ε ≤ 1) (hθ0 : 0 < θ) (hθ1 : θ ≤ 1) (hα0 : 0 < α) (hα1 : α ≤ 1) (hN256' : 256 * ↑r ≤ N * (α ^ 2 * γ)) (hN4 : 4 ≤ N) (hDn3 : 3 ≤ Dn) (hdnhalf : Dn / 2 ≤ dn) (hkn0 : 0 ≤ kn) (hkn3 : kn ≤ θ * ε ^ 2 * γ * α ^ 2 * Dn / (8192 * ↑r)) (hp0 : 0 < p) (hpγ : ↑r * Dn * p = γ) (hLhalf : 1 / 2 ≤ L) (htdef : t = ε * γ * Dn / 16) (hAN : α * N ≤ Ac) : N * (2 * p * (↑r ^ 2 * kn * Dn ^ 2) * (1 + p * ↑r * Dn + (p * ↑r * Dn) ^ 2) / t ^ 2) / (θ * N) + (N * (Dn * p) + N ^ 2 * (kn * p + 4 * ↑r ^ 2 * kn * Dn ^ 2 * p ^ 3)) / (Ac * (dn * (p * L)) / 2) ^ 2 < 1

The numeric smallness condition consumed by LeanPool.AsymptoticTrianglePacking.Internal.exists_sharp_round_band, at the parameters of LeanPool.AsymptoticTrianglePacking.Internal.sharpRoundFor_of_two_gamma_le_eps (tolerance t = εγDn/16, codegree kn ≤ θε²γα²Dn/(8192r)).

theorem LeanPool.AsymptoticTrianglePacking.Internal.sharpRoundFor_of_two_gamma_le_eps (r : ℕ) (hr2 : 2 ≤ r) (γ ε θ α : ℝ) (hγ0 : 0 < γ) (hγ1 : γ ≤ 1 / 2) (hε1 : ε ≤ 1) (hγε : 2 * γ ≤ ε) (hθ0 : 0 < θ) (hθ1 : θ ≤ 1) (hα0 : 0 < α) (hα1 : α ≤ 1) : SharpRoundFor r γ ε θ α (256 * ↑r / (α ^ 2 * γ) + 96 / ε + 4) (θ * ε ^ 2 * γ * α ^ 2 / (16384 * ↑r))

The sharp LeanPool.AsymptoticTrianglePacking.Internal round, assembled, in the regime 2γ ≤ ε — the regime the tight-band schedule LeanPool.AsymptoticTrianglePacking.Internal.exists_tightParams actually uses (ε = 4((r−1)/r)γ ≥ 2γ).

theorem LeanPool.AsymptoticTrianglePacking.Internal.sharpRoundHyp_of_two_gamma_le_eps (r : ℕ) (hr2 : 2 ≤ r) (γ ε θ α : ℝ) (hγ0 : 0 < γ) (hγ1 : γ ≤ 1 / 2) (hε1 : ε ≤ 1) (hγε : 2 * γ ≤ ε) (hθ0 : 0 < θ) (hθ1 : θ ≤ 1) (hα0 : 0 < α) (hα1 : α ≤ 1) : ∃ (D₀ : ℝ), 0 < D₀ ∧ ∃ (c₀ : ℝ), 0 < c₀ ∧ SharpRoundFor r γ ε θ α D₀ c₀

LeanPool.AsymptoticTrianglePacking.Internal.SharpRoundHyp in the regime 2γ ≤ ε.

This is exactly the body of LeanPool.AsymptoticTrianglePacking.Internal.SharpRoundHyp with the extra hypothesis 2 * γ ≤ ε; the witnesses are D₀ = 256r/(α²γ) + 96/ε + 4 and c₀ = θε²γα²/(16384r).

The restriction is not an artefact of the bookkeeping: the mean safe degree of a vertex genuinely carries a second-order term of size Θ(γ²Δ) (the pairs of neighbours of v inside a single edge that are covered simultaneously), while SharpRoundFor allows an absolute error of only εγΔ. So some hypothesis of the form γ = O(ε) is necessary for a round built from the uniform retention p = γ/(rΔ). The constant 2 is below the schedule's own ratio: LeanPool.AsymptoticTrianglePacking.Internal.exists_tightParams sets ε = 4((r−1)/r)γ ≥ 2γ.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sharpRoundHyp_of_gamma_le_eps (r : ℕ) (hr2 : 2 ≤ r) (γ ε θ α : ℝ) (hγ0 : 0 < γ) (hγ1 : γ ≤ 1 / 2) (hε1 : ε ≤ 1) (hγε : 8 * γ ≤ ε) (hθ0 : 0 < θ) (hθ1 : θ ≤ 1) (hα0 : 0 < α) (hα1 : α ≤ 1) : ∃ (D₀ : ℝ), 0 < D₀ ∧ ∃ (c₀ : ℝ), 0 < c₀ ∧ SharpRoundFor r γ ε θ α D₀ c₀

LeanPool.AsymptoticTrianglePacking.Internal.SharpRoundHyp in the regime 8γ ≤ ε, a special case of LeanPool.AsymptoticTrianglePacking.Internal.sharpRoundHyp_of_two_gamma_le_eps.