LeanPool.AsymptoticTrianglePacking.Internal — Module C4b-3b (measurability) : the covered event is

measurable

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

To integrate the residual degree (turning survival probabilities into an expected-value bound) we need the covered events to be measurable. Since the retained set at ω is H.filter (ω ∈ A ·) and the round's matching / covered set are finite Boolean combinations of the retention events A e (over the finite edge set H), each covered event is measurable.

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

theorem LeanPool.AsymptoticTrianglePacking.Internal.measurableSet_vertex_covered {V : Type u_1} [DecidableEq V] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] {H : Finset (Finset V)} {p : ℝ} (ρ : BernoulliRetention H p) (x : V) : MeasurableSet {ω : Ω | x ∈ Hypergraph.support (Hypergraph.roundMatching (retainedSet H ρ ω))}

Measurability of the vertex-covered event. {ω | x ∈ covered(ω)} is measurable: it is a finite Boolean combination of the retention events ρ.A e, e ∈ H.

Hint: x ∈ support (roundMatching (retainedSet H ρ ω)) unfolds to ∃ e ∈ retainedSet H ρ ω, x ∈ e ∧ (∀ f ∈ retainedSet H ρ ω, f ≠ e → Disjoint e f), and e ∈ retainedSet H ρ ω ↔ e ∈ H ∧ ω ∈ ρ.A e. Rewrite the set as a finite ⋃ e ∈ H.filter (x ∈ ·), (ρ.A e ∩ ⋂ f ∈ H.filter (fun f => f ≠ e ∧ ¬ Disjoint e f), (ρ.A f)ᶜ) (or an equivalent finite Boolean combination), then close by MeasurableSet.iUnion / .biUnion / .iInter / .inter / .compl using ρ.meas. All index sets are finite Finsets, so the combination is finite.