A total pointer from a family of cells

Category: 1-Mathlib. No CSD content.

A recurring pattern: a probability space is carved into finitely many disjoint measurable cells carrying prescribed weights, and one wants a total readout function whose fibres are those cells. Totality is the only wrinkle — the cells generally cover the space up to a null set, not exactly — so the leftover is sent to a default index and shown not to matter.

Extracted at the second consumer (CONVENTIONS.md §9, rule of two):

• RecordLayer.cdfDeIsolationInteraction — the CDF cells on the fibre ℝ;
• the competing-clock race cells on the fibre Fin (n+1) → ℝ (Mathlib/Probability/CompetingExponentials.lean).

Both need exactly cellPointer and measure_cellPointer_preimage.

noncomputable def MeasureTheory.cellPointer {F : Type u_1} {ι : Type u_2} [Fintype ι] (C : ι → Set F) (i₀ : ι) (x : F) : ι

The total pointer of a cell family: report the cell containing x, or the default i₀ when x lies in none of them.

Equations

• MeasureTheory.cellPointer C i₀ x = if h : ∃ (i : ι), x ∈ C i then h.choose else i₀

theorem MeasureTheory.cellPointer_eq_of_mem {F : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] {C : ι → Set F} (hdisj : Pairwise (Function.onFun Disjoint C)) (i₀ : ι) {x : F} {i : ι} (hx : x ∈ C i) : cellPointer C i₀ x = i

theorem MeasureTheory.cellPointer_preimage {F : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] {C : ι → Set F} (hdisj : Pairwise (Function.onFun Disjoint C)) (i₀ i : ι) : cellPointer C i₀ ⁻¹' {i} = C i ∪ if i = i₀ then (⋃ (j : ι), C j)ᶜ else ∅

The pointer's fibre over i: the cell, together with the leftover when i is the default.

theorem MeasureTheory.measurable_cellPointer {F : Type u_1} {ι : Type u_2} [MeasurableSpace F] [Fintype ι] [DecidableEq ι] [MeasurableSpace ι] {C : ι → Set F} (hmeas : ∀ (i : ι), MeasurableSet (C i)) (hdisj : Pairwise (Function.onFun Disjoint C)) (i₀ : ι) : Measurable (cellPointer C i₀)

theorem MeasureTheory.measure_cellPointer_preimage {F : Type u_1} {ι : Type u_2} [MeasurableSpace F] [Fintype ι] [DecidableEq ι] {ν : Measure F} [IsProbabilityMeasure ν] {C : ι → Set F} (hmeas : ∀ (i : ι), MeasurableSet (C i)) (hdisj : Pairwise (Function.onFun Disjoint C)) {r : ι → ℝ} (hrnn : ∀ (i : ι), 0 ≤ r i) (hr : ∀ (i : ι), ν (C i) = ENNReal.ofReal (r i)) (hsum : ∑ i : ι, r i = 1) (i₀ i : ι) : ν (cellPointer C i₀ ⁻¹' {i}) = ENNReal.ofReal (r i)

★ The pointer's fibres carry the cell weights. The leftover is null because the cells are disjoint and their weights already exhaust the probability, so the default index gains nothing.