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 1 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. 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 family of subsets of the observation space indexed by a finite index set, each of which is measurable, which are pairwise disjoint, and whose union is the whole observation space, the partition constructed from these sets assigns every observation to the unique index of the set containing it.
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 is the set of observations assigned to that index by the partition.
Definition (Lean source)
parameters
def
given by
p.cell ⁻¹' {j}
def cellMass reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Given a measurable classifier partition, a measure on the observation space, and a cell index, the cell mass is the measure of that cell, represented as a nonnegative real 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)
def cellObservationLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Given a measurable classifier partition, a probability measure on the observation space, and a cell index, the within-cell observation law is the normalized restriction of that probability measure to the cell when the cell has positive probability, and is the original probability measure when the cell has probability zero.
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 sample of observation--real-mark pairs, the cell indices are precisely 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 sample of observation--real-mark pairs, the restriction to that cell retains exactly the pairs whose observations belong to the cell, in 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 sample of observation--real-mark pairs, the partition-wise restriction assigns to every cell index the sample obtained by retaining exactly the pairs in that cell, in 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 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
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 — The classifier constructed from a disjoint measurable cover has exactly the supplied sets as its fibres.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 :ι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.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 — 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.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 — Cell masses sum to one under a probability law.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 — Let the observation space and the cell-index space each be equipped with a $\sigma$-algebra. For a finite measurable partition of the observation space indexed by the cell-index space, a probability measure on the observation space, and a cell index, the assertion that the associated within-cell observation law is a probability measure holds, including when the selected 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 — A positive-mass within-cell law assigns probability one to its own 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 — Restriction to one measurable cell is a measurable map on finite marked sequences.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. 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
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 — 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.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 3 core · 2 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 gatherWord reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Given an assignment of each of positions to a cell index and an -tuple of points, the cell-wise regrouping assigns to each cell the tuple of points at positions assigned to that cell, ordered by their original positions.
Definition (Lean source)
parameters
def
given by
fun j k => z (wordUnshuffleEquiv w ⟨j, k⟩)
def fixedPartitionEmbed reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteMeasurablePartition
Given a nonnegative integer count for every cell index and for each cell index, a tuple of points having its specified count, the fixed partition embedding assigns to every cell index the finite sample with that count and that tuple of points.
Definition (Lean source)
lemma map_restrictPartition_finiteMarkedPoissonSampleLaw reviewed
⚑ 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
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
2 supporting declarations (lemmas, instances)
-
measurable_gatherWordlemma — Regrouping an n-tuple of points by the cell word w is a measurable map.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 = MeasurableEquiv.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 (MeasurableEquiv.piCurry _).measurable.comp (MeasurableEquiv.piCongrLeft _ (wordEquiv w)).measurable -
measurable_fixedPartitionEmbedlemma — Embedding one fixed-size point tuple per cell into one finite sample per cell is a measurable map.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)