Mathlib.Probability.Poisson.FinitePartition.Partition
Finite-partition constructions for Poisson counts, their cell laws, and splitting identities.
Basic 9 core · 8 supporting 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 reviewed
⚑ 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. The structure itself does not require the index type to be finite or singletons of it to be measurable; results that need finitely many cells or measurable individual cells assume those conditions separately.
Definition (Lean source)
parameters
fields
The cell containing an observation.
cell :
X → ι
Cell membership is measurable.
measurable_cell :
Measurable cell
def ofSets reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Given a finite family of candidate cells, if each cell is measurable, distinct cells are disjoint, and the cells cover the space, the constructed partition assigns each observation to its unique cell.
Definition (Lean source)
parameters
X :
Type u_1
ι :
Type u_2
A :
ι → Set X
hA :
∀ j, MeasurableSet (A j)
hdis :
Pairwise (fun i j => Disjoint (A i) (A j))
hcover :
⋃ j, A j = univ
def
given by
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 reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Given a measurable classifier partition and a cell index, the cell set consists of the observations assigned to that index.
Definition (Lean source)
parameters
def
given by
p.cell ⁻¹' {j}
def cellMass reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Given a measurable classifier partition, an observation measure, and a cell index, the cell mass is the measure of that cell as a nonnegative number. A cell of infinite measure is sent to zero by this conversion, so it is the cell's mass for finite (in particular probability) measures, as used throughout.
Definition (Lean source)
parameters
def
cellMass p P j :
ℝ≥0
given by
(P (p.cellSet j)).toNNReal
def cellObservationLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Given a measurable classifier partition, an observation probability law, and a cell index, the within-cell observation law is the normalized restriction to a positive-mass cell and the original law when the cell has zero mass.
Definition (Lean source)
parameters
X :
Type u_1
ι :
Type u_2
p :
P :
j :
ι
def
given by
if h : P (p.cellSet j) = 0 then P else (P (p.cellSet j))⁻¹ • P.restrict (p.cellSet j)
def cellIndices reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Given a measurable classifier partition, a cell index, and a finite marked sample, the cell indices are exactly the original sample positions whose observations belong to that cell.
Definition (Lean source)
parameters
given by
by classical exact Finset.univ.filter (fun k => p.cell (s.points k).1 = j)
def restrictCell reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Given a measurable classifier partition, a cell index, and a finite marked sample, the restriction to that cell retains exactly the pairs in the cell, preserving their original relative order.
Definition (Lean source)
parameters
def
given by
by classical let t := p.cellIndices j s exact ⟨t.card, fun k
=> s.points (t.orderIsoOfFin rfl k)⟩
def restrictPartition reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Given a measurable classifier partition and a finite marked sample, the partition-wise restriction assigns each cell the pairs in that cell, preserving their original relative order.
Definition (Lean source)
parameters
def
given by
fun j => p.restrictCell j s
lemma measurable_restrictPartition reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
For a finite measurable partition, simultaneously restricting a finite marked sample to every cell is measurable.
Formal statement
hypotheses
conclusion
Measurable p.restrictPartition
Proof (Lean source)
@[fun_prop]
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 — For a family of candidate cells, if each cell is measurable, distinct cells are disjoint, and the cells cover the observation space, then for each cell index, the corresponding classifier fibre is exactly the supplied cell.hypothesesX :sharedType u_1ι :sharedType u_2A :ι → Set XhA :∀ j, MeasurableSet (A j)hdis :Pairwise (fun i j => Disjoint (A i) (A j))hcover :⋃ j, A j = univj :ιconclusion(ofSets A hA hdis hcover).cell ⁻¹' {j} = A jProof (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 — For a measurable classifier partition and a cell index, the corresponding cell is measurable.hypothesesconclusionMeasurableSet (p.cellSet j)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 — For a measurable classifier partition, if two cell indices are distinct, their corresponding 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 — For a measurable classifier partition, the union of all its cells is the whole observation space.hypothesesconclusion⋃ j : ι, p.cellSet j = univProof (Lean source)
lemma iUnion_cellSet (p : FiniteMeasurablePartition X ι) : ⋃ j : ι, p.cellSet j = univ := by ext x simp [cellSet] -
sum_cellMasslemma — For a measurable classifier partition and an observation probability law, the masses of all partition cells sum to one.hypothesesX :sharedType u_1ι :sharedType u_2p :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 for a measurable classifier partition, an observation probability law, and a selected cell, including when that cell has probability zero.parametersX :sharedType u_1ι :sharedType u_2p :P :j :ιinstancegiven byby 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 — For a measurable classifier partition, an observation probability law, and a selected cell, if that cell has positive mass, its normalized within-cell law assigns probability one to the cell.hypothesesX :sharedType u_1ι :sharedType u_2p :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 — For a measurable classifier partition and a selected cell, restricting a finite marked sample to that cell is measurable.hypothesesconclusionMeasurable (p.restrictCell j)Proof (Lean source)
@[fun_prop] 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 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 reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Cell counts are Poisson. For a finite measurable partition, an observation probability law, a real-valued mark law, a nonnegative intensity, and a selected cell, the cell count is Poisson with mean equal to intensity times cell mass.
Formal statement
hypotheses
X :
Type u_1
ι :
Type u_2
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 — For a measurable classifier partition, an observation probability law, a real-valued mark law, a nonnegative intensity, a selected cell, and a count, the restricted cell law is its Poisson mass times the embedded product law.hypothesesX :sharedType u_1ι :sharedType u_2p :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 8 core · 4 supporting 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.
def wordHistogram reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
For a finite label sequence and a label, the histogram count is the number of positions carrying that label.
Definition (Lean source)
parameters
def
wordHistogram w j :
ℕ
given by
by classical exact (Finset.univ.filter fun k => w k = j).card
def histogramWords reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
For a sequence length and a vector of label counts, the set of label sequences with that histogram collects every length-n sequence whose number of positions carrying each label equals the prescribed count.
Definition (Lean source)
parameters
ι :
Type u_2
n :
ℕ
c :
ι → ℕ
given by
by classical exact Finset.univ.filter fun w => ∀ j, wordHistogram w j = c j
def wordIndices reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
For a finite label sequence and a label, the label-index set contains exactly the positions carrying that label.
def wordFiberEquiv reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
For a finite label sequence and a label, the ordered correspondence matches occurrence numbers for that label with exactly the positions where it occurs.
Definition (Lean source)
parameters
def
given by
by classical exact ((wordIndices w j).orderIsoOfFin (wordIndices_card w j).symm).toEquiv.trans (Equiv.subtypeEquiv (Equiv.refl _) (by simp [wordIndices]))
def wordUnshuffleEquiv reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
For a finite label sequence, the unshuffling correspondence matches all label-specific occurrence slots with the original sample positions.
Definition (Lean source)
parameters
def
given by
by classical exact (Equiv.sigmaCongrRight fun j => wordFiberEquiv w j).trans (Equiv.sigmaFiberEquiv w)
def gatherWord reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Given an assignment of positions to cell indices and a tuple of points, the cell-wise regrouping assigns each cell the points with its label in their original order.
Definition (Lean source)
def fixedPartitionEmbed reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Given a count for every cell and a matching point tuple for every cell, the fixed partition embedding assigns each cell the finite sample with that count and tuple.
Definition (Lean source)
lemma map_restrictPartition_finiteMarkedPoissonSampleLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Partition splitting. For a finite measurable partition, an observation probability law, a real-valued mark law, and a nonnegative intensity, cell restrictions are independent marked Poisson samples with mass-scaled intensities.
Formal statement
hypotheses
X :
Type u_1
ι :
Type u_2
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
4 supporting declarations (lemmas, instances)
-
histogramWords_cardtheorem — If the label counts sum to the sequence length, then the number of label sequences with that histogram is the multinomial coefficient of the counts.hypothesesι :sharedType u_2n :ℕc :ι → ℕhc :∑ j, c j = nconclusionProof (Lean source)
theorem histogramWords_card (n : ℕ) (c : ι → ℕ) (hc : ∑ j, c j = n) : (histogramWords n c).card = multinomial univ c := by classical let e : (Σ j : ι, Fin (c j)) ≃ Fin n := Fintype.equivOfCardEq (by simpa using hc) let w₀ : Fin n → ι := wordOfEquiv c e have hw₀ (j : ι) : wordHistogram w₀ j = c j := wordOfEquiv_histogram c e j let H : Set (Fin n → ι) := {w | ∀ j, wordHistogram w j = c j} letI : Fintype (Perm (Fin n))ᵈᵐᵃ := Fintype.ofEquiv (Perm (Fin n)) DomMulAct.mk have horbit : MulAction.orbit (Perm (Fin n))ᵈᵐᵃ w₀ = H := by ext w constructor · rintro ⟨g, rfl⟩ intro j rw [← hw₀ j] unfold wordHistogram rw [← Fintype.card_subtype, ← Fintype.card_subtype] apply Fintype.card_congr exact Equiv.subtypeEquiv (DomMulAct.mk.symm g : Perm (Fin n)) (by intro k simp [DomMulAct.smul_apply]) · intro hw have hcard (j : ι) : card {k : Fin n // w₀ k = j} = card {k : Fin n // w k = j} := by rw [Fintype.card_subtype, Fintype.card_subtype] exact (hw₀ j).trans (hw j).symm let g : Perm (Fin n) := Equiv.ofFiberEquiv fun j => Fintype.equivOfCardEq (hcard j) refine ⟨DomMulAct.mk g.symm, ?_⟩ funext k change (DomMulAct.mk g.symm • w₀) k = w k rw [DomMulAct.smul_apply] change w₀ (g.symm k) = w k symm have hg := Equiv.ofFiberEquiv_map (fun j => Fintype.equivOfCardEq (hcard j)) (g.symm k) change w (g (g.symm k)) = w₀ (g.symm k) at hg simpa using hg have hcardH : card H = (histogramWords n c).card := by rw [Fintype.card_subtype] congr 1 have horbitCard : card H * ∏ j, (c j).factorial = n.factorial := by have hos := MulAction.card_orbit_mul_card_stabilizer_eq_card_group (Perm (Fin n))ᵈᵐᵃ w₀ have hstab : card (MulAction.stabilizer (Perm (Fin n))ᵈᵐᵃ w₀) = ∏ j, (c j).factorial := by rw [show card (MulAction.stabilizer (Perm (Fin n))ᵈᵐᵃ w₀) = card {g : Perm (Fin n) // w₀ ∘ g = w₀} by apply Fintype.card_congr exact Equiv.subtypeEquiv DomMulAct.mk.symm (fun g => DomMulAct.mem_stabilizer_iff), DomMulAct.stabilizer_card w₀] congr 2 with j rw [Fintype.card_subtype] change (wordHistogram w₀ j).factorial = (c j).factorial exact congrArg factorial (hw₀ j) have hdom : card (Perm (Fin n))ᵈᵐᵃ = n.factorial := by rw [← Fintype.card_congr (DomMulAct.mk : Perm (Fin n) ≃ (Perm (Fin n))ᵈᵐᵃ), Fintype.card_perm, Fintype.card_fin] have horbitCardEq : card (MulAction.orbit (Perm (Fin n))ᵈᵐᵃ w₀) = card H := Fintype.card_congr (Equiv.setCongr horbit) rw [horbitCardEq, hstab, hdom] at hos exact hos have hmulti := Nat.multinomial_spec univ c rw [hc] at hmulti rw [← hcardH] apply Nat.eq_of_mul_eq_mul_right (Nat.prod_factorial_pos univ c) simpa [mul_comm] using horbitCard.trans hmulti.symm -
wordIndices_cardlemma — For a finite label sequence and a label, the number of its positions equals its histogram count.hypothesesconclusion(wordIndices w j).card = wordHistogram w jProof (Lean source)
lemma wordIndices_card {n : ℕ} (w : Fin n → ι) (j : ι) : (wordIndices w j).card = wordHistogram w j := by rfl -
measurable_gatherWordlemma — For a finite cell-label sequence, regrouping a tuple of points by those labels is measurable.hypothesesconclusionMeasurable (gatherWord (Y := Y) w)Proof (Lean source)
@[fun_prop] lemma measurable_gatherWord {Y : Type*} [MeasurableSpace Y] {n : ℕ} (w : Fin n → ι) : Measurable (gatherWord (Y := Y) w) := by have hfun : gatherWord (Y := Y) w = piCurry (fun j : ι => fun _ : Fin (wordHistogram w j) => Y) ∘ MeasurableEquiv.piCongrLeft (fun _ : Σ j : ι, Fin (wordHistogram w j) => Y) (wordEquiv w) := by funext z j k simp only [Function.comp_apply] rw [MeasurableEquiv.piCurry_apply] change z (wordUnshuffleEquiv w ⟨j, k⟩) = (Equiv.piCongrLeft (fun _ : Σ j, Fin (wordHistogram w j) => Y) (wordEquiv w)) z ⟨j, k⟩ rw [Equiv.piCongrLeft_apply] simp [wordEquiv] exact (eq_rec_constant _ _).symm rw [hfun] exact (piCurry _).measurable.comp (MeasurableEquiv.piCongrLeft _ (wordEquiv w)).measurable -
measurable_fixedPartitionEmbedlemma — For a prescribed count in every cell, embedding one tuple per cell as finite samples is measurable.hypothesesconclusionMeasurable (fixedPartitionEmbed (Y := Y) c)Proof (Lean source)
@[fun_prop] lemma measurable_fixedPartitionEmbed {Y : Type*} [MeasurableSpace Y] (c : ι → ℕ) : Measurable (fixedPartitionEmbed (Y := Y) c) := by apply measurable_pi_lambda intro j exact (measurable_fixedSizeEmbed (c j)).comp (measurable_pi_apply j)