LeanPool.AsymptoticTrianglePacking.Internal — the first two moments of the loss weight

coverWeight H v C = ∑_{u ≠ v} codeg(v,u)·1[u ∈ C] (LeanPool.AsymptoticTrianglePacking.Internal.Tight.CoverWeight) is a NONNEGATIVE LINEAR combination of the one-round covering indicators. Consequently its mean and its centred second moment are exactly computable from the two covering laws already established:

• prob_vertex_covered_eq — 𝔼[1[u covered]] = coverRate H p u (exact);
• prob_two_vertices_covered_le — ℙ(u,u' covered) ≤ deg·deg·p² + codeg·p.

Results:

• integral_coverWeight — 𝔼[coverWeight] = ∑_{u ≠ v} codeg(v,u)·q_u;
• integral_sq_centered_coverWeight — the centred second moment as the exact double sum ∑_{u,u'} codeg(v,u)·codeg(v,u')·(ℙ(u,u' covered) − q_u q_{u'});
• centered_second_moment_le — the quantitative bound 𝔼[(coverWeight − 𝔼)²] ≤ κ·A·q_hi + ε₂·A², with A = ∑_{u ≠ v} codeg(v,u) = (r−1)deg(v), κ the codegree bound and ε₂ any bound on the pair excess ℙ(u,u' cov) − q_u q_{u'}.

The diagonal term is O(κ·d·γ) and the off-diagonal term O(d²·ε₂); both are o(d²) in the nibble regime, which is precisely the concentration the residual degree cannot have.

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

The covering indicator

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

The indicator that u is covered by the round matching.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.coverInd ρ u ω = if u ∈ Hypergraph.covered (LeanPool.AsymptoticTrianglePacking.Internal.retainedSet H ρ ω) then 1 else 0

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

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

theorem LeanPool.AsymptoticTrianglePacking.Internal.integral_coverInd {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 : V) : ∫ (ω : Ω), coverInd ρ u ω = coverRate H p u

theorem LeanPool.AsymptoticTrianglePacking.Internal.coverInd_mul {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (u u' : V) : (fun (ω : Ω) => coverInd ρ u ω * coverInd ρ u' ω) = ({ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)} ∩ {ω : Ω | u' ∈ Hypergraph.covered (retainedSet H ρ ω)}).indicator 1

The product of two covering indicators is the indicator of the joint event.

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

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

The centred covering indicator

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

The centred covering indicator 1[u covered] − q_u.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.coverIndC ρ u ω = LeanPool.AsymptoticTrianglePacking.Internal.coverInd ρ u ω - LeanPool.AsymptoticTrianglePacking.Internal.coverRate H p u

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

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

The pair covariance.

The loss weight as a linear form

theorem LeanPool.AsymptoticTrianglePacking.Internal.coverWeight_eq_linear {V : Type u_1} [DecidableEq V] [Fintype V] (H : Finset (Finset V)) (v : V) (C : Finset V) : ↑(coverWeight H v C) = ∑ u ∈ Finset.univ.erase v, ↑(Hypergraph.codegree H v u) * if u ∈ C then 1 else 0

coverWeight written as a linear form in the covering indicators.

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

The loss weight of v as a random variable.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.lossWeight ρ v ω = ∑ u ∈ Finset.univ.erase v, ↑(Hypergraph.codegree H v u) * LeanPool.AsymptoticTrianglePacking.Internal.coverInd ρ u ω

noncomputable def LeanPool.AsymptoticTrianglePacking.Internal.lossWeightMean {V : Type u_1} [DecidableEq V] [Fintype V] (H : Finset (Finset V)) (p : ℝ) (v : V) : ℝ

Its deterministic mean.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.lossWeightMean H p v = ∑ u ∈ Finset.univ.erase v, ↑(Hypergraph.codegree H v u) * LeanPool.AsymptoticTrianglePacking.Internal.coverRate H p u

theorem LeanPool.AsymptoticTrianglePacking.Internal.lossWeight_eq' {V : Type u_1} [DecidableEq V] [Fintype V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (v : V) (ω : Ω) : ↑(coverWeight H v (Hypergraph.covered (retainedSet H ρ ω))) = lossWeight ρ v ω

theorem LeanPool.AsymptoticTrianglePacking.Internal.integral_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) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (v : V) : ∫ (ω : Ω), lossWeight ρ v ω = lossWeightMean H p v

The mean of the loss weight.

theorem LeanPool.AsymptoticTrianglePacking.Internal.lossWeight_sub_mean {V : Type u_1} [DecidableEq V] [Fintype V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (v : V) (ω : Ω) : lossWeight ρ v ω - lossWeightMean H p v = ∑ u ∈ Finset.univ.erase v, ↑(Hypergraph.codegree H v u) * coverIndC ρ u ω

The centred loss weight as a linear form in the centred indicators.

theorem LeanPool.AsymptoticTrianglePacking.Internal.integral_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) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (v : V) : ∫ (ω : Ω), (lossWeight ρ v ω - lossWeightMean H p v) ^ 2 = ∑ u ∈ Finset.univ.erase v, ∑ u' ∈ Finset.univ.erase v, ↑(Hypergraph.codegree H v u) * ↑(Hypergraph.codegree H v u') * (MeasureTheory.volume.real ({ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)} ∩ {ω : Ω | u' ∈ Hypergraph.covered (retainedSet H ρ ω)}) - coverRate H p u * coverRate H p u')

The centred second moment of the loss weight, as an exact double sum.