LeanPool.AsymptoticTrianglePacking.Internal — the variance of the loss weight

Quantitative form of LeanPool.AsymptoticTrianglePacking.Internal.integral_sq_centered_lossWeight. Two ingredients:

• pair_excess_le — the pair excess ℙ(u,u' covered) − q_u q_{u'} is at most 2rΔ³p³ + κp. Both summands are genuinely of higher order than q ≈ Δp: the first because it carries an extra factor rΔp ≈ γ, the second because it carries the CODEGREE κ. (The exact covering rate q_u is bounded below by deg(u)·p(1−p)^{rΔ}, coverRate_ge, which is what lets the crude second-moment bound deg·deg·p² of prob_two_vertices_covered_le be traded against the product q_u q_{u'}.)
• sum_codegree_erase_eq — ∑_{u ≠ v} codeg(v,u) = (r−1)·deg(v), the total weight of the linear form.

Together they give centered_second_moment_le:

𝔼[(loss − 𝔼 loss)²] ≤ κ·A·q_hi + ε₂·A², A = (r−1)·deg(v),

which in the nibble regime p = γ/(rΔ), κ = μΔ is O(μΔ²γ + Δ²(γ³/r² + μγ)) = o(Δ²). This is the concentration that the residual degree does not have.

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

theorem LeanPool.AsymptoticTrianglePacking.Internal.coverRate_ge {V : Type u_1} [DecidableEq V] {H : Finset (Finset V)} {p : ℝ} {r Δ : ℕ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hr : Hypergraph.IsUniform H r) (hΔ : ∀ (y : V), Hypergraph.degree H y ≤ Δ) (x : V) : ↑(Hypergraph.degree H x) * (p * (1 - p) ^ (r * Δ)) ≤ coverRate H p x

Lower bound on the exact covering rate.

theorem LeanPool.AsymptoticTrianglePacking.Internal.pair_excess_le {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) (hΔ : ∀ (y : V), Hypergraph.degree H y ≤ Δ) (hκ : ∀ (y z : V), y ≠ z → Hypergraph.codegree H y z ≤ κ) {x y : V} (hxy : x ≠ y) : MeasureTheory.volume.real ({ω : Ω | x ∈ Hypergraph.covered (retainedSet H ρ ω)} ∩ {ω : Ω | y ∈ Hypergraph.covered (retainedSet H ρ ω)}) - coverRate H p x * coverRate H p y ≤ 2 * ↑r * ↑Δ ^ 3 * p ^ 3 + ↑κ * p

The pair excess. For x ≠ y, ℙ(x,y covered) − q_x q_y ≤ 2rΔ³p³ + κp.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sum_codegree_erase_eq {V : Type u_1} [DecidableEq V] [Fintype V] {H : Finset (Finset V)} {r : ℕ} (hr : Hypergraph.IsUniform H r) (v : V) : ∑ u ∈ Finset.univ.erase v, Hypergraph.codegree H v u = (r - 1) * Hypergraph.degree H v

The total weight of the linear form: ∑_{u ≠ v} codeg(v,u) = (r−1)·deg(v).

theorem LeanPool.AsymptoticTrianglePacking.Internal.centered_second_moment_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) (v : V) {κ : ℕ} {qhi ε₂ : ℝ} (hκ : ∀ (u : V), u ≠ v → Hypergraph.codegree H v u ≤ κ) (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' ≤ ε₂) : ∫ (ω : Ω), (lossWeight ρ v ω - lossWeightMean H p v) ^ 2 ≤ (↑κ * ∑ u ∈ Finset.univ.erase v, ↑(Hypergraph.codegree H v u)) * qhi + ε₂ * (∑ u ∈ Finset.univ.erase v, ↑(Hypergraph.codegree H v u)) ^ 2

The quantitative variance bound for the loss weight.