LeanPool.AsymptoticTrianglePacking.Internal — the SAFE degree and its SHARP expectation

The residual degree deg_res(v) of a vertex is not the right random variable for the nibble invariant: it collapses to 0 on the event "v itself is covered", an event of constant probability ≈ γ, so deg_res(v) has standard deviation of order d and cannot concentrate. The classical fix is to track instead the safe degree

safeDegree H C v = #{e ∈ H : v ∈ e, (e \ {v}) ∩ C = ∅},

the number of edges at v whose OTHER vertices all survive the round. It agrees with the residual degree exactly on the event {v ∉ C} (safeDegree_eq_residual_degree_of_not_covered), which is the only event on which the residual degree at v matters, and — unlike the residual degree — it is a sum of deg(v) indicators none of which is governed by a single common event.

This file computes its expectation SHARPLY, two-sidedly:

∑_{e ∋ v} (1 − ∑_{u ∈ e∖v} q_u) ≤ 𝔼[safeDeg(v)] ≤ ∑_{e ∋ v} (1 − ∑_{u ∈ e∖v} q_u + pairs),

with q_u = coverRate H p u the EXACT covering rate of u (prob_vertex_covered_eq) and pairs the second-order Bonferroni correction, bounded by prob_two_vertices_covered_le. The two bounds agree to second order, which is exactly what the loose brackets residual_degree_expectation_lower/upper fail to do.

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

The safe degree

def LeanPool.AsymptoticTrianglePacking.Internal.safeDegree {V : Type u_1} [DecidableEq V] (H : Finset (Finset V)) (C : Finset V) (v : V) : ℕ

The safe degree. The number of edges at v whose vertices OTHER than v all avoid C.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.safeDegree H C v = {e ∈ H | v ∈ e ∧ Disjoint (e.erase v) C}.card

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeDegree_eq_residual_degree_of_not_covered {V : Type u_1} [DecidableEq V] {H R : Finset (Finset V)} {v : V} (hv : v ∉ Hypergraph.covered R) : safeDegree H (Hypergraph.covered R) v = Hypergraph.degree (Hypergraph.residual H R) v

On the event that v is not covered, the safe degree IS the residual degree.

theorem LeanPool.AsymptoticTrianglePacking.Internal.residual_degree_le_safeDegree {V : Type u_1} [DecidableEq V] {H R : Finset (Finset V)} (v : V) : Hypergraph.degree (Hypergraph.residual H R) v ≤ safeDegree H (Hypergraph.covered R) v

The residual degree never exceeds the safe degree.

The safe-degree indicator and its expectation

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

The indicator that all vertices of e other than v survive the round.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.safeIndicator ρ v e ω = if Disjoint (e.erase v) (Hypergraph.covered (LeanPool.AsymptoticTrianglePacking.Internal.retainedSet H ρ ω)) then 1 else 0

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeEvent_eq_compl {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (v : V) (e : Finset V) : {ω : Ω | Disjoint (e.erase v) (Hypergraph.covered (retainedSet H ρ ω))} = (⋃ u ∈ e.erase v, {ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)})ᶜ

The "all other vertices survive" event is the complement of the union of covering events.

theorem LeanPool.AsymptoticTrianglePacking.Internal.measurableSet_safeEvent {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (v : V) (e : Finset V) : MeasurableSet {ω : Ω | Disjoint (e.erase v) (Hypergraph.covered (retainedSet H ρ ω))}

theorem LeanPool.AsymptoticTrianglePacking.Internal.integrable_safeIndicator {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 : Finset V) : MeasureTheory.Integrable (safeIndicator ρ v e) MeasureTheory.volume

theorem LeanPool.AsymptoticTrianglePacking.Internal.integral_safeIndicator {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 : Finset V) : ∫ (ω : Ω), safeIndicator ρ v e ω = 1 - MeasureTheory.volume.real (⋃ u ∈ e.erase v, {ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)})

The expectation of the safe indicator is 1 − ℙ(some other vertex of e is covered).

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeDegree_eq_sum {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) = ∑ e ∈ H with v ∈ e, safeIndicator ρ v e ω

The safe degree is the sum of the safe indicators of the edges through v.

theorem LeanPool.AsymptoticTrianglePacking.Internal.integrable_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)) MeasureTheory.volume

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeDegree_expectation_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) = ∑ e ∈ H with v ∈ e, (1 - MeasureTheory.volume.real (⋃ u ∈ e.erase v, {ω : Ω | u ∈ Hypergraph.covered (retainedSet H ρ ω)}))

The expectation of the safe degree, as a sum over the edges at v.

The sharp two-sided expectation

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeDegree_expectation_ge {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 ∈ H with v ∈ e, (1 - ∑ u ∈ e.erase v, coverRate H p u) ≤ ∫ (ω : Ω), ↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v)

Sharp LOWER bound on the expected safe degree (union bound on the covering events). 𝔼[safeDeg(v)] ≥ ∑_{e ∋ v} (1 − ∑_{u ∈ e∖v} q_u).

theorem LeanPool.AsymptoticTrianglePacking.Internal.safeDegree_expectation_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) : ∫ (ω : Ω), ↑(safeDegree H (Hypergraph.covered (retainedSet H ρ ω)) v) ≤ ∑ e ∈ H with v ∈ e, (1 - ∑ u ∈ e.erase v, coverRate H p u + ∑ u ∈ e.erase v, ∑ u' ∈ (e.erase v).erase u, (↑(Hypergraph.degree H u) * ↑(Hypergraph.degree H u') * p ^ 2 + ↑(Hypergraph.codegree H u u') * p))

Sharp UPPER bound on the expected safe degree (second Bonferroni inequality, with the pairwise corrections). 𝔼[safeDeg(v)] ≤ ∑_{e ∋ v} (1 − ∑_{u} q_u + ∑_{u ≠ u'} ℙ(u,u' both covered)).