Stat.FiniteRaoBlackwell.Poisson.FinitePartition
This roll-up module exports the ordered finite-label splitting law for one iid pool, its capped fixed-sample conditional mean, its explicit finite expansion, and the bounded squared-risk transfer to independent Poisson l
NestedEventMoment 8 core · 7 supporting · 4 submodules The fixed-count identity is mixed over the Poisson sample size to give a total, division-free joint factorial moment. NestedEventRatioMean 9 core · 15 supporting · 5 submodules For arbitrary probability laws and measurable nested events, the total mean identity multiplies the success-fraction expectation by containing-event mass.
Basic 9 core · 0 supporting Defines the ordered label streams, the Poisson and label auxiliary experiment, and its capped conditional expectation on one fixed iid pool. ★ labelLaw_isProbabilityMeasure
A single iid pool with independently assigned finite labels
Defines the ordered label streams, the Poisson and label auxiliary experiment, and its capped conditional expectation on one fixed iid pool.
def labelLaw reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.Poisson.FinitePartition
For label masses summing to one, the label law assigns each label its specified mass. It is given by the finite mass function's probability measure.
theorem labelLaw_isProbabilityMeasure reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.Poisson.FinitePartition
The finite label law is a probability measure when its label masses sum to one.
Formal statement
hypotheses
I :
Type u_2
p :
I → ℝ≥0
hp :
∑ i, p i = 1
conclusion
IsProbabilityMeasure (labelLaw p hp)
Proof (Lean source)
theorem labelLaw_isProbabilityMeasure (p : I → ℝ≥0) (hp : ∑ i, p i = 1) :
IsProbabilityMeasure (labelLaw p hp) := by
classical
unfold labelLaw
infer_instance
def unshuffle reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.Poisson.FinitePartition
Given a finite sequence of labeled observations, ordered label streams retain observations of each label in their original relative order. They are given by the label-wise regrouping.
Definition (Lean source)
parameters
def
given by
fun i
=> ⟨wordHistogram (fun k => (s.2 k).2) i, gatherWord (fun k => (s.2 k).2) (fun k => (s.2 k).1) i⟩
def labeledPrefix reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.Poisson.FinitePartition
Given a fixed iid pool, an admissible count, and labels for that prefix, its ordered label streams preserve within-label arrival order. They are given by unshuffling the labeled prefix.
Definition (Lean source)
def cappedStatistic reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.Poisson.FinitePartition
Given a fixed pool, a Poisson count and label vector, a stream statistic, and an overflow value, the capped statistic evaluates the labeled prefix when it fits and uses the overflow value otherwise. It is given by the capacity test.
Definition (Lean source)
parameters
X :
Type u_1
I :
Type u_2
n :
ℕ
x :
Fin n → X
T :
(I → FiniteSample X) → ℝ
zOver :
ℝ
z :
ℕ × (Fin n → I)
def
cappedStatistic x T zOver z :
ℝ
given by
if h : z.1
≤ n then T (labeledPrefix x z.1 h (fun k => z.2 ⟨k.val, lt_of_lt_of_le k.isLt h⟩)) else zOver
def auxiliaryLaw reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.Poisson.FinitePartition
Given label masses summing to one, a Poisson mean, and pool size, the auxiliary law draws an independent Poisson count and independent labels for all positions of the fixed pool. It is given by their product measure.
Definition (Lean source)
parameters
I :
Type u_2
p :
I → ℝ≥0
hp :
∑ i, p i = 1
lambda :
ℝ≥0
n :
ℕ
given by
by letI := labelLaw_isProbabilityMeasure p hp exact (poissonMeasure lambda).prod (Measure.pi (fun _ : Fin n => labelLaw p hp))
def fixedStatistic reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.Poisson.FinitePartition
Given label masses summing to one, a Poisson mean, a fixed iid pool, a stream statistic, and an overflow value, the fixed-sample statistic averages the capped statistic over the independent count and labels. It is given by that auxiliary expectation.
Definition (Lean source)
parameters
X :
Type u_1
I :
Type u_2
p :
I → ℝ≥0
hp :
∑ i, p i = 1
lambda :
ℝ≥0
n :
ℕ
x :
Fin n → X
T :
(I → FiniteSample X) → ℝ
zOver :
ℝ
def
fixedStatistic p hp lambda x T zOver :
ℝ
given by
∫ z, cappedStatistic x T zOver z ∂auxiliaryLaw p hp lambda n
def labeledStreamLaw reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.Poisson.FinitePartition
Given an observation law, label masses summing to one, and a Poisson mean, the uncapped ordered-stream law labels a finite Poisson sample and unshuffles it by label. It is given by the mapped marked-Poisson law.
Definition (Lean source)
parameters
X :
Type u_1
I :
Type u_2
P :
p :
I → ℝ≥0
hp :
∑ i, p i = 1
lambda :
ℝ≥0
def
given by
by letI := labelLaw_isProbabilityMeasure p hp exact Measure.map unshuffle (finitePoissonSampleLaw (P.prod (labelLaw p hp)) lambda)
def fixedPoolLaw reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.Poisson.FinitePartition
Given an observation law and a pool size, the fixed iid pool law has independent observations at each of its positions. It is given by the finite iid product measure.
Definition (Lean source)
parameters
given by
Measure.pi (fun _ : Fin n => P)
CountVector 1 core · 1 supporting The histogram probability of an iid finite label word combines with its Poisson total count to give independent Poisson cell counts. ★ poisson_label_word_coefficient_eq
Count-vector coefficients and independent Poisson fibres
The histogram probability of an iid finite label word combines with its Poisson total count to give independent Poisson cell counts. The independent stream law has the corresponding fixed-count product fibres.
theorem poisson_label_word_coefficient_eq reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.Poisson.FinitePartition
Given label masses summing to one, a Poisson mean, and a prescribed vector of label counts, the Poisson mass of the total count times the total probability of label words with that histogram equals the product of the label-specific Poisson masses.
Formal statement
hypotheses
I :
Type u_2
p :
I → ℝ≥0
hp :
∑ i, p i = 1
lambda :
ℝ≥0
c :
I → ℕ
conclusion
(poissonMeasure lambda) ({∑ i, c i} : Set ℕ) * (∑ w : Fin (∑ i, c i) → I, if ∀ i, wordHistogram w i = c i then ∏ k, (p (w k) : ℝ≥0∞) else 0)
= ∏ i, (poissonMeasure (lambda * p i)) ({c i} : Set ℕ)
Proof (Lean source)
theorem poisson_label_word_coefficient_eq
(p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0) (c : I → ℕ) :
(poissonMeasure lambda) ({∑ i, c i} : Set ℕ) *
(∑ w : Fin (∑ i, c i) → I,
if ∀ i, wordHistogram w i = c i then
∏ k, (p (w k) : ℝ≥0∞) else 0) =
∏ i, (poissonMeasure (lambda * p i)) ({c i} : Set ℕ) := by
classical
let n := ∑ i, c i
let H := histogramWords n c
have hweight (w : Fin n → I) (hw : w ∈ H) :
∏ k, (p (w k) : ℝ≥0∞) = ∏ i, (p i : ℝ≥0∞) ^ c i := by
rw [← Finset.prod_fiberwise (Finset.univ : Finset (Fin n)) w
(fun k => (p (w k) : ℝ≥0∞))]
apply Finset.prod_congr rfl
intro i _
have hi := (Finset.mem_filter.1 hw).2 i
have hfactor : (∏ k ∈ (Finset.univ.filter fun k : Fin n => w k = i),
(p (w k) : ℝ≥0∞)) =
(p i : ℝ≥0∞) ^ wordHistogram w i := by
rw [wordHistogram]
calc
(∏ k ∈ (Finset.univ.filter fun k : Fin n => w k = i),
(p (w k) : ℝ≥0∞)) =
∏ _k ∈ (Finset.univ.filter fun k : Fin n => w k = i),
(p i : ℝ≥0∞) := by
apply Finset.prod_congr rfl
intro k hk
rw [(Finset.mem_filter.1 hk).2]
_ = (p i : ℝ≥0∞) ^
(Finset.univ.filter fun k : Fin n => w k = i).card := by
rw [Finset.prod_const]
rw [hfactor, hi]
have hsum :
(∑ w : Fin n → I,
if ∀ i, wordHistogram w i = c i then
∏ k, (p (w k) : ℝ≥0∞) else 0) =
(H.card : ℝ≥0∞) * ∏ i, (p i : ℝ≥0∞) ^ c i := by
simp only [← Finset.sum_filter]
change (∑ w ∈ H, ∏ k, (p (w k) : ℝ≥0∞)) =
(H.card : ℝ≥0∞) * ∏ i, (p i : ℝ≥0∞) ^ c i
rw [Finset.sum_congr rfl (fun w hw => hweight w hw)]
simp
rw [hsum]
rw [← mul_assoc]
have hcard : H.card = Nat.multinomial Finset.univ c :=
histogramWords_card n c rfl
simp_rw [poissonMeasure_singleton]
rw [hcard]
change (ofReal (poissonPMFReal lambda (∑ i, c i)) *
(Nat.multinomial Finset.univ c : ℝ≥0∞)) *
∏ i : I, (p i : ℝ≥0∞) ^ c i =
∏ i : I, ofReal (poissonPMFReal (lambda * p i) (c i))
have hreal :
poissonPMFReal lambda (∑ i, c i) *
(Nat.multinomial Finset.univ c : ℝ) *
∏ i : I, (p i : ℝ) ^ c i =
∏ i : I, poissonPMFReal (lambda * p i) (c i) := by
unfold poissonPMFReal
push_cast
simp_rw [mul_pow]
rw [Finset.prod_div_distrib, Finset.prod_mul_distrib,
Finset.prod_mul_distrib,
Finset.prod_pow_eq_pow_sum Finset.univ c (lambda : ℝ),
← Real.exp_sum]
have hpR : ∑ i : I, (p i : ℝ) = 1 := by
exact_mod_cast hp
have hexp : ∑ i : I, -((lambda : ℝ) * (p i : ℝ)) = -(lambda : ℝ) := by
rw [show (fun i : I => -((lambda : ℝ) * (p i : ℝ))) =
fun i => -(lambda : ℝ) * (p i : ℝ) by
funext i
ring]
rw [← Finset.mul_sum, hpR, mul_one]
rw [hexp]
have hmulti := Nat.multinomial_spec Finset.univ c
have hmultiR := congrArg (fun m : ℕ => (m : ℝ)) hmulti
push_cast at hmultiR
field_simp
rw [← hmultiR]
ring
have hof := congrArg ofReal hreal
rw [ENNReal.ofReal_prod_of_nonneg
(fun i _ => poissonPMFReal_nonneg)] at hof
have hp0 : 0 ≤ poissonPMFReal lambda (∑ i, c i) := poissonPMFReal_nonneg
have hppow : ∀ i : I, 0 ≤ (p i : ℝ) ^ c i := fun i => by positivity
rw [ENNReal.ofReal_mul (mul_nonneg hp0 (Nat.cast_nonneg _)),
ENNReal.ofReal_mul hp0, ENNReal.ofReal_natCast,
ENNReal.ofReal_prod_of_nonneg (fun i _ => hppow i)] at hof
simp_rw [ENNReal.ofReal_pow (NNReal.coe_nonneg _)] at hof
simp only [ENNReal.ofReal_coe_nnreal] at hof
exact hof
1 supporting declaration (lemmas, instances)
-
independentStreamLaw_restrict_countVector_eqtheorem — Given an iid observation law, label masses, a Poisson mean, and a prescribed label-count vector, the independent finite-Poisson stream law on that count-vector fibre is the product of the count probabilities times independent fixed-length iid streams.hypothesesX :sharedType u_1I :sharedType u_2P :p :I → ℝ≥0lambda :ℝ≥0c :I → ℕconclusion(Measure.pi (fun i : I => finitePoissonSampleLaw P (lambda * p i))).restrict {s | ∀ i, (s i).count = c i}= (∏ i, (poissonMeasure (lambda * p i)) ({c i} : Set ℕ)) • Measure.pi (fun i : I => Measure.map (fixedSizeEmbed (c i)) (Measure.pi (fun _ : Fin (c i) => P)))Proof (Lean source)
theorem independentStreamLaw_restrict_countVector_eq (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (lambda : ℝ≥0) (c : I → ℕ) : (Measure.pi (fun i : I => finitePoissonSampleLaw P (lambda * p i))).restrict {s | ∀ i, (s i).count = c i} = (∏ i, (poissonMeasure (lambda * p i)) ({c i} : Set ℕ)) • Measure.pi (fun i : I => Measure.map (fixedSizeEmbed (c i)) (Measure.pi (fun _ : Fin (c i) => P))) := by classical have hB : {s : I → FiniteSample X | ∀ i, (s i).count = c i} = Set.univ.pi (fun i : I => FiniteSample.count ⁻¹' ({c i} : Set ℕ)) := by ext s simp letI (i : I) : IsProbabilityMeasure (Measure.map (fixedSizeEmbed (c i)) (Measure.pi fun _ : Fin (c i) => P)) := Measure.isProbabilityMeasure_map (measurable_fixedSizeEmbed (c i)).aemeasurable letI (i : I) : IsFiniteMeasure (poissonMeasure (lambda * p i) ({c i} : Set ℕ) • Measure.map (fixedSizeEmbed (c i)) (Measure.pi fun _ : Fin (c i) => P)) := ⟨by rw [Measure.smul_apply, measure_univ] simpa using measure_lt_top (poissonMeasure (lambda * p i)) ({c i} : Set ℕ)⟩ letI (i : I) : SigmaFinite (poissonMeasure (lambda * p i) ({c i} : Set ℕ) • Measure.map (fixedSizeEmbed (c i)) (Measure.pi fun _ : Fin (c i) => P)) := IsFiniteMeasure.toSigmaFinite _ rw [hB, Measure.restrict_pi_pi] simp_rw [finitePoissonSampleLaw_restrict_count_eq] apply Measure.pi_eq intro s hs rw [Measure.smul_apply, Measure.pi_pi] simp_rw [Measure.smul_apply, smul_eq_mul] exact Finset.prod_mul_distrib.symm
Expansion 1 core · 0 supporting This module gives the explicit finite count-and-label-map expression for the capped conditional mean, so downstream estimators can identify an existing Rao--Blackwellized formula without changing its definition. ★ fixedStatistic_eq_finite_sum
Finite count-and-label expansion
This module gives the explicit finite count-and-label-map expression for the capped conditional mean, so downstream estimators can identify an existing Rao--Blackwellized formula without changing its definition.
theorem fixedStatistic_eq_finite_sum reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.Poisson.FinitePartition
Given label masses summing to one, a Poisson mean, a fixed pool, a stream statistic, and an overflow value, the conditional mean equals the explicit finite sum over admissible counts and label maps, plus the Poisson overflow mass times the overflow value.
Formal statement
hypotheses
X :
Type u_1
I :
Type u_2
p :
I → ℝ≥0
hp :
∑ i, p i = 1
lambda :
ℝ≥0
n :
ℕ
x :
Fin n → X
T :
(I → FiniteSample X) → ℝ
zOver :
ℝ
conclusion
fixedStatistic p hp lambda x T zOver
= (∑ M : Fin (n + 1), (poissonMeasure lambda).real {M.val} * ∑ w : Fin M.val → I, (∏ k : Fin M.val, (p (w k) : ℝ)) * T (labeledPrefix x M.val (le_of_lt_succ M.isLt) w))
Proof (Lean source)
theorem fixedStatistic_eq_finite_sum
(p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0)
{n : ℕ} (x : Fin n → X) (T : (I → FiniteSample X) → ℝ)
(zOver : ℝ) :
fixedStatistic p hp lambda x T zOver =
(∑ M : Fin (n + 1),
(poissonMeasure lambda).real {M.val} *
∑ w : Fin M.val → I,
(∏ k : Fin M.val, (p (w k) : ℝ)) *
T (labeledPrefix x M.val (le_of_lt_succ M.isLt) w)) +
(poissonMeasure lambda).real (Ioi n) * zOver := by
classical
let μ : Measure ℕ := poissonMeasure lambda
let ρ : Measure (Fin n → I) := Measure.pi (fun _ : Fin n => labelLaw p hp)
let f : ℕ × (Fin n → I) → ℝ := cappedStatistic x T zOver
haveI : IsProbabilityMeasure ρ := by
dsimp [ρ]
haveI := labelLaw_isProbabilityMeasure p hp
infer_instance
haveI : IsProbabilityMeasure μ := by
dsimp [μ]
infer_instance
have hfinite : (range f).Finite := by
let g : Fin (n + 1) × (Fin n → I) → ℝ :=
fun z => f (z.1.val, z.2)
have hsub : range f ⊆ Set.insert zOver (range g) := by
rintro a ⟨z, rfl⟩
by_cases hz : z.1 ≤ n
· right
exact ⟨(⟨z.1, Nat.lt_succ_of_le hz⟩, z.2), rfl⟩
· left
simp [f, cappedStatistic, hz]
exact (Set.finite_range g).insert zOver |>.subset hsub
obtain ⟨C, hC⟩ := hfinite.isBounded.exists_norm_le
have hf : Integrable f (μ.prod ρ) := by
apply Integrable.of_bound (C := C)
· exact (measurable_of_countable f).aestronglyMeasurable
· filter_upwards [] with z
exact hC (f z) ⟨z, rfl⟩
have hprod :
fixedStatistic p hp lambda x T zOver =
∫ m : ℕ, (∫ w : Fin n → I, f (m, w) ∂ρ) ∂μ := by
change (∫ z, f z ∂μ.prod ρ) = _
exact integral_prod f hf
have hslice (m : ℕ) (hm : m ≤ n) :
(∫ w : Fin n → I, f (m, w) ∂ρ) =
∑ w : Fin m → I, (∏ k, (p (w k) : ℝ)) *
T (labeledPrefix x m hm w) := by
let q : (Fin n → I) → (Fin m → I) :=
fun w k => w ⟨k.val, lt_of_lt_of_le k.isLt hm⟩
have hq : Measurable q := by fun_prop
have hmeas : Measurable (fun w : Fin m → I => T (labeledPrefix x m hm w)) :=
measurable_of_countable _
calc
(∫ w : Fin n → I, f (m, w) ∂ρ) =
∫ w : Fin n → I, T (labeledPrefix x m hm (q w)) ∂ρ := by
congr 1
funext w
simp [f, cappedStatistic, hm, q]
_ = ∫ w : Fin m → I, T (labeledPrefix x m hm w)
∂Measure.map q ρ :=
(integral_map hq.aemeasurable hmeas.aestronglyMeasurable).symm
_ = ∫ w : Fin m → I, T (labeledPrefix x m hm w)
∂Measure.pi (fun _ : Fin m => labelLaw p hp) := by
rw [show Measure.map q ρ = Measure.pi (fun _ : Fin m => labelLaw p hp) from
map_labelPrefix_pi p hp hm]
_ = _ := integral_label_pi_eq_sum p hp m _
have htail (m : ℕ) (hm : n < m) :
(∫ w : Fin n → I, f (m, w) ∂ρ) = zOver := by
have hn : ¬ m ≤ n := Nat.not_le.mpr hm
simp [f, cappedStatistic, hn, ρ]
let g : ℕ → ℝ := fun m => ∫ w : Fin n → I, f (m, w) ∂ρ
have hg : Integrable g μ := hf.integral_prod_left
have hcap : (↑(range (n + 1)) : Set ℕ) = Iic n := by
ext m
simp
have hfirst :
(∫ m in Iic n, g m ∂μ) =
∑ M : Fin (n + 1), μ.real {M.val} *
∑ w : Fin M.val → I, (∏ k, (p (w k) : ℝ)) *
T (labeledPrefix x M.val (le_of_lt_succ M.isLt) w) := by
rw [← hcap, setIntegral_finset (range (n + 1)) hg.integrableOn]
simp_rw [smul_eq_mul]
rw [← Fin.sum_univ_eq_sum_range]
apply Finset.sum_congr rfl
intro M _
change μ.real {M.val} * (∫ w : Fin n → I, f (M.val, w) ∂ρ) = _
rw [hslice M.val (le_of_lt_succ M.isLt)]
have hlast : (∫ m in Ioi n, g m ∂μ) = μ.real (Ioi n) * zOver := by
rw [setIntegral_congr_fun measurableSet_Ioi (fun m hm => htail m hm)]
simp [Measure.real_def]
rw [hprod]
calc
(∫ m, g m ∂μ) =
(∫ m in Iic n, g m ∂μ) + (∫ m in Ioi n, g m ∂μ) := by
simpa only [Set.compl_Iic] using
(integral_add_compl measurableSet_Iic hg).symm
_ = _ := by rw [hfirst, hlast]
Law 1 core · 5 supporting The unshuffled marked Poisson sample has independent label streams. ★ map_unshuffle_restrict_histogram_eq
Fixed-word laws for labeled Poisson samples
The unshuffled marked Poisson sample has independent label streams. Capping a fixed iid pool preserves the corresponding nonoverflow law, and averaging the cap has an explicit finite count-and-label expansion.
theorem map_unshuffle_restrict_histogram_eq reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.Poisson.FinitePartition
Given an observation probability law, finite label masses, and a prescribed label-count vector, restricting an iid marked tuple of the matching total length to that histogram and unshuffling it gives the sum of the matching label-word weights times independent fixed-length iid observation streams.
Formal statement
hypotheses
X :
Type u_1
I :
Type u_2
P :
p :
I → ℝ≥0
hp :
∑ i, p i = 1
c :
I → ℕ
conclusion
Measure.map (fun z : Fin (∑ i, c i) → X × I => unshuffle (⟨∑ i, c i, z⟩ : FiniteSample (X × I))) ((Measure.pi (fun _ : Fin (∑ i, c i) => P.prod (labelLaw p hp))).restrict {z | ∀ i, wordHistogram (fun k => (z k).2) i = c i})
= (∑ w : Fin (∑ i, c i) → I, if ∀ i, wordHistogram w i = c i then ∏ k, (p (w k) : ℝ≥0∞) else 0) • Measure.pi (fun i : I => Measure.map (fixedSizeEmbed (c i)) (Measure.pi (fun _ : Fin (c i) => P)))
Proof (Lean source)
theorem map_unshuffle_restrict_histogram_eq
(P : Measure X) [IsProbabilityMeasure P]
(p : I → ℝ≥0) (hp : ∑ i, p i = 1) (c : I → ℕ) :
Measure.map
(fun z : Fin (∑ i, c i) → X × I =>
unshuffle (⟨∑ i, c i, z⟩ : FiniteSample (X × I)))
((Measure.pi (fun _ : Fin (∑ i, c i) => P.prod (labelLaw p hp))).restrict
{z | ∀ i, wordHistogram (fun k => (z k).2) i = c i}) =
(∑ w : Fin (∑ i, c i) → I,
if ∀ i, wordHistogram w i = c i then
∏ k, (p (w k) : ℝ≥0∞) else 0) •
Measure.pi (fun i : I =>
Measure.map (fixedSizeEmbed (c i))
(Measure.pi (fun _ : Fin (c i) => P))) := by
-- The histogram event is the disjoint union of its finite label-word
-- fibres. Map each restricted fibre with
-- `map_unshuffle_restrict_labelWord`; all matching words have identical
-- target product laws, so factor that measure out of the finite sum.
classical
let m := ∑ i, c i
let μ : Measure (Fin m → X × I) :=
Measure.pi (fun _ : Fin m => P.prod (labelLaw p hp))
let f : (Fin m → X × I) → (I → FiniteSample X) :=
fun z => unshuffle (⟨m, z⟩ : FiniteSample (X × I))
let good : (Fin m → I) → Prop := fun w => ∀ i, wordHistogram w i = c i
let fibre : (Fin m → I) → Set (Fin m → X × I) :=
fun w => {z | (fun k => (z k).2) = w}
let cell : (Fin m → I) → Set (Fin m → X × I) :=
fun w => if good w then fibre w else ∅
have hmeas (w : Fin m → I) : MeasurableSet (cell w) := by
dsimp [cell]
split
· exact (measurable_pi_lambda _ fun k =>
measurable_snd.comp (measurable_pi_apply k)) (measurableSet_singleton w)
· exact MeasurableSet.empty
have hdisj : ((Finset.univ : Finset (Fin m → I)) : Set (Fin m → I)).Pairwise
(fun w v => Disjoint (cell w) (cell v)) := by
intro w _ v _ hne
apply Set.disjoint_left.mpr
intro z hzw hzv
dsimp [cell] at hzw hzv
split_ifs at hzw hzv <;> try simp_all
exact hne (hzw.symm.trans hzv)
have hunion : (⋃ w ∈ (Finset.univ : Finset (Fin m → I)), cell w) =
{z | good (fun k => (z k).2)} := by
ext z
simp only [Set.mem_iUnion, Finset.mem_univ, Set.mem_ofPred_eq]
constructor
· rintro ⟨w, _, hw⟩
dsimp [cell] at hw
split_ifs at hw with h
· exact (show (fun k => (z k).2) = w from hw) ▸ h
· simpa using hw
· intro hz
refine ⟨fun k => (z k).2, by simp, ?_⟩
simp [cell, hz, fibre]
have hpartition : μ.restrict {z | good (fun k => (z k).2)} =
∑ w : Fin m → I, μ.restrict (cell w) := by
rw [← hunion, Measure.restrict_biUnion_finset hdisj hmeas,
Measure.sum_fintype]
simpa [Finset.sum_coe_sort]
have hfixed (w : Fin m → I) :
Measure.map f (μ.restrict (cell w)) =
(if good w then ∏ k, (p (w k) : ℝ≥0∞) else 0) •
Measure.pi (fun i : I =>
Measure.map (fixedSizeEmbed (c i))
(Measure.pi (fun _ : Fin (c i) => P))) := by
by_cases hw : good w
· simp only [cell, if_pos hw]
rw [map_unshuffle_restrict_labelWord P p hp w]
congr 1
change ∀ i, wordHistogram w i = c i at hw
exact congrArg Measure.pi (funext fun i => by rw [hw i])
· simp [cell, hw]
change Measure.map f (μ.restrict {z | good (fun k => (z k).2)}) = _
rw [hpartition, Measure.map_finset_sum]
· simp_rw [hfixed]
rw [Finset.sum_smul]
· exact measurable_unshuffle.comp (measurable_fixedSizeEmbed m) |>.aemeasurable
5 supporting declarations (lemmas, instances)
-
measurable_unshuffletheorem — Unshuffling finite labeled samples into ordered label streams is measurable.hypothesesX :sharedType u_1I :sharedType u_2conclusionMeasurable (unshuffle (X := X) (I := I))Proof (Lean source)
@[fun_prop] theorem measurable_unshuffle : Measurable (unshuffle (X := X) (I := I)) := by classical apply measurable_pi_lambda intro i t ht rw [MeasurableSpace.measurableSet_iInf] intro n change MeasurableSet {z : Fin n → X × I | unshuffle (⟨n, z⟩ : FiniteSample (X × I)) i ∈ t} have hsection : {z : Fin n → X × I | unshuffle (⟨n, z⟩ : FiniteSample (X × I)) i ∈ t} = ⋃ w : Fin n → I, {z | (fun k => (z k).2) = w} ∩ {z | (⟨wordHistogram w i, gatherWord w (fun k => (z k).1) i⟩ : FiniteSample X) ∈ t} := by ext z simp only [Set.mem_ofPred_eq, Set.mem_iUnion, Set.mem_inter_iff] constructor · intro hz refine ⟨fun k => (z k).2, rfl, ?_⟩ exact hz · rintro ⟨w, hw, hz⟩ subst w exact hz rw [hsection] apply MeasurableSet.iUnion intro w apply MeasurableSet.inter · exact (measurable_pi_lambda _ fun k => measurable_snd.comp (measurable_pi_apply k)) (measurableSet_singleton w) · exact ((measurable_fixedSizeEmbed (wordHistogram w i)).comp ((measurable_pi_apply i).comp ((measurable_gatherWord w).comp (measurable_pi_lambda _ fun k => measurable_fst.comp (measurable_pi_apply k))))) ht -
map_gatherWord_iid_pitheorem — For a fixed finite label word, regrouping iid observations by that word has the product law of iid tuples in its label cells, with each tuple length given by the number of occurrences of its label.hypothesesconclusionMeasure.map (gatherWord w) (Measure.pi (fun _ : Fin m => P))= Measure.pi (fun i : I => Measure.pi (fun _ : Fin (wordHistogram w i) => P))Proof (Lean source)
theorem map_gatherWord_iid_pi {m : ℕ} (w : Fin m → I) (P : Measure X) [IsProbabilityMeasure P] : Measure.map (gatherWord w) (Measure.pi (fun _ : Fin m => P)) = Measure.pi (fun i : I => Measure.pi (fun _ : Fin (wordHistogram w i) => P)) := by let e := (wordUnshuffleEquiv w).symm let reindex := MeasurableEquiv.piCongrLeft (fun _ : Σ i : I, Fin (wordHistogram w i) => X) e have hreindex : Measure.map reindex (Measure.pi fun _ : Fin m => P) = Measure.pi fun _ : Σ i : I, Fin (wordHistogram w i) => P := by exact Measure.pi_map_piCongrLeft e (fun _ : Σ i : I, Fin (wordHistogram w i) => P) have hfun : gatherWord (Y := X) w = piCurry (fun i : I => fun _ : Fin (wordHistogram w i) => X) ∘ reindex := by funext z i k simp only [Function.comp_apply] rw [MeasurableEquiv.piCurry_apply] change z (wordUnshuffleEquiv w ⟨i, k⟩) = (Equiv.piCongrLeft (fun _ : Σ i : I, Fin (wordHistogram w i) => X) e) z ⟨i, k⟩ rw [Equiv.piCongrLeft_apply] simp [e] rw [hfun, ← Measure.map_map (piCurry _).measurable reindex.measurable, hreindex] simpa only [Measure.infinitePi_eq_pi] using Measure.infinitePi_map_piCurry (fun i : I => fun _ : Fin (wordHistogram w i) => P) -
map_unshuffle_restrict_labelWordtheorem — Given an observation probability law, finite label masses, and a fixed label word, the law of iid marked observations restricted to that word, then unshuffled, is its word probability times the product of the corresponding fixed-length iid observation streams.hypothesesconclusionMeasure.map (fun z : Fin m → X × I => unshuffle (⟨m, z⟩ : FiniteSample (X × I))) ((Measure.pi (fun _ : Fin m => P.prod (labelLaw p hp))).restrict {z | (fun k => (z k).2) = w})= (∏ k, (p (w k) : ℝ≥0∞)) • Measure.pi (fun i : I => Measure.map (fixedSizeEmbed (wordHistogram w i)) (Measure.pi (fun _ : Fin (wordHistogram w i) => P)))Proof (Lean source)
theorem map_unshuffle_restrict_labelWord (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (hp : ∑ i, p i = 1) {m : ℕ} (w : Fin m → I) : Measure.map (fun z : Fin m → X × I => unshuffle (⟨m, z⟩ : FiniteSample (X × I))) ((Measure.pi (fun _ : Fin m => P.prod (labelLaw p hp))).restrict {z | (fun k => (z k).2) = w}) = (∏ k, (p (w k) : ℝ≥0∞)) • Measure.pi (fun i : I => Measure.map (fixedSizeEmbed (wordHistogram w i)) (Measure.pi (fun _ : Fin (wordHistogram w i) => P))) := by classical letI := labelLaw_isProbabilityMeasure p hp let e := MeasurableEquiv.arrowProdEquivProdArrow X I (Fin m) let μ : Measure (Fin m → X) := Measure.pi (fun _ => P) let ν : Measure (Fin m → I) := Measure.pi (fun _ => labelLaw p hp) have hmass (i : I) : labelLaw p hp {i} = (p i : ℝ≥0∞) := by unfold labelLaw rw [PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton i), PMF.ofFintype_apply] have hν : ν {w} = ∏ k, (p (w k) : ℝ≥0∞) := by simp only [ν, Measure.pi_singleton, hmass] have hpre : e ⁻¹' (univ ×ˢ {w}) = {z : Fin m → X × I | (fun k => (z k).2) = w} := by ext z simp [e, MeasurableEquiv.arrowProdEquivProdArrow, Equiv.arrowProdEquivProdArrow] have hsource : Measure.map e ((Measure.pi (fun _ : Fin m => P.prod (labelLaw p hp))).restrict {z | (fun k => (z k).2) = w}) = (∏ k, (p (w k) : ℝ≥0∞)) • Measure.map (fun x : Fin m → X => (x, w)) μ := by rw [← hpre, ← Measure.restrict_map e.measurable (MeasurableSet.univ.prod (measurableSet_singleton w)), (measurePreserving_arrowProdEquivProdArrow X I (Fin m) (fun _ => P) (fun _ => labelLaw p hp)).map_eq] change (μ.prod ν).restrict (univ ×ˢ {w}) = _ rw [← Measure.prod_restrict, Measure.restrict_univ, Measure.restrict_singleton, hν, Measure.prod_smul_right, Measure.prod_dirac] have htarget : Measure.map (fun x : Fin m → X => fun i => fixedSizeEmbed (wordHistogram w i) (gatherWord w x i)) μ = Measure.pi (fun i : I => Measure.map (fixedSizeEmbed (wordHistogram w i)) (Measure.pi (fun _ : Fin (wordHistogram w i) => P))) := by change Measure.map ((fun y i => fixedSizeEmbed (wordHistogram w i) (y i)) ∘ gatherWord w) μ = _ calc _ = Measure.map (fun y => fun i => fixedSizeEmbed (wordHistogram w i) (y i)) (Measure.map (gatherWord w) μ) := (Measure.map_map (measurable_pi_lambda _ fun i => (measurable_fixedSizeEmbed _).comp (measurable_pi_apply i)) (measurable_gatherWord w)).symm _ = _ := by rw [map_gatherWord_iid_pi w P] exact Measure.pi_map_pi (fun i => (measurable_fixedSizeEmbed _).aemeasurable) calc _ = Measure.map (fun q : (Fin m → X) × (Fin m → I) => unshuffle (⟨m, fun k => (q.1 k, q.2 k)⟩ : FiniteSample (X × I))) (Measure.map e ((Measure.pi (fun _ : Fin m => P.prod (labelLaw p hp))).restrict {z | (fun k => (z k).2) = w})) := by rw [Measure.map_map] · rfl · exact measurable_unshuffle.comp (measurable_fixedSizeEmbed m |>.comp (measurable_pi_lambda _ fun k => ((measurable_pi_apply k).comp measurable_fst).prodMk ((measurable_pi_apply k).comp measurable_snd))) · exact e.measurable _ = _ := by rw [hsource, Measure.map_smul] congr 1 calc Measure.map (fun q : (Fin m → X) × (Fin m → I) => unshuffle (⟨m, fun k => (q.1 k, q.2 k)⟩ : FiniteSample (X × I))) (Measure.map (fun x : Fin m → X => (x, w)) μ) = Measure.map (fun x : Fin m → X => unshuffle (⟨m, fun k => (x k, w k)⟩ : FiniteSample (X × I))) μ := by rw [Measure.map_map] · rfl · exact measurable_unshuffle.comp (measurable_fixedSizeEmbed m |>.comp (measurable_pi_lambda _ fun k => ((measurable_pi_apply k).comp measurable_fst).prodMk ((measurable_pi_apply k).comp measurable_snd))) · fun_prop _ = _ := by convert htarget using 1 congr 1 -
map_joint_prefix_pitheorem — For an iid observation law, label masses summing to one, a pool size, and a shorter prefix length, pairing the observation and label prefixes gives iid marked observations.hypothesesX :sharedType u_1I :sharedType u_2P :p :I → ℝ≥0hp :∑ i, p i = 1n m :ℕh :m ≤ nProof (Lean source)
theorem map_joint_prefix_pi (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (hp : ∑ i, p i = 1) {n m : ℕ} (h : m ≤ n) : Measure.map (fun z : (Fin n → X) × (Fin n → I) => fun k : Fin m => (z.1 ⟨k.val, lt_of_lt_of_le k.isLt h⟩, z.2 ⟨k.val, lt_of_lt_of_le k.isLt h⟩)) ((fixedPoolLaw P n).prod (Measure.pi (fun _ : Fin n => labelLaw p hp))) = Measure.pi (fun _ : Fin m => P.prod (labelLaw p hp)) := by classical letI := labelLaw_isProbabilityMeasure p hp let Q := labelLaw p hp let μ := P.prod Q let pair : (Fin n → X) × (Fin n → I) → (Fin n → X × I) := fun z k => (z.1 k, z.2 k) let pref : (Fin n → X × I) → (Fin m → X × I) := fun z k => z ⟨k.val, lt_of_lt_of_le k.isLt h⟩ have hpair : Measure.map pair ((fixedPoolLaw P n).prod (Measure.pi (fun _ : Fin n => Q))) = Measure.pi (fun _ : Fin n => μ) := by have he : pair = (MeasurableEquiv.arrowProdEquivProdArrow X I (Fin n)).symm := by funext z k rfl rw [he] exact (measurePreserving_arrowProdEquivProdArrow X I (Fin n) (fun _ => P) (fun _ => Q)).symm.map_eq have hprefix : Measure.map pref (Measure.pi (fun _ : Fin n => μ)) = Measure.pi (fun _ : Fin m => μ) := by symm refine Measure.pi_eq (fun s hs => ?_) rw [Measure.map_apply (by fun_prop) (.univ_pi hs)] have hpre : pref ⁻¹' (Set.univ.pi s) = Set.univ.pi (fun j : Fin n => if hj : j.val < m then s ⟨j.val, hj⟩ else univ) := by ext z simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, true_implies] constructor · intro hz j split · exact hz ⟨j.val, ‹j.val < m›⟩ · trivial · intro hz k simpa [pref] using hz ⟨k.val, lt_of_lt_of_le k.isLt h⟩ rw [hpre, Measure.pi_pi] let t : Finset (Fin n) := Finset.univ.filter fun j => j.val < m have ht (j : t) : j.val.val < m := by simpa only [t, mem_filter, Finset.mem_univ, true_and] using j.property let e : Fin m ≃ t := { toFun := fun k => ⟨⟨k.val, lt_of_lt_of_le k.isLt h⟩, by simp [t, k.isLt]⟩ invFun := fun j => ⟨j.val.val, ht j⟩ left_inv := fun k => by rfl right_inv := fun j => by ext; rfl } calc (∏ j : Fin n, μ (if hj : j.val < m then s ⟨j.val, hj⟩ else univ)) = ∏ j : Fin n, if hj : j.val < m then μ (s ⟨j.val, hj⟩) else 1 := by apply Fintype.prod_congr intro j split <;> simp _ = ∏ j : t, μ (s ⟨j.val.val, ht j⟩) := by rw [Finset.prod_dite] simp only [Finset.prod_const_one, mul_one] apply Fintype.prod_congr intro j congr 2 _ = ∏ k : Fin m, μ (s k) := by symm apply Fintype.prod_equiv e intro k rfl calc Measure.map (fun z : (Fin n → X) × (Fin n → I) => fun k : Fin m => (z.1 ⟨k.val, lt_of_lt_of_le k.isLt h⟩, z.2 ⟨k.val, lt_of_lt_of_le k.isLt h⟩)) ((fixedPoolLaw P n).prod (Measure.pi (fun _ : Fin n => Q))) = Measure.map pref (Measure.map pair ((fixedPoolLaw P n).prod (Measure.pi (fun _ : Fin n => Q)))) := by rw [Measure.map_map (by fun_prop) (by fun_prop)] rfl _ = Measure.pi (fun _ : Fin m => μ) := by rw [hpair, hprefix] -
unshuffle_total_counttheorem — The total length of the ordered label streams equals the length of the original labeled sample.hypothesesconclusion∑ i, ((unshuffle s) i).count = s.countProof (Lean source)
theorem unshuffle_total_count (s : FiniteSample (X × I)) : ∑ i, ((unshuffle s) i).count = s.count := by classical let w : Fin s.count → I := fun k => (s.2 k).2 have h := Finset.card_eq_sum_card_fiberwise (s := (Finset.univ : Finset (Fin s.count))) (t := (Finset.univ : Finset I)) (f := w) (fun k _ => Finset.mem_univ (w k)) change ∑ i, wordHistogram w i = s.count simpa [wordHistogram, w] using h.symm
Risk 1 core · 7 supporting Conditional averaging over a Poisson count and finite labels contracts squared loss. ★ fixedRisk_le_independentRisk_add_tail
Squared-risk transfer for a capped labeled Poisson experiment
Conditional averaging over a Poisson count and finite labels contracts squared loss. The cap contributes at most interval diameter squared times the scalar Poisson upper-tail probability.
theorem fixedRisk_le_independentRisk_add_tail reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.Poisson.FinitePartition
For an iid observation law, label masses summing to one, a Poisson mean, a pool size, a measurable stream statistic confined to an interval, a target in that interval, and an overflow value in it, fixed-sample squared risk is at most independent Poisson-stream risk plus squared interval diameter times the Poisson upper tail.
Formal statement
hypotheses
X :
Type u_1
I :
Type u_2
P :
p :
I → ℝ≥0
hp :
∑ i, p i = 1
lambda :
ℝ≥0
n :
ℕ
T :
(I → FiniteSample X) → ℝ
hT :
a b theta zOver :
ℝ
hTmem :
∀ s, T s ∈ Icc a b
htheta :
theta ∈ Icc a b
hzOver :
zOver ∈ Icc a b
conclusion
≤ sqRisk (Measure.pi (fun i : I => finitePoissonSampleLaw P (lambda * p i))) T theta
Proof (Lean source)
theorem fixedRisk_le_independentRisk_add_tail
(P : Measure X) [IsProbabilityMeasure P]
(p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0) (n : ℕ)
{T : (I → FiniteSample X) → ℝ} (hT : Measurable T)
{a b theta zOver : ℝ}
(hTmem : ∀ s, T s ∈ Icc a b)
(htheta : theta ∈ Icc a b) (hzOver : zOver ∈ Icc a b) :
sqRisk (fixedPoolLaw P n)
(fun x => fixedStatistic p hp lambda x T zOver) theta ≤
sqRisk (Measure.pi (fun i : I => finitePoissonSampleLaw P (lambda * p i)))
T theta +
(b - a) ^ 2 * (poissonMeasure lambda).real (Ioi n) := by
exact (fixedRisk_le_cappedRisk P p hp lambda n hT hTmem hzOver theta).trans
(cappedRisk_le_independentRisk_add_tail P p hp lambda n hT hTmem htheta hzOver)
7 supporting declarations (lemmas, instances)
-
sqRisk_capped_splittheorem — Given an iid observation law, finite label masses, a Poisson mean, a pool size, a measurable interval-bounded stream statistic, an interval-bounded overflow value, and a target, the capped squared risk is the sum of its nonoverflow and overflow restrictions.hypothesesX :sharedType u_1I :sharedType u_2P :p :I → ℝ≥0hp :∑ i, p i = 1lambda :ℝ≥0n :ℕT :(I → FiniteSample X) → ℝhT :a b zOver :ℝhTmem :∀ s, T s ∈ Icc a bhzOver :zOver ∈ Icc a btheta :ℝconclusionsqRisk ((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)) (fun z => cappedStatistic z.1 T zOver z.2) theta= sqRisk (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | z.2.1 ≤ n}) (fun z => cappedStatistic z.1 T zOver z.2) theta+ sqRisk (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | n < z.2.1}) (fun z => cappedStatistic z.1 T zOver z.2) thetaProof (Lean source)
theorem sqRisk_capped_split (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0) (n : ℕ) {T : (I → FiniteSample X) → ℝ} (hT : Measurable T) {a b zOver : ℝ} (hTmem : ∀ s, T s ∈ Icc a b) (hzOver : zOver ∈ Icc a b) (theta : ℝ) : sqRisk ((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)) (fun z => cappedStatistic z.1 T zOver z.2) theta = sqRisk (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | z.2.1 ≤ n}) (fun z => cappedStatistic z.1 T zOver z.2) theta + sqRisk (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | n < z.2.1}) (fun z => cappedStatistic z.1 T zOver z.2) theta := by letI : IsProbabilityMeasure (auxiliaryLaw p hp lambda n) := by unfold auxiliaryLaw letI := labelLaw_isProbabilityMeasure p hp infer_instance letI : IsProbabilityMeasure (fixedPoolLaw P n) := by unfold fixedPoolLaw infer_instance let μ : Measure ((Fin n → X) × (ℕ × (Fin n → I))) := (fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n) letI : IsProbabilityMeasure μ := by dsimp [μ] infer_instance have hMeas : Measurable (fun z : (Fin n → X) × (ℕ × (Fin n → I)) => cappedStatistic z.1 T zOver z.2) := by let g : ℕ × ((Fin n → X) × (Fin n → I)) → ℝ := fun z => cappedStatistic z.2.1 T zOver (z.1, z.2.2) have hg : Measurable g := by apply measurable_from_prod_countable_right intro m by_cases hm : m ≤ n · have hprefix : Measurable (fun z : (Fin n → X) × (Fin n → I) => labeledPrefix z.1 m hm (fun k => z.2 ⟨k.val, lt_of_lt_of_le k.isLt hm⟩)) := by exact measurable_unshuffle.comp (measurable_fixedSizeEmbed m |>.comp (measurable_pi_lambda _ fun k => ((measurable_pi_apply _).comp measurable_fst).prodMk ((measurable_pi_apply _).comp measurable_snd))) have heq : (fun y : (Fin n → X) × (Fin n → I) => g (m, y)) = (fun y => T (labeledPrefix y.1 m hm (fun k => y.2 ⟨k.val, lt_of_lt_of_le k.isLt hm⟩))) := by funext y simp [g, cappedStatistic, hm] rw [heq] exact hT.comp hprefix · simpa [g, cappedStatistic, hm] using (measurable_const : Measurable (fun _ : (Fin n → X) × (Fin n → I) => zOver)) exact hg.comp ((measurable_fst.comp measurable_snd).prodMk (measurable_fst.prodMk (measurable_snd.comp measurable_snd))) have hBound : UniformlyBounded (fun z : (Fin n → X) × (ℕ × (Fin n → I)) => cappedStatistic z.1 T zOver z.2) := by refine ⟨max |a| |b|, (abs_nonneg a).trans (le_max_left _ _), ?_⟩ intro z by_cases hm : z.2.1 ≤ n · simp only [cappedStatistic, dif_pos hm] exact abs_le_max_abs_abs (hTmem _).1 (hTmem _).2 · simp only [cappedStatistic, dif_neg hm] exact abs_le_max_abs_abs hzOver.1 hzOver.2 obtain ⟨M, hM, hTb⟩ := hBound let s : Set ((Fin n → X) × (ℕ × (Fin n → I))) := {z | z.2.1 ≤ n} have hs : MeasurableSet s := (measurable_fst.comp measurable_snd) measurableSet_Iic have hlossInt : Integrable (fun z => (cappedStatistic z.1 T zOver z.2 - theta) ^ 2) μ := by refine (integrable_const ((M + |theta|) ^ 2)).mono' ((hMeas.sub measurable_const).pow_const 2).aestronglyMeasurable ?_ filter_upwards [] with z rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _), sq_le_sq, abs_of_nonneg (add_nonneg hM (abs_nonneg theta))] exact (abs_sub _ _).trans (add_le_add (hTb z) le_rfl) have hsInt : Integrable (fun z => (cappedStatistic z.1 T zOver z.2 - theta) ^ 2) (μ.restrict s) := hlossInt.restrict have hscInt : Integrable (fun z => (cappedStatistic z.1 T zOver z.2 - theta) ^ 2) (μ.restrict sᶜ) := hlossInt.restrict have hscompl : sᶜ = {z | n < z.2.1} := by ext z simp [s, not_le] unfold sqRisk rw [← hscompl] change (∫ z, (cappedStatistic z.1 T zOver z.2 - theta) ^ 2 ∂μ) = (∫ z, (cappedStatistic z.1 T zOver z.2 - theta) ^ 2 ∂μ.restrict s) + (∫ z, (cappedStatistic z.1 T zOver z.2 - theta) ^ 2 ∂μ.restrict sᶜ) conv_lhs => rw [← Measure.restrict_add_restrict_compl (μ := μ) hs, integral_add_measure hsInt hscInt] -
fixedRisk_le_cappedRisktheorem — For an iid observation law, label masses summing to one, a Poisson mean, a pool size, a measurable stream statistic confined to an interval, and an overflow value in that interval, conditional averaging does not increase squared risk.hypothesesX :sharedType u_1I :sharedType u_2P :p :I → ℝ≥0hp :∑ i, p i = 1lambda :ℝ≥0n :ℕT :(I → FiniteSample X) → ℝhT :a b zOver :ℝhTmem :∀ s, T s ∈ Icc a bhzOver :zOver ∈ Icc a btheta :ℝconclusion≤ sqRisk ((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)) (fun z => cappedStatistic z.1 T zOver z.2) thetaProof (Lean source)
theorem fixedRisk_le_cappedRisk (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0) (n : ℕ) {T : (I → FiniteSample X) → ℝ} (hT : Measurable T) {a b zOver : ℝ} (hTmem : ∀ s, T s ∈ Icc a b) (hzOver : zOver ∈ Icc a b) (theta : ℝ) : sqRisk (fixedPoolLaw P n) (fun x => fixedStatistic p hp lambda x T zOver) theta ≤ sqRisk ((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)) (fun z => cappedStatistic z.1 T zOver z.2) theta := by letI : IsProbabilityMeasure (auxiliaryLaw p hp lambda n) := by unfold auxiliaryLaw letI := labelLaw_isProbabilityMeasure p hp infer_instance letI : IsProbabilityMeasure (fixedPoolLaw P n) := by unfold fixedPoolLaw infer_instance let K : Kernel (Fin n → X) ((Fin n → X) × (ℕ × (Fin n → I))) := mechanismKernel (auxiliaryLaw p hp lambda n) id have hK : IsMarkovKernel K := by dsimp [K] exact instIsMarkovKernelMechanismKernel _ measurable_id letI := hK have hMeas : Measurable (fun z : (Fin n → X) × (ℕ × (Fin n → I)) => cappedStatistic z.1 T zOver z.2) := by let g : ℕ × ((Fin n → X) × (Fin n → I)) → ℝ := fun z => cappedStatistic z.2.1 T zOver (z.1, z.2.2) have hg : Measurable g := by apply measurable_from_prod_countable_right intro m by_cases hm : m ≤ n · have hprefix : Measurable (fun z : (Fin n → X) × (Fin n → I) => labeledPrefix z.1 m hm (fun k => z.2 ⟨k.val, lt_of_lt_of_le k.isLt hm⟩)) := by exact measurable_unshuffle.comp (measurable_fixedSizeEmbed m |>.comp (measurable_pi_lambda _ fun k => ((measurable_pi_apply _).comp measurable_fst).prodMk ((measurable_pi_apply _).comp measurable_snd))) have heq : (fun y : (Fin n → X) × (Fin n → I) => g (m, y)) = (fun y => T (labeledPrefix y.1 m hm (fun k => y.2 ⟨k.val, lt_of_lt_of_le k.isLt hm⟩))) := by funext y simp [g, cappedStatistic, hm] rw [heq] exact hT.comp hprefix · simpa [g, cappedStatistic, hm] using (measurable_const : Measurable (fun _ : (Fin n → X) × (Fin n → I) => zOver)) exact hg.comp ((measurable_fst.comp measurable_snd).prodMk (measurable_fst.prodMk (measurable_snd.comp measurable_snd))) have hBound : UniformlyBounded (fun z : (Fin n → X) × (ℕ × (Fin n → I)) => cappedStatistic z.1 T zOver z.2) := by refine ⟨max |a| |b|, (abs_nonneg a).trans (le_max_left _ _), ?_⟩ intro z by_cases hm : z.2.1 ≤ n · simp only [cappedStatistic, dif_pos hm] exact abs_le_max_abs_abs (hTmem _).1 (hTmem _).2 · simp only [cappedStatistic, dif_neg hm] exact abs_le_max_abs_abs hzOver.1 hzOver.2 have hmean : kernelMean K (fun z : (Fin n → X) × (ℕ × (Fin n → I)) => cappedStatistic z.1 T zOver z.2) = (fun x => fixedStatistic p hp lambda x T zOver) := by funext x unfold kernelMean K fixedStatistic rw [mechanismKernel_apply _ measurable_id x] exact integral_map measurable_prodMk_left.aemeasurable hMeas.aestronglyMeasurable have hcomp : K ∘ₘ fixedPoolLaw P n = (fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n) := by have hgraph := map_graph_prod_eq_compProd (fixedPoolLaw P n) (auxiliaryLaw p hp lambda n) (show Measurable (fun z : (Fin n → X) × (ℕ × (Fin n → I)) => z) from measurable_id) have hsnd := congrArg (Measure.map snd) hgraph rw [Measure.map_map measurable_snd (show Measurable (fun z : (Fin n → X) × (ℕ × (Fin n → I)) => (z.1, z)) from measurable_fst.prodMk measurable_id)] at hsnd change _ = ((fixedPoolLaw P n) ⊗ₘ K).snd at hsnd rw [Measure.snd_compProd] at hsnd simpa [Function.comp_def, K] using hsnd.symm rw [← hmean, ← hcomp] exact sqRisk_kernelMean_le_comp (fixedPoolLaw P n) K hMeas hBound theta -
sqRisk_capped_restrict_nonoverflow_eqtheorem — For an iid observation law, label masses summing to one, a Poisson mean, a pool size, a measurable stream statistic, an overflow value, and a target, the capped squared risk on nonoverflow equals the uncapped stream risk restricted to total count at most the pool size.hypothesesX :sharedType u_1I :sharedType u_2P :p :I → ℝ≥0hp :∑ i, p i = 1lambda :ℝ≥0n :ℕT :(I → FiniteSample X) → ℝhT :zOver theta :ℝconclusionsqRisk (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | z.2.1 ≤ n}) (fun z => cappedStatistic z.1 T zOver z.2) thetaProof (Lean source)
theorem sqRisk_capped_restrict_nonoverflow_eq (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0) (n : ℕ) {T : (I → FiniteSample X) → ℝ} (hT : Measurable T) (zOver theta : ℝ) : sqRisk (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | z.2.1 ≤ n}) (fun z => cappedStatistic z.1 T zOver z.2) theta = sqRisk ((labeledStreamLaw P p hp lambda).restrict {s | ∑ i, (s i).count ≤ n}) T theta := by let f : (Fin n → X) × (ℕ × (Fin n → I)) → I → FiniteSample X := fun z => if h : z.2.1 ≤ n then labeledPrefix z.1 z.2.1 h (fun k => z.2.2 ⟨k.val, lt_of_lt_of_le k.isLt h⟩) else fun _ => (⟨0, Fin.elim0⟩ : FiniteSample X) have hf : Measurable f := by let g : ℕ × ((Fin n → X) × (Fin n → I)) → I → FiniteSample X := fun z => if h : z.1 ≤ n then labeledPrefix z.2.1 z.1 h (fun k => z.2.2 ⟨k.val, lt_of_lt_of_le k.isLt h⟩) else fun _ => (⟨0, Fin.elim0⟩ : FiniteSample X) have hg : Measurable g := by apply measurable_from_prod_countable_right intro m by_cases hm : m ≤ n · have hprefix : Measurable (fun z : (Fin n → X) × (Fin n → I) => labeledPrefix z.1 m hm (fun k => z.2 ⟨k.val, lt_of_lt_of_le k.isLt hm⟩)) := by exact measurable_unshuffle.comp (measurable_fixedSizeEmbed m |>.comp (measurable_pi_lambda _ fun k => ((measurable_pi_apply _).comp measurable_fst).prodMk ((measurable_pi_apply _).comp measurable_snd))) simpa only [g, hm, dite_true] using hprefix · simpa only [g, hm, dite_false] using (measurable_const : Measurable (fun _ : (Fin n → X) × (Fin n → I) => (fun _ => (⟨0, Fin.elim0⟩ : FiniteSample X)))) exact hg.comp (by fun_prop : Measurable (fun z : (Fin n → X) × (ℕ × (Fin n → I)) => (z.2.1, (z.1, z.2.2)))) unfold sqRisk rw [← map_capped_restrict_nonoverflow P p hp lambda n] rw [integral_map (μ := ((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | z.2.1 ≤ n}) (φ := f) (f := fun s => (T s - theta) ^ 2) hf.aemeasurable ((hT.sub measurable_const).pow_const 2).aestronglyMeasurable] apply integral_congr_ae filter_upwards [ae_restrict_mem ((measurable_fst.comp measurable_snd) measurableSet_Iic)] with z hz simp [f, cappedStatistic, hz] -
sqRisk_capped_restrict_overflow_eqtheorem — For an iid observation law, label masses summing to one, a Poisson mean, a pool size, a stream statistic, an overflow value, and a target, the capped squared risk on overflow equals the constant overflow loss times the Poisson upper tail.hypothesesX :sharedType u_1I :sharedType u_2P :p :I → ℝ≥0hp :∑ i, p i = 1lambda :ℝ≥0n :ℕT :(I → FiniteSample X) → ℝzOver theta :ℝconclusionsqRisk (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | n < z.2.1}) (fun z => cappedStatistic z.1 T zOver z.2) thetaProof (Lean source)
theorem sqRisk_capped_restrict_overflow_eq (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0) (n : ℕ) (T : (I → FiniteSample X) → ℝ) (zOver theta : ℝ) : sqRisk (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | n < z.2.1}) (fun z => cappedStatistic z.1 T zOver z.2) theta = (zOver - theta) ^ 2 * (poissonMeasure lambda).real (Ioi n) := by -- The integrand is constant on overflow. The event depends only on the -- Poisson count, so its product-law mass is the scalar upper tail. letI := labelLaw_isProbabilityMeasure p hp haveI : IsProbabilityMeasure (fixedPoolLaw P n) := by unfold fixedPoolLaw infer_instance unfold sqRisk have hae : ∀ᵐ z ∂ ((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | n < z.2.1}, (cappedStatistic z.1 T zOver z.2 - theta) ^ 2 = (zOver - theta) ^ 2 := by have hs : MeasurableSet {z : (Fin n → X) × (ℕ × (Fin n → I)) | n < z.2.1} := (measurable_fst.comp measurable_snd) measurableSet_Ioi filter_upwards [ae_restrict_mem hs] with z hz simp [cappedStatistic, not_le_of_gt hz] rw [integral_congr_ae hae, integral_const] simp only [smul_eq_mul, measureReal_def] have hset : {z : (Fin n → X) × (ℕ × (Fin n → I)) | n < z.2.1} = (Set.univ : Set (Fin n → X)) ×ˢ (Ioi n ×ˢ (Set.univ : Set (Fin n → I))) := by ext z simp have haux : (auxiliaryLaw p hp lambda n) (Ioi n ×ˢ (Set.univ : Set (Fin n → I))) = (poissonMeasure lambda) (Ioi n) := by unfold auxiliaryLaw rw [Measure.prod_prod] simp rw [Measure.restrict_apply_univ, hset, Measure.prod_prod] simp [haux, mul_comm] -
sqRisk_labeledStreamLaw_restrict_nonoverflow_letheorem — For an iid observation law, label masses summing to one, a Poisson mean, a pool size, a measurable uniformly bounded stream statistic, and a target, restricting the uncapped stream law to total counts at most the pool size cannot increase squared risk.hypothesesX :sharedType u_1I :sharedType u_2P :p :I → ℝ≥0hp :∑ i, p i = 1lambda :ℝ≥0n :ℕT :(I → FiniteSample X) → ℝhT :hTb :theta :ℝconclusion≤ sqRisk (labeledStreamLaw P p hp lambda) T thetaProof (Lean source)
theorem sqRisk_labeledStreamLaw_restrict_nonoverflow_le (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0) (n : ℕ) {T : (I → FiniteSample X) → ℝ} (hT : Measurable T) (hTb : UniformlyBounded T) (theta : ℝ) : sqRisk ((labeledStreamLaw P p hp lambda).restrict {s | ∑ i, (s i).count ≤ n}) T theta ≤ sqRisk (labeledStreamLaw P p hp lambda) T theta := by -- Show bounded-loss integrability; split the measure into the measurable -- nonoverflow event and its complement, then discard nonnegative loss. obtain ⟨M, hM, hTb⟩ := hTb let μ : Measure (I → FiniteSample X) := labeledStreamLaw P p hp lambda letI := labelLaw_isProbabilityMeasure p hp haveI : IsProbabilityMeasure μ := by unfold μ labeledStreamLaw exact Measure.isProbabilityMeasure_map measurable_unshuffle.aemeasurable let s : Set (I → FiniteSample X) := {z | ∑ i, (z i).count ≤ n} have hs : MeasurableSet s := by have hc : Measurable (fun z : I → FiniteSample X => ∑ i, (z i).count) := by fun_prop exact hc measurableSet_Iic have hlossInt : Integrable (fun z => (T z - theta) ^ 2) μ := by refine (integrable_const ((M + |theta|) ^ 2)).mono' ((hT.sub measurable_const).pow_const 2).aestronglyMeasurable ?_ filter_upwards [] with z rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _), sq_le_sq, abs_of_nonneg (add_nonneg hM (abs_nonneg theta))] exact (abs_sub _ _).trans (add_le_add (hTb z) le_rfl) have hsInt : Integrable (fun z => (T z - theta) ^ 2) (μ.restrict s) := hlossInt.restrict have hscInt : Integrable (fun z => (T z - theta) ^ 2) (μ.restrict sᶜ) := hlossInt.restrict unfold sqRisk change (∫ z, (T z - theta) ^ 2 ∂μ.restrict s) ≤ ∫ z, (T z - theta) ^ 2 ∂μ conv_rhs => rw [← Measure.restrict_add_restrict_compl (μ := μ) hs, integral_add_measure hsInt hscInt] exact le_add_of_nonneg_right (integral_nonneg fun z => sq_nonneg (T z - theta)) -
sqRisk_capped_restrict_nonoverflow_le_independenttheorem — For an iid observation law, label masses summing to one, a Poisson mean, a pool size, a measurable stream statistic, a uniform bound, an overflow value, and a target, the nonoverflow capped risk is at most independent-stream risk.hypothesesX :sharedType u_1I :sharedType u_2P :p :I → ℝ≥0hp :∑ i, p i = 1lambda :ℝ≥0n :ℕT :(I → FiniteSample X) → ℝhT :hTb :zOver theta :ℝconclusionsqRisk (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | z.2.1 ≤ n}) (fun z => cappedStatistic z.1 T zOver z.2) theta≤ sqRisk (Measure.pi (fun i : I => finitePoissonSampleLaw P (lambda * p i))) T thetaProof (Lean source)
theorem sqRisk_capped_restrict_nonoverflow_le_independent (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0) (n : ℕ) {T : (I → FiniteSample X) → ℝ} (hT : Measurable T) (hTb : UniformlyBounded T) (zOver theta : ℝ) : sqRisk (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | z.2.1 ≤ n}) (fun z => cappedStatistic z.1 T zOver z.2) theta ≤ sqRisk (Measure.pi (fun i : I => finitePoissonSampleLaw P (lambda * p i))) T theta := by rw [sqRisk_capped_restrict_nonoverflow_eq P p hp lambda n hT zOver theta, ← labeledStreamLaw_eq_independent P p hp lambda] exact sqRisk_labeledStreamLaw_restrict_nonoverflow_le P p hp lambda n hT hTb theta -
cappedRisk_le_independentRisk_add_tailtheorem — For an iid observation law, label masses summing to one, a Poisson mean, a pool size, a measurable stream statistic confined to an interval, a target in that interval, and an overflow value in it, capped risk is bounded by independent-stream risk plus squared interval diameter times the Poisson upper tail.hypothesesX :sharedType u_1I :sharedType u_2P :p :I → ℝ≥0hp :∑ i, p i = 1lambda :ℝ≥0n :ℕT :(I → FiniteSample X) → ℝhT :a b theta zOver :ℝhTmem :∀ s, T s ∈ Icc a bhtheta :theta ∈ Icc a bhzOver :zOver ∈ Icc a bconclusionsqRisk ((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)) (fun z => cappedStatistic z.1 T zOver z.2) theta≤ sqRisk (Measure.pi (fun i : I => finitePoissonSampleLaw P (lambda * p i))) T thetaProof (Lean source)
theorem cappedRisk_le_independentRisk_add_tail (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0) (n : ℕ) {T : (I → FiniteSample X) → ℝ} (hT : Measurable T) {a b theta zOver : ℝ} (hTmem : ∀ s, T s ∈ Icc a b) (htheta : theta ∈ Icc a b) (hzOver : zOver ∈ Icc a b) : sqRisk ((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)) (fun z => cappedStatistic z.1 T zOver z.2) theta ≤ sqRisk (Measure.pi (fun i : I => finitePoissonSampleLaw P (lambda * p i))) T theta + (b - a) ^ 2 * (poissonMeasure lambda).real (Ioi n) := by -- Split at count ≤ n. On the good piece, use the capped law theorem and -- independent stream law; discard complementary nonnegative risk. On -- overflow, use the constant loss `(zOver - theta)^2 ≤ (b-a)^2` and the -- Poisson count marginal of the auxiliary law. have hTb : UniformlyBounded T := by refine ⟨max |a| |b|, (abs_nonneg a).trans (le_max_left _ _), ?_⟩ intro s exact abs_le_max_abs_abs (hTmem s).1 (hTmem s).2 have hsq : (zOver - theta) ^ 2 ≤ (b - a) ^ 2 := by have hleft : 0 ≤ (b - a) - (zOver - theta) := by linarith [hzOver.2, htheta.1] have hright : 0 ≤ (b - a) + (zOver - theta) := by linarith [hzOver.1, htheta.2] nlinarith [mul_nonneg hleft hright] calc sqRisk ((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)) (fun z => cappedStatistic z.1 T zOver z.2) theta = sqRisk (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | z.2.1 ≤ n}) (fun z => cappedStatistic z.1 T zOver z.2) theta + sqRisk (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | n < z.2.1}) (fun z => cappedStatistic z.1 T zOver z.2) theta := sqRisk_capped_split P p hp lambda n hT hTmem hzOver theta _ ≤ sqRisk (Measure.pi (fun i : I => finitePoissonSampleLaw P (lambda * p i))) T theta + sqRisk (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | n < z.2.1}) (fun z => cappedStatistic z.1 T zOver z.2) theta := by exact add_le_add_left (sqRisk_capped_restrict_nonoverflow_le_independent P p hp lambda n hT hTb zOver theta) _ _ = sqRisk (Measure.pi (fun i : I => finitePoissonSampleLaw P (lambda * p i))) T theta + (zOver - theta) ^ 2 * (poissonMeasure lambda).real (Ioi n) := by rw [sqRisk_capped_restrict_overflow_eq P p hp lambda n T zOver theta] _ ≤ _ := by exact add_le_add_right (mul_le_mul_of_nonneg_right hsq measureReal_nonneg) _
StreamLaw 1 core · 6 supporting This module identifies the ordered label streams of a marked Poisson sample with independent finite Poisson samples and transports that law to the nonoverflow part of a single capped iid pool. ★ labeledStreamLaw_eq_independent
Ordered labeled Poisson stream laws
This module identifies the ordered label streams of a marked Poisson sample with independent finite Poisson samples and transports that law to the nonoverflow part of a single capped iid pool.
theorem labeledStreamLaw_eq_independent reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.Poisson.FinitePartition
Given an observation probability law, label masses summing to one, and a Poisson mean, the unshuffled streams are independent finite Poisson samples, with label-specific mean lambda * p i.
Formal statement
hypotheses
X :
Type u_1
I :
Type u_2
P :
p :
I → ℝ≥0
hp :
∑ i, p i = 1
lambda :
ℝ≥0
conclusion
labeledStreamLaw P p hp lambda
= Measure.pi (fun i : I => finitePoissonSampleLaw P (lambda * p i))
Proof (Lean source)
theorem labeledStreamLaw_eq_independent
(P : Measure X) [IsProbabilityMeasure P]
(p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0) :
labeledStreamLaw P p hp lambda =
Measure.pi (fun i : I => finitePoissonSampleLaw P (lambda * p i)) := by
-- Partition both measures by the complete label-count vector. On every
-- fibre, use the two fixed-count identities above; then sum the pairwise
-- disjoint restrictions. This keeps arbitrary measurable observation spaces.
classical
have hcover :
(⋃ c : I → ℕ, {s : I → FiniteSample X | ∀ i, (s i).count = c i}) =
univ := by
ext s
simp only [Set.mem_iUnion, Set.mem_setOf_eq, Set.mem_univ, iff_true]
exact ⟨fun i => (s i).count, fun i => rfl⟩
apply Measure.ext_of_iUnion_eq_univ hcover
intro c
exact (labeledStreamLaw_restrict_countVector_eq P p hp lambda c).trans
(independentStreamLaw_restrict_countVector_eq P p lambda c).symm
6 supporting declarations (lemmas, instances)
-
map_labeledPrefix_joint_eqtheorem — Given an iid observation law, label masses summing to one, a pool size, and an admissible prefix length, unshuffling the labeled fixed-pool prefix has the same law as unshuffling an iid marked tuple of that length.hypothesesX :sharedType u_1I :sharedType u_2P :p :I → ℝ≥0hp :∑ i, p i = 1n m :ℕh :m ≤ nconclusionMeasure.map (fun z : (Fin n → X) × (Fin n → I) => labeledPrefix z.1 m h (fun k => z.2 ⟨k.val, lt_of_lt_of_le k.isLt h⟩)) ((fixedPoolLaw P n).prod (Measure.pi (fun _ : Fin n => labelLaw p hp)))= Measure.map (fun z : Fin m → X × I => unshuffle (⟨m, z⟩ : FiniteSample (X × I))) (Measure.pi (fun _ : Fin m => P.prod (labelLaw p hp)))Proof (Lean source)
theorem map_labeledPrefix_joint_eq (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (hp : ∑ i, p i = 1) {n m : ℕ} (h : m ≤ n) : Measure.map (fun z : (Fin n → X) × (Fin n → I) => labeledPrefix z.1 m h (fun k => z.2 ⟨k.val, lt_of_lt_of_le k.isLt h⟩)) ((fixedPoolLaw P n).prod (Measure.pi (fun _ : Fin n => labelLaw p hp))) = Measure.map (fun z : Fin m → X × I => unshuffle (⟨m, z⟩ : FiniteSample (X × I))) (Measure.pi (fun _ : Fin m => P.prod (labelLaw p hp))) := by rw [← map_joint_prefix_pi P p hp h] rw [Measure.map_map] · rfl · exact measurable_unshuffle.comp (measurable_fixedSizeEmbed m) · fun_prop -
labeledStreamLaw_restrict_totalCount_eqtheorem — Given an observation probability law, label masses summing to one, a Poisson mean, and a count, the uncapped labeled-stream law on its total-count fibre is Poisson mass times the law of an unshuffled iid marked tuple.hypothesesX :sharedType u_1I :sharedType u_2P :p :I → ℝ≥0hp :∑ i, p i = 1lambda :ℝ≥0m :ℕconclusion(labeledStreamLaw P p hp lambda).restrict {s | ∑ i, (s i).count = m}= (poissonMeasure lambda) {m} • Measure.map (fun z : Fin m → X × I => unshuffle (⟨m, z⟩ : FiniteSample (X × I))) (Measure.pi (fun _ : Fin m => P.prod (labelLaw p hp)))Proof (Lean source)
theorem labeledStreamLaw_restrict_totalCount_eq (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0) (m : ℕ) : (labeledStreamLaw P p hp lambda).restrict {s | ∑ i, (s i).count = m} = (poissonMeasure lambda) {m} • Measure.map (fun z : Fin m → X × I => unshuffle (⟨m, z⟩ : FiniteSample (X × I))) (Measure.pi (fun _ : Fin m => P.prod (labelLaw p hp))) := by letI := labelLaw_isProbabilityMeasure p hp let Q := P.prod (labelLaw p hp) have hset : MeasurableSet {s : I → FiniteSample X | ∑ i, (s i).count = m} := by have hc : Measurable (fun s : I → FiniteSample X => ∑ i, (s i).count) := by fun_prop exact hc (measurableSet_singleton m) have hpre : unshuffle (X := X) (I := I) ⁻¹' {s | ∑ i, (s i).count = m} = FiniteSample.count ⁻¹' ({m} : Set ℕ) := by ext s simp [unshuffle_total_count] unfold labeledStreamLaw rw [Measure.restrict_map measurable_unshuffle hset, hpre, finitePoissonSampleLaw_restrict_count_eq Q lambda m, Measure.map_smul, Measure.map_map] · rfl · exact measurable_unshuffle · exact measurable_fixedSizeEmbed m -
labeledStreamLaw_restrict_countVector_eq_histogramMaptheorem — Given an iid observation law, label masses summing to one, a Poisson mean, and a label-count vector, restricting the unshuffled Poisson law to that count vector equals the Poisson mass of its total length times the unshuffled fixed-length marked law restricted to the corresponding word histogram.hypothesesX :sharedType u_1I :sharedType u_2P :p :I → ℝ≥0hp :∑ i, p i = 1lambda :ℝ≥0c :I → ℕconclusion(labeledStreamLaw P p hp lambda).restrict {s | ∀ i, (s i).count = c i}= (poissonMeasure lambda) ({∑ i, c i} : Set ℕ) • Measure.map (fun z : Fin (∑ i, c i) → X × I => unshuffle (⟨∑ i, c i, z⟩ : FiniteSample (X × I))) ((Measure.pi (fun _ : Fin (∑ i, c i) => P.prod (labelLaw p hp))).restrict {z | ∀ i, wordHistogram (fun k => (z k).2) i = c i})Proof (Lean source)
theorem labeledStreamLaw_restrict_countVector_eq_histogramMap (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0) (c : I → ℕ) : (labeledStreamLaw P p hp lambda).restrict {s | ∀ i, (s i).count = c i} = (poissonMeasure lambda) ({∑ i, c i} : Set ℕ) • Measure.map (fun z : Fin (∑ i, c i) → X × I => unshuffle (⟨∑ i, c i, z⟩ : FiniteSample (X × I))) ((Measure.pi (fun _ : Fin (∑ i, c i) => P.prod (labelLaw p hp))).restrict {z | ∀ i, wordHistogram (fun k => (z k).2) i = c i}) := by -- Restrict the fixed-total-count identity once more. The inverse image of -- the count-vector event under `unshuffle` is the word-histogram event, -- since each stream length is its label's word histogram. let A : Set (I → FiniteSample X) := {s | ∀ i, (s i).count = c i} let B : Set (I → FiniteSample X) := {s | ∑ i, (s i).count = ∑ i, c i} let H : Set (Fin (∑ i, c i) → X × I) := {z | ∀ i, wordHistogram (fun k => (z k).2) i = c i} let f : (Fin (∑ i, c i) → X × I) → I → FiniteSample X := fun z => unshuffle (⟨∑ i, c i, z⟩ : FiniteSample (X × I)) have hAB : A ⊆ B := by intro s hs exact Finset.sum_congr rfl (fun i _ => hs i) have hA : MeasurableSet A := by have hset : A = ⋂ i : I, {s : I → FiniteSample X | (s i).count = c i} := by ext s simp [A] rw [hset] apply MeasurableSet.iInter intro i have hm : Measurable (fun s : I → FiniteSample X => (s i).count) := by fun_prop exact hm (measurableSet_singleton (c i)) have hf : Measurable f := measurable_unshuffle.comp (measurable_fixedSizeEmbed (∑ i, c i)) have hpre : f ⁻¹' A = H := by ext z change (∀ i, ((unshuffle (⟨∑ i, c i, z⟩ : FiniteSample (X × I))) i).count = c i) ↔ (∀ i, wordHistogram (fun k => (z k).2) i = c i) rfl change (labeledStreamLaw P p hp lambda).restrict A = (poissonMeasure lambda) {∑ i, c i} • Measure.map f ((Measure.pi (fun _ : Fin (∑ i, c i) => P.prod (labelLaw p hp))).restrict H) calc (labeledStreamLaw P p hp lambda).restrict A = ((labeledStreamLaw P p hp lambda).restrict B).restrict A := (Measure.restrict_restrict_of_subset hAB).symm _ = ((poissonMeasure lambda) {∑ i, c i} • Measure.map f (Measure.pi (fun _ : Fin (∑ i, c i) => P.prod (labelLaw p hp)))).restrict A := by rw [show B = {s : I → FiniteSample X | ∑ i, (s i).count = ∑ i, c i} from rfl, labeledStreamLaw_restrict_totalCount_eq] _ = _ := by rw [Measure.restrict_smul, Measure.restrict_map hf hA, hpre] -
labeledStreamLaw_restrict_countVector_eqtheorem — Given an iid observation law, label masses summing to one, a Poisson mean, and a prescribed label-count vector, the uncapped unshuffled law on that count-vector fibre is the product of the count probabilities times independent fixed-length iid streams.hypothesesX :sharedType u_1I :sharedType u_2P :p :I → ℝ≥0hp :∑ i, p i = 1lambda :ℝ≥0c :I → ℕconclusion(labeledStreamLaw P p hp lambda).restrict {s | ∀ i, (s i).count = c i}= (∏ i, (poissonMeasure (lambda * p i)) ({c i} : Set ℕ)) • Measure.pi (fun i : I => Measure.map (fixedSizeEmbed (c i)) (Measure.pi (fun _ : Fin (c i) => P)))Proof (Lean source)
theorem labeledStreamLaw_restrict_countVector_eq (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0) (c : I → ℕ) : (labeledStreamLaw P p hp lambda).restrict {s | ∀ i, (s i).count = c i} = (∏ i, (poissonMeasure (lambda * p i)) ({c i} : Set ℕ)) • Measure.pi (fun i : I => Measure.map (fixedSizeEmbed (c i)) (Measure.pi (fun _ : Fin (c i) => P))) := by -- Restrict first to total count `∑ i, c i`, then partition the iid label -- words by their histogram. On each word, `map_gatherWord_iid_pi` gives -- the same product of fixed-length iid observation laws. Sum the word -- coefficients with `poisson_label_word_coefficient_eq`. rw [labeledStreamLaw_restrict_countVector_eq_histogramMap P p hp lambda c, map_unshuffle_restrict_histogram_eq P p hp c, smul_smul, poisson_label_word_coefficient_eq p hp lambda c] -
map_labeledPrefix_restrict_count_eqtheorem — On a Poisson mean and label masses summing to one, an observation law, and an exact admissible Poisson count, the labeled fixed-pool experiment has Poisson mass at that count times the law of an unshuffled iid marked tuple of that length.hypothesesX :sharedType u_1I :sharedType u_2P :p :I → ℝ≥0hp :∑ i, p i = 1lambda :ℝ≥0n m :ℕh :m ≤ nconclusionMeasure.map (fun z : (Fin n → X) × (ℕ × (Fin n → I)) => labeledPrefix z.1 m h (fun k => z.2.2 ⟨k.val, lt_of_lt_of_le k.isLt h⟩)) (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | z.2.1 = m})= (poissonMeasure lambda) {m} • Measure.map (fun z : Fin m → X × I => unshuffle (⟨m, z⟩ : FiniteSample (X × I))) (Measure.pi (fun _ : Fin m => P.prod (labelLaw p hp)))Proof (Lean source)
theorem map_labeledPrefix_restrict_count_eq (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0) {n m : ℕ} (h : m ≤ n) : Measure.map (fun z : (Fin n → X) × (ℕ × (Fin n → I)) => labeledPrefix z.1 m h (fun k => z.2.2 ⟨k.val, lt_of_lt_of_le k.isLt h⟩)) (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | z.2.1 = m}) = (poissonMeasure lambda) {m} • Measure.map (fun z : Fin m → X × I => unshuffle (⟨m, z⟩ : FiniteSample (X × I))) (Measure.pi (fun _ : Fin m => P.prod (labelLaw p hp))) := by classical haveI := labelLaw_isProbabilityMeasure p hp haveI : IsProbabilityMeasure (fixedPoolLaw P n) := by unfold fixedPoolLaw infer_instance let L : Measure (Fin n → I) := Measure.pi (fun _ => labelLaw p hp) let c : ℝ≥0∞ := (poissonMeasure lambda) {m} have hs : {z : (Fin n → X) × (ℕ × (Fin n → I)) | z.2.1 = m} = univ ×ˢ (({m} : Set ℕ) ×ˢ univ) := by ext z simp have haux : (auxiliaryLaw p hp lambda n).restrict (({m} : Set ℕ) ×ˢ univ) = c • Measure.map (Prod.mk m) L := by unfold auxiliaryLaw rw [← Measure.prod_restrict, Measure.restrict_univ, Measure.restrict_singleton, Measure.prod_smul_left, Measure.dirac_prod] let f : (Fin n → X) × (ℕ × (Fin n → I)) → I → FiniteSample X := fun z => labeledPrefix z.1 m h (fun k => z.2.2 ⟨k.val, lt_of_lt_of_le k.isLt h⟩) let g : (Fin n → X) × (Fin n → I) → I → FiniteSample X := fun z => labeledPrefix z.1 m h (fun k => z.2 ⟨k.val, lt_of_lt_of_le k.isLt h⟩) have hf : Measurable f := by exact measurable_unshuffle.comp (measurable_fixedSizeEmbed m |>.comp (measurable_pi_lambda _ fun k => ((measurable_pi_apply _).comp measurable_fst).prodMk ((measurable_pi_apply _).comp measurable_snd.snd))) have hprod : (fixedPoolLaw P n).prod (Measure.map (Prod.mk m) L) = Measure.map (map id (Prod.mk m)) ((fixedPoolLaw P n).prod L) := by simpa only [Measure.map_id] using (Measure.map_prod_map (fixedPoolLaw P n) L measurable_id measurable_prodMk_left) calc Measure.map f (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | z.2.1 = m}) = Measure.map f ((fixedPoolLaw P n).prod ((auxiliaryLaw p hp lambda n).restrict (({m} : Set ℕ) ×ˢ univ))) := by rw [hs, ← Measure.prod_restrict, Measure.restrict_univ] _ = c • Measure.map g ((fixedPoolLaw P n).prod L) := by rw [haux, Measure.prod_smul_right, Measure.map_smul, hprod, Measure.map_map] · rfl · exact hf · fun_prop _ = _ := by rw [map_labeledPrefix_joint_eq P p hp h] -
map_capped_restrict_nonoverflowtheorem — Given an observation probability law, label masses summing to one, a Poisson mean, and a pool size, the capped fixed-pool experiment on nonoverflow has the same ordered-stream law as the uncapped labeled Poisson experiment restricted to total count at most the pool size.hypothesesX :sharedType u_1I :sharedType u_2P :p :I → ℝ≥0hp :∑ i, p i = 1lambda :ℝ≥0n :ℕconclusionMeasure.map (fun z : (Fin n → X) × (ℕ × (Fin n → I)) => if h : z.2.1 ≤ n then labeledPrefix z.1 z.2.1 h (fun k => z.2.2 ⟨k.val, lt_of_lt_of_le k.isLt h⟩) else fun _ => (⟨0, Fin.elim0⟩ : FiniteSample X)) (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | z.2.1 ≤ n})= (labeledStreamLaw P p hp lambda).restrict {s | ∑ i, (s i).count ≤ n}Proof (Lean source)
theorem map_capped_restrict_nonoverflow (P : Measure X) [IsProbabilityMeasure P] (p : I → ℝ≥0) (hp : ∑ i, p i = 1) (lambda : ℝ≥0) (n : ℕ) : Measure.map (fun z : (Fin n → X) × (ℕ × (Fin n → I)) => if h : z.2.1 ≤ n then labeledPrefix z.1 z.2.1 h (fun k => z.2.2 ⟨k.val, lt_of_lt_of_le k.isLt h⟩) else fun _ => (⟨0, Fin.elim0⟩ : FiniteSample X)) (((fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n)).restrict {z | z.2.1 ≤ n}) = (labeledStreamLaw P p hp lambda).restrict {s | ∑ i, (s i).count ≤ n} := by classical let μ := (fixedPoolLaw P n).prod (auxiliaryLaw p hp lambda n) let ν := labeledStreamLaw P p hp lambda let f : (Fin n → X) × (ℕ × (Fin n → I)) → I → FiniteSample X := fun z => if h : z.2.1 ≤ n then labeledPrefix z.1 z.2.1 h (fun k => z.2.2 ⟨k.val, lt_of_lt_of_le k.isLt h⟩) else fun _ => (⟨0, Fin.elim0⟩ : FiniteSample X) have hf : Measurable f := by let g : ℕ × ((Fin n → X) × (Fin n → I)) → I → FiniteSample X := fun z => if h : z.1 ≤ n then labeledPrefix z.2.1 z.1 h (fun k => z.2.2 ⟨k.val, lt_of_lt_of_le k.isLt h⟩) else fun _ => (⟨0, Fin.elim0⟩ : FiniteSample X) have hg : Measurable g := by apply measurable_from_prod_countable_right intro m by_cases hm : m ≤ n · have hprefix : Measurable (fun z : (Fin n → X) × (Fin n → I) => labeledPrefix z.1 m hm (fun k => z.2 ⟨k.val, lt_of_lt_of_le k.isLt hm⟩)) := by exact measurable_unshuffle.comp (measurable_fixedSizeEmbed m |>.comp (measurable_pi_lambda _ fun k => ((measurable_pi_apply _).comp measurable_fst).prodMk ((measurable_pi_apply _).comp measurable_snd))) simpa only [g, hm, dite_true] using hprefix · simpa only [g, hm, dite_false] using (measurable_const : Measurable (fun _ : (Fin n → X) × (Fin n → I) => (fun _ => (⟨0, Fin.elim0⟩ : FiniteSample X)))) exact hg.comp (by fun_prop : Measurable (fun z : (Fin n → X) × (ℕ × (Fin n → I)) => (z.2.1, (z.1, z.2.2)))) have hfiber (m : Fin (n + 1)) : Measure.map f (μ.restrict {z | z.2.1 = m.val}) = ν.restrict {s | ∑ i, (s i).count = m.val} := by have hm : m.val ≤ n := Nat.le_of_lt_succ m.isLt have hmap : Measure.map f (μ.restrict {z | z.2.1 = m.val}) = Measure.map (fun z : (Fin n → X) × (ℕ × (Fin n → I)) => labeledPrefix z.1 m.val hm (fun k => z.2.2 ⟨k.val, lt_of_lt_of_le k.isLt hm⟩)) (μ.restrict {z | z.2.1 = m.val}) := by apply Measure.map_congr filter_upwards [ae_restrict_mem (by exact (measurable_fst.comp measurable_snd) (measurableSet_singleton m.val) : MeasurableSet {z : (Fin n → X) × (ℕ × (Fin n → I)) | z.2.1 = m.val})] with z hz rcases z with ⟨x, ⟨k, w⟩⟩ change k = m.val at hz subst k simp [f, hm] rw [hmap, map_labeledPrefix_restrict_count_eq P p hp lambda hm, ← labeledStreamLaw_restrict_totalCount_eq P p hp lambda m.val] have hsource : {z : (Fin n → X) × (ℕ × (Fin n → I)) | z.2.1 ≤ n} = ⋃ m : Fin (n + 1), {z | z.2.1 = m.val} := by ext z simp only [Set.mem_iUnion] constructor · intro hz exact ⟨⟨z.2.1, Nat.lt_succ_of_le hz⟩, rfl⟩ · rintro ⟨m, hm⟩ change z.2.1 = m.val at hm change z.2.1 ≤ n rw [hm] exact Nat.le_of_lt_succ m.isLt have htarget : {s : I → FiniteSample X | ∑ i, (s i).count ≤ n} = ⋃ m : Fin (n + 1), {s | ∑ i, (s i).count = m.val} := by ext s simp only [Set.mem_iUnion] constructor · intro hs exact ⟨⟨∑ i, (s i).count, Nat.lt_succ_of_le hs⟩, rfl⟩ · rintro ⟨m, hm⟩ change (∑ i, (s i).count) = m.val at hm change (∑ i, (s i).count) ≤ n rw [hm] exact Nat.le_of_lt_succ m.isLt have hsource_disjoint : Pairwise (onFun Disjoint (fun m : Fin (n + 1) => {z : (Fin n → X) × (ℕ × (Fin n → I)) | z.2.1 = m.val})) := by intro a b hab change Disjoint {z : (Fin n → X) × (ℕ × (Fin n → I)) | z.2.1 = a.val} {z : (Fin n → X) × (ℕ × (Fin n → I)) | z.2.1 = b.val} rw [Set.disjoint_left] intro z hza hzb apply hab apply Fin.ext exact hza.symm.trans hzb have htarget_disjoint : Pairwise (onFun Disjoint (fun m : Fin (n + 1) => {s : I → FiniteSample X | ∑ i, (s i).count = m.val})) := by intro a b hab change Disjoint {s : I → FiniteSample X | ∑ i, (s i).count = a.val} {s : I → FiniteSample X | ∑ i, (s i).count = b.val} rw [Set.disjoint_left] intro s hsa hsb apply hab apply Fin.ext exact hsa.symm.trans hsb change Measure.map f (μ.restrict {z | z.2.1 ≤ n}) = ν.restrict {s | ∑ i, (s i).count ≤ n} rw [hsource, Measure.restrict_iUnion hsource_disjoint (fun m => (measurable_fst.comp measurable_snd) (measurableSet_singleton m.val)), Measure.map_sum hf.aemeasurable, htarget, Measure.restrict_iUnion htarget_disjoint (fun m => by have hc : Measurable (fun s : I → FiniteSample X => ∑ i, (s i).count) := by fun_prop exact hc (measurableSet_singleton m.val))] congr 1 funext m exact hfiber m