LeanPool.AsymptoticTrianglePacking.Internal — the mean of the Bonferroni correction

The upper half of the safe-degree sandwich (LeanPool.AsymptoticTrianglePacking.Internal.safeDegree_add_coverWeight_le) pays the Bonferroni correction pairWeight H v C = ∑_{e ∋ v} C(|(e∖v) ∩ C|, 2). This file bounds its mean.

• sum_pair_ind_nat — the ordered-pair count ∑_{u ∈ D} ∑_{u' ∈ D∖u} 1[u ∈ C]1[u' ∈ C] equals k(k−1) with k = |D ∩ C|, hence dominates C(k,2);
• pairWeight_le_pairCount — pathwise, pairWeight ≤ pairCount, the ordered-pair count of the covering indicators;
• integral_pairCount_le — 𝔼[pairCount] ≤ deg(v)·(r−1)²·ε_pair, where ε_pair bounds the joint covering probability of two distinct vertices (prob_two_vertices_covered_le gives ε_pair = Δ²p² + κp).

In the nibble regime this is O(deg(v)·r²(γ² + μγ)) — second order against the first-order loss deg(v)·(r−1)q ≈ deg(v)·γ, so Markov's inequality makes it negligible for all but a tiny fraction of the vertices.

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

The ordered-pair count

theorem LeanPool.AsymptoticTrianglePacking.Internal.sum_pair_ind_nat {V : Type u_1} [DecidableEq V] (D C : Finset V) : (∑ u ∈ D, ∑ u' ∈ D.erase u, (if u ∈ C then 1 else 0) * if u' ∈ C then 1 else 0) = (D ∩ C).card * ((D ∩ C).card - 1)

The ordered-pair count of a finite set against C.

theorem LeanPool.AsymptoticTrianglePacking.Internal.choose_two_le_sum_pair_ind {V : Type u_1} [DecidableEq V] (D C : Finset V) : (D ∩ C).card.choose 2 ≤ ∑ u ∈ D, ∑ u' ∈ D.erase u, (if u ∈ C then 1 else 0) * if u' ∈ C then 1 else 0

C(k,2) is dominated by the ordered-pair count.

The pair count as a random variable

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

The ordered-pair count of covering indicators at v.

Equations

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

theorem LeanPool.AsymptoticTrianglePacking.Internal.pairWeight_le_pairCount {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (v : V) (ω : Ω) : ↑(pairWeight H v (Hypergraph.covered (retainedSet H ρ ω))) ≤ pairCount ρ v ω

Pathwise, the Bonferroni correction is dominated by the pair count.

theorem LeanPool.AsymptoticTrianglePacking.Internal.integrable_pairCount {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 (pairCount ρ v) MeasureTheory.volume

theorem LeanPool.AsymptoticTrianglePacking.Internal.integral_pairCount_le {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} {r : ℕ} {εpair : ℝ} (ρ : BernoulliRetention H p) (hr : Hypergraph.IsUniform H r) (hr1 : 1 ≤ r) (hpair : ∀ (u u' : V), u ≠ u' → MeasureTheory.volume.real ({ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)} ∩ {ω : Ω | u' ∈ Hypergraph.covered (retainedSet H ρ ω)}) ≤ εpair) (hε0 : 0 ≤ εpair) (v : V) : ∫ (ω : Ω), pairCount ρ v ω ≤ ↑(Hypergraph.degree H v) * (↑r - 1) ^ 2 * εpair

The mean of the pair count.

LeanPool.AsymptoticTrianglePacking.Internal — the TIGHT round

This is the analytic heart of the classical (tight-band) nibble: a SINGLE outcome of one nibble round which simultaneously

• covers a fixed fraction of the vertices, and
• leaves all but a prescribed number of vertices with a safe degree in a TWO-SIDED band of width 2t + s around the SAME centre deg(v) − 𝔼[loss(v)].

The two bounds are centred at the same value — that is what "tight band" means, and it is what the 8:1-band single-round peeling (LeanPool.AsymptoticTrianglePacking.Internal.CeilRoundInv, refuted through LeanPool.AsymptoticTrianglePacking.Internal.NibbleRoundProb) cannot deliver.

The proof avoids any union bound over the vertex set. Instead the two failure modes are aggregated into one nonnegative functional tightBad whose mean is small, and Markov's inequality is applied twice: once to tightBad (too many irregular vertices) and once to the uncovered count (too little coverage). The two failure probabilities add up to < 1, so a good outcome exists.

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

Basic positivity and integrability

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

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

theorem LeanPool.AsymptoticTrianglePacking.Internal.integrable_sq_centered_lossWeight {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) (v : V) : MeasureTheory.Integrable (fun (ω : Ω) => (lossWeight ρ v ω - lossWeightMean H p v) ^ 2) MeasureTheory.volume

The covered count

theorem LeanPool.AsymptoticTrianglePacking.Internal.coveredCount_eq_sum {V : Type u_1} [DecidableEq V] [Fintype V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (ω : Ω) : ↑(Hypergraph.covered (retainedSet H ρ ω)).card = ∑ v : V, coverInd ρ v ω

theorem LeanPool.AsymptoticTrianglePacking.Internal.integrable_coveredCount {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Finite V] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) : MeasureTheory.Integrable (fun (ω : Ω) => ↑(Hypergraph.covered (retainedSet H ρ ω)).card) MeasureTheory.volume

theorem LeanPool.AsymptoticTrianglePacking.Internal.integral_coveredCount {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) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : ∫ (ω : Ω), ↑(Hypergraph.covered (retainedSet H ρ ω)).card = ∑ v : V, coverRate H p v

The aggregated bad functional

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

The aggregated badness of an outcome: ∑_v [(loss_v − 𝔼loss_v)²/t² + pairCount_v/s]. It dominates the number of vertices that fail either of the two tolerances.

Equations

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

theorem LeanPool.AsymptoticTrianglePacking.Internal.tightBad_nonneg {V : Type u_1} [DecidableEq V] [Fintype V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) {t s : ℝ} (ht : 0 < t) (hs : 0 < s) (ω : Ω) : 0 ≤ tightBad ρ t s ω

theorem LeanPool.AsymptoticTrianglePacking.Internal.integrable_tightBad {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 s : ℝ) : MeasureTheory.Integrable (tightBad ρ t s) MeasureTheory.volume

theorem LeanPool.AsymptoticTrianglePacking.Internal.card_tightBadSet_le {V : Type u_1} [DecidableEq V] [Fintype V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) {t s : ℝ} (ht : 0 < t) (hs : 0 < s) (ω : Ω) : ↑{v : V | t ≤ |lossWeight ρ v ω - lossWeightMean H p v| ∨ s ≤ pairCount ρ v ω}.card ≤ tightBad ρ t s ω

The number of vertices failing either tolerance is at most the aggregated badness.

theorem LeanPool.AsymptoticTrianglePacking.Internal.integral_tightBad_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 s Vb Pb : ℝ} (ht : 0 < t) (hs : 0 < s) (hVb : ∀ (v : V), ∫ (ω : Ω), (lossWeight ρ v ω - lossWeightMean H p v) ^ 2 ≤ Vb) (hPb : ∀ (v : V), ∫ (ω : Ω), pairCount ρ v ω ≤ Pb) : ∫ (ω : Ω), tightBad ρ t s ω ≤ ↑(Fintype.card V) * (Vb / t ^ 2 + Pb / s)

The mean of the aggregated badness, from per-vertex bounds.

The tight round

theorem LeanPool.AsymptoticTrianglePacking.Internal.exists_tight_round_on {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) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (G : Finset V) {t s a Vb Pb qlo : ℝ} (ht : 0 < t) (hs : 0 < s) (ha : 0 < a) (hVb : ∀ (v : V), ∫ (ω : Ω), (lossWeight ρ v ω - lossWeightMean H p v) ^ 2 ≤ Vb) (hPb : ∀ (v : V), ∫ (ω : Ω), pairCount ρ v ω ≤ Pb) (hqlo1 : qlo ≤ 1) (hqlo : ∀ v ∈ G, qlo ≤ coverRate H p v) (hN : 0 < Fintype.card V) (hsmall : ↑(Fintype.card V) * (Vb / t ^ 2 + Pb / s) * (2 * ↑(Fintype.card V) - ↑G.card * qlo) < a * (↑G.card * qlo)) : ∃ (ω : Ω) (B : Finset V), ↑B.card < a ∧ (∀ v ∉ B, ↑(Hypergraph.degree H v) - lossWeightMean H p v - t ≤ ↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v) ∧ ↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v) ≤ ↑(Hypergraph.degree H v) - lossWeightMean H p v + t + s) ∧ ↑G.card * qlo / 2 < ↑(Hypergraph.covered (retainedSet H ρ ω)).card

The tight round, relative to a good set. Only the vertices of G are required to have a guaranteed covering rate, and only their number enters the coverage conclusion. This is the form consumed by the iteration, where G is the set of vertices still carrying a full degree.

theorem LeanPool.AsymptoticTrianglePacking.Internal.exists_tight_round {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) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {t s a Vb Pb qlo : ℝ} (ht : 0 < t) (hs : 0 < s) (ha : 0 < a) (hVb : ∀ (v : V), ∫ (ω : Ω), (lossWeight ρ v ω - lossWeightMean H p v) ^ 2 ≤ Vb) (hPb : ∀ (v : V), ∫ (ω : Ω), pairCount ρ v ω ≤ Pb) (hqlo1 : qlo ≤ 1) (hqlo : ∀ (v : V), qlo ≤ coverRate H p v) (hN : 0 < Fintype.card V) (hsmall : ↑(Fintype.card V) * (Vb / t ^ 2 + Pb / s) * (2 - qlo) < a * qlo) : ∃ (ω : Ω) (B : Finset V), ↑B.card < a ∧ (∀ v ∉ B, ↑(Hypergraph.degree H v) - lossWeightMean H p v - t ≤ ↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v) ∧ ↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v) ≤ ↑(Hypergraph.degree H v) - lossWeightMean H p v + t + s) ∧ ↑(Fintype.card V) * qlo / 2 < ↑(Hypergraph.covered (retainedSet H ρ ω)).card

The tight round. There is an outcome of the nibble round which covers more than a qlo/2-fraction of the vertices and, outside an exceptional set of fewer than a vertices, leaves every safe degree in the two-sided band of width 2t + s around deg(v) − 𝔼[loss(v)].