LeanPool.AsymptoticTrianglePacking.Internal — the joint matching probability of TWO edges

The variance of the safe degree (LeanPool.AsymptoticTrianglePacking.Internal.safeDegree) is controlled by the covariance of the covering events of two vertices, and the cancellation that makes that covariance small requires the exact joint law of two edges entering the round matching:

• two edges that meet can never both be matched (prob_two_matched_of_not_disjoint);
• two disjoint edges f, g are both matched exactly when both are retained and no edge of conflicts f ∪ conflicts g is retained, an event of probability p²(1−p)^{|conflicts f ∪ conflicts g|} (prob_two_matched_disjoint);
• since |A ∪ B| = |A| + |B| − |A ∩ B| and 1 − (1−p)^k ≤ kp, this differs from the product p(1−p)^{c(f)} · p(1−p)^{c(g)} of the two individual matching probabilities by at most |conflicts f ∩ conflicts g|·p³ (prob_two_matched_le).

The last statement is the quantitative brick: summed over the edges at two distinct vertices, the error carries a factor of the CODEGREE (LeanPool.AsymptoticTrianglePacking.Internal.sum_conflicts_inter_card_le), which is what makes the nibble's residual degrees concentrate.

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

theorem LeanPool.AsymptoticTrianglePacking.Internal.prob_retain_avoid {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) {T C : Finset (Finset V)} (hT : T ⊆ H) (hC : C ⊆ H) (hTC : Disjoint T C) : MeasureTheory.volume ((⋂ e ∈ T, ρ.A e) ∩ ⋂ h ∈ C, (ρ.A h)ᶜ) = ENNReal.ofReal (p ^ T.card * (1 - p) ^ C.card)

The general retention pattern probability. For disjoint families T, C ⊆ H, the event that every edge of T is retained and no edge of C is has probability p^|T|·(1−p)^|C|.

theorem LeanPool.AsymptoticTrianglePacking.Internal.prob_two_matched_of_not_disjoint {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) {f g : Finset V} (hne : f ≠ g) (hmeet : ¬Disjoint f g) : {ω : Ω | f ∈ Hypergraph.roundMatching (retainedSet H ρ ω)} ∩ {ω : Ω | g ∈ Hypergraph.roundMatching (retainedSet H ρ ω)} = ∅

Two intersecting edges are never both in the round matching.

theorem LeanPool.AsymptoticTrianglePacking.Internal.twoMatchedEvent_eq {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) {f g : Finset V} (hf : f ∈ H) (hg : g ∈ H) : {ω : Ω | f ∈ Hypergraph.roundMatching (retainedSet H ρ ω)} ∩ {ω : Ω | g ∈ Hypergraph.roundMatching (retainedSet H ρ ω)} = ρ.A f ∩ ρ.A g ∩ ⋂ h ∈ Hypergraph.conflicts H f ∪ Hypergraph.conflicts H g, (ρ.A h)ᶜ

The joint matching event of two edges. Both f and g are matched exactly when both are retained and nothing in conflicts f ∪ conflicts g is.

theorem LeanPool.AsymptoticTrianglePacking.Internal.prob_two_matched_disjoint {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) {f g : Finset V} (hf : f ∈ H) (hg : g ∈ H) (hne : f ≠ g) (hdisj : Disjoint f g) : MeasureTheory.volume ({ω : Ω | f ∈ Hypergraph.roundMatching (retainedSet H ρ ω)} ∩ {ω : Ω | g ∈ Hypergraph.roundMatching (retainedSet H ρ ω)}) = ENNReal.ofReal (p ^ 2 * (1 - p) ^ (Hypergraph.conflicts H f ∪ Hypergraph.conflicts H g).card)

The joint matching probability of two disjoint edges.

theorem LeanPool.AsymptoticTrianglePacking.Internal.prob_two_matched_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) {f g : Finset V} (hf : f ∈ H) (hg : g ∈ H) (hne : f ≠ g) : MeasureTheory.volume.real ({ω : Ω | f ∈ Hypergraph.roundMatching (retainedSet H ρ ω)} ∩ {ω : Ω | g ∈ Hypergraph.roundMatching (retainedSet H ρ ω)}) ≤ p * (1 - p) ^ (Hypergraph.conflicts H f).card * (p * (1 - p) ^ (Hypergraph.conflicts H g).card) + ↑(Hypergraph.conflicts H f ∩ Hypergraph.conflicts H g).card * p ^ 3

The joint matching probability against the product of the individual ones. The two differ by at most |conflicts f ∩ conflicts g|·p³ — the brick that produces the codegree factor in the variance of the safe degree.

LeanPool.AsymptoticTrianglePacking.Internal — the conflict-overlap count at two distinct vertices

Pure Finset combinatorics, no probability. The variance estimate for the safe degree needs the following triple count: summing, over the edges f through u and the edges g through a DIFFERENT vertex u', the number of edges conflicting with both, one gets a bound carrying a factor of the CODEGREE κ:

∑_{f ∋ u} ∑_{g ∋ u'} |conflicts f ∩ conflicts g| ≤ 4 r² κ Δ².

(The corresponding statement at u = u' is false — there the sum is of order Δ³ — which is exactly why the residual degree of a vertex does not concentrate while its SAFE degree does.)

Proof. Writing S = ∑_{h ∈ H} a(h)·b(h) with a(h) = #{f ∋ u : h ∈ conflicts f} and b(h) = #{g ∋ u' : h ∈ conflicts g} (conflictCountAt), split on whether u' ∈ h:

• ∑_{h ∈ H} a(h) = ∑_{f ∋ u} |conflicts f| ≤ Δ·rΔ;
• for u' ∉ h, every g ∋ u' meeting h does so at a vertex w ≠ u', so b(h) ≤ r·κ;
• for u' ∈ h and u ∈ h there are at most codeg(u,u') ≤ κ such h, and a(h), b(h) ≤ Δ;
• for u' ∈ h and u ∉ h there are at most deg(u') ≤ Δ such h, a(h) ≤ rκ and b(h) ≤ Δ.

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

def LeanPool.AsymptoticTrianglePacking.Internal.conflictCountAt {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (x : V) (h : Finset V) : ℕ

The number of edges through x that conflict with a given edge h.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.conflictCountAt H x h = {f ∈ {f ∈ H | x ∈ f} | h ∈ Hypergraph.conflicts H f}.card

theorem LeanPool.AsymptoticTrianglePacking.Internal.conflictCountAt_le_degree {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (x : V) (h : Finset V) : conflictCountAt H x h ≤ Hypergraph.degree H x

conflictCountAt is bounded by the degree of x.

theorem LeanPool.AsymptoticTrianglePacking.Internal.conflictCountAt_le_sum_codegree {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) {x : V} {h : Finset V} : conflictCountAt H x h ≤ ∑ w ∈ h, Hypergraph.codegree H x w

If x ∉ h, then every edge through x conflicting with h meets h at a vertex ≠ x, so conflictCountAt is bounded by a sum of codegrees.

theorem LeanPool.AsymptoticTrianglePacking.Internal.conflictCountAt_le_of_notMem {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 ≤ κ) {x : V} {h : Finset V} (hh : h ∈ H) (hxh : x ∉ h) : conflictCountAt H x h ≤ r * κ

With uniformity and a codegree bound: if x ∉ h, then conflictCountAt H x h ≤ r·κ.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sum_conflictCountAt {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (x : V) : ∑ h ∈ H, conflictCountAt H x h = ∑ f ∈ H with x ∈ f, (Hypergraph.conflicts H f).card

Double counting: summing conflictCountAt H x · over all edges gives the total conflict count of the edges through x.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sum_conflictCountAt_le {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {r Δ : ℕ} (hr : Hypergraph.IsUniform H r) (hΔ : ∀ (y : V), Hypergraph.degree H y ≤ Δ) (x : V) : ∑ h ∈ H, conflictCountAt H x h ≤ Δ * (r * Δ)

The total conflict count of the edges through x is at most Δ·rΔ.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sum_sum_conflicts_inter_eq {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (u u' : V) : ∑ f ∈ H with u ∈ f, ∑ g ∈ H with u' ∈ g, (Hypergraph.conflicts H f ∩ Hypergraph.conflicts H g).card = ∑ h ∈ H, conflictCountAt H u h * conflictCountAt H u' h

The double sum of conflict overlaps, written as a single sum over edges.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sum_conflicts_inter_card_le {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {r Δ κ : ℕ} (hr : Hypergraph.IsUniform H r) (hr1 : 1 ≤ r) (hΔ : ∀ (x : V), Hypergraph.degree H x ≤ Δ) (hκ : ∀ (x y : V), x ≠ y → Hypergraph.codegree H x y ≤ κ) {u u' : V} (huu' : u ≠ u') : ∑ f ∈ H with u ∈ f, ∑ g ∈ H with u' ∈ g, (Hypergraph.conflicts H f ∩ Hypergraph.conflicts H g).card ≤ 4 * r ^ 2 * κ * Δ ^ 2

The conflict-overlap count at two DISTINCT vertices. ∑_{f ∋ u} ∑_{g ∋ u'} |conf f ∩ conf g| ≤ 4 r² κ Δ², where Δ bounds the degrees and κ the codegrees of distinct pairs.

LeanPool.AsymptoticTrianglePacking.Internal — the CODEGREE-tightened pair excess and loss variance

LeanPool.AsymptoticTrianglePacking.Internal.pair_excess_le bounds the pair excess

ℙ(u, u' covered) − q_u q_{u'} ≤ 2 r Δ³ p³ + κ p

by trading the crude product bound deg(u)·deg(u')·p² against the exact rates. Its Δ³p³ term is too lossy for the nibble: fed into LeanPool.AsymptoticTrianglePacking.Internal.centered_second_moment_le it contributes (r−1)²Δ² · 2rΔ³p³ ≈ Δ² γ³ to the variance of the loss weight (with p = γ/((r−1)Δ)), i.e. a standard deviation of order γ^{3/2}Δ, whose Chebyshev failure probability at the natural scale t = ξγΔ is ≈ γ/ξ² — of the same order as the per-round covering rate ≈ γ, hence useless for an exceptional set that must be a small fraction of the coverage.

This file replaces that term by a CODEGREE-controlled one:

ℙ(u, u' covered) − q_u q_{u'} ≤ κ p + 4 r² κ Δ² p³ (pair_excess_le_codegree)

for distinct u, u'. The proof is the exact edge-pair decomposition, not a union bound:

• {u covered} ∩ {u' covered} = ⋃_{f ∋ u} ⋃_{g ∋ u'} (M_f ∩ M_g) with M_f the event that f enters the round matching;
• for f ≠ g the joint matching probability differs from the product q_f q_g by at most |conflicts f ∩ conflicts g|·p³ (LeanPool.AsymptoticTrianglePacking.Internal.prob_two_matched_le — zero when f and g meet);
• the diagonal f = g occurs for at most codeg(u,u') ≤ κ edges, each contributing at most p;
• LeanPool.AsymptoticTrianglePacking.Internal.sum_conflicts_inter_card_le sums the conflict overlaps to 4 r² κ Δ².

Consequently (centered_second_moment_le_codegree)

𝔼[(loss − 𝔼loss)²] ≤ κ·(r−1)Δ·(Δp) + (κp + 4r²κΔ²p³)·((r−1)Δ)²,

which in the nibble regime p = γ/((r−1)Δ), κ = μΔ is O(r μ γ Δ²) — a factor μ (the relative codegree, which the nibble hypothesis lets us choose as small as we like) below the previous O(rγ³Δ²/(r−1)), and it is the bound whose Chebyshev failure probability at scale t = ξγΔ is O(rμ/(ξ²γ)), i.e. arbitrarily small compared with the covering rate γ.

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

theorem LeanPool.AsymptoticTrianglePacking.Internal.prob_matchingEvent {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) {e : Finset V} (he : e ∈ H) : MeasureTheory.volume.real {ω : Ω | e ∈ Hypergraph.roundMatching (retainedSet H ρ ω)} = p * (1 - p) ^ (Hypergraph.conflicts H e).card

The matching event of a single edge has probability p·(1−p)^{c(e)}.

theorem LeanPool.AsymptoticTrianglePacking.Internal.twoCovered_eq_biUnion {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (u u' : V) : {ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)} ∩ {ω : Ω | u' ∈ Hypergraph.covered (retainedSet H ρ ω)} = ⋃ f ∈ {f ∈ H | u ∈ f}, ⋃ g ∈ {g ∈ H | u' ∈ g}, {ω : Ω | f ∈ Hypergraph.roundMatching (retainedSet H ρ ω)} ∩ {ω : Ω | g ∈ Hypergraph.roundMatching (retainedSet H ρ ω)}

The joint covering event of two vertices is the union of the joint matching events of the edge pairs through them.

theorem LeanPool.AsymptoticTrianglePacking.Internal.prob_two_vertices_covered_le_sum {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) (u u' : V) : MeasureTheory.volume.real ({ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)} ∩ {ω : Ω | u' ∈ Hypergraph.covered (retainedSet H ρ ω)}) ≤ coverRate H p u * coverRate H p u' + ↑(Hypergraph.codegree H u u') * p + (∑ f ∈ H with u ∈ f, ∑ g ∈ H with u' ∈ g, ↑(Hypergraph.conflicts H f ∩ Hypergraph.conflicts H g).card) * p ^ 3

The codegree-tightened joint covering bound. For distinct u, u', ℙ(u,u' covered) ≤ q_u q_{u'} + codeg(u,u')·p + (∑_{f ∋ u} ∑_{g ∋ u'} |conf f ∩ conf g|)·p³.

theorem LeanPool.AsymptoticTrianglePacking.Internal.pair_excess_le_codegree {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} {r Δ κ : ℕ} (ρ : BernoulliRetention H p) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hr : Hypergraph.IsUniform H r) (hr1 : 1 ≤ r) (hΔ : ∀ (y : V), Hypergraph.degree H y ≤ Δ) (hκ : ∀ (y z : V), y ≠ z → Hypergraph.codegree H y z ≤ κ) {u u' : V} (huu' : u ≠ u') : MeasureTheory.volume.real ({ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)} ∩ {ω : Ω | u' ∈ Hypergraph.covered (retainedSet H ρ ω)}) - coverRate H p u * coverRate H p u' ≤ ↑κ * p + 4 * ↑r ^ 2 * ↑κ * ↑Δ ^ 2 * p ^ 3

The codegree-tightened pair excess. For distinct u, u',

ℙ(u,u' covered) − q_u q_{u'} ≤ κ p + 4 r² κ Δ² p³.

Both summands carry the codegree bound κ; in the nibble regime κ = μΔ, p = γ/((r−1)Δ) this is O(rμγ/(r−1)), whereas LeanPool.AsymptoticTrianglePacking.Internal.pair_excess_le gives only O(rγ³/(r−1)³ + μγ/(r−1)).

theorem LeanPool.AsymptoticTrianglePacking.Internal.centered_second_moment_le_codegree {V : Type u_1} [DecidableEq V] [Fintype V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {H : Finset (Finset V)} {p : ℝ} {r Δ κ : ℕ} (ρ : BernoulliRetention H p) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hr1 : 1 ≤ 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) : ∫ (ω : Ω), (lossWeight ρ v ω - lossWeightMean H p v) ^ 2 ≤ ↑κ * ((↑r - 1) * ↑Δ) * (↑Δ * p) + (↑κ * p + 4 * ↑r ^ 2 * ↑κ * ↑Δ ^ 2 * p ^ 3) * ((↑r - 1) * ↑Δ) ^ 2

The codegree-tightened variance of the loss weight.

𝔼[(loss − 𝔼loss)²] ≤ κ·(r−1)Δ·(Δp) + (κp + 4r²κΔ²p³)·((r−1)Δ)².

Compare LeanPool.AsymptoticTrianglePacking.Internal.centered_second_moment_le_params, whose second factor is Δ²p² + κp: the term Δ²p² (of order γ² with p = γ/((r−1)Δ)) is replaced by 4r²κΔ²p³ (of order r²μγ³), so the whole bound acquires the codegree factor κ.

LeanPool.AsymptoticTrianglePacking.Internal — the VARIANCE of the covered count, and Chebyshev for

the coverage

LeanPool.AsymptoticTrianglePacking.Internal.exists_tight_round_on controls the coverage of a nibble round by MARKOV applied to the number of uncovered vertices. That is extremely lossy: it only gives

ℙ(covered ≤ N·q/2) ≤ 1 − q/2,

so the competing badness event has to have probability < q/2 ≈ γ/2, and the Markov bound on the badness then forces the deviation tolerances t, s to be of the same order as the whole per-round degree drop γΔ — a band far too wide to be iterated over ≍ γ^{-1}log(1/β) rounds.

This file removes that bottleneck. The covered count Cov = ∑_v 1[v covered] is a sum of indicators whose pair covariances are exactly the pair excesses controlled by LeanPool.AsymptoticTrianglePacking.Internal.pair_excess_le_codegree, so

Var(Cov) ≤ N·q_hi + N²·ε₂, (coveredCount_variance_le)

with ε₂ the (codegree-controlled) pair excess. Chebyshev then gives a coverage failure probability ≤ 4·Var/Q², which in the nibble regime Q ≈ Nγ, ε₂ ≈ μγ is

4/(Nγ) + 4μ/γ,

i.e. ≤ 1/2 as soon as N ≥ 16/γ and μ ≤ γ/16 — INDEPENDENTLY of the deviation tolerances.

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

theorem LeanPool.AsymptoticTrianglePacking.Internal.coveredCount_sub_mean_eq {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, coverRate H p v = ∑ v : V, coverIndC ρ v ω

The centred covered count is the sum of the centred covering indicators.

theorem LeanPool.AsymptoticTrianglePacking.Internal.integrable_sq_centered_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) : MeasureTheory.Integrable (fun (ω : Ω) => (↑(Hypergraph.covered (retainedSet H ρ ω)).card - ∑ v : V, coverRate H p v) ^ 2) MeasureTheory.volume

The centred covered count is square integrable.

theorem LeanPool.AsymptoticTrianglePacking.Internal.integral_sq_centered_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) ^ 2 = ∑ u : V, ∑ u' : V, (MeasureTheory.volume.real ({ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)} ∩ {ω : Ω | u' ∈ Hypergraph.covered (retainedSet H ρ ω)}) - coverRate H p u * coverRate H p u')

The variance of the covered count, as an exact double sum of pair excesses.

theorem LeanPool.AsymptoticTrianglePacking.Internal.coveredCount_variance_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) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {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' ≤ ε₂) : ∫ (ω : Ω), (↑(Hypergraph.covered (retainedSet H ρ ω)).card - ∑ v : V, coverRate H p v) ^ 2 ≤ ↑(Fintype.card V) * qhi + ↑(Fintype.card V) ^ 2 * ε₂

The variance bound for the covered count. With covering rates at most q_hi and pair excesses at most ε₂, the covered count has variance at most N·q_hi + N²·ε₂.

theorem LeanPool.AsymptoticTrianglePacking.Internal.prob_coverage_deviation_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) {Q Cvar : ℝ} (hQ : 0 < Q) (hvar : ∫ (ω : Ω), (↑(Hypergraph.covered (retainedSet H ρ ω)).card - ∑ v : V, coverRate H p v) ^ 2 ≤ Cvar) : MeasureTheory.volume.real {ω : Ω | (Q / 2) ^ 2 ≤ (↑(Hypergraph.covered (retainedSet H ρ ω)).card - ∑ v : V, coverRate H p v) ^ 2} ≤ Cvar / (Q / 2) ^ 2

Chebyshev for the coverage. If the mean coverage is at least Q > 0 and the variance is at most Cvar, the probability that the covered count deviates by Q/2 or more is at most Cvar/(Q/2)².