Stat.FiniteRaoBlackwell.Poisson.PairedHistogram.HistogramReconstruction
This roll-up module provides parameter-free uniform reconstruction of finite ordered Poisson samples from count histograms, exact reconstruction identities, and total-variation transport for one or two experiments.
CountLaw 2 core · 1 supporting This module defines the product law of independent singleton-cell Poisson counts and identifies it with the histogram image of a finite Poisson sample. ★ finitePoissonSampleLaw_map_histogram
Independent Poisson law of a finite-sample histogram
This module defines the product law of independent singleton-cell Poisson counts and identifies it with the histogram image of a finite Poisson sample.
def independentPoissonCountLaw reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.PairedPoissonHistogram
Given a finite-alphabet probability law and a Poisson intensity, the independent Poisson count law is the product over alphabet symbols of Poisson laws with rates equal to intensity times singleton probability.
Definition (Lean source)
parameters
X :
P :
lambda :
ℝ≥0
def
given by
Measure.pi fun x : X ↦ poissonMeasure (lambda * (P {x}).toNNReal)
theorem finitePoissonSampleLaw_map_histogram reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.PairedPoissonHistogram
Given a finite-alphabet probability law and a Poisson intensity, the histogram of its finite Poisson sample has the product law of independent Poisson cell counts.
Formal statement
hypotheses
X :
P :
lambda :
ℝ≥0
conclusion
Measure.map (fun s : FiniteSample X ↦ finiteSampleHistogram s.points) (finitePoissonSampleLaw P lambda)
= independentPoissonCountLaw P lambda
Proof (Lean source)
theorem finitePoissonSampleLaw_map_histogram
{X : Type*} [Fintype X] [MeasurableSpace X]
[MeasurableSingletonClass X] [DecidableEq X]
(P : Measure X) [IsProbabilityMeasure P] (lambda : ℝ≥0) :
Measure.map (fun s : FiniteSample X ↦ finiteSampleHistogram s.points)
(finitePoissonSampleLaw P lambda) =
independentPoissonCountLaw P lambda := by
let p : FiniteMeasurablePartition X X :=
{ cell := id
measurable_cell := measurable_id }
let R : Measure ℝ := Measure.dirac 0
let markedCounts : FiniteSample (X × ℝ) → X → ℕ :=
fun s x => (p.restrictCell x s).count
let countFamily : (X → FiniteSample (X × ℝ)) → X → ℕ :=
fun q x => (q x).count
have hcountFamily : Measurable countFamily :=
measurable_pi_lambda _ fun x =>
measurable_finiteSample_count.comp (measurable_pi_apply x)
have hmarked :
Measure.map markedCounts (finiteMarkedPoissonSampleLaw P R lambda) =
Measure.pi (fun x : X =>
poissonMeasure (lambda * p.cellMass P x)) := by
calc
Measure.map markedCounts (finiteMarkedPoissonSampleLaw P R lambda) =
Measure.map countFamily
(Measure.map p.restrictPartition
(finiteMarkedPoissonSampleLaw P R lambda)) := by
rw [Measure.map_map hcountFamily p.measurable_restrictPartition]
rfl
_ = Measure.map countFamily
(Measure.pi (fun x : X =>
finiteMarkedPoissonSampleLaw (p.cellObservationLaw P x) R
(lambda * p.cellMass P x))) := by
rw [p.map_restrictPartition_finiteMarkedPoissonSampleLaw]
_ = Measure.pi (fun x : X => Measure.map FiniteSample.count
(finiteMarkedPoissonSampleLaw (p.cellObservationLaw P x) R
(lambda * p.cellMass P x))) := by
exact Measure.pi_map_pi
(fun _ => measurable_finiteSample_count.aemeasurable)
_ = Measure.pi (fun x : X =>
poissonMeasure (lambda * p.cellMass P x)) := by
congr with x
rw [finiteMarkedPoissonSampleLaw_map_count]
have herase := map_finitePoissonSampleLaw_finiteSampleMap
(P.prod (Measure.dirac (0 : ℝ))) Prod.fst measurable_fst lambda
have hprod : Measure.map Prod.fst (P.prod (Measure.dirac (0 : ℝ))) = P := by
rw [Measure.map_fst_prod, measure_univ, one_smul]
have herase' :
Measure.map (finiteSampleMap Prod.fst)
(finitePoissonSampleLaw (P.prod (Measure.dirac (0 : ℝ))) lambda) =
finitePoissonSampleLaw P lambda := by
simpa only [hprod] using herase
have hcounts (s : FiniteSample (X × ℝ)) :
markedCounts s =
finiteSampleHistogram (finiteSampleMap Prod.fst s).points := by
classical
rcases s with ⟨n, points⟩
funext x
unfold markedCounts finiteSampleHistogram
FiniteMeasurablePartition.restrictCell
simp only [FiniteSample.count, finiteSampleMap, FiniteSample.points]
unfold FiniteMeasurablePartition.cellIndices
let q : Fin n → Prop := fun i =>
p.cell (FiniteSample.points
(⟨n, points⟩ : FiniteSample (X × ℝ)) i).1 = x
let hq : DecidablePred q := fun _ => Classical.propDecidable _
letI : DecidablePred q := hq
change (Finset.univ.filter q).card =
card {i : Fin n // (points i).1 = x}
calc
(Finset.univ.filter q).card = card {i : Fin n // q i} :=
(Fintype.card_subtype q).symm
_ = card {i : Fin n // (points i).1 = x} :=
Fintype.card_congr (Equiv.subtypeEquivRight fun i => by
simp [q, p, FiniteSample.points])
have hhist : Measurable
(fun s : FiniteSample X => finiteSampleHistogram s.points) := by
apply measurable_to_countable'
intro c
rw [MeasurableSpace.measurableSet_iInf]
intro n
change MeasurableSet ((Sigma.mk n) ⁻¹'
{s : FiniteSample X | finiteSampleHistogram s.points = c})
exact (Set.to_countable _).measurableSet
unfold independentPoissonCountLaw
change _ = Measure.pi (fun x : X =>
poissonMeasure (lambda * p.cellMass P x))
rw [← hmarked, ← herase',
show finiteMarkedPoissonSampleLaw P (Measure.dirac (0 : ℝ)) lambda =
finitePoissonSampleLaw (P.prod (Measure.dirac (0 : ℝ))) lambda by rfl,
Measure.map_map hhist
(measurable_finiteSampleMap Prod.fst measurable_fst)]
exact congrArg
(fun f : FiniteSample (X × ℝ) → (X → ℕ) =>
Measure.map f
(finitePoissonSampleLaw (P.prod (Measure.dirac (0 : ℝ))) lambda))
(funext fun s => (hcounts s).symm)
1 supporting declaration (lemmas, instances)
-
independentPoissonCountLaw_isProbabilityMeasureinstance — Given a finite-alphabet probability law and a Poisson intensity, the independent Poisson count law is a probability law.parametersX :P :lambda :ℝ≥0instanceindependentPoissonCountLaw_isProbabilityMeasure P lambda :IsProbabilityMeasure (independentPoissonCountLaw P lambda)given byby unfold independentPoissonCountLaw infer_instance
Kernel 3 core · 3 supporting This module constructs the parameter-free Markov kernel which reconstructs a finite ordered sample uniformly from the orderings compatible with a supplied finite count vector, and records its singleton mass and support i ★ histogramReconstructionKernel_histogram_eq
The uniform histogram-fibre kernel
This module constructs the parameter-free Markov kernel which reconstructs a finite ordered sample uniformly from the orderings compatible with a supplied finite count vector, and records its singleton mass and support identities.
def histogramReconstructionPMF reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.PairedPoissonHistogram
Given a finite count vector, the histogram reconstruction distribution is uniform over all ordered samples having exactly those counts. Its definition depends only on the count vector, not on a sampling law or intensity.
Definition (Lean source)
parameters
X :
c :
X → ℕ
def
given by
by classical letI : Nonempty (HistogramFiber c) := histogramFiber_nonempty c exact (uniformOfFintype (HistogramFiber c)).map (fun x ↦ fixedSizeEmbed (histogramTotal c) x.1)
def histogramReconstructionKernel reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.PairedPoissonHistogram
On a finite measurable alphabet, the histogram reconstruction kernel sends every count vector to the uniform distribution on its ordered histogram fibre.
Definition (Lean source)
parameters
X :
def
given by
Kernel.ofFunOfCountable fun c ↦ (histogramReconstructionPMF c).toMeasure
theorem histogramReconstructionKernel_histogram_eq reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.PairedPoissonHistogram
Given a count vector, reconstruction is supported entirely on finite ordered samples whose histogram is exactly that vector.
Formal statement
hypotheses
X :
c :
X → ℕ
conclusion
= 1
Proof (Lean source)
theorem histogramReconstructionKernel_histogram_eq
{X : Type*} [Fintype X] [MeasurableSpace X]
[MeasurableSingletonClass X] [DecidableEq X]
(c : X → ℕ) :
histogramReconstructionKernel X c
{s : FiniteSample X | finiteSampleHistogram s.points = c} = 1 := by
-- Rewrite the PMF map on this event. Every fibre element lands in it by
-- its subtype certificate, so the preimage is `univ`.
classical
change (histogramReconstructionPMF c).toMeasure
{s : FiniteSample X | finiteSampleHistogram s.points = c} = 1
have hs : MeasurableSet
{s : FiniteSample X | finiteSampleHistogram s.points = c} := by
rw [MeasurableSpace.measurableSet_iInf]
intro n
change @MeasurableSet (Fin n → X) inferInstance
((Sigma.mk (β := fun k => Fin k → X) n) ⁻¹'
{s : FiniteSample X | finiteSampleHistogram s.points = c})
exact Set.Finite.measurableSet (Set.toFinite _)
rw [PMF.toMeasure_apply_eq_toOuterMeasure_apply _ hs]
unfold histogramReconstructionPMF
rw [PMF.toOuterMeasure_map_apply]
have hpre :
(fun x : HistogramFiber c => fixedSizeEmbed (histogramTotal c) x.1) ⁻¹'
{s : FiniteSample X | finiteSampleHistogram s.points = c} = univ := by
ext x
simp only [mem_preimage, mem_ofPred_eq, mem_univ, iff_true]
exact x.2
rw [hpre]
letI : MeasurableSpace (HistogramFiber c) := ⊤
rw [← PMF.toMeasure_apply_eq_toOuterMeasure_apply _ MeasurableSet.univ]
exact measure_univ
3 supporting declarations (lemmas, instances)
-
histogramReconstructionKernel_isMarkovKernelinstance — On a finite measurable alphabet, the histogram reconstruction channel is a Markov kernel.parametersX :instancegiven byisProbabilityMeasure c := by change IsProbabilityMeasure (histogramReconstructionPMF c).toMeasure infer_instance -
histogramReconstructionKernel_singletontheorem — Given a count vector and one compatible ordering, the reconstruction kernel assigns that ordered sample the reciprocal of the histogram-fibre cardinality.Proof (Lean source)
theorem histogramReconstructionKernel_singleton {X : Type*} [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] [DecidableEq X] (c : X → ℕ) (x : HistogramFiber c) : histogramReconstructionKernel X c {fixedSizeEmbed (histogramTotal c) x.1} = (card (HistogramFiber c) : ℝ≥0∞)⁻¹ := by -- Unfold to `toMeasure`; the embedding of the subtype fibre into the -- dependent finite-sample type is injective, so its mapped singleton has -- the uniform source singleton mass. classical change (histogramReconstructionPMF c).toMeasure {fixedSizeEmbed (histogramTotal c) x.1} = _ have hs : MeasurableSet ({fixedSizeEmbed (histogramTotal c) x.1} : Set (FiniteSample X)) := by rw [MeasurableSpace.measurableSet_iInf] intro n change @MeasurableSet (Fin n → X) inferInstance ((Sigma.mk (β := fun k => Fin k → X) n) ⁻¹' ({fixedSizeEmbed (histogramTotal c) x.1} : Set (FiniteSample X))) by_cases hn : n = histogramTotal c · subst n convert (measurableSet_singleton x.1) ext y simp [fixedSizeEmbed] · convert MeasurableSet.empty ext y simp only [mem_preimage, mem_singleton_iff, mem_empty_iff_false, iff_false] intro h exact hn (Sigma.mk.inj_iff.mp h).1 rw [PMF.toMeasure_apply_singleton _ _ hs] unfold histogramReconstructionPMF rw [PMF.map_apply, tsum_eq_single x] · simp [fixedSizeEmbed] · intro a hax simp only [PMF.uniformOfFintype_apply, ite_eq_right_iff] intro h exact (hax (Subtype.ext (eq_of_heq (Sigma.mk.inj_iff.mp h).2).symm)).elim -
map_histogram_histogramReconstructionKerneltheorem — Given a count vector, pushing its reconstruction through the histogram map returns the point mass at the original count vector.hypothesesX :c :X → ℕconclusionMeasure.map (fun s : FiniteSample X ↦ finiteSampleHistogram s.points) (histogramReconstructionKernel X c)= Measure.dirac cProof (Lean source)
theorem map_histogram_histogramReconstructionKernel {X : Type*} [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] [DecidableEq X] (c : X → ℕ) : Measure.map (fun s : FiniteSample X ↦ finiteSampleHistogram s.points) (histogramReconstructionKernel X c) = Measure.dirac c := by -- Both sides are probability measures on a countable space. Extensionality -- on singletons reduces the claim to the preceding support identity, or -- directly simplify the composition of the PMF map with the constant -- histogram map on `HistogramFiber c`. classical let hist := fun s : FiniteSample X => finiteSampleHistogram s.points have hhist : Measurable hist := by apply measurable_to_countable' intro d change MeasurableSet {s : FiniteSample X | finiteSampleHistogram s.points = d} rw [MeasurableSpace.measurableSet_iInf] intro n change @MeasurableSet (Fin n → X) inferInstance ((Sigma.mk (β := fun k => Fin k → X) n) ⁻¹' {s : FiniteSample X | finiteSampleHistogram s.points = d}) exact Set.Finite.measurableSet (Set.toFinite _) change Measure.map hist (histogramReconstructionPMF c).toMeasure = Measure.dirac c rw [PMF.toMeasure_map hist (histogramReconstructionPMF c) hhist] unfold histogramReconstructionPMF rw [PMF.map_comp] have hcomp : hist ∘ (fun x : HistogramFiber c => fixedSizeEmbed (histogramTotal c) x.1) = Function.const _ c := by funext x exact x.2 rw [hcomp, PMF.map_const, PMF.toMeasure_pure]
PairedTransport 2 core · 2 supporting This module forms the independent product of two histogram reconstruction channels and transfers total variation from paired count experiments to paired ordered finite Poisson samples over possibly unequal finite alphabe ★ pairedIndependentPoissonCountLaw_comp_reconstruction
Paired histogram reconstruction transport
This module forms the independent product of two histogram reconstruction channels and transfers total variation from paired count experiments to paired ordered finite Poisson samples over possibly unequal finite alphabets.
def pairedHistogramReconstructionKernel reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.PairedPoissonHistogram
On two finite measurable alphabets, the paired histogram reconstruction kernel independently reconstructs the two ordered samples from their two count vectors.
Definition (Lean source)
parameters
def
pairedHistogramReconstructionKernel X Y :
given by
(histogramReconstructionKernel X).parallelComp (histogramReconstructionKernel Y)
theorem pairedIndependentPoissonCountLaw_comp_reconstruction reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.PairedPoissonHistogram
Given two finite-alphabet probability laws and possibly different Poisson intensities, independently reconstructing their product count law recovers the product of their ordered finite Poisson sample laws exactly.
Formal statement
hypotheses
X Y :
P :
Q :
lambdaX lambdaY :
ℝ≥0
conclusion
pairedHistogramReconstructionKernel X Y ∘ₘ ((independentPoissonCountLaw P lambdaX).prod (independentPoissonCountLaw Q lambdaY))
Proof (Lean source)
theorem pairedIndependentPoissonCountLaw_comp_reconstruction
{X Y : Type*}
[Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] [DecidableEq X]
[Fintype Y] [MeasurableSpace Y] [MeasurableSingletonClass Y] [DecidableEq Y]
(P : Measure X) [IsProbabilityMeasure P]
(Q : Measure Y) [IsProbabilityMeasure Q]
(lambdaX lambdaY : ℝ≥0) :
pairedHistogramReconstructionKernel X Y ∘ₘ
((independentPoissonCountLaw P lambdaX).prod
(independentPoissonCountLaw Q lambdaY)) =
(finitePoissonSampleLaw P lambdaX).prod
(finitePoissonSampleLaw Q lambdaY) := by
unfold pairedHistogramReconstructionKernel
calc
((histogramReconstructionKernel X) ∥ₖ
(histogramReconstructionKernel Y)) ∘ₘ
((independentPoissonCountLaw P lambdaX).prod
(independentPoissonCountLaw Q lambdaY)) =
((histogramReconstructionKernel X) ∥ₖ Kernel.id) ∘ₘ
((Kernel.id ∥ₖ (histogramReconstructionKernel Y)) ∘ₘ
((independentPoissonCountLaw P lambdaX).prod
(independentPoissonCountLaw Q lambdaY))) := by
rw [Measure.comp_assoc, Kernel.parallelComp_comp_parallelComp,
Kernel.comp_id, Kernel.id_comp]
_ = ((histogramReconstructionKernel X) ∥ₖ Kernel.id) ∘ₘ
((independentPoissonCountLaw P lambdaX).prod
((histogramReconstructionKernel Y) ∘ₘ
independentPoissonCountLaw Q lambdaY)) := by
rw [← Measure.prod_comp_right]
_ = ((histogramReconstructionKernel X) ∘ₘ
independentPoissonCountLaw P lambdaX).prod
((histogramReconstructionKernel Y) ∘ₘ
independentPoissonCountLaw Q lambdaY) := by
rw [Measure.prod_comp_left]
_ = (finitePoissonSampleLaw P lambdaX).prod
(finitePoissonSampleLaw Q lambdaY) := by
rw [independentPoissonCountLaw_comp_reconstruction,
independentPoissonCountLaw_comp_reconstruction]
2 supporting declarations (lemmas, instances)
-
pairedHistogramReconstructionKernel_isMarkovKernelinstance — On two finite measurable alphabets, the independent paired histogram reconstruction channel is a Markov kernel.parametersinstancepairedHistogramReconstructionKernel_isMarkovKernel X Y :given byby unfold pairedHistogramReconstructionKernel infer_instance -
tvDist_paired_finitePoissonSampleLaw_le_countstheorem — Given two pairs of probability laws on possibly different finite alphabets and arbitrary, potentially unequal Poisson intensities, the total variation distance between the paired ordered Poisson experiments is no larger than the distance between their paired independent count experiments.hypothesesX Y :PX0 PX1 :PY0 PY1 :lambdaX0 lambdaX1 lambdaY0 lambdaY1 :ℝ≥0conclusiontvDist ((finitePoissonSampleLaw PX0 lambdaX0).prod (finitePoissonSampleLaw PY0 lambdaY0)) ((finitePoissonSampleLaw PX1 lambdaX1).prod (finitePoissonSampleLaw PY1 lambdaY1))≤ tvDist ((independentPoissonCountLaw PX0 lambdaX0).prod (independentPoissonCountLaw PY0 lambdaY0)) ((independentPoissonCountLaw PX1 lambdaX1).prod (independentPoissonCountLaw PY1 lambdaY1))Proof (Lean source)
theorem tvDist_paired_finitePoissonSampleLaw_le_counts {X Y : Type*} [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] [DecidableEq X] [Fintype Y] [MeasurableSpace Y] [MeasurableSingletonClass Y] [DecidableEq Y] (PX0 PX1 : Measure X) [IsProbabilityMeasure PX0] [IsProbabilityMeasure PX1] (PY0 PY1 : Measure Y) [IsProbabilityMeasure PY0] [IsProbabilityMeasure PY1] (lambdaX0 lambdaX1 lambdaY0 lambdaY1 : ℝ≥0) : tvDist ((finitePoissonSampleLaw PX0 lambdaX0).prod (finitePoissonSampleLaw PY0 lambdaY0)) ((finitePoissonSampleLaw PX1 lambdaX1).prod (finitePoissonSampleLaw PY1 lambdaY1)) ≤ tvDist ((independentPoissonCountLaw PX0 lambdaX0).prod (independentPoissonCountLaw PY0 lambdaY0)) ((independentPoissonCountLaw PX1 lambdaX1).prod (independentPoissonCountLaw PY1 lambdaY1)) := by rw [← pairedIndependentPoissonCountLaw_comp_reconstruction, ← pairedIndependentPoissonCountLaw_comp_reconstruction] exact tvDist_bind_le _ _ (pairedHistogramReconstructionKernel X Y)
Reconstruction 2 core · 1 supporting This module states the fixed-total and Poissonized identities obtained by mixing the parameter-free uniform histogram-fibre reconstruction kernel. ★ independentPoissonCountLaw_comp_reconstruction
Reconstruction of finite ordered samples from histograms
This module states the fixed-total and Poissonized identities obtained by mixing the parameter-free uniform histogram-fibre reconstruction kernel.
def multinomialHistogramLaw reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.PairedPoissonHistogram
Given a finite-alphabet probability law and a fixed sample size, the multinomial histogram law is the count-vector image of the ordered iid product law.
Definition (Lean source)
parameters
X :
P :
n :
ℕ
def
given by
Measure.map finiteSampleHistogram (Measure.pi fun _ : Fin n ↦ P)
theorem independentPoissonCountLaw_comp_reconstruction reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.PairedPoissonHistogram
Given a finite-alphabet probability law and a Poisson intensity, passing its independent cell counts through the parameter-free reconstruction kernel recovers the ordered finite Poisson sample law exactly.
Formal statement
hypotheses
X :
P :
lambda :
ℝ≥0
conclusion
histogramReconstructionKernel X ∘ₘ independentPoissonCountLaw P lambda
= finitePoissonSampleLaw P lambda
Proof (Lean source)
theorem independentPoissonCountLaw_comp_reconstruction
{X : Type*} [Fintype X] [MeasurableSpace X]
[MeasurableSingletonClass X] [DecidableEq X]
(P : Measure X) [IsProbabilityMeasure P] (lambda : ℝ≥0) :
histogramReconstructionKernel X ∘ₘ independentPoissonCountLaw P lambda =
finitePoissonSampleLaw P lambda := by
let K := histogramReconstructionKernel X
let ν := independentPoissonCountLaw P lambda
let μ := finitePoissonSampleLaw P lambda
have hpiece (N : ℕ) :
K ∘ₘ ν.restrict (histogramTotal ⁻¹' ({N} : Set ℕ)) =
μ.restrict (FiniteSample.count ⁻¹' ({N} : Set ℕ)) := by
rw [show ν.restrict (histogramTotal ⁻¹' ({N} : Set ℕ)) =
(poissonMeasure lambda) {N} • multinomialHistogramLaw P N by
exact independentPoissonCountLaw_restrict_histogramTotal_eq P lambda N,
Measure.bind_smul, multinomialHistogramLaw_comp_reconstruction,
show μ.restrict (FiniteSample.count ⁻¹' ({N} : Set ℕ)) =
(poissonMeasure lambda) {N} •
Measure.map (fixedSizeEmbed N) (Measure.pi fun _ : Fin N ↦ P) by
exact finitePoissonSampleLaw_restrict_count_eq P lambda N]
calc
K ∘ₘ ν = K ∘ₘ Measure.sum (fun N ↦
ν.restrict (histogramTotal ⁻¹' ({N} : Set ℕ))) := by
rw [← measure_eq_sum_restrict_histogramTotal ν]
_ = Measure.sum (fun N ↦ K ∘ₘ
ν.restrict (histogramTotal ⁻¹' ({N} : Set ℕ))) := by
exact Measure.bind_sum _ _ K.aemeasurable
_ = Measure.sum (fun N ↦
μ.restrict (FiniteSample.count ⁻¹' ({N} : Set ℕ))) := by
congr 1
funext N
exact hpiece N
_ = μ := (measure_eq_sum_restrict_finiteSample_count μ).symm
1 supporting declaration (lemmas, instances)
-
multinomialHistogramLaw_comp_reconstructiontheorem — Given a finite-alphabet probability law and a fixed sample size, uniformly reconstructing its multinomial histogram recovers the embedded ordered iid sample law exactly.Proof (Lean source)
theorem multinomialHistogramLaw_comp_reconstruction {X : Type*} [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] [DecidableEq X] (P : Measure X) [IsProbabilityMeasure P] (n : ℕ) : histogramReconstructionKernel X ∘ₘ multinomialHistogramLaw P n = Measure.map (fixedSizeEmbed n) (Measure.pi fun _ : Fin n ↦ P) := by classical let μ := Measure.pi fun _ : Fin n ↦ P apply Measure.ext_of_singleton rintro ⟨m, z⟩ by_cases hmn : m = n · subst m have hkernel (x : Fin n → X) : histogramReconstructionKernel X (finiteSampleHistogram x) {fixedSizeEmbed n z} = if finiteSampleHistogram x = finiteSampleHistogram z then (card (HistogramFiber (finiteSampleHistogram z)) : ℝ≥0∞)⁻¹ else 0 := by split_ifs with hx · rw [hx] have htot : histogramTotal (finiteSampleHistogram z) = n := histogramTotal_finiteSampleHistogram z let z' : Fin (histogramTotal (finiteSampleHistogram z)) → X := fun i ↦ z (cast htot i) have hz' : finiteSampleHistogram z' = finiteSampleHistogram z := by funext a unfold finiteSampleHistogram apply Fintype.card_congr exact Equiv.subtypeEquiv (finCongr htot) (fun i ↦ by rfl) let w : HistogramFiber (finiteSampleHistogram z) := ⟨z', hz'⟩ have hw := histogramReconstructionKernel_singleton (X := X) (finiteSampleHistogram z) w have hembed : fixedSizeEmbed (histogramTotal (finiteSampleHistogram z)) w.1 = fixedSizeEmbed n z := by apply Sigma.ext htot apply (Fin.heq_fun_iff htot).2 intro i simp only [w, z', fixedSizeEmbed] congr rw [hembed] at hw exact hw · let E : Set (FiniteSample X) := {s | finiteSampleHistogram s.points = finiteSampleHistogram x} have hE : MeasurableSet E := measurableSet_finiteSampleHistogram_eq (finiteSampleHistogram x) have hEc : histogramReconstructionKernel X (finiteSampleHistogram x) Eᶜ = 0 := by rw [measure_compl hE (measure_ne_top _ _), histogramReconstructionKernel_histogram_eq] simp apply measure_mono_null (t := Eᶜ) _ hEc intro s hs simp only [Set.mem_singleton_iff] at hs subst s simp only [Set.mem_compl_iff, FiniteSample.points, fixedSizeEmbed] change finiteSampleHistogram z ≠ finiteSampleHistogram x exact fun h ↦ hx h.symm have hmass (x : Fin n → X) (hx : finiteSampleHistogram x = finiteSampleHistogram z) : μ {x} = μ {z} := finiteProductMass_eq_of_histogram_eq P hx rw [Measure.bind_apply (measurableSet_finiteSample_singleton _) (histogramReconstructionKernel X).aemeasurable] unfold multinomialHistogramLaw rw [lintegral_map ((histogramReconstructionKernel X).measurable_coe (measurableSet_finiteSample_singleton _)) (measurable_of_countable _), lintegral_fintype] change (∑ x, histogramReconstructionKernel X (finiteSampleHistogram x) {fixedSizeEmbed n z} * μ {x}) = _ simp_rw [hkernel] rw [Measure.map_apply (measurable_fixedSizeEmbed n) (measurableSet_finiteSample_singleton _)] have hpre : fixedSizeEmbed n ⁻¹' ({(⟨n, z⟩ : FiniteSample X)} : Set (FiniteSample X)) = {z} := by ext x simp [fixedSizeEmbed] rw [hpre] let p : (Fin n → X) → Prop := fun x ↦ finiteSampleHistogram x = finiteSampleHistogram z have hsum : (∑ x, (if p x then (card (HistogramFiber (finiteSampleHistogram z)) : ℝ≥0∞)⁻¹ else 0) * μ {x}) = ∑ x ∈ (Finset.univ.filter p), (card (HistogramFiber (finiteSampleHistogram z)) : ℝ≥0∞)⁻¹ * μ {x} := by rw [Finset.sum_filter] apply Finset.sum_congr rfl intro x _ by_cases hx : p x · have hx' : finiteSampleHistogram x = finiteSampleHistogram z := hx simp [hx, hx'] · have hx' : ¬finiteSampleHistogram x = finiteSampleHistogram z := hx simp [hx, hx'] change (∑ x, (if p x then (card (HistogramFiber (finiteSampleHistogram z)) : ℝ≥0∞)⁻¹ else 0) * μ {x}) = μ {z} rw [hsum] have hcard : (Finset.univ.filter p).card = card (HistogramFiber (finiteSampleHistogram z)) := by rw [← Fintype.card_subtype p] apply Fintype.card_congr let e : (Fin n → X) ≃ (Fin (histogramTotal (finiteSampleHistogram z)) → X) := Equiv.arrowCongr (finCongr (histogramTotal_finiteSampleHistogram z).symm) (Equiv.refl X) exact Equiv.subtypeEquiv e (fun x ↦ by change p x ↔ finiteSampleHistogram (e x) = finiteSampleHistogram z rw [show finiteSampleHistogram (e x) = finiteSampleHistogram x by exact finiteSampleHistogram_arrowCongr (histogramTotal_finiteSampleHistogram z) x]) have hconst : (∑ x ∈ (Finset.univ.filter p), (card (HistogramFiber (finiteSampleHistogram z)) : ℝ≥0∞)⁻¹ * μ {x}) = ∑ _x ∈ (Finset.univ.filter p), (card (HistogramFiber (finiteSampleHistogram z)) : ℝ≥0∞)⁻¹ * μ {z} := by apply Finset.sum_congr rfl intro x hx rw [hmass x (Finset.mem_filter.mp hx).2] rw [hconst, Finset.sum_const, hcard] letI : Nonempty (HistogramFiber (finiteSampleHistogram z)) := histogramFiber_nonempty _ rw [nsmul_eq_mul, ← mul_assoc, ENNReal.mul_inv_cancel] · simp · simpa using Fintype.card_ne_zero · exact ENNReal.natCast_ne_top _ · rw [Measure.bind_apply (measurableSet_finiteSample_singleton _) (histogramReconstructionKernel X).aemeasurable] unfold multinomialHistogramLaw rw [lintegral_map ((histogramReconstructionKernel X).measurable_coe (measurableSet_finiteSample_singleton _)) (measurable_of_countable _)] have hzero : ∀ x : Fin n → X, histogramReconstructionKernel X (finiteSampleHistogram x) {⟨m, z⟩} = 0 := by intro x let E : Set (FiniteSample X) := {s | finiteSampleHistogram s.points = finiteSampleHistogram x} have hE : MeasurableSet E := measurableSet_finiteSampleHistogram_eq (finiteSampleHistogram x) have hEc : histogramReconstructionKernel X (finiteSampleHistogram x) Eᶜ = 0 := by rw [measure_compl hE (measure_ne_top _ _), histogramReconstructionKernel_histogram_eq] simp apply measure_mono_null (t := Eᶜ) _ hEc intro s hs simp only [Set.mem_singleton_iff] at hs subst s simp only [Set.mem_compl_iff, FiniteSample.points] intro hz apply hmn calc m = histogramTotal (finiteSampleHistogram z) := (histogramTotal_finiteSampleHistogram z).symm _ = histogramTotal (finiteSampleHistogram x) := congrArg histogramTotal hz _ = n := histogramTotal_finiteSampleHistogram x simp_rw [hzero] simp rw [Measure.map_apply (measurable_fixedSizeEmbed n) (measurableSet_finiteSample_singleton _)] have hpre : fixedSizeEmbed n ⁻¹' ({⟨m, z⟩} : Set (FiniteSample X)) = ∅ := by ext x simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_empty_iff_false, iff_false] intro hx exact hmn (Sigma.mk.inj_iff.mp hx).1.symm rw [hpre, measure_empty]