Mathlib.Probability.FiniteMarkedPoissonPartition.Partition
Finite measurable partitions of a marked observation space: restriction maps, exact independent cell experiments, and marginal cell-count laws.
Basic 9 core · 8 supporting 9 to review This file represents a finite measurable partition by its measurable cell classifier. ★ measurable_restrictPartition
Finite measurable partitions and restriction maps
This file represents a finite measurable partition by its measurable cell classifier. It defines the cell sets, their normalized observation laws, and the measurable restriction maps that stably filter a finite marked sequence.
structure FiniteMeasurablePartition unreviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
A finite measurable partition of the sample space X into cells indexed by ι, represented by a classifier assigning each observation to its cell — the cells are the fibres of this map — where that classifier is measurable.
Definition (Lean source)
parameters
fields
The cell containing an observation.
cell :
X → ι
Cell membership is measurable.
measurable_cell :
Measurable cell
def ofSets unreviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
A finite family of measurable, pairwise disjoint sets covering the whole space determines its unique measurable classifier partition.
Definition (Lean source)
noncomputable def ofSets (A : ι → Set X)
(hA : ∀ j, MeasurableSet (A j))
(hdis : Pairwise (fun i j => Disjoint (A i) (A j)))
(hcover : ⋃ j, A j = univ) : FiniteMeasurablePartition X ι := by
classical
have hex : ∀ x : X, ∃ j : ι, x ∈ A j := by
intro x
have hx : x ∈ ⋃ j, A j := by rw [hcover]; exact Set.mem_univ x
simpa only [Set.mem_iUnion] using hx
let c : X → ι := fun x => choose (hex x)
have hc_mem (x : X) : x ∈ A (c x) := Classical.choose_spec (hex x)
have hc_fiber (j : ι) : c ⁻¹' {j} = A j := by
ext x
simp only [Set.mem_preimage, Set.mem_singleton_iff]
constructor
· intro hx
rw [← hx]
exact hc_mem x
· intro hx
by_contra hne
exact Set.disjoint_left.1 (hdis hne) (hc_mem x) hx
exact ⟨c, measurable_to_countable' fun j => hc_fiber j ▸ hA j⟩
def cellSet unreviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
The measurable set forming cell j of a classifier partition.
Definition (Lean source)
def cellMass unreviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
The probability mass of a cell, represented as a nonnegative real.
Definition (Lean source)
noncomputable def cellMass (p : FiniteMeasurablePartition X ι) (P : Measure X) (j : ι) :
ℝ≥0 :=
(P (p.cellSet j)).toNNReal
def cellObservationLaw unreviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
The within-cell observation law is the normalised restriction when the cell has positive mass and the ambient probability law when its mass is zero.
Definition (Lean source)
noncomputable def cellObservationLaw (p : FiniteMeasurablePartition X ι)
(P : Measure X) [IsProbabilityMeasure P] (j : ι) : Measure X :=
if h : P (p.cellSet j) = 0 then P
else (P (p.cellSet j))⁻¹ • P.restrict (p.cellSet j)
def cellIndices unreviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Indices of the marked observations belonging to cell j.
Definition (Lean source)
noncomputable def cellIndices (p : FiniteMeasurablePartition X ι) (j : ι)
(s : FiniteSample (X × ℝ)) : Finset (Fin s.count) := by
classical
exact Finset.univ.filter (fun k => p.cell (s.points k).1 = j)
def restrictCell unreviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Restrict a finite marked sequence to one cell, preserving the original relative order of all points that lie in that cell.
Definition (Lean source)
noncomputable def restrictCell (p : FiniteMeasurablePartition X ι) (j : ι)
(s : FiniteSample (X × ℝ)) : FiniteSample (X × ℝ) := by
classical
let t := p.cellIndices j s
exact ⟨t.card, fun k => s.points (t.orderIsoOfFin rfl k)⟩
def restrictPartition unreviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Restrict a finite marked sequence simultaneously to every partition cell.
Definition (Lean source)
noncomputable def restrictPartition (p : FiniteMeasurablePartition X ι)
(s : FiniteSample (X × ℝ)) : ι → FiniteSample (X × ℝ) :=
fun j => p.restrictCell j s
lemma measurable_restrictPartition unreviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
For a finite measurable partition p of the sample space into cells indexed by ι, the map sending a finite marked sequence to its family of restrictions to every cell simultaneously is measurable.
Formal statement
Proof (Lean source)
lemma measurable_restrictPartition (p : FiniteMeasurablePartition X ι) :
Measurable p.restrictPartition := by
unfold restrictPartition
exact measurable_pi_lambda _ fun j => p.measurable_restrictCell j
8 supporting declarations (lemmas, instances)
-
ofSets_cellSetlemma — The classifier constructed from a disjoint measurable cover has exactly the supplied sets as its fibres.hypothesesA :ι → Set XhA :∀ j, MeasurableSet (A j)hdis :Pairwise (fun i j => Disjoint (A i) (A j))hcover :⋃ j, A j = univj :ιProof (Lean source)
lemma ofSets_cellSet (A : ι → Set X) (hA : ∀ j, MeasurableSet (A j)) (hdis : Pairwise (fun i j => Disjoint (A i) (A j))) (hcover : ⋃ j, A j = univ) (j : ι) : (ofSets A hA hdis hcover).cell ⁻¹' {j} = A j := by classical unfold ofSets dsimp only ext x simp only [Set.mem_preimage, Set.mem_singleton_iff] constructor · intro hx rw [← hx] exact Classical.choose_spec (show ∃ k, x ∈ A k by have hx' : x ∈ ⋃ k, A k := by rw [hcover]; exact Set.mem_univ x simpa only [Set.mem_iUnion] using hx') · intro hx let hex : ∃ k, x ∈ A k := by have hx' : x ∈ ⋃ k, A k := by rw [hcover]; exact Set.mem_univ x simpa only [Set.mem_iUnion] using hx' by_contra hne exact Set.disjoint_left.1 (hdis hne) (Classical.choose_spec hex) hx -
measurableSet_cellSetlemma — Every classifier cell is measurable.Proof (Lean source)
lemma measurableSet_cellSet (p : FiniteMeasurablePartition X ι) (j : ι) : MeasurableSet (p.cellSet j) := by exact (measurableSet_singleton j).preimage p.measurable_cell -
disjoint_cellSetlemma — Distinct classifier cells are disjoint.hypothesesconclusionDisjoint (p.cellSet i) (p.cellSet j)Proof (Lean source)
lemma disjoint_cellSet (p : FiniteMeasurablePartition X ι) {i j : ι} (hij : i ≠ j) : Disjoint (p.cellSet i) (p.cellSet j) := by apply Set.disjoint_left.2 intro x hxi hxj exact hij (hxi.symm.trans hxj) -
iUnion_cellSetlemma — The union of all classifier cells is the whole observation space.Proof (Lean source)
lemma iUnion_cellSet (p : FiniteMeasurablePartition X ι) : ⋃ j : ι, p.cellSet j = univ := by ext x simp [cellSet] -
sum_cellMasslemma — Cell masses sum to one under a probability law.hypothesesp :P :conclusion∑ j, p.cellMass P j = 1Proof (Lean source)
lemma sum_cellMass (p : FiniteMeasurablePartition X ι) (P : Measure X) [IsProbabilityMeasure P] : ∑ j, p.cellMass P j = 1 := by apply ENNReal.coe_injective rw [ENNReal.coe_finset_sum] simp only [ENNReal.coe_one, cellMass] simp_rw [ENNReal.coe_toNNReal (measure_ne_top P _)] calc ∑ j, P (p.cellSet j) = P (⋃ j ∈ (Finset.univ : Finset ι), p.cellSet j) := by symm apply measure_biUnion_finset · intro i _ j _ hij exact p.disjoint_cellSet hij · intro j _ exact p.measurableSet_cellSet j _ = P (⋃ j, p.cellSet j) := by simp _ = 1 := by rw [p.iUnion_cellSet, measure_univ] -
cellObservationLaw_isProbabilityMeasureinstance — The within-cell observation law is a probability measure, including the zero-mass fallback branch.instance cellObservationLaw_isProbabilityMeasure (p : FiniteMeasurablePartition X ι) (P : Measure X) [IsProbabilityMeasure P] (j : ι) : IsProbabilityMeasure (p.cellObservationLaw P j) := by unfold cellObservationLaw split_ifs with h · infer_instance · constructor rw [Measure.smul_apply, Measure.restrict_apply MeasurableSet.univ] simpa using ENNReal.inv_mul_cancel h (measure_ne_top P _) -
cellObservationLaw_apply_cellSetlemma — A positive-mass within-cell law assigns probability one to its own cell.hypothesesp :P :j :ιhj :P (p.cellSet j) ≠ 0conclusionp.cellObservationLaw P j (p.cellSet j) = 1Proof (Lean source)
lemma cellObservationLaw_apply_cellSet (p : FiniteMeasurablePartition X ι) (P : Measure X) [IsProbabilityMeasure P] (j : ι) (hj : P (p.cellSet j) ≠ 0) : p.cellObservationLaw P j (p.cellSet j) = 1 := by rw [cellObservationLaw, dif_neg hj, Measure.smul_apply, Measure.restrict_apply (p.measurableSet_cellSet j)] simpa using ENNReal.inv_mul_cancel hj (measure_ne_top P _) -
measurable_restrictCelllemma — Restriction to one measurable cell is a measurable map on finite marked sequences.Proof (Lean source)
lemma measurable_restrictCell (p : FiniteMeasurablePartition X ι) (j : ι) : Measurable (p.restrictCell j) := by classical intro s hs rw [MeasurableSpace.measurableSet_iInf] at hs ⊢ intro n change MeasurableSet (fixedSizeEmbed n ⁻¹' (p.restrictCell j ⁻¹' s)) rw [show fixedSizeEmbed n ⁻¹' (p.restrictCell j ⁻¹' s) = ⋃ t : Finset (Fin n), {x : Fin n → X × ℝ | p.cellIndices j (fixedSizeEmbed n x) = t} ∩ (fun x : Fin n → X × ℝ => fun k => x (t.orderIsoOfFin rfl k)) ⁻¹' (fixedSizeEmbed t.card ⁻¹' s) by ext x simp only [mem_preimage, mem_iUnion, mem_inter_iff, mem_setOf_eq] constructor · intro hx let t := p.cellIndices j (fixedSizeEmbed n x) refine ⟨t, rfl, ?_⟩ exact hx · rintro ⟨t, ht, hx⟩ subst t exact hx] apply MeasurableSet.iUnion intro t apply MeasurableSet.inter · rw [show {x : Fin n → X × ℝ | p.cellIndices j (fixedSizeEmbed n x) = t} = ⋂ k : Fin n, if k ∈ t then {x : Fin n → X × ℝ | p.cell (x k).1 = j} else {x : Fin n → X × ℝ | p.cell (x k).1 = j}ᶜ by ext x simp only [Set.mem_setOf_eq, Set.mem_iInter] refine Iff.trans Finset.ext_iff ?_ simp only [cellIndices, FiniteSample.count, FiniteSample.points, fixedSizeEmbed, mem_filter, Finset.mem_univ, true_and] apply forall_congr' intro k by_cases hkt : k ∈ t · simp only [hkt, if_true, Set.mem_setOf_eq] constructor · intro h exact (Finset.mem_filter.1 (h.2 hkt)).2 · intro hk constructor · intro _ exact hkt · intro _ exact Finset.mem_filter.2 ⟨Finset.mem_univ _, hk⟩ · simp only [hkt, if_false, Set.mem_compl_iff, Set.mem_setOf_eq] constructor · intro h hk have hkf : k ∈ ({k | p.cell (x k).1 = j} : Finset (Fin n)) := Finset.mem_filter.2 ⟨Finset.mem_univ _, hk⟩ exact hkt (h.1 hkf) · intro hk constructor · intro hkf exact (hk (Finset.mem_filter.1 hkf).2).elim · intro hkt' exact (hkt hkt').elim] apply MeasurableSet.iInter intro k split_ifs · exact (p.measurable_cell.comp ((measurable_pi_apply k).fst)) (measurableSet_singleton j) · exact ((p.measurable_cell.comp ((measurable_pi_apply k).fst)) (measurableSet_singleton j)).compl · have hst : MeasurableSet (fixedSizeEmbed t.card ⁻¹' s) := hs t.card exact hst.preimage (by fun_prop)
CellLaws 1 core · 1 supporting 1 to review This file derives each cell's Poisson count law and its exact conditional marked sample law from the joint finite-partition splitting theorem. ★ map_restrictCell_count_finiteMarkedPoissonSampleLaw
Marginal laws for partition cells
This file derives each cell's Poisson count law and its exact conditional marked sample law from the joint finite-partition splitting theorem.
lemma map_restrictCell_count_finiteMarkedPoissonSampleLaw unreviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Cell counts are Poisson. Under the marked Poisson sample law with base probability measure P, mark distribution R, and nonnegative intensity lam, the number of marked observations landing in cell j of the finite measurable partition p, viewed as a random variable, is Poisson distributed with mean equal to lam times the P-mass of cell j.
Formal statement
hypotheses
p :
P :
R :
lam :
ℝ≥0
j :
ι
conclusion
Measure.map (fun s => (p.restrictCell j s).count) (finiteMarkedPoissonSampleLaw P R lam)
= poissonMeasure (lam * p.cellMass P j)
Proof (Lean source)
lemma map_restrictCell_count_finiteMarkedPoissonSampleLaw
[StandardBorelSpace X]
(p : FiniteMeasurablePartition X ι)
(P : Measure X) [IsProbabilityMeasure P]
(R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) (j : ι) :
Measure.map (fun s => (p.restrictCell j s).count)
(finiteMarkedPoissonSampleLaw P R lam) =
poissonMeasure (lam * p.cellMass P j) := by
/-
Prefer deriving this from the joint splitting theorem by mapping the `j`th
coordinate and then the measurable count map; `Measure.pi_map_eval` gives
the marginal of the finite product. A separate thinning calculation should
only be used if it materially shortens the proof.
-/
classical
let μ := finiteMarkedPoissonSampleLaw P R lam
let ν : ι → Measure (FiniteSample (X × ℝ)) := fun k =>
finiteMarkedPoissonSampleLaw (p.cellObservationLaw P k) R
(lam * p.cellMass P k)
have hjoint : Measure.map p.restrictPartition μ = Measure.pi ν := by
exact map_restrictPartition_finiteMarkedPoissonSampleLaw p P R lam
have hcell : Measure.map (p.restrictCell j) μ = ν j := by
calc
Measure.map (p.restrictCell j) μ =
Measure.map (Function.eval j)
(Measure.map p.restrictPartition μ) := by
rw [Measure.map_map (measurable_pi_apply j)
p.measurable_restrictPartition]
rfl
_ = Measure.map (Function.eval j) (Measure.pi ν) := by rw [hjoint]
_ = ν j := by
rw [Measure.pi_map_eval]
simp [ν]
change Measure.map (FiniteSample.count ∘ p.restrictCell j) μ =
poissonMeasure (lam * p.cellMass P j)
rw [← Measure.map_map measurable_finiteSample_count
(p.measurable_restrictCell j), hcell]
exact finiteMarkedPoissonSampleLaw_map_count
(p.cellObservationLaw P j) R (lam * p.cellMass P j)
1 supporting declaration (lemmas, instances)
-
cellLaw_restrict_count_eqlemma — On its count-n fibre, the jth cell experiment is the Poisson mass at n times n independent draws from the normalised restriction and mark law.hypothesesp :P :R :lam :ℝ≥0j :ιn :ℕconclusion(finiteMarkedPoissonSampleLaw (p.cellObservationLaw P j) R (lam * p.cellMass P j)).restrict (FiniteSample.count ⁻¹' ({n} : Set ℕ))= (poissonMeasure (lam * p.cellMass P j)) ({n} : Set ℕ) • Measure.map (fixedSizeEmbed n) (Measure.pi (fun _ : Fin n => (p.cellObservationLaw P j).prod R))Proof (Lean source)
lemma cellLaw_restrict_count_eq (p : FiniteMeasurablePartition X ι) (P : Measure X) [IsProbabilityMeasure P] (R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) (j : ι) (n : ℕ) : (finiteMarkedPoissonSampleLaw (p.cellObservationLaw P j) R (lam * p.cellMass P j)).restrict (FiniteSample.count ⁻¹' ({n} : Set ℕ)) = (poissonMeasure (lam * p.cellMass P j)) ({n} : Set ℕ) • Measure.map (fixedSizeEmbed n) (Measure.pi (fun _ : Fin n => (p.cellObservationLaw P j).prod R)) := by exact finiteMarkedPoissonSampleLaw_restrict_count_eq (p.cellObservationLaw P j) R (lam * p.cellMass P j) n
Splitting 1 core · 0 supporting 1 to review This file proves the exact joint law of the restrictions of a finite marked Poisson sample to the cells of a finite measurable partition. ★ map_restrictPartition_finiteMarkedPoissonSampleLaw
Poisson splitting across a finite partition
This file proves the exact joint law of the restrictions of a finite marked Poisson sample to the cells of a finite measurable partition. The proof tracks the complete vector of cell counts and combines the multinomial count allocation with the conditional product laws within cells.
lemma map_restrictPartition_finiteMarkedPoissonSampleLaw unreviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Partition splitting. Under the marked Poisson sample law with base probability measure P, mark distribution R, and nonnegative intensity lam, restricting the sample to each cell of the finite measurable partition p yields, jointly across cells, the product of independent marked Poisson sample laws, one per cell j, each with base measure p.cellObservationLaw P j, mark distribution R, and intensity lam times the P-mass of cell j.
Formal statement
hypotheses
p :
P :
R :
lam :
ℝ≥0
conclusion
Measure.map p.restrictPartition (finiteMarkedPoissonSampleLaw P R lam)
= Measure.pi (fun j : ι => finiteMarkedPoissonSampleLaw (p.cellObservationLaw P j) R (lam * p.cellMass P j))
Proof (Lean source)
lemma map_restrictPartition_finiteMarkedPoissonSampleLaw
[StandardBorelSpace X]
(p : FiniteMeasurablePartition X ι)
(P : Measure X) [IsProbabilityMeasure P]
(R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) :
Measure.map p.restrictPartition (finiteMarkedPoissonSampleLaw P R lam) =
Measure.pi (fun j : ι =>
finiteMarkedPoissonSampleLaw (p.cellObservationLaw P j) R
(lam * p.cellMass P j)) := by
/-
Proof route for the filler: disintegrate both sides over the complete cell-count
vector `c : ι → ℕ`. On a fixed global count, partition the i.i.d. tuple
by its classifier word; each word with histogram `c` pushes forward to the
same product of the fixed-size within-cell laws, up to coordinate
reindexing. Count the words in that histogram fibre and combine its
multinomial factor with the scalar Poisson mass. The resulting coefficient
is the product of the cell Poisson masses. Treat zero-mass cells before
cancelling cell masses. `Measure.pi_map_piCongrLeft` and
`measurePreserving_piCongrLeft` are the intended permutation tools.
-/
let μ := Measure.map p.restrictPartition
(finiteMarkedPoissonSampleLaw P R lam)
let ν := Measure.pi (fun j : ι =>
finiteMarkedPoissonSampleLaw (p.cellObservationLaw P j) R
(lam * p.cellMass P j))
have hrest (c : ι → ℕ) :
μ.restrict (partitionCountFiber (Y := X × ℝ) c) =
ν.restrict (partitionCountFiber (Y := X × ℝ) c) := by
rw [show μ = Measure.map p.restrictPartition
(finiteMarkedPoissonSampleLaw P R lam) by rfl,
map_restrictPartition_restrict_partitionCountFiber p P R lam c]
rw [show ν = Measure.pi (fun j : ι =>
finiteMarkedPoissonSampleLaw (p.cellObservationLaw P j) R
(lam * p.cellMass P j)) by rfl,
pi_cellLaws_restrict_partitionCountFiber p P R lam c]
rw [poisson_multinomial_coefficient lam (p.cellMass P)
(p.sum_cellMass P) c]
have hdis : Pairwise (onFun Disjoint
(fun c : ι → ℕ => partitionCountFiber (Y := X × ℝ) c)) := by
intro c d hcd
apply Set.disjoint_left.2
intro q hqc hqd
apply hcd
funext j
exact (hqc j).symm.trans (hqd j)
have hcover : ⋃ c : ι → ℕ, partitionCountFiber (Y := X × ℝ) c = univ := by
ext q
simp only [Set.mem_iUnion, Set.mem_univ, iff_true]
exact ⟨fun j => (q j).count, fun _ => rfl⟩
change μ = ν
calc
μ = μ.restrict univ := by rw [Measure.restrict_univ]
_ = μ.restrict (⋃ c : ι → ℕ,
partitionCountFiber (Y := X × ℝ) c) := by rw [hcover]
_ = Measure.sum (fun c : ι → ℕ =>
μ.restrict (partitionCountFiber (Y := X × ℝ) c)) := by
exact Measure.restrict_iUnion hdis measurableSet_partitionCountFiber
_ = Measure.sum (fun c : ι → ℕ =>
ν.restrict (partitionCountFiber (Y := X × ℝ) c)) := by
congr 1
funext c
exact hrest c
_ = ν.restrict (⋃ c : ι → ℕ,
partitionCountFiber (Y := X × ℝ) c) := by
exact (Measure.restrict_iUnion hdis measurableSet_partitionCountFiber).symm
_ = ν.restrict univ := by rw [hcover]
_ = ν := Measure.restrict_univ