Mathlib.Probability.FiniteMarkedPoissonPartition
Finite marked Poisson experiment infrastructure: finite samples, exact partition splitting, canonical mark-ordered superposition, retained independent prefixes, depoissonization bridges, and the finite-measure KL identity.
Partition 1 to review
13 core · 11 supporting · 3 submodules Finite measurable partitions of a marked observation space: restriction maps, exact independent cell experiments, and marginal cell-count laws. Superposition 1 to review
12 core · 18 supporting · 2 submodules Finite superposition of cell configurations, canonical ordering by independent real marks, and the retained-prefix product-law bridge.
Basic 12 core · 12 supporting This file turns an independent Poisson count and infinite i.i.d. ★ finiteMarkedPoissonSampleLaw_restrict_count_eq★ map_totalizedPrefix_restrict_nonoverflow
Finite Poisson samples
This file turns an independent Poisson count and infinite i.i.d. stream into a genuine finite sequence. It records the count law and the exact, unnormalised fixed-count fibre law. The latter is the convenient measure-theoretic form of the statement that, conditional on the count, the observations are i.i.d.
abbrev FiniteSample reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
For an observation space, a finite sample is a nonnegative integer sample size together with one observation for each position below that size.
Definition (Lean source)
def count reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteSample
The number of observations in a finite sequence.
Definition (Lean source)
def points reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition.FiniteSample
The coordinates of a finite sequence at its dependent finite index type.
Definition (Lean source)
def fixedSizeEmbed reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Given a nonnegative integer sample size and a tuple of observations indexed by its positions, the fixed-size embedding is the finite sample having that size and those observations.
Definition (Lean source)
parameters
def
given by
⟨n, x⟩
def streamToFiniteSample reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Given a pair consisting of a nonnegative integer and an infinite observation stream, the associated finite sample has that integer as its size and retains exactly the corresponding initial segment of the stream.
Definition (Lean source)
parameters
X :
Type u_1
z :
ℕ × (ℕ → X)
def
given by
⟨z.1, fun i => z.2 i⟩
def finitePoissonSampleLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Given a probability measure on the observation space and a nonnegative Poisson mean, the finite Poisson sample law is the distribution obtained by drawing a Poisson count with that mean and an independent infinite sequence of independent observations from that probability measure, then retaining the initial segment selected by the count.
Definition (Lean source)
def finiteMarkedPoissonSampleLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Given a probability measure for observations, a probability measure for real-valued marks, and a nonnegative Poisson mean, the finite marked Poisson sample law is the finite Poisson sample law whose independent observation--mark pairs have the product of those two measures as their common distribution.
Definition (Lean source)
lemma finiteMarkedPoissonSampleLaw_restrict_count_eq reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Fix a nonnegative Poisson rate lam. For an observation law P and an independent mark law R, restricting the finite marked Poisson sample law to the event that the observed count equals n yields exactly poissonMeasure lam {n} times the pushforward, under the fixed-size embedding, of n independent draws from the product measure P.prod R.
Formal statement
hypotheses
X :
Type u_1
P :
R :
lam :
ℝ≥0
n :
ℕ
conclusion
= (poissonMeasure lam) ({n} : Set ℕ) • Measure.map (fixedSizeEmbed n) (Measure.pi (fun _ : Fin n => P.prod R))
Proof (Lean source)
lemma finiteMarkedPoissonSampleLaw_restrict_count_eq
(P : Measure X) [IsProbabilityMeasure P]
(R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) (n : ℕ) :
(finiteMarkedPoissonSampleLaw P R lam).restrict
(FiniteSample.count ⁻¹' ({n} : Set ℕ)) =
(poissonMeasure lam) ({n} : Set ℕ) •
Measure.map (fixedSizeEmbed n)
(Measure.pi (fun _ : Fin n => P.prod R)) := by
exact finitePoissonSampleLaw_restrict_count_eq (P.prod R) lam n
def prefixOfLE reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Given a fixed array, a requested prefix length, and a proof that the request fits in the array, the finite sample consisting of exactly that prefix retains the first m coordinates.
Definition (Lean source)
def cappedPrefix reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
For a fixed array and a requested length, the capped prefix is the genuine prefix in the right summand when the request fits and the distinguished left summand on overflow, so overflow is never confused with an empty observation.
Definition (Lean source)
parameters
def
given by
def totalizedPrefix reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
For an overflow finite sample, a fixed array, and a requested length, the totalized capped prefix agrees with the genuine prefix off overflow and uses the specified value on overflow.
Definition (Lean source)
theorem map_totalizedPrefix_restrict_nonoverflow reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
For an observation probability law, a Poisson mean, for a fixed sample size, and an arbitrary overflow totalization, the totalized prefix of that many iid observations and an independent Poisson count, restricted to nonoverflow, has exactly the finite Poisson sample law restricted to counts at most n.
Formal statement
hypotheses
X :
Type u_1
P :
lambda :
ℝ≥0
n :
ℕ
overflow :
conclusion
Measure.map (fun z : (Fin n → X) × ℕ ↦ totalizedPrefix overflow z.1 z.2) (((Measure.pi (fun _ : Fin n ↦ P)).prod (poissonMeasure lambda)).restrict (snd ⁻¹' Iic n))
Proof (Lean source)
theorem map_totalizedPrefix_restrict_nonoverflow
(P : Measure X) [IsProbabilityMeasure P] (lambda : ℝ≥0)
(n : ℕ) (overflow : FiniteSample X) :
Measure.map (fun z : (Fin n → X) × ℕ ↦
totalizedPrefix overflow z.1 z.2)
(((Measure.pi (fun _ : Fin n ↦ P)).prod (poissonMeasure lambda)).restrict
(Prod.snd ⁻¹' Iic n)) =
(finitePoissonSampleLaw P lambda).restrict
(FiniteSample.count ⁻¹' Iic n) := by
-- Decompose both restrictions as the countable sum over `m : Iic n`.
-- On each fibre, product restriction and `finitePoissonSampleLaw_restrict_count_eq`
-- both reduce to the Poisson atom at `m` times the map of the same `m`-prefix law.
classical
let Qn : Measure (Fin n → X) := Measure.pi (fun _ : Fin n ↦ P)
let μ : Measure ((Fin n → X) × ℕ) := Qn.prod (poissonMeasure lambda)
let ν : Measure (FiniteSample X) := finitePoissonSampleLaw P lambda
let f : ((Fin n → X) × ℕ) → FiniteSample X := fun z ↦
totalizedPrefix overflow z.1 z.2
have hf : Measurable f := measurable_totalizedPrefix overflow
have hfiber (m : Fin (n + 1)) :
Measure.map f (μ.restrict (Prod.snd ⁻¹' ({m.val} : Set ℕ))) =
ν.restrict (FiniteSample.count ⁻¹' ({m.val} : Set ℕ)) := by
have hm : m.val ≤ n := Nat.le_of_lt_succ m.isLt
have hs : Prod.snd ⁻¹' ({m.val} : Set ℕ) =
(Set.univ : Set (Fin n → X)) ×ˢ ({m.val} : Set ℕ) := by
ext z
simp
rw [finitePoissonSampleLaw_restrict_count_eq]
rw [hs, ← Measure.prod_restrict, Measure.restrict_univ,
Measure.restrict_singleton, Measure.prod_smul_right, Measure.map_smul,
Measure.prod_dirac, Measure.map_map hf (by fun_prop)]
have hfun : f ∘ (fun x : Fin n → X ↦ (x, m.val)) =
fixedSizeEmbed m.val ∘ (fun x : Fin n → X ↦ fun i : Fin m.val ↦
x ⟨i, lt_of_lt_of_le i.isLt hm⟩) := by
funext x
simp [f, totalizedPrefix, cappedPrefix, hm, prefixOfLE, fixedSizeEmbed]
rw [hfun, ← Measure.map_map (measurable_fixedSizeEmbed m.val) (by fun_prop),
map_prefixCoordinates_pi P hm]
have hsource : (Prod.snd : ((Fin n → X) × ℕ) → ℕ) ⁻¹' Iic n =
⋃ m : Fin (n + 1),
(Prod.snd : ((Fin n → X) × ℕ) → ℕ) ⁻¹' ({m.val} : Set ℕ) := by
ext z
simp only [Set.mem_preimage, Set.mem_Iic, Set.mem_iUnion, Set.mem_singleton_iff]
constructor
· intro hz
exact ⟨⟨z.2, Nat.lt_succ_of_le hz⟩, rfl⟩
· rintro ⟨m, hm⟩
rw [hm]
exact Nat.le_of_lt_succ m.isLt
have htarget : (FiniteSample.count : FiniteSample X → ℕ) ⁻¹' Iic n =
⋃ m : Fin (n + 1),
(FiniteSample.count : FiniteSample X → ℕ) ⁻¹' ({m.val} : Set ℕ) := by
ext z
simp only [Set.mem_preimage, Set.mem_Iic, Set.mem_iUnion, Set.mem_singleton_iff]
constructor
· intro hz
exact ⟨⟨z.count, Nat.lt_succ_of_le hz⟩, rfl⟩
· rintro ⟨m, hm⟩
rw [hm]
exact Nat.le_of_lt_succ m.isLt
have hsource_disjoint : Pairwise (onFun Disjoint
(fun m : Fin (n + 1) ↦
(Prod.snd : ((Fin n → X) × ℕ) → ℕ) ⁻¹' ({m.val} : Set ℕ))) := by
intro a b hab
change Disjoint
((Prod.snd : ((Fin n → X) × ℕ) → ℕ) ⁻¹' ({a.val} : Set ℕ))
((Prod.snd : ((Fin n → X) × ℕ) → ℕ) ⁻¹' ({b.val} : Set ℕ))
rw [Set.disjoint_left]
intro z hza hzb
simp only [Set.mem_preimage, Set.mem_singleton_iff] at hza hzb
apply hab
apply Fin.ext
exact hza.symm.trans hzb
have htarget_disjoint : Pairwise (onFun Disjoint
(fun m : Fin (n + 1) ↦
(FiniteSample.count : FiniteSample X → ℕ) ⁻¹' ({m.val} : Set ℕ))) := by
intro a b hab
change Disjoint
((FiniteSample.count : FiniteSample X → ℕ) ⁻¹' ({a.val} : Set ℕ))
((FiniteSample.count : FiniteSample X → ℕ) ⁻¹' ({b.val} : Set ℕ))
rw [Set.disjoint_left]
intro z hza hzb
simp only [Set.mem_preimage, Set.mem_singleton_iff] at hza hzb
apply hab
apply Fin.ext
exact hza.symm.trans hzb
change Measure.map f (μ.restrict (Prod.snd ⁻¹' Iic n)) =
ν.restrict (FiniteSample.count ⁻¹' Iic n)
rw [hsource, Measure.restrict_iUnion hsource_disjoint
(fun m ↦ measurable_snd (measurableSet_singleton m.val)),
Measure.map_sum hf.aemeasurable, htarget,
Measure.restrict_iUnion htarget_disjoint
(fun m ↦ measurable_finiteSample_count (measurableSet_singleton m.val))]
congr 1
funext m
exact hfiber m
12 supporting declarations (lemmas, instances)
-
poissonMeasure_singleton_eq_poissonPMFlemma — The Poisson law with mean r gives the single count n exactly the Poisson probability mass at n.Proof (Lean source)
lemma poissonMeasure_singleton_eq_poissonPMF (r : ℝ≥0) (n : ℕ) : poissonMeasure r {n} = poissonPMF r n := by rw [poissonMeasure_singleton, ← poissonPMFReal_ofReal_eq_poissonPMF] rfl -
measurable_fixedSizeEmbedlemma — Embedding a fixed-size tuple into the finite-sequence space is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_fixedSizeEmbed (n : ℕ) : Measurable (fixedSizeEmbed (X := X) n) := by change Measurable (Sigma.mk n) apply Measurable.of_le_map exact iInf_le _ n -
measurable_finiteSample_countlemma — Reading the count of a finite sequence is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_finiteSample_count : Measurable (FiniteSample.count : FiniteSample X → ℕ) := by apply measurable_to_countable' intro n change MeasurableSet ({s : FiniteSample X | s.1 = n}) rw [MeasurableSpace.measurableSet_iInf] intro m change MeasurableSet ((Sigma.mk m) ⁻¹' {s : FiniteSample X | s.1 = n}) by_cases hmn : m = n · subst m simp · convert MeasurableSet.empty using 1 ext x simp [hmn] -
measurable_streamToFiniteSamplelemma — Truncating a count-and-stream outcome to its selected prefix is measurable.hypothesesX :sharedType u_1conclusionMeasurable (streamToFiniteSample : (ℕ × (ℕ → X)) → FiniteSample X)Proof (Lean source)
@[fun_prop] lemma measurable_streamToFiniteSample : Measurable (streamToFiniteSample : (ℕ × (ℕ → X)) → FiniteSample X) := by intro s hs rw [MeasurableSpace.measurableSet_iInf] at hs rw [show streamToFiniteSample ⁻¹' s = ⋃ n : ℕ, {z : ℕ × (ℕ → X) | z.1 = n} ∩ (fun z : ℕ × (ℕ → X) => fun i : Fin n => z.2 i) ⁻¹' (fixedSizeEmbed n ⁻¹' s) by ext z simp only [mem_preimage, mem_iUnion, mem_inter_iff, mem_setOf_eq] constructor · intro hz exact ⟨z.1, rfl, hz⟩ · rintro ⟨n, hn, hz⟩ subst n exact hz] apply MeasurableSet.iUnion intro n apply MeasurableSet.inter · exact measurable_fst (measurableSet_singleton n) · have hsn : MeasurableSet (fixedSizeEmbed n ⁻¹' s) := hs n exact hsn.preimage (by fun_prop) -
finitePoissonSampleLaw_isProbabilityMeasureinstance — Let the observation space be equipped with a $\sigma$-algebra. For a probability measure on that space and a nonnegative Poisson mean, the assertion that the finite Poisson sample law is a probability measure holds.parametersinstancefinitePoissonSampleLaw_isProbabilityMeasure P lam :given byby unfold finitePoissonSampleLaw exact Measure.isProbabilityMeasure_map measurable_streamToFiniteSample.aemeasurable -
finitePoissonSampleLaw_map_countlemma — The count of a finite Poisson sample has scalar Poisson law with the requested mean.hypothesesconclusionMeasure.map FiniteSample.count (finitePoissonSampleLaw P lam) = poissonMeasure lamProof (Lean source)
lemma finitePoissonSampleLaw_map_count (P : Measure X) [IsProbabilityMeasure P] (lam : ℝ≥0) : Measure.map FiniteSample.count (finitePoissonSampleLaw P lam) = poissonMeasure lam := by unfold finitePoissonSampleLaw rw [Measure.map_map measurable_finiteSample_count measurable_streamToFiniteSample] change Measure.map fst (poissonIIDStreamLaw P lam) = poissonMeasure lam exact poissonIIDStreamLaw_map_count P lam -
finitePoissonSampleLaw_restrict_count_eqlemma — On the fibre where the count equals n, the finite Poisson law is the Poisson mass at n times the embedded n-fold product law.hypothesesconclusion= (poissonMeasure lam) ({n} : Set ℕ) • Measure.map (fixedSizeEmbed n) (Measure.pi (fun _ : Fin n => P))Proof (Lean source)
lemma finitePoissonSampleLaw_restrict_count_eq (P : Measure X) [IsProbabilityMeasure P] (lam : ℝ≥0) (n : ℕ) : (finitePoissonSampleLaw P lam).restrict (FiniteSample.count ⁻¹' ({n} : Set ℕ)) = (poissonMeasure lam) ({n} : Set ℕ) • Measure.map (fixedSizeEmbed n) (Measure.pi (fun _ : Fin n => P)) := by unfold finitePoissonSampleLaw poissonIIDStreamLaw rw [Measure.restrict_map measurable_streamToFiniteSample (measurable_finiteSample_count (X := X) (measurableSet_singleton n))] have hpre : streamToFiniteSample ⁻¹' (FiniteSample.count ⁻¹' ({n} : Set ℕ)) = ({n} : Set ℕ) ×ˢ (Set.univ : Set (ℕ → X)) := by ext z simp [streamToFiniteSample, FiniteSample.count] rw [hpre, ← Measure.restrict_prod_eq_prod_univ, Measure.restrict_singleton, Measure.prod_smul_left, Measure.map_smul, Measure.dirac_prod, Measure.map_map measurable_streamToFiniteSample (by fun_prop)] change (poissonMeasure lam) {n} • Measure.map (fixedSizeEmbed n ∘ fun z : ℕ → X => fun i : Fin n => z i) (iidStreamLaw P) = _ rw [← Measure.map_map (measurable_fixedSizeEmbed n) (by fun_prop), iidStreamLaw_map_finPrefix] -
finiteMarkedPoissonSampleLaw_isProbabilityMeasureinstance — Let the observation space be equipped with a $\sigma$-algebra. For a probability measure on the observation space, a probability measure on real-valued marks, and a nonnegative Poisson mean, the assertion that the finite marked Poisson sample law is a probability measure holds.parametersX :sharedType u_1P :R :lam :ℝ≥0instancefiniteMarkedPoissonSampleLaw_isProbabilityMeasure P R lam :given byby unfold finiteMarkedPoissonSampleLaw infer_instance -
finiteMarkedPoissonSampleLaw_map_countlemma — The count of a finite marked Poisson sample has scalar Poisson law with mean lam.hypothesesX :sharedType u_1P :R :lam :ℝ≥0conclusionMeasure.map FiniteSample.count (finiteMarkedPoissonSampleLaw P R lam) = poissonMeasure lamProof (Lean source)
lemma finiteMarkedPoissonSampleLaw_map_count (P : Measure X) [IsProbabilityMeasure P] (R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) : Measure.map FiniteSample.count (finiteMarkedPoissonSampleLaw P R lam) = poissonMeasure lam := by exact finitePoissonSampleLaw_map_count (P.prod R) lam -
measurable_prefixOfLEtheorem — For a fixed admissible length, taking that prefix is a measurable map of the fixed array.hypothesesX :sharedType u_1n m :ℕh :m ≤ nconclusionProof (Lean source)
@[fun_prop] theorem measurable_prefixOfLE {n m : ℕ} (h : m ≤ n) : Measurable (fun x : Fin n → X ↦ prefixOfLE x m h) := by -- Compose `measurable_fixedSizeEmbed` with the coordinate restriction map. apply (measurable_fixedSizeEmbed m).comp fun_prop -
measurable_cappedPrefixtheorem — For fixed array length, the option-valued capped prefix is jointly measurable in the array and requested count, with the left summand recording every overflow outcome.hypothesesX :sharedType u_1n :ℕconclusionProof (Lean source)
@[fun_prop] theorem measurable_cappedPrefix (n : ℕ) : Measurable (fun z : (Fin n → X) × ℕ ↦ cappedPrefix z.1 z.2) := by -- Partition the countable count coordinate into the measurable fibres `{m}`. apply measurable_from_prod_countable_left intro m unfold cappedPrefix change Measurable (fun x : Fin n → X ↦ if h : m ≤ n then inr (prefixOfLE x m h) else inl ()) split · exact measurable_inr.comp (measurable_prefixOfLE (X := X) ‹m ≤ n›) · fun_prop -
measurable_totalizedPrefixtheorem — For a specified overflow sample, the map from a fixed array and count to its totalized capped prefix is measurable.hypothesesconclusionProof (Lean source)
@[fun_prop] theorem measurable_totalizedPrefix {n : ℕ} (overflow : FiniteSample X) : Measurable (fun z : (Fin n → X) × ℕ ↦ totalizedPrefix overflow z.1 z.2) := by -- Compose `measurable_cappedPrefix` with measurable sum elimination. exact (measurable_const.sumElim measurable_id).comp (measurable_cappedPrefix n)
KL 4 core · 4 supporting This file packages a finite measure as a Poisson count with mean equal to its mass times a scalar intensity and conditionally i.i.d. ★ klDiv_finiteMeasureMarkedPoissonLaw
Relative entropy of finite Poisson experiments
This file packages a finite measure as a Poisson count with mean equal to its mass times a scalar intensity and conditionally i.i.d. points from its normalisation. It states the extended-real KL identity for two equal-mass finite intensity measures and the monotone upper-bound form used in testing arguments. A shared independent real mark law is carried throughout.
def finiteMeasureMass reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Given a finite measure on the observation space, the finite-measure mass is its total mass on the whole observation space, represented as a nonnegative real number.
Definition (Lean source)
parameters
X :
Type u_1
ν :
def
finiteMeasureMass ν :
ℝ≥0
def normalizedFiniteMeasure reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Given a finite measure on the observation space and a fallback probability measure on that space, the normalized finite measure is the fallback probability measure when the finite measure is zero, and otherwise is that finite measure divided by its total mass.
Definition (Lean source)
def finiteMeasureMarkedPoissonLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Given a finite intensity measure on the observation space, a fallback probability measure on that space, a probability measure for real-valued marks, and a nonnegative scalar intensity, the finite-measure marked Poisson law is the finite marked Poisson sample law with observation distribution equal to the normalized intensity measure and Poisson mean equal to the scalar intensity times the total intensity mass.
Definition (Lean source)
parameters
X :
Type u_1
ν :
P₀ :
R :
lam :
ℝ≥0
def
given by
lemma klDiv_finiteMeasureMarkedPoissonLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Fix a nonnegative Poisson rate lam and suppose the finite intensity measures ν₀ and ν₁ have equal total mass. Then, for a common baseline probability measure P₀ and mark law R, the KL divergence between the finite-measure marked Poisson experiments generated by ν₀ and by ν₁ equals lam times the KL divergence between ν₀ and ν₁.
Formal statement
Proof (Lean source)
lemma klDiv_finiteMeasureMarkedPoissonLaw
[StandardBorelSpace X]
(ν₀ ν₁ : Measure X) [IsFiniteMeasure ν₀] [IsFiniteMeasure ν₁]
(P₀ : Measure X) [IsProbabilityMeasure P₀]
(R : Measure ℝ) [IsProbabilityMeasure R]
(lam : ℝ≥0) (hmass : ν₀ univ = ν₁ univ) :
klDiv
(finiteMeasureMarkedPoissonLaw ν₀ P₀ R lam)
(finiteMeasureMarkedPoissonLaw ν₁ P₀ R lam) =
(lam : ℝ≥0∞) * klDiv ν₀ ν₁ := by
by_cases hν₀ : ν₀ = 0
· subst ν₀
have hν₁ : ν₁ = 0 := by
apply Measure.measure_univ_eq_zero.mp
simpa using hmass.symm
subst ν₁
simp [finiteMeasureMarkedPoissonLaw, finiteMeasureMass,
normalizedFiniteMeasure]
have hν₁ : ν₁ ≠ 0 := by
intro h
apply hν₀
apply Measure.measure_univ_eq_zero.mp
simpa [h] using hmass
have hm : finiteMeasureMass ν₀ = finiteMeasureMass ν₁ := by
simp only [finiteMeasureMass]
rw [hmass]
unfold finiteMeasureMarkedPoissonLaw
rw [← hm, klDiv_finiteMarkedPoissonSampleLaw]
have hrecover₀ := finiteMeasureMass_smul_normalizedFiniteMeasure ν₀ P₀ hν₀
have hrecover₁ := finiteMeasureMass_smul_normalizedFiniteMeasure ν₁ P₀ hν₁
have hrecover₁' : finiteMeasureMass ν₀ • normalizedFiniteMeasure ν₁ P₀ = ν₁ := by
rw [hm]
exact hrecover₁
have hKL : klDiv ν₀ ν₁ =
(finiteMeasureMass ν₀ : ℝ≥0∞) * klDiv
(normalizedFiniteMeasure ν₀ P₀) (normalizedFiniteMeasure ν₁ P₀) := by
calc
klDiv ν₀ ν₁ = klDiv
(finiteMeasureMass ν₀ • normalizedFiniteMeasure ν₀ P₀)
(finiteMeasureMass ν₀ • normalizedFiniteMeasure ν₁ P₀) := by
exact congrArg₂ klDiv hrecover₀.symm hrecover₁'.symm
_ = _ := InformationTheory.klDiv_smul_same (finiteMeasureMass ν₀)
calc
((lam * finiteMeasureMass ν₀ : ℝ≥0) : ℝ≥0∞) *
klDiv
(normalizedFiniteMeasure ν₀ P₀) (normalizedFiniteMeasure ν₁ P₀) =
(lam : ℝ≥0∞) * ((finiteMeasureMass ν₀ : ℝ≥0∞) *
klDiv
(normalizedFiniteMeasure ν₀ P₀) (normalizedFiniteMeasure ν₁ P₀)) := by
simp only [ENNReal.coe_mul]
rw [mul_assoc]
_ = (lam : ℝ≥0∞) * klDiv ν₀ ν₁ := by
rw [hKL]
4 supporting declarations (lemmas, instances)
-
normalizedFiniteMeasure_isProbabilityMeasureinstance — For every measurable observation space, finite measure on that space, and probability measure on the same space, the normalized finite measure is a probability measure.parametersinstancenormalizedFiniteMeasure_isProbabilityMeasure ν P₀ :given byby classical rw [normalizedFiniteMeasure] split_ifs with hν · infer_instance · rw [isProbabilityMeasure_iff, Measure.smul_apply _ _ univ] have hmass : ν univ≠ 0 := by exact fun h ↦ hν (Measure.measure_univ_eq_zero.mp h) exact ENNReal.inv_mul_cancel hmass (ne_of_lt (measure_lt_top ν univ)) -
finiteMeasureMarkedPoissonLaw_isProbabilityMeasureinstance — For every measurable observation space, finite intensity measure on that space, fallback probability measure on that space, probability distribution for real-valued marks, and nonnegative scalar intensity, the resulting finite-measure marked Poisson law is a probability measure.parametersX :sharedType u_1ν :P₀ :R :lam :ℝ≥0instancefiniteMeasureMarkedPoissonLaw_isProbabilityMeasure ν P₀ R lam :IsProbabilityMeasure (finiteMeasureMarkedPoissonLaw ν P₀ R lam)given byby unfold finiteMeasureMarkedPoissonLaw infer_instance -
finiteMeasureMarkedPoissonLaw_map_countlemma — The count in the finite-measure marked Poisson experiment is Poisson with mean lam times the total mass of the intensity measure.hypothesesX :sharedType u_1ν :P₀ :R :lam :ℝ≥0conclusionMeasure.map FiniteSample.count (finiteMeasureMarkedPoissonLaw ν P₀ R lam)= poissonMeasure (lam * finiteMeasureMass ν)Proof (Lean source)
lemma finiteMeasureMarkedPoissonLaw_map_count (ν : Measure X) [IsFiniteMeasure ν] (P₀ : Measure X) [IsProbabilityMeasure P₀] (R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) : Measure.map FiniteSample.count (finiteMeasureMarkedPoissonLaw ν P₀ R lam) = poissonMeasure (lam * finiteMeasureMass ν) := by exact finiteMarkedPoissonSampleLaw_map_count (normalizedFiniteMeasure ν P₀) R (lam * finiteMeasureMass ν) -
klDiv_finiteMeasureMarkedPoissonLaw_lelemma — A one-point finite-measure KL bound transfers directly to the corresponding marked Poisson experiments after multiplication by the scalar intensity.Proof (Lean source)
lemma klDiv_finiteMeasureMarkedPoissonLaw_le [StandardBorelSpace X] (ν₀ ν₁ : Measure X) [IsFiniteMeasure ν₀] [IsFiniteMeasure ν₁] (P₀ : Measure X) [IsProbabilityMeasure P₀] (R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) (B : ℝ≥0∞) (hmass : ν₀ univ = ν₁ univ) (hKL : klDiv ν₀ ν₁ ≤ B) : klDiv (finiteMeasureMarkedPoissonLaw ν₀ P₀ R lam) (finiteMeasureMarkedPoissonLaw ν₁ P₀ R lam) ≤ (lam : ℝ≥0∞) * B := by rw [klDiv_finiteMeasureMarkedPoissonLaw ν₀ ν₁ P₀ R lam hmass] exact mul_le_mul_right hKL (lam : ℝ≥0∞)
Depoissonization 4 core · 12 supporting This file provides measurable maps between dependent finite samples, padded streams, and canonical marked configurations. ★ markedPoissonKL_le_two_mul_of_piKL
Finite-sample maps and de-Poissonization
This file provides measurable maps between dependent finite samples, padded streams, and canonical marked configurations. It also records the Poisson count identity and a reusable exponential lower-tail bound used to transfer random-size experiments to fixed sample sizes.
def finiteSampleMap reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Given a map from one observation space to another and a finite sample in the first space, the mapped finite sample has the same size and applies the map to every observation.
Definition (Lean source)
parameters
def
given by
⟨s.count, fun i => f (s.points i)⟩
lemma markedPoissonKL_le_two_mul_of_piKL reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Consider a sample size n that is at least 1 and a nonnegative KL budget B, and suppose the KL divergence between n independent identically distributed draws from P and from Q is at most B. Then the KL divergence between the marked Poisson experiments with mean count 2n, mark law R, and intensity measures P and Q respectively (both built over the same baseline P) is at most 2B.
Formal statement
Proof (Lean source)
lemma markedPoissonKL_le_two_mul_of_piKL
{X : Type*} [MeasurableSpace X] [StandardBorelSpace X]
(P Q : Measure X) [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
(R : Measure ℝ) [IsProbabilityMeasure R]
(n : ℕ) (hn : 1 ≤ n) {B : ℝ} (hB : 0 ≤ B)
(hpi : klDiv
(Measure.pi (fun _ : Fin n => P))
(Measure.pi (fun _ : Fin n => Q)) ≤ ofReal B) :
klDiv
(finiteMeasureMarkedPoissonLaw P P R (2 * n))
(finiteMeasureMarkedPoissonLaw Q P R (2 * n)) ≤
ofReal (2 * B) := by
let i : Fin n := ⟨0, lt_of_lt_of_le Nat.zero_lt_one hn⟩
have hone_le : klDiv P Q ≤
klDiv (Measure.pi (fun _ : Fin n => P))
(Measure.pi (fun _ : Fin n => Q)) := by
have h := klDiv_map_le
(measurable_pi_apply i) (μ := Measure.pi (fun _ : Fin n => P))
(ν := Measure.pi (fun _ : Fin n => Q))
rw [Measure.pi_map_eval, Measure.pi_map_eval] at h
simpa using h
have hprod_ne : klDiv
(Measure.pi (fun _ : Fin n => P))
(Measure.pi (fun _ : Fin n => Q)) ≠ ⊤ :=
ne_top_of_le_ne_top ENNReal.ofReal_ne_top hpi
have hone_ne : klDiv P Q ≠ ⊤ :=
ne_top_of_le_ne_top hprod_ne hone_le
have hguards := InformationTheory.klDiv_ne_top_iff.mp hone_ne
have hreal := Causalean.Mathlib.InformationTheory.productKL_tensorization_of_finite
n P Q hguards.1 hguards.2
have heq : klDiv
(Measure.pi (fun _ : Fin n => P))
(Measure.pi (fun _ : Fin n => Q)) =
(n : ℝ≥0∞) * klDiv P Q := by
have hmul : (n : ℝ≥0∞) * klDiv P Q ≠ ⊤ :=
ENNReal.mul_ne_top (ENNReal.natCast_ne_top n) hone_ne
apply (ENNReal.toReal_eq_toReal_iff' hprod_ne hmul).mp
rw [ENNReal.toReal_mul, ENNReal.toReal_natCast]
exact hreal
rw [klDiv_finiteMeasureMarkedPoissonLaw P Q P R (2 * n) (by simp)]
rw [show (((2 : ℝ≥0) * (n : ℝ≥0) : ℝ≥0) : ℝ≥0∞) =
(2 : ℝ≥0∞) * (n : ℝ≥0∞) by norm_num,
mul_assoc, ← heq]
calc
(2 : ℝ≥0∞) * klDiv
(Measure.pi (fun _ : Fin n => P))
(Measure.pi (fun _ : Fin n => Q)) ≤
2 * ofReal B := mul_le_mul_right hpi 2
_ = ofReal (2 * B) := by
rw [ENNReal.ofReal_mul (by norm_num : (0 : ℝ) ≤ 2)]
norm_num
def canonicalPrefixObservations reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Given a fallback observation, a nonnegative integer prefix length, and a finite sample of observation--real-mark pairs, the canonical prefix observations are the first observations when the sample has at least pairs, and otherwise are the constant -tuple of the fallback observation.
Definition (Lean source)
parameters
def
given by
if h : n ≤ s.count then fun k => (s.points (Fin.castLE h k)).1 else fun _ => x₀
def finiteSamplePaddedStream reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Given a fallback observation and a finite sample, the padded stream representation is the pair consisting of its size and an infinite stream that agrees with the sample at positions below that size and equals the fallback observation thereafter.
Definition (Lean source)
parameters
def
finiteSamplePaddedStream x0 s :
ℕ × (ℕ → X)
given by
(s.count, fun k => if h : k < s.count then s.points ⟨k, h⟩ else x0)
12 supporting declarations (lemmas, instances)
-
measurable_finiteSampleMaplemma — Pointwise mapping of dependent finite samples is measurable.hypothesesconclusionProof (Lean source)
@[fun_prop] lemma measurable_finiteSampleMap {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (f : X → Y) (hf : Measurable f) : Measurable (finiteSampleMap f : FiniteSample X → FiniteSample Y) := by intro s hs rw [MeasurableSpace.measurableSet_iInf] at hs ⊢ intro n let g : (Fin n → X) → (Fin n → Y) := fun x i => f (x i) have hg : Measurable g := measurable_pi_lambda _ fun i => hf.comp (measurable_pi_apply i) have hsn := hs n change MeasurableSet (fixedSizeEmbed n ⁻¹' s) at hsn change MeasurableSet ((fun x : Fin n → X => ⟨n, fun i => f (x i)⟩) ⁻¹' s) exact hsn.preimage hg -
finiteSampleMap_fixedSizeEmbedlemma — Mapping commutes with fixed-size embedding.hypothesesconclusionProof (Lean source)
lemma finiteSampleMap_fixedSizeEmbed {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (f : X → Y) (n : ℕ) (x : Fin n → X) : finiteSampleMap f (fixedSizeEmbed n x) = fixedSizeEmbed n (fun i => f (x i)) := rfl -
cellObservationLaw_eq_of_restrict_eqlemma — Equal restrictions and equal cell masses give equal normalized cell laws.hypothesesX ι :p :μ ν :j :ιhpos :μ (p.cellSet j) ≠ 0hmass :μ (p.cellSet j) = ν (p.cellSet j)hrest :μ.restrict (p.cellSet j) = ν.restrict (p.cellSet j)conclusionp.cellObservationLaw μ j = p.cellObservationLaw ν jProof (Lean source)
lemma cellObservationLaw_eq_of_restrict_eq {X ι : Type*} [MeasurableSpace X] [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (p : FiniteMeasurablePartition X ι) (μ ν : Measure X) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (j : ι) (hpos : μ (p.cellSet j) ≠ 0) (hmass : μ (p.cellSet j) = ν (p.cellSet j)) (hrest : μ.restrict (p.cellSet j) = ν.restrict (p.cellSet j)) : p.cellObservationLaw μ j = p.cellObservationLaw ν j := by unfold FiniteMeasurablePartition.cellObservationLaw have hν : ν (p.cellSet j) ≠ 0 := by simpa [← hmass] rw [dif_neg hpos, dif_neg hν, ← hmass, hrest] -
measurable_canonicalPrefixObservationslemma — Reading a fixed prefix from a canonical finite configuration is measurable.hypothesesconclusionProof (Lean source)
@[fun_prop] lemma measurable_canonicalPrefixObservations {X : Type*} [MeasurableSpace X] (x₀ : X) (n : ℕ) : Measurable (canonicalPrefixObservations x₀ n : FiniteSample (X × ℝ) → Fin n → X) := by unfold canonicalPrefixObservations apply measurable_pi_lambda intro k t ht rw [MeasurableSpace.measurableSet_iInf] intro m change MeasurableSet ((fun x : Fin m → X × ℝ => (if h : n ≤ m then fun k => (x (Fin.castLE h k)).1 else fun _ => x₀) k) ⁻¹' t) by_cases h : n ≤ m · simp only [dif_pos h] exact ht.preimage ((measurable_pi_apply (Fin.castLE h k)).fst) · simp only [dif_neg h] exact measurable_const ht -
map_canonicalPrefixObservations_restrict_count_gelemma — On the successful-count event, the canonical marked-Poisson configuration's first n observations have the unnormalised product law.hypothesesX :Type*P :lam :ℝ≥0x₀ :Xn :ℕconclusionMeasure.map (canonicalPrefixObservations x₀ n) ((canonicalMarkedPoissonSampleLaw P R lam).restrict (FiniteSample.count ⁻¹' Ici n))Proof (Lean source)
lemma map_canonicalPrefixObservations_restrict_count_ge {X : Type*} [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] (R : Measure ℝ) [IsProbabilityMeasure R] [NullSingletonClass R] (lam : ℝ≥0) (x₀ : X) (n : ℕ) : Measure.map (canonicalPrefixObservations x₀ n) ((canonicalMarkedPoissonSampleLaw P R lam).restrict (FiniteSample.count ⁻¹' Ici n)) = (poissonMeasure lam) (Ici n) • Measure.pi (fun _ : Fin n => P) := by let μ := finiteMarkedPoissonSampleLaw P R lam have hcount : orderByMarks ⁻¹' (FiniteSample.count ⁻¹' Ici n : Set (FiniteSample (X × ℝ))) = FiniteSample.count ⁻¹' Ici n := by ext s change (n ≤ (orderByMarks s).count) ↔ n ≤ s.count rw [orderByMarks_count] rw [canonicalMarkedPoissonSampleLaw, Measure.restrict_map measurable_orderByMarks (measurable_finiteSample_count (measurableSet_Ici)), hcount, Measure.map_map (measurable_canonicalPrefixObservations x₀ n) measurable_orderByMarks] have hfun : canonicalPrefixObservations x₀ n ∘ orderByMarks = retainedObservations x₀ n := by funext s unfold canonicalPrefixObservations retainedObservations by_cases h : n ≤ s.count · simp only [orderByMarks_count, dif_pos h, Function.comp_apply] funext k congr 2 · simp only [orderByMarks_count, dif_neg h, Function.comp_apply] rw [hfun] exact map_retainedObservations_restrict_count_ge P R lam x₀ n -
poisson_two_n_lower_taillemma — The lower tail used in de-Poissonization is exponentially small.Proof (Lean source)
lemma poisson_two_n_lower_tail (n : ℕ) : (poissonMeasure (2 * n)) {k | k < n} ≤ ofReal (exp (-(n : ℝ) * (1 - log 2))) := by rw [show {k : ℕ | k < n} = (↑(range n) : Set ℕ) by ext k; simp] rw [← MeasureTheory.sum_measure_singleton] simp_rw [poissonMeasure_singleton_eq_poissonPMF] have hterm : ∀ k ∈ range n, poissonPMF (2 * n) k ≤ ofReal (exp (-(n : ℝ) * (1 - log 2))) * poissonPMF n k := by intro k hk have hreal : poissonPMFReal (2 * (n : ℝ≥0)) k ≤ exp (-(n : ℝ) * (1 - log 2)) * poissonPMFReal (n : ℝ≥0) k := by unfold poissonPMFReal rw [← mul_div_assoc] apply (div_le_div_iff_of_pos_right (by positivity : (0 : ℝ) < k.factorial)).2 have hn0 : (0 : ℝ) ≤ n := by positivity have hpow : (2 : ℝ) ^ k ≤ 2 ^ n := pow_le_pow_right₀ (by norm_num) (Finset.mem_range.1 hk).le have htarget : exp (-(n : ℝ) * (1 - log 2)) = exp (-(n : ℝ)) * (2 : ℝ) ^ n := by rw [show -(n : ℝ) * (1 - log 2) = -(n : ℝ) + log 2 * n by ring, Real.exp_add, show log 2 * (n : ℝ) = (n : ℝ) * log 2 by ring, Real.exp_nat_mul, Real.exp_log (by norm_num : (0 : ℝ) < 2)] have hexp2 : exp (-((2 : ℝ) * (n : ℝ))) = exp (-(n : ℝ)) * exp (-(n : ℝ)) := by rw [← Real.exp_add] congr 1 ring norm_num only [NNReal.smul_def, NNReal.coe_natCast, NNReal.coe_mul, Nat.cast_ofNat] rw [mul_pow, htarget] change exp (-(2 * (n : ℝ))) * ((2 : ℝ) ^ k * (n : ℝ) ^ k) ≤ _ rw [hexp2] calc exp (-(n : ℝ)) * exp (-(n : ℝ)) * ((2 : ℝ) ^ k * (n : ℝ) ^ k) = (exp (-(n : ℝ)) * exp (-(n : ℝ)) * (n : ℝ) ^ k) * 2 ^ k := by ring _ ≤ (exp (-(n : ℝ)) * exp (-(n : ℝ)) * (n : ℝ) ^ k) * 2 ^ n := mul_le_mul_of_nonneg_left hpow (by positivity) _ = exp (-(n : ℝ)) * 2 ^ n * (exp (-(n : ℝ)) * (n : ℝ) ^ k) := by ring unfold poissonPMF change ofReal (poissonPMFReal (2 * n) k) ≤ ofReal (exp (-(n : ℝ) * (1 - log 2))) * ofReal (poissonPMFReal n k) rw [← ENNReal.ofReal_mul (Real.exp_pos _).le] exact ENNReal.ofReal_le_ofReal hreal calc ∑ k ∈ range n, poissonPMF (2 * n) k ≤ ∑ k ∈ range n, ofReal (exp (-(n : ℝ) * (1 - log 2))) * poissonPMF n k := Finset.sum_le_sum hterm _ = ofReal (exp (-(n : ℝ) * (1 - log 2))) * ∑ k ∈ range n, poissonPMF n k := by rw [Finset.mul_sum] _ ≤ ofReal (exp (-(n : ℝ) * (1 - log 2))) * 1 := by gcongr exact ((poissonPMF n).property.summable.sum_le_tsum _ (fun _ _ => bot_le)).trans_eq (poissonPMF n).property.tsum_eq _ = _ := mul_one _ -
finiteSamplePaddedStream_measurablelemmaProof (Lean source)
@[fun_prop] lemma finiteSamplePaddedStream_measurable {X : Type*} [MeasurableSpace X] (x0 : X) : Measurable (finiteSamplePaddedStream x0) := by intro t ht rw [MeasurableSpace.measurableSet_iInf] intro n change MeasurableSet ((fun s : Fin n → X => finiteSamplePaddedStream x0 ⟨n, s⟩) ⁻¹' t) apply ht.preimage apply measurable_const.prodMk apply measurable_pi_lambda intro k by_cases hk : k < n · let i : Fin n := ⟨k, hk⟩ simpa [finiteSamplePaddedStream, FiniteSample.count, FiniteSample.points, hk, i] using (measurable_pi_apply i : Measurable (fun s : Fin n → X => s i)) · simp [finiteSamplePaddedStream, FiniteSample.count, hk] -
streamToFiniteSample_paddedStreamlemmahypothesesconclusionstreamToFiniteSample (finiteSamplePaddedStream x0 s) = sProof (Lean source)
lemma streamToFiniteSample_paddedStream {X : Type*} [MeasurableSpace X] (x0 : X) (s : FiniteSample X) : streamToFiniteSample (finiteSamplePaddedStream x0 s) = s := by cases s with | mk n s => change (⟨n, fun k => if h : k < n then s ⟨k, h⟩ else x0⟩ : Σ n : ℕ, Fin n → X) = ⟨n, s⟩ congr funext k simp -
finiteSamplePaddedStream_rangelemmahypothesesX :Type*x0 :Xconclusionrange (finiteSamplePaddedStream x0) = {z : ℕ × (ℕ → X) | ∀ k, z.1 ≤ k → z.2 k = x0}Proof (Lean source)
lemma finiteSamplePaddedStream_range {X : Type*} [MeasurableSpace X] (x0 : X) : range (finiteSamplePaddedStream x0) = {z : ℕ × (ℕ → X) | ∀ k, z.1 ≤ k → z.2 k = x0} := by ext z constructor · rintro ⟨s, rfl⟩ k hk have hnot : ¬k < s.count := Nat.not_lt_of_ge hk simp [finiteSamplePaddedStream, hnot] · intro hz refine ⟨streamToFiniteSample z, ?_⟩ apply Prod.ext · rfl · funext k by_cases hk : k < z.1 · simp [finiteSamplePaddedStream, FiniteSample.count, FiniteSample.points, streamToFiniteSample, hk] · simp [finiteSamplePaddedStream, FiniteSample.count, FiniteSample.points, streamToFiniteSample, hk, hz k (Nat.le_of_not_gt hk)] -
finiteSample_standardBorelSpaceinstance — For every nonempty standard Borel observation space equipped with its measurable structure, the space of finite samples from that observation space is a standard Borel space.parametersX :instancegiven byby let x0 : X := Classical.choice ‹Nonempty X› let rangeSet : Set (ℕ × (ℕ → X)) := range (finiteSamplePaddedStream x0) have hrange : MeasurableSet rangeSet := by dsimp [rangeSet] rw [finiteSamplePaddedStream_range x0] rw [show {z : ℕ × (ℕ → X) | ∀ k, z.1 ≤ k → z.2 k = x0} = ⋂ k : ℕ, {z | k < z.1} ∪ {z | z.2 k = x0} by ext z simp only [Set.mem_setOf_eq, Set.mem_iInter, Set.mem_union] constructor · intro h k by_cases hk : k < z.1 · exact inl hk · exact inr (h k (Nat.le_of_not_gt hk)) · intro h k hk exact (h k).resolve_left (Nat.not_lt_of_ge hk)] apply MeasurableSet.iInter intro k exact (measurableSet_lt measurable_const measurable_fst).union ((measurableSet_singleton x0).preimage ((measurable_pi_apply k).comp measurable_snd)) let e : FiniteSample X ≃ᵐ rangeSet := { toEquiv := { toFun := fun s => ⟨finiteSamplePaddedStream x0 s, ⟨s, rfl⟩⟩ invFun := fun z => streamToFiniteSample z.1 left_inv := streamToFiniteSample_paddedStream x0 right_inv := by intro z apply Subtype.ext obtain ⟨s, hs⟩ := z.2 change finiteSamplePaddedStream x0 (streamToFiniteSample z.1) = z.1 rw [← hs, streamToFiniteSample_paddedStream] } measurable_toFun := by exact (finiteSamplePaddedStream_measurable x0).subtype_mk (h := fun s => ⟨s, rfl⟩) measurable_invFun := by exact measurable_streamToFiniteSample.comp measurable_subtype_coe } letI hsb : StandardBorelSpace rangeSet := hrange.standardBorel letI upgraded : UpgradedStandardBorel rangeSet := upgradeStandardBorel rangeSet letI : TopologicalSpace rangeSet := upgraded.toTopologicalSpace letI : BorelSpace rangeSet := upgraded.toBorelSpace letI : PolishSpace rangeSet := upgraded.toPolishSpace let tau : TopologicalSpace (FiniteSample X) := (inferInstance : TopologicalSpace rangeSet).induced e refine ⟨⟨tau, ?_, ?_⟩⟩ · exact e.measurableEmbedding.borelSpace ⟨rfl⟩ · exact e.toEquiv.polishSpace_induced -
canonicalMarkedPoissonSampleLaw_map_countlemmahypothesesX :Type*P :R :lam :ℝ≥0conclusionMeasure.map FiniteSample.count (canonicalMarkedPoissonSampleLaw P R lam)= poissonMeasure lamProof (Lean source)
lemma canonicalMarkedPoissonSampleLaw_map_count {X : Type*} [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] (R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) : Measure.map FiniteSample.count (canonicalMarkedPoissonSampleLaw P R lam) = poissonMeasure lam := by unfold canonicalMarkedPoissonSampleLaw rw [Measure.map_map measurable_finiteSample_count measurable_orderByMarks] simpa only [Function.comp_def, orderByMarks_count] using finiteMarkedPoissonSampleLaw_map_count P R lam -
finiteMeasureMarkedPoissonLaw_probability_eqtheorem — When the intensity measure is already a probability law, the finite-measure Poisson wrapper agrees with the ordinary marked-Poisson sample law.hypothesesX :Type*P :P0 :R :lam :ℝ≥0conclusionfiniteMeasureMarkedPoissonLaw P P0 R lam = finiteMarkedPoissonSampleLaw P R lamProof (Lean source)
theorem finiteMeasureMarkedPoissonLaw_probability_eq {X : Type*} [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] (P0 : Measure X) [IsProbabilityMeasure P0] (R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) : finiteMeasureMarkedPoissonLaw P P0 R lam = finiteMarkedPoissonSampleLaw P R lam := by have hP : P ≠ 0 := by intro h have : P univ = 1 := by simp simp [h] at this have hnorm : normalizedFiniteMeasure P P0 = P := by unfold normalizedFiniteMeasure rw [dif_neg hP] simp have hmass : finiteMeasureMass P = 1 := by unfold finiteMeasureMass simp unfold finiteMeasureMarkedPoissonLaw rw [hmass, mul_one] congr 2
IIDPoisson 3 core · 4 supporting This file provides the paper-neutral count-and-stream probability space used as the elementary input to finite marked Poisson constructions. ★ iidStreamLaw_map_finPrefix
I.i.d. streams paired with an independent Poisson count
This file provides the paper-neutral count-and-stream probability space used as the elementary input to finite marked Poisson constructions. An infinite i.i.d. stream has exact finite product marginals, and pairing it with an independent scalar Poisson count preserves both the count and prefix laws.
def iidStreamLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Given a probability measure on a measurable sample space, the law of an infinite independent and identically distributed stream is the product probability measure on infinite sequences whose every coordinate has that measure as its marginal.
Definition (Lean source)
parameters
X :
Type u_1
P :
def
given by
Measure.infinitePi (fun _ : ℕ => P)
lemma iidStreamLaw_map_finPrefix reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Every finite prefix of length n of an infinite stream whose coordinates are i.i.d. with common law P has exactly the corresponding n-fold product law.
Formal statement
hypotheses
conclusion
Measure.map (fun z : ℕ → X => fun i : Fin n => z i) (iidStreamLaw P)
= Measure.pi (fun _ : Fin n => P)
Proof (Lean source)
lemma iidStreamLaw_map_finPrefix (P : Measure X) [IsProbabilityMeasure P] (n : ℕ) :
Measure.map (fun z : ℕ → X => fun i : Fin n => z i) (iidStreamLaw P) =
Measure.pi (fun _ : Fin n => P) := by
unfold iidStreamLaw
symm
apply Measure.pi_eq
intro s hs
rw [Measure.map_apply (by fun_prop) (.univ_pi hs)]
rw [show (fun z : ℕ → X => fun i : Fin n => z i) ⁻¹' Set.univ.pi s =
pi (range n)
(fun i : ℕ => if h : i < n then s ⟨i, h⟩ else univ) by
ext z
simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, forall_const]
constructor
· intro hz i hi
have hin : i < n := by simpa using hi
rw [dif_pos hin]
simpa using hz ⟨i, hin⟩
· intro hz i
have hi := hz (i : ℕ)
(show (i : ℕ) ∈ range n from Finset.mem_range.mpr i.2)
rw [dif_pos i.2] at hi
simpa using hi]
rw [Measure.infinitePi_pi (μ := fun _ : ℕ => P)
(s := range n)
(t := fun i : ℕ => if h : i < n then s ⟨i, h⟩ else univ)]
· rw [Finset.prod_range]
simp
· intro i hi
rw [dif_pos (Finset.mem_range.1 hi)]
exact hs _
def poissonIIDStreamLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkedPoissonPartition
Given a probability measure on a measurable sample space and a nonnegative Poisson rate, the joint count-and-stream law is the product law of a Poisson count with that rate and an independent infinite stream whose coordinates are independent with the given common distribution.
Definition (Lean source)
parameters
def
given by
4 supporting declarations (lemmas, instances)
-
iidStreamLaw_isProbabilityMeasureinstance — For every measurable sample space and probability measure on that space, the law of the infinite independent and identically distributed stream is a probability measure. -
poissonIIDStreamLaw_isProbabilityMeasureinstance — For every measurable sample space, probability measure on that space, and nonnegative Poisson rate, the joint law of an independent Poisson count and an independent and identically distributed stream is a probability measure. -
poissonIIDStreamLaw_map_countlemma — The count coordinate has the requested scalar Poisson law.hypothesesconclusionProof (Lean source)
lemma poissonIIDStreamLaw_map_count (P : Measure X) [IsProbabilityMeasure P] (lam : ℝ≥0) : Measure.map fst (poissonIIDStreamLaw P lam) = poissonMeasure lam := by unfold poissonIIDStreamLaw iidStreamLaw rw [Measure.map_fst_prod, measure_univ, one_smul] -
poissonIIDStreamLaw_map_finPrefixlemma — Every finite stream prefix remains an exact product sample after pairing the stream with an independent Poisson count.hypothesesconclusionMeasure.map (fun z : ℕ × (ℕ → X) => fun i : Fin n => z.2 i) (poissonIIDStreamLaw P lam)= Measure.pi (fun _ : Fin n => P)Proof (Lean source)
lemma poissonIIDStreamLaw_map_finPrefix (P : Measure X) [IsProbabilityMeasure P] (lam : ℝ≥0) (n : ℕ) : Measure.map (fun z : ℕ × (ℕ → X) => fun i : Fin n => z.2 i) (poissonIIDStreamLaw P lam) = Measure.pi (fun _ : Fin n => P) := by rw [show (fun z : ℕ × (ℕ → X) => fun i : Fin n => z.2 i) = (fun z : ℕ → X => fun i : Fin n => z i) ∘ snd by rfl, ← Measure.map_map (by fun_prop) (by fun_prop)] unfold poissonIIDStreamLaw rw [Measure.map_snd_prod, measure_univ, one_smul, iidStreamLaw_map_finPrefix]