LeanPool.AsymptoticTrianglePacking.Internal — Module C4b-1 : probability that an edge survives a

nibble round

Standalone, Mathlib-only. Foundation for the Rödl-nibble project.

The retention is now modelled as genuine independent events A e ("edge e is retained"), each with probability p (a Bernoulli retention — stronger than the [0,1]-mean-p indicators of C2/C3/C4a, which only recorded the mean). An edge e ends up in the round's matching exactly when it is retained and none of its conflicting edges is retained. By independence, that probability factors as p · (1-p)^{c(e)}, where c(e) = |conflicts H e|.

conflicts comes from LeanPool.AsymptoticTrianglePacking.Internal.Conflict. Must be placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

structure LeanPool.AsymptoticTrianglePacking.Internal.BernoulliRetention {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] (H : Finset (Finset V)) (p : ℝ) : Type (max u_1 u_2)

A Bernoulli retention on H with parameter p: an independent family of events A e ("edge e is retained"), each of probability p on the edges of H.

• A : Finset V → Set Ω

  The event that the edge is retained in a nibble round.

• meas (e : Finset V) : MeasurableSet (self.A e)
• indep : ProbabilityTheory.iIndepSet self.A MeasureTheory.volume
• prob (e : Finset V) : e ∈ H → MeasureTheory.volume (self.A e) = ENNReal.ofReal p

theorem LeanPool.AsymptoticTrianglePacking.Internal.edge_survives_prob {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 (ρ.A e ∩ ⋂ f ∈ Hypergraph.conflicts H e, (ρ.A f)ᶜ) = ENNReal.ofReal (p * (1 - p) ^ (Hypergraph.conflicts H e).card)

C4b-1 — edge survival probability. The event that e is retained and none of its conflicting edges is retained has probability p · (1-p)^{c(e)}. Proof: the events A e and the complements (A f)ᶜ for f ∈ conflicts H e are jointly independent (all distinct, since conflicts H e excludes e); the measure of their intersection factors as the product ℙ(A e) · ∏_{f} ℙ((A f)ᶜ) = p · (1-p)^{c(e)} (each conflict f ∈ H, so ρ.prob applies, and ℙ((A f)ᶜ) = 1 - p).