Stat.FiniteRaoBlackwell.Poisson.IndependentPrefix.ProductPools
This roll-up module exports the finite heterogeneous extension of independent Poisson-prefix Rao--Blackwell transfer: exact product laws, capped fixed-pool statistics, summed overflow-tail risk control, and a direct thre
Basic 14 core · 9 supporting This module provides the measurable experiment, exact product laws, and capped implementation for finitely many heterogeneous iid pools, each given an independent Poisson prefix length. ★ map_totalizedPrefixFamily_restrict_nonoverflow
Finite families of independent Poisson prefixes
This module provides the measurable experiment, exact product laws, and capped implementation for finitely many heterogeneous iid pools, each given an independent Poisson prefix length.
abbrev FixedPools reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given a family of observation alphabets and pool capacities, fixed pools give each coordinate an ordered iid observation pool. They are represented by the dependent family of coordinate pools.
Definition (Lean source)
abbrev RandomizedPools reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given a family of observation alphabets and pool capacities, the randomized pool family appends one requested prefix length to each coordinate pool. It is represented by the dependent family of pool-length pairs.
Definition (Lean source)
parameters
given by
(i : I) → (Fin (N i) → X i) × ℕ
abbrev PrefixFamily reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given a family of observation alphabets, a prefix family contains one variable-length finite sample for each coordinate. It is represented by the dependent family of finite samples.
Definition (Lean source)
parameters
I :
Type uI
X :
I → Type uX
∀ i, MeasurableSpace (X i)
def
given by
(i : I) → FiniteSample (X i)
abbrev PoissonStreamFamily reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given a family of observation alphabets, a Poisson stream family gives each coordinate a requested count and an infinite observation stream. It is represented by the dependent family of count-stream pairs.
Definition (Lean source)
parameters
I :
Type uI
X :
I → Type uX
∀ i, MeasurableSpace (X i)
given by
(i : I) → ℕ × (ℕ → X i)
def fixedPoolsLaw reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given coordinatewise probability laws and pool capacities, the fixed-pool law makes the observations iid within and independent across pools. It is given by the finite product of coordinatewise iid laws.
Definition (Lean source)
def randomizedPoolsLaw reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given coordinatewise probability laws, Poisson intensities, and pool capacities, the randomized-pool law makes pools, counts, and coordinates mutually independent. It is given by the finite product of pool-count laws.
Definition (Lean source)
parameters
I :
Type uI
I → Type uX
P :
(i : I) → Measure (X i)
∀ i, IsProbabilityMeasure (P i)
lambda :
I → ℝ≥0
N :
I → ℕ
def
given by
def independentPoissonPrefixLaw reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given coordinatewise probability laws and Poisson intensities, the independent Poisson-prefix law is the joint law of all untruncated iid prefixes. It is given by the finite product of coordinatewise Poisson sample laws.
Definition (Lean source)
parameters
I :
Type uI
I → Type uX
P :
(i : I) → Measure (X i)
∀ i, IsProbabilityMeasure (P i)
lambda :
I → ℝ≥0
def
given by
Measure.pi (fun i ↦ finitePoissonSampleLaw (P i) (lambda i))
def independentPoissonStreamLaw reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given coordinatewise probability laws and Poisson intensities, the independent count-and-stream law independently supplies a count and iid stream in every coordinate. It is given by the finite product of coordinatewise stream laws.
Definition (Lean source)
parameters
I :
Type uI
I → Type uX
P :
(i : I) → Measure (X i)
∀ i, IsProbabilityMeasure (P i)
lambda :
I → ℝ≥0
def
given by
Measure.pi (fun i ↦ poissonIIDStreamLaw (P i) (lambda i))
def nonoverflowSet reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given pool capacities, the joint nonoverflow event is the event that every requested prefix fits its coordinate pool. It is given by the coordinatewise capacity bounds.
Definition (Lean source)
parameters
I :
Type uI
I → Type uX
N :
I → ℕ
def
given by
{z | ∀ i, (z i).2 ≤ N i}
def overflowSet reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given pool capacities, the overflow event is the event that at least one requested prefix exceeds its coordinate pool. It is given by the union of marginal overflow events.
Definition (Lean source)
parameters
I :
Type uI
I → Type uX
N :
I → ℕ
def
given by
{z | ∃ i, N i < (z i).2}
def streamFamilyToPrefixFamily reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given a count-and-stream family, its prefix family retains the requested initial segment of every stream. It is given by coordinatewise stream truncation.
Definition (Lean source)
def totalizedPrefixFamily reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given fallback prefixes and a randomized pool family, the totalized prefix family uses genuine prefixes when available and the corresponding fallback otherwise. It is given by coordinatewise one-pool totalization.
Definition (Lean source)
def cappedPrefixStatistic reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given a prefix statistic, an overflow value, and a randomized pool family, the capped-prefix statistic uses genuine prefixes precisely when every request fits. It is given by the joint capacity test.
Definition (Lean source)
parameters
def
cappedPrefixStatistic T zOver z :
ℝ
given by
if h : ∀ i, (z i).2 ≤ N i then T (fun i ↦ prefixOfLE (z i).1 (z i).2 (h i)) else zOver
theorem map_totalizedPrefixFamily_restrict_nonoverflow reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given coordinatewise probability laws, Poisson intensities, pool capacities, and fallback prefixes, mapping jointly nonoverflowing randomized pools to totalized prefixes gives the restricted untruncated product law.
Formal statement
hypotheses
I :
Type uI
I → Type uX
P :
(i : I) → Measure (X i)
∀ i, IsProbabilityMeasure (P i)
lambda :
I → ℝ≥0
N :
I → ℕ
overflow :
conclusion
Measure.map (totalizedPrefixFamily overflow) ((randomizedPoolsLaw P lambda N).restrict (nonoverflowSet (X := X) N))
= (independentPoissonPrefixLaw P lambda).restrict {s : PrefixFamily X | ∀ i, (s i).count ≤ N i}
Proof (Lean source)
theorem map_totalizedPrefixFamily_restrict_nonoverflow
(P : (i : I) → Measure (X i)) [∀ i, IsProbabilityMeasure (P i)]
(lambda : I → ℝ≥0) (N : I → ℕ) (overflow : PrefixFamily X) :
Measure.map (totalizedPrefixFamily overflow)
((randomizedPoolsLaw P lambda N).restrict (nonoverflowSet (X := X) N)) =
(independentPoissonPrefixLaw P lambda).restrict
{s : PrefixFamily X | ∀ i, (s i).count ≤ N i} := by
rw [show nonoverflowSet (X := X) N =
Set.univ.pi (fun i ↦ snd ⁻¹' Iic (N i)) by
ext z
simp [nonoverflowSet]]
unfold randomizedPoolsLaw independentPoissonPrefixLaw totalizedPrefixFamily
rw [Measure.restrict_pi_pi]
rw [Measure.pi_map_pi fun i ↦
(measurable_totalizedPrefix (overflow i)).aemeasurable]
simp_rw [map_totalizedPrefix_restrict_nonoverflow]
rw [← Measure.restrict_pi_pi]
congr 1
ext s
simp
9 supporting declarations (lemmas, instances)
-
measurableSet_prefixNonoverflowSettheorem — Given pool capacities, the event that every untruncated prefix fits its coordinate capacity is measurable.hypothesesI :sharedType uII → Type uXN :I → ℕconclusionMeasurableSet {s : PrefixFamily X | ∀ i, (s i).count ≤ N i}Proof (Lean source)
theorem measurableSet_prefixNonoverflowSet (N : I → ℕ) : MeasurableSet {s : PrefixFamily X | ∀ i, (s i).count ≤ N i} := by rw [show {s : PrefixFamily X | ∀ i, (s i).count ≤ N i} = Set.univ.pi (fun i ↦ (FiniteSample.count : FiniteSample (X i) → ℕ) ⁻¹' Iic (N i)) by ext s simp] exact MeasurableSet.univ_pi (X := fun i ↦ FiniteSample (X i)) fun i ↦ (measurable_finiteSample_count (X := X i)) measurableSet_Iic -
measurableSet_nonoverflowSettheorem — Given pool capacities, the joint nonoverflow event is measurable.hypothesesI :sharedType uII → Type uXN :I → ℕconclusionMeasurableSet (nonoverflowSet (X := X) N)Proof (Lean source)
theorem measurableSet_nonoverflowSet (N : I → ℕ) : MeasurableSet (nonoverflowSet (X := X) N) := by rw [show nonoverflowSet (X := X) N = Set.univ.pi (fun i ↦ (Prod.snd : ((Fin (N i) → X i) × ℕ) → ℕ) ⁻¹' Iic (N i)) by ext z simp [nonoverflowSet]] exact MeasurableSet.univ_pi (X := fun i ↦ (Fin (N i) → X i) × ℕ) fun i ↦ (measurable_snd : Measurable (Prod.snd : ((Fin (N i) → X i) × ℕ) → ℕ)) measurableSet_Iic -
measurableSet_overflowSettheorem — Given pool capacities, the union of marginal overflow events is measurable.hypothesesI :sharedType uII → Type uXN :I → ℕconclusionMeasurableSet (overflowSet (X := X) N)Proof (Lean source)
theorem measurableSet_overflowSet (N : I → ℕ) : MeasurableSet (overflowSet (X := X) N) := by rw [show overflowSet (X := X) N = ⋃ i, (fun z : RandomizedPools X N ↦ (z i).2) ⁻¹' Ioi (N i) by ext z simp [overflowSet]] exact MeasurableSet.iUnion fun i ↦ (measurable_snd.comp (measurable_pi_apply i)) measurableSet_Ioi -
nonoverflowSet_eq_compl_overflowSettheorem — Given pool capacities, joint nonoverflow is the complement of the overflow event.hypothesesI :sharedType uII → Type uXN :I → ℕconclusionnonoverflowSet (X := X) N = (overflowSet (X := X) N)ᶜProof (Lean source)
theorem nonoverflowSet_eq_compl_overflowSet (N : I → ℕ) : nonoverflowSet (X := X) N = (overflowSet (X := X) N)ᶜ := by ext z simp [nonoverflowSet, overflowSet, not_lt] -
measurable_streamFamilyToPrefixFamilytheorem — Conversion of count-and-stream families to prefix families is measurable.hypothesesI :sharedType uII → Type uXconclusionMeasurable (streamFamilyToPrefixFamily (I := I) (X := X))Proof (Lean source)
@[fun_prop] theorem measurable_streamFamilyToPrefixFamily : Measurable (streamFamilyToPrefixFamily (I := I) (X := X)) := by apply measurable_pi_lambda intro i exact measurable_streamToFiniteSample.comp (measurable_pi_apply i) -
map_independentPoissonStreamLaw_eq_independentPoissonPrefixLawtheorem — Given coordinatewise probability laws and Poisson intensities, mapping independent count-and-stream coordinates to prefixes gives exactly the independent Poisson-prefix law.hypothesesI :sharedType uII → Type uXP :(i : I) → Measure (X i)∀ i, IsProbabilityMeasure (P i)lambda :I → ℝ≥0conclusionMeasure.map (streamFamilyToPrefixFamily (I := I) (X := X)) (independentPoissonStreamLaw P lambda)= independentPoissonPrefixLaw P lambdaProof (Lean source)
theorem map_independentPoissonStreamLaw_eq_independentPoissonPrefixLaw (P : (i : I) → Measure (X i)) [∀ i, IsProbabilityMeasure (P i)] (lambda : I → ℝ≥0) : Measure.map (streamFamilyToPrefixFamily (I := I) (X := X)) (independentPoissonStreamLaw P lambda) = independentPoissonPrefixLaw P lambda := by unfold streamFamilyToPrefixFamily independentPoissonStreamLaw independentPoissonPrefixLaw finitePoissonSampleLaw rw [Measure.pi_map_pi fun i ↦ measurable_streamToFiniteSample.aemeasurable] -
measurable_totalizedPrefixFamilytheorem — Given fallback prefixes, coordinatewise totalization is measurable.hypothesesI :sharedType uII → Type uXI → ℕoverflow :conclusionProof (Lean source)
@[fun_prop] theorem measurable_totalizedPrefixFamily {N : I → ℕ} (overflow : PrefixFamily X) : Measurable (totalizedPrefixFamily (I := I) overflow : RandomizedPools X N → PrefixFamily X) := by apply measurable_pi_lambda intro i exact (measurable_totalizedPrefix (overflow i)).comp (measurable_pi_apply i) -
measurable_cappedPrefixStatistictheorem — Given a measurable prefix statistic and an overflow value, the capped-prefix statistic is measurable.hypothesesconclusionMeasurable (cappedPrefixStatistic (I := I) (N := N) T zOver)Proof (Lean source)
@[fun_prop] theorem measurable_cappedPrefixStatistic {N : I → ℕ} {T : PrefixFamily X → ℝ} (hT : Measurable T) (zOver : ℝ) : Measurable (cappedPrefixStatistic (I := I) (N := N) T zOver) := by classical let overflow : PrefixFamily X := fun _ ↦ ⟨0, Fin.elim0⟩ have hfun : cappedPrefixStatistic (I := I) (N := N) T zOver = (nonoverflowSet (X := X) N).piecewise (T ∘ totalizedPrefixFamily overflow) (fun _ ↦ zOver) := by funext z by_cases h : ∀ i, (z i).2 ≤ N i · rw [cappedPrefixStatistic, dif_pos h] rw [Set.piecewise, if_pos (show z ∈ nonoverflowSet (X := X) N from h)] congr 1 funext i simp [totalizedPrefixFamily, totalizedPrefix, cappedPrefix, h i] · rw [cappedPrefixStatistic, dif_neg h] simp [Set.piecewise, nonoverflowSet, h] rw [hfun] exact Measurable.piecewise (measurableSet_nonoverflowSet N) (hT.comp (measurable_totalizedPrefixFamily overflow)) measurable_const -
cappedPrefixStatistic_eq_off_overflowtheorem — Given a prefix statistic, an overflow value, fallback prefixes, a randomized pool family, and evidence of no overflow, the capped statistic equals the statistic of the totalized prefixes.hypothesesI :sharedType uII → Type uXI → ℕT :PrefixFamily X → ℝzOver :ℝoverflow :z :RandomizedPools X Nhz :z ∉ overflowSet (X := X) NconclusioncappedPrefixStatistic T zOver z = T (totalizedPrefixFamily overflow z)Proof (Lean source)
theorem cappedPrefixStatistic_eq_off_overflow {N : I → ℕ} (T : PrefixFamily X → ℝ) (zOver : ℝ) (overflow : PrefixFamily X) (z : RandomizedPools X N) (hz : z ∉ overflowSet (X := X) N) : cappedPrefixStatistic T zOver z = T (totalizedPrefixFamily overflow z) := by have h : ∀ i, (z i).2 ≤ N i := by intro i exact Nat.le_of_not_gt fun hi ↦ hz ⟨i, hi⟩ rw [cappedPrefixStatistic, dif_pos h] congr 1 funext i simp [totalizedPrefixFamily, totalizedPrefix, cappedPrefix, h i]
Risk 3 core · 8 supporting This module averages the capped statistic over all independent Poisson counts, proves squared-risk contraction, and bounds the overflow contribution by the sum of the heterogeneous marginal Poisson upper tails. ★ sqRisk_prefixRaoBlackwellStatistic_le
Rao--Blackwell risk transfer for finite prefix families
This module averages the capped statistic over all independent Poisson counts, proves squared-risk contraction, and bounds the overflow contribution by the sum of the heterogeneous marginal Poisson upper tails.
def independentPoissonCountKernel reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given Poisson intensities, the independent Poisson-count kernel keeps every fixed pool and independently attaches one requested length in every coordinate. It is given by the product Poisson mechanism.
Definition (Lean source)
parameters
I :
Type uI
I → Type uX
I → ℕ
lambda :
I → ℝ≥0
def
given by
mechanismKernel (Measure.pi (fun i ↦ poissonMeasure (lambda i))) (fun z i ↦ (z.1 i, z.2 i))
def prefixRaoBlackwellStatistic reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given Poisson intensities, a prefix statistic, and an overflow value, the prefix Rao--Blackwell statistic averages the capped statistic over all requested lengths conditional on fixed pools. It is given by the count-kernel mean.
Definition (Lean source)
parameters
def
prefixRaoBlackwellStatistic lambda T zOver :
FixedPools X N → ℝ
given by
kernelMean (independentPoissonCountKernel lambda) (cappedPrefixStatistic T zOver)
theorem sqRisk_prefixRaoBlackwellStatistic_le reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given coordinatewise probability laws, Poisson intensities, pool capacities, a measurable prefix statistic, an ordered outcome interval, a statistic confined to that interval, a target in it, and an overflow value in it, fixed-pool Rao--Blackwell risk is bounded by untruncated Poissonized risk plus squared interval diameter times the summed upper tails.
Formal statement
hypotheses
I :
Type uI
I → Type uX
P :
(i : I) → Measure (X i)
∀ i, IsProbabilityMeasure (P i)
lambda :
I → ℝ≥0
N :
I → ℕ
T :
PrefixFamily X → ℝ
hT :
a b theta zOver :
ℝ
hab :
a ≤ b
hTmem :
∀ s, T s ∈ Icc a b
htheta :
theta ∈ Icc a b
hzOver :
zOver ∈ Icc a b
conclusion
sqRisk (fixedPoolsLaw P N) (prefixRaoBlackwellStatistic lambda T zOver) theta
≤ sqRisk (independentPoissonPrefixLaw P lambda) T theta
Proof (Lean source)
theorem sqRisk_prefixRaoBlackwellStatistic_le
(P : (i : I) → Measure (X i)) [∀ i, IsProbabilityMeasure (P i)]
(lambda : I → ℝ≥0) (N : I → ℕ)
{T : PrefixFamily X → ℝ} (hT : Measurable T)
{a b theta zOver : ℝ} (hab : a ≤ b)
(hTmem : ∀ s, T s ∈ Icc a b)
(htheta : theta ∈ Icc a b) (hzOver : zOver ∈ Icc a b) :
sqRisk (fixedPoolsLaw P N)
(prefixRaoBlackwellStatistic lambda T zOver) theta ≤
sqRisk (independentPoissonPrefixLaw P lambda) T theta +
(b - a) ^ 2 *
∑ i, (poissonMeasure (lambda i)).real (Ioi (N i)) := by
-- Split capped risk over nonoverflow/overflow. Rewrite the good part with
-- the restricted-law theorem; the bad statistic is constantly `zOver`, so
-- its loss is at most `(b-a)^2`, then apply the finite union tail bound.
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 hCappedBound : UniformlyBounded
(cappedPrefixStatistic (N := N) T zOver) := by
refine ⟨max |a| |b|, (abs_nonneg a).trans (le_max_left _ _), ?_⟩
intro z
by_cases h : ∀ i, (z i).2 ≤ N i
· rw [cappedPrefixStatistic, dif_pos h]
exact abs_le_max_abs_abs (hTmem _).1 (hTmem _).2
· rw [cappedPrefixStatistic, dif_neg h]
exact abs_le_max_abs_abs hzOver.1 hzOver.2
let μ : Measure (RandomizedPools X N) := randomizedPoolsLaw P lambda N
letI : IsProbabilityMeasure μ := by
unfold μ randomizedPoolsLaw
infer_instance
let s : Set (RandomizedPools X N) := nonoverflowSet (X := X) N
have hs : MeasurableSet s := measurableSet_nonoverflowSet N
obtain ⟨M, hM, hCappedBoundM⟩ := hCappedBound
have hlossInt : Integrable
(fun z ↦ (cappedPrefixStatistic T zOver z - theta) ^ 2) μ := by
refine (integrable_const ((M + |theta|) ^ 2)).mono'
(((measurable_cappedPrefixStatistic hT zOver).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 (hCappedBoundM z) le_rfl)
have hsplit :
sqRisk μ (cappedPrefixStatistic T zOver) theta =
sqRisk (μ.restrict s) (cappedPrefixStatistic T zOver) theta +
sqRisk (μ.restrict sᶜ) (cappedPrefixStatistic T zOver) theta := by
unfold sqRisk
conv_lhs => rw [← Measure.restrict_add_restrict_compl (μ := μ) hs,
integral_add_measure hlossInt.restrict hlossInt.restrict]
have hsc : sᶜ = overflowSet (X := X) N := by
simp only [s, nonoverflowSet_eq_compl_overflowSet, compl_compl]
have hoverflowSq : (zOver - theta) ^ 2 ≤ (b - a) ^ 2 := by
have hdist : |zOver - theta| ≤ b - a := by
simpa [Real.dist_eq] using Real.dist_le_of_mem_Icc hzOver htheta
rw [← sq_abs (zOver - theta)]
exact (sq_le_sq₀ (abs_nonneg _) (sub_nonneg.mpr hab)).2 hdist
have hbadEq :
sqRisk (μ.restrict (overflowSet (X := X) N))
(cappedPrefixStatistic T zOver) theta =
(zOver - theta) ^ 2 * μ.real (overflowSet (X := X) N) := by
unfold sqRisk
have hae : ∀ᵐ z ∂μ.restrict (overflowSet (X := X) N),
(cappedPrefixStatistic T zOver z - theta) ^ 2 =
(zOver - theta) ^ 2 := by
filter_upwards [ae_restrict_mem (measurableSet_overflowSet N)] with z hz
obtain ⟨i, hi⟩ := hz
rw [cappedPrefixStatistic, dif_neg]
exact fun h ↦ (Nat.not_lt_of_ge (h i)) hi
rw [integral_congr_ae hae, integral_const]
simp only [smul_eq_mul, measureReal_def]
rw [Measure.restrict_apply_univ]
ring
have hoverflowMass :
μ.real (overflowSet (X := X) N) ≤
∑ i, (poissonMeasure (lambda i)).real (Ioi (N i)) := by
simpa [μ] using overflowSet_measureReal_le_sum_poisson_tails P lambda N
have hbadLe :
sqRisk (μ.restrict (overflowSet (X := X) N))
(cappedPrefixStatistic T zOver) theta ≤
(b - a) ^ 2 *
∑ i, (poissonMeasure (lambda i)).real (Ioi (N i)) := by
rw [hbadEq]
calc
(zOver - theta) ^ 2 * μ.real (overflowSet (X := X) N) ≤
(b - a) ^ 2 * μ.real (overflowSet (X := X) N) :=
mul_le_mul_of_nonneg_right hoverflowSq (by positivity)
_ ≤ (b - a) ^ 2 *
∑ i, (poissonMeasure (lambda i)).real (Ioi (N i)) :=
mul_le_mul_of_nonneg_left hoverflowMass (sq_nonneg _)
calc
sqRisk (fixedPoolsLaw P N)
(prefixRaoBlackwellStatistic lambda T zOver) theta ≤
sqRisk μ (cappedPrefixStatistic T zOver) theta := by
exact sqRisk_prefixRaoBlackwellStatistic_le_capped
P lambda N hT hTmem hzOver
_ = sqRisk (μ.restrict s) (cappedPrefixStatistic T zOver) theta +
sqRisk (μ.restrict sᶜ) (cappedPrefixStatistic T zOver) theta := hsplit
_ = sqRisk ((independentPoissonPrefixLaw P lambda).restrict
{z : PrefixFamily X | ∀ i, (z i).count ≤ N i}) T theta +
sqRisk (μ.restrict (overflowSet (X := X) N))
(cappedPrefixStatistic T zOver) theta := by
rw [show μ.restrict s =
(randomizedPoolsLaw P lambda N).restrict (nonoverflowSet (X := X) N) from rfl,
sqRisk_cappedPrefixStatistic_restrict_nonoverflow_eq
P lambda N hT zOver theta, hsc]
_ ≤ sqRisk (independentPoissonPrefixLaw P lambda) T theta +
(b - a) ^ 2 *
∑ i, (poissonMeasure (lambda i)).real (Ioi (N i)) :=
add_le_add
(sqRisk_independentPoissonPrefixLaw_restrict_nonoverflow_le
P lambda N hT hTb theta)
hbadLe
8 supporting declarations (lemmas, instances)
-
isMarkovKernelinstance — Given Poisson intensities, the independent Poisson-count kernel is a Markov kernel.parametersI :sharedType uII → Type uXI → ℕlambda :I → ℝ≥0instancegiven byby unfold independentPoissonCountKernel exact instIsMarkovKernelMechanismKernel _ (by fun_prop) -
independentPoissonCountKernel_comp_fixedPoolsLawtheorem — Given coordinatewise probability laws, Poisson intensities, and pool capacities, mixing the count kernel over fixed pools gives the randomized-pool law.hypothesesI :sharedType uII → Type uXP :(i : I) → Measure (X i)∀ i, IsProbabilityMeasure (P i)lambda :I → ℝ≥0N :I → ℕconclusionindependentPoissonCountKernel (X := X) lambda ∘ₘ fixedPoolsLaw P N= randomizedPoolsLaw P lambda NProof (Lean source)
theorem independentPoissonCountKernel_comp_fixedPoolsLaw (P : (i : I) → Measure (X i)) [∀ i, IsProbabilityMeasure (P i)] (lambda : I → ℝ≥0) (N : I → ℕ) : independentPoissonCountKernel (X := X) lambda ∘ₘ fixedPoolsLaw P N = randomizedPoolsLaw P lambda N := by -- Express the composition as a graph pushforward. A measurable -- reassociation sends `(pools, counts)` to `fun i ↦ (pools i, counts i)`; -- identify its law with the pi of coordinate products via `Measure.pi_map_pi`. let μ : Measure (FixedPools X N) := fixedPoolsLaw P N let ν : Measure (I → ℕ) := Measure.pi (fun i ↦ poissonMeasure (lambda i)) let Φ : FixedPools X N × (I → ℕ) → RandomizedPools X N := fun z i ↦ (z.1 i, z.2 i) let Ψ : RandomizedPools X N → FixedPools X N × (I → ℕ) := fun z ↦ ((fun i ↦ (z i).1), fun i ↦ (z i).2) letI : IsProbabilityMeasure μ := by unfold μ fixedPoolsLaw infer_instance have hΦ : Measurable Φ := by fun_prop have hΨ : Measurable Ψ := by fun_prop have hgraph : Measure.map (fun p ↦ (p.1, Φ p)) (μ.prod ν) = μ.compProd (independentPoissonCountKernel lambda) := by simpa [independentPoissonCountKernel, μ, ν, Φ] using (map_graph_prod_eq_compProd μ ν hΦ) have hsnd := congrArg (Measure.map snd) hgraph rw [Measure.map_map measurable_snd (show Measurable (fun p ↦ (p.1, Φ p)) from measurable_fst.prodMk hΦ)] at hsnd change Measure.map Φ (μ.prod ν) = (μ ⊗ₘ independentPoissonCountKernel lambda).snd at hsnd rw [Measure.snd_compProd] at hsnd have hsplit : Measure.map Ψ (randomizedPoolsLaw P lambda N) = μ.prod ν := by simpa [randomizedPoolsLaw, fixedPoolsLaw, μ, ν, Ψ] using (measurePreserving_splitPiProd (I := I) (μ := fun i ↦ Measure.pi (fun _ : Fin (N i) ↦ P i)) (ν := fun i ↦ poissonMeasure (lambda i))).map_eq have hperm : Measure.map Φ (μ.prod ν) = randomizedPoolsLaw P lambda N := by rw [← hsplit, Measure.map_map hΦ hΨ] have hcomp : Φ ∘ Ψ = id := by funext z i rfl rw [hcomp, Measure.map_id] exact hsnd.symm.trans hperm -
measurable_prefixRaoBlackwellStatistictheorem — Given Poisson intensities, a measurable prefix statistic, and an overflow value, the prefix Rao--Blackwell statistic is measurable.hypothesesconclusionMeasurable (prefixRaoBlackwellStatistic (N := N) lambda T zOver)Proof (Lean source)
@[fun_prop] theorem measurable_prefixRaoBlackwellStatistic {N : I → ℕ} (lambda : I → ℝ≥0) {T : PrefixFamily X → ℝ} (hT : Measurable T) (zOver : ℝ) : Measurable (prefixRaoBlackwellStatistic (N := N) lambda T zOver) := by -- Unfold and apply `measurable_kernelMean` to the capped measurability lemma. exact measurable_kernelMean _ (measurable_cappedPrefixStatistic hT zOver) -
prefixRaoBlackwellStatistic_eq_integraltheorem — Given Poisson intensities, a prefix statistic, evidence that it is measurable, an overflow value, and fixed pools, the Rao--Blackwell statistic equals its explicit count integral.hypothesesI :sharedType uII → Type uXI → ℕlambda :I → ℝ≥0T :PrefixFamily X → ℝhT :zOver :ℝpools :FixedPools X NconclusionprefixRaoBlackwellStatistic lambda T zOver pools= ∫ counts : I → ℕ, cappedPrefixStatistic T zOver (fun i ↦ (pools i, counts i)) ∂(Measure.pi (fun i ↦ poissonMeasure (lambda i)))Proof (Lean source)
theorem prefixRaoBlackwellStatistic_eq_integral {N : I → ℕ} (lambda : I → ℝ≥0) (T : PrefixFamily X → ℝ) (hT : Measurable T) (zOver : ℝ) (pools : FixedPools X N) : prefixRaoBlackwellStatistic lambda T zOver pools = ∫ counts : I → ℕ, cappedPrefixStatistic T zOver (fun i ↦ (pools i, counts i)) ∂(Measure.pi (fun i ↦ poissonMeasure (lambda i))) := by -- Follow the two-pool theorem: unfold `kernelMean`, rewrite -- `mechanismKernel_apply`, then use `integral_map`. unfold prefixRaoBlackwellStatistic kernelMean independentPoissonCountKernel rw [mechanismKernel_apply _ (show Measurable (fun z : FixedPools X N × (I → ℕ) ↦ fun i ↦ (z.1 i, z.2 i)) from by fun_prop) pools] exact integral_map (show Measurable (fun counts : I → ℕ ↦ fun i ↦ (pools i, counts i)) from by fun_prop).aemeasurable (measurable_cappedPrefixStatistic hT zOver).aestronglyMeasurable -
sqRisk_prefixRaoBlackwellStatistic_le_cappedtheorem — Given coordinatewise probability laws, Poisson intensities, pool capacities, a measurable prefix statistic, a statistic confined to an interval, and an overflow value in that interval, conditional averaging cannot increase squared risk relative to the capped randomized experiment, for any target.hypothesesI :sharedType uII → Type uXP :(i : I) → Measure (X i)∀ i, IsProbabilityMeasure (P i)lambda :I → ℝ≥0N :I → ℕT :PrefixFamily X → ℝhT :a b theta zOver :ℝhTmem :∀ s, T s ∈ Icc a bhzOver :zOver ∈ Icc a bconclusionsqRisk (fixedPoolsLaw P N) (prefixRaoBlackwellStatistic lambda T zOver) theta≤ sqRisk (randomizedPoolsLaw P lambda N) (cappedPrefixStatistic T zOver) thetaProof (Lean source)
theorem sqRisk_prefixRaoBlackwellStatistic_le_capped (P : (i : I) → Measure (X i)) [∀ i, IsProbabilityMeasure (P i)] (lambda : I → ℝ≥0) (N : I → ℕ) {T : PrefixFamily X → ℝ} (hT : Measurable T) {a b theta zOver : ℝ} (hTmem : ∀ s, T s ∈ Icc a b) (hzOver : zOver ∈ Icc a b) : sqRisk (fixedPoolsLaw P N) (prefixRaoBlackwellStatistic lambda T zOver) theta ≤ sqRisk (randomizedPoolsLaw P lambda N) (cappedPrefixStatistic T zOver) theta := by -- Bound the capped statistic by `max |a| |b|`, apply -- `sqRisk_kernelMean_le_comp`, and rewrite the composed law. letI : IsProbabilityMeasure (fixedPoolsLaw P N) := by unfold fixedPoolsLaw infer_instance have hCappedBound : UniformlyBounded (cappedPrefixStatistic (N := N) T zOver) := by refine ⟨max |a| |b|, (abs_nonneg a).trans (le_max_left _ _), ?_⟩ intro z by_cases h : ∀ i, (z i).2 ≤ N i · rw [cappedPrefixStatistic, dif_pos h] exact abs_le_max_abs_abs (hTmem _).1 (hTmem _).2 · rw [cappedPrefixStatistic, dif_neg h] exact abs_le_max_abs_abs hzOver.1 hzOver.2 calc sqRisk (fixedPoolsLaw P N) (prefixRaoBlackwellStatistic lambda T zOver) theta ≤ sqRisk (independentPoissonCountKernel (X := X) lambda ∘ₘ fixedPoolsLaw P N) (cappedPrefixStatistic T zOver) theta := by exact sqRisk_kernelMean_le_comp (fixedPoolsLaw P N) (independentPoissonCountKernel lambda) (measurable_cappedPrefixStatistic hT zOver) hCappedBound theta _ = sqRisk (randomizedPoolsLaw P lambda N) (cappedPrefixStatistic T zOver) theta := by rw [independentPoissonCountKernel_comp_fixedPoolsLaw] -
sqRisk_cappedPrefixStatistic_restrict_nonoverflow_eqtheorem — Given coordinatewise probability laws, Poisson intensities, pool capacities, a measurable prefix statistic, an overflow value, and a target, capped risk on joint nonoverflow equals restricted untruncated-prefix risk.hypothesesI :sharedType uII → Type uXP :(i : I) → Measure (X i)∀ i, IsProbabilityMeasure (P i)lambda :I → ℝ≥0N :I → ℕT :PrefixFamily X → ℝhT :zOver theta :ℝconclusionsqRisk ((randomizedPoolsLaw P lambda N).restrict (nonoverflowSet (X := X) N)) (cappedPrefixStatistic T zOver) theta= sqRisk ((independentPoissonPrefixLaw P lambda).restrict {s : PrefixFamily X | ∀ i, (s i).count ≤ N i}) T thetaProof (Lean source)
theorem sqRisk_cappedPrefixStatistic_restrict_nonoverflow_eq (P : (i : I) → Measure (X i)) [∀ i, IsProbabilityMeasure (P i)] (lambda : I → ℝ≥0) (N : I → ℕ) {T : PrefixFamily X → ℝ} (hT : Measurable T) (zOver theta : ℝ) : sqRisk ((randomizedPoolsLaw P lambda N).restrict (nonoverflowSet (X := X) N)) (cappedPrefixStatistic T zOver) theta = sqRisk ((independentPoissonPrefixLaw P lambda).restrict {s : PrefixFamily X | ∀ i, (s i).count ≤ N i}) T theta := by -- Pull the loss back through `totalizedPrefixFamily` using `integral_map`; -- on the restricted source use `cappedPrefixStatistic_eq_off_overflow`. let overflow : PrefixFamily X := fun _ ↦ ⟨0, Fin.elim0⟩ unfold sqRisk rw [← map_totalizedPrefixFamily_restrict_nonoverflow P lambda N overflow] rw [integral_map (μ := (randomizedPoolsLaw P lambda N).restrict (nonoverflowSet (X := X) N)) (φ := totalizedPrefixFamily overflow) (f := fun s : PrefixFamily X ↦ (T s - theta) ^ 2) (measurable_totalizedPrefixFamily overflow).aemeasurable ((hT.sub measurable_const).pow_const 2).aestronglyMeasurable] apply integral_congr_ae filter_upwards [ae_restrict_mem (measurableSet_nonoverflowSet N)] with z hz rw [nonoverflowSet_eq_compl_overflowSet] at hz rw [cappedPrefixStatistic_eq_off_overflow T zOver overflow z hz] -
sqRisk_independentPoissonPrefixLaw_restrict_nonoverflow_letheorem — Given coordinatewise probability laws, Poisson intensities, pool capacities, a measurable prefix statistic, a uniform bound, and a target, restricting to coordinatewise nonoverflow cannot increase untruncated Poissonized squared risk.hypothesesI :sharedType uII → Type uXP :(i : I) → Measure (X i)∀ i, IsProbabilityMeasure (P i)lambda :I → ℝ≥0N :I → ℕT :PrefixFamily X → ℝhT :hTb :theta :ℝconclusionsqRisk ((independentPoissonPrefixLaw P lambda).restrict {s : PrefixFamily X | ∀ i, (s i).count ≤ N i}) T theta≤ sqRisk (independentPoissonPrefixLaw P lambda) T thetaProof (Lean source)
theorem sqRisk_independentPoissonPrefixLaw_restrict_nonoverflow_le (P : (i : I) → Measure (X i)) [∀ i, IsProbabilityMeasure (P i)] (lambda : I → ℝ≥0) (N : I → ℕ) {T : PrefixFamily X → ℝ} (hT : Measurable T) (hTb : UniformlyBounded T) (theta : ℝ) : sqRisk ((independentPoissonPrefixLaw P lambda).restrict {s : PrefixFamily X | ∀ i, (s i).count ≤ N i}) T theta ≤ sqRisk (independentPoissonPrefixLaw P lambda) T theta := by -- Establish bounded-loss integrability, split the full measure into the -- measurable good set and its complement, and discard the nonnegative term. obtain ⟨M, hM, hTb⟩ := hTb let μ : Measure (PrefixFamily X) := independentPoissonPrefixLaw P lambda letI : IsProbabilityMeasure μ := by unfold μ independentPoissonPrefixLaw infer_instance let s : Set (PrefixFamily X) := {z | ∀ i, (z i).count ≤ N i} have hs : MeasurableSet s := measurableSet_prefixNonoverflowSet N 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)) -
overflowSet_measureReal_le_sum_poisson_tailstheorem — Given coordinatewise probability laws, Poisson intensities, and pool capacities, the probability of any overflow is bounded by the sum of marginal Poisson upper-tail probabilities.hypothesesI :sharedType uII → Type uXP :(i : I) → Measure (X i)∀ i, IsProbabilityMeasure (P i)lambda :I → ℝ≥0N :I → ℕconclusion(randomizedPoolsLaw P lambda N).real (overflowSet (X := X) N)Proof (Lean source)
theorem overflowSet_measureReal_le_sum_poisson_tails (P : (i : I) → Measure (X i)) [∀ i, IsProbabilityMeasure (P i)] (lambda : I → ℝ≥0) (N : I → ℕ) : (randomizedPoolsLaw P lambda N).real (overflowSet (X := X) N) ≤ ∑ i, (poissonMeasure (lambda i)).real (Ioi (N i)) := by -- Rewrite overflow as `⋃ i, {z | N i < (z i).2}`, apply -- `measureReal_iUnion_fintype_le`, and evaluate each pi-coordinate cylinder. let μ : Measure (RandomizedPools X N) := randomizedPoolsLaw P lambda N letI : IsProbabilityMeasure μ := by unfold μ randomizedPoolsLaw infer_instance let E : I → Set (RandomizedPools X N) := fun i ↦ (fun z ↦ (z i).2) ⁻¹' Ioi (N i) have hOverflow : overflowSet (X := X) N = ⋃ i, E i := by ext z simp [overflowSet, E] have hcoord (i : I) : μ.real (E i) = (poissonMeasure (lambda i)).real (Ioi (N i)) := by have hset : MeasurableSet {w : (Fin (N i) → X i) × ℕ | N i < w.2} := measurableSet_Ioi.preimage measurable_snd have hEval : Measure.map (Function.eval i) μ = (Measure.pi (fun _ : Fin (N i) ↦ P i)).prod (poissonMeasure (lambda i)) := by simpa [μ, randomizedPoolsLaw] using (measurePreserving_eval (μ := fun i ↦ (Measure.pi (fun _ : Fin (N i) ↦ P i)).prod (poissonMeasure (lambda i))) i).map_eq calc μ.real (E i) = (Measure.map (Function.eval i) μ).real {w : (Fin (N i) → X i) × ℕ | N i < w.2} := by rw [map_measureReal_apply (measurable_pi_apply i) hset] rfl _ = ((Measure.pi (fun _ : Fin (N i) ↦ P i)).prod (poissonMeasure (lambda i))).real {w : (Fin (N i) → X i) × ℕ | N i < w.2} := by rw [hEval] _ = (poissonMeasure (lambda i)).real (Ioi (N i)) := by rw [show {w : (Fin (N i) → X i) × ℕ | N i < w.2} = (Set.univ : Set (Fin (N i) → X i)) ×ˢ Ioi (N i) by ext w simp] simp rw [show (randomizedPoolsLaw P lambda N) = μ from rfl, hOverflow] exact (measureReal_iUnion_fintype_le μ E).trans_eq (Finset.sum_congr rfl fun i _ ↦ hcoord i)
ThreePool 6 core · 7 supporting This module specializes the finite-family risk theorem to one pool on an alphabet A and two distinct, independently prefixed pools sharing alphabet B and observation law Q. ★ finiteAlphabet_threePoolSharedLaw_risk_le
Direct finite-alphabet three-pool specialization
This module specializes the finite-family risk theorem to one pool on an
alphabet A and two distinct, independently prefixed pools sharing alphabet
B and observation law Q. Capacities and Poisson intensities remain fully
heterogeneous across the three coordinates.
inductive ThreePoolIndex reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
The three-pool index distinguishes one complete pool from two independently randomized shared-alphabet pools. [Its complete coordinate is available](step:complete), [its left shared coordinate is available](step:sharedLeft), and [its right shared coordinate is available](step:sharedRight).
Definition (Lean source)
inductive
ThreePoolIndex :
Type
constructors
complete :
sharedLeft :
sharedRight :
abbrev ThreePoolAlphabet reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given the complete-pool alphabet and the shared-pool alphabet, the three-pool alphabet family assigns the latter independently to both shared coordinates. It is given by the coordinate case split.
Definition (Lean source)
parameters
A :
Type uX
B :
Type uX
def
given by
fun i ↦ match i with | .complete => A | .sharedLeft => B | .sharedRight => B
def threePoolObservationLaw reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given the complete-pool law and the shared-pool law, the three-pool observation-law family assigns the shared law separately to both shared coordinates. It is given by the coordinate case split.
def threePoolCapacity reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given the complete-pool capacity, the left shared-pool capacity, and the right shared-pool capacity, the three-pool capacity function records all three without identifying the shared pools. It is given by the coordinate case split.
Definition (Lean source)
parameters
NComplete NLeft NRight :
ℕ
def
given by
clause 1
| .complete => NComplete
clause 2
| .sharedLeft => NLeft
clause 3
| .sharedRight => NRight
def threePoolIntensity reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
Given the complete-pool intensity, the left shared-pool intensity, and the right shared-pool intensity, the three-pool intensity function records all three independently. It is given by the coordinate case split.
Definition (Lean source)
parameters
lambdaComplete lambdaLeft lambdaRight :
ℝ≥0
def
given by
clause 1
| .complete => lambdaComplete
clause 2
| .sharedLeft => lambdaLeft
clause 3
| .sharedRight => lambdaRight
7 supporting declarations (lemmas, instances)
-
instDecidableEqThreePoolIndexinstance — Decidable equality for the three-pool index distinguishes exactly its equal and unequal coordinate labels. It is given by the nine constructor comparisons.instancegiven byfun x y=> by cases x <;> cases y · exact isTrue rfl · exact isFalse (by intro h; cases h) · exact isFalse (by intro h; cases h) · exact isFalse (by intro h; cases h) · exact isTrue rfl · exact isFalse (by intro h; cases h) · exact isFalse (by intro h; cases h) · exact isFalse (by intro h; cases h) · exact isTrue rfl -
instFintypeThreePoolIndexinstance — The three-pool index has a finite enumeration. The enumeration is given and its completeness certificate is given.instancegiven byclause 1elems := {.complete, .sharedLeft, .sharedRight}clause 2complete i := by cases i <;> simp -
threePoolAlphabetMeasurableSpaceinstance — Given a complete-pool alphabet and a shared-pool alphabet, the coordinatewise measurable-space structure is inherited from the corresponding alphabet. It is given by the three coordinate cases.parametersinstancegiven byclause 1| .complete => inferInstanceclause 2| .sharedLeft => inferInstanceclause 3| .sharedRight => inferInstance -
threePoolAlphabetFintypeinstance — Given a complete-pool alphabet and a shared-pool alphabet, the coordinatewise finite-type structure is inherited from the corresponding alphabet. It is given by the three coordinate cases.parametersinstancegiven byclause 1| .complete => inferInstanceclause 2| .sharedLeft => inferInstanceclause 3| .sharedRight => inferInstance -
threePoolAlphabetDecidableEqinstance — Given a complete-pool alphabet and a shared-pool alphabet, the coordinatewise decidable-equality structure is inherited from the corresponding alphabet. It is given by the three coordinate cases.parametersinstancegiven byclause 1| .complete => inferInstanceclause 2| .sharedLeft => inferInstanceclause 3| .sharedRight => inferInstance -
threePoolAlphabetMeasurableSingletonClassinstance — Given a complete-pool alphabet and a shared-pool alphabet, the coordinatewise measurable-singleton structure is inherited from the corresponding alphabet. It is given by the three coordinate cases.parametersA :Type uXB :Type uXi :instancegiven byclause 1| .complete => inferInstanceclause 2| .sharedLeft => inferInstanceclause 3| .sharedRight => inferInstance -
threePoolObservationLawIsProbabilityMeasureinstance — Given the complete-pool law, the shared-pool law, and a coordinate, the assigned observation law is a probability measure. It is given by the coordinate case split.parametersinstancethreePoolObservationLawIsProbabilityMeasure P Q i :given byby cases i <;> simp only [threePoolObservationLaw] <;> infer_instance
Transfer 1 core · 2 supporting This module turns a bounded statistic for heterogeneous independent Poisson prefixes into a total measurable statistic for fixed finite pools. ★ finite_prefix_transfer
Finite-prefix risk transfer for independent product pools
This module turns a bounded statistic for heterogeneous independent Poisson prefixes into a total measurable statistic for fixed finite pools. It controls zero-output overflow by marginal Poisson tails and specializes those tails when each Poisson mean is one eighth of its pool size.
theorem finite_prefix_transfer reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix.FiniteFamily
For a finite coordinate type, coordinatewise observation spaces, coordinatewise probability laws, fixed pool capacities, a prefix statistic, its measurability, its values between minus one and one, a target, a proposed risk bound, the target's membership between minus one and one, and the Poissonized squared-risk bound, finite independent prefix averaging at one-eighth intensities is measurable, remains between minus one and one, and has fixed-pool squared risk at most that bound plus the sum over coordinates of the exponential of minus the pool capacity. Here each coordinate's Poisson mean is one eighth of its pool capacity and the averaged statistic outputs zero whenever some Poisson count exceeds its capacity.
Formal statement
hypotheses
I :
∀ i, MeasurableSpace (X i)
P :
∀ i, Measure (X i)
∀ i, IsProbabilityMeasure (P i)
N :
I → Nat
T :
PrefixFamily X → Real
hT :
hTmem :
∀ s, T s ∈ Icc (-1) 1
theta Ab :
htheta :
theta ∈ Icc (-1) 1
conclusion
conclusion 1
conclusion 2
s :
conclusion 3
sqRisk (fixedPoolsLaw P N) (prefixRaoBlackwellStatistic (N := N) (fun i => (N i : NNReal) / 8) T 0) theta
Proof (Lean source)
theorem finite_prefix_transfer {I : Type*} [Fintype I]
{X : I → Type*} [∀ i, MeasurableSpace (X i)]
(P : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (P i)]
(N : I → Nat) {T : PrefixFamily X → Real}
(hT : Measurable T) (hTmem : ∀ s, T s ∈ Icc (-1) 1)
{theta Ab : Real} (htheta : theta ∈ Icc (-1) 1)
(hA : sqRisk (independentPoissonPrefixLaw P (fun i => (N i : NNReal) / 8)) T theta ≤ Ab) :
Measurable (prefixRaoBlackwellStatistic (N := N) (fun i => (N i : NNReal) / 8) T 0) ∧
(∀ s, prefixRaoBlackwellStatistic (N := N) (fun i => (N i : NNReal) / 8) T 0 s ∈ Icc
(-1) 1) ∧
sqRisk (fixedPoolsLaw P N)
(prefixRaoBlackwellStatistic (N := N) (fun i => (N i : NNReal) / 8) T 0) theta ≤
Ab + ∑ i, exp (-(N i : Real)) := by
classical
have hCb : ∀ z : RandomizedPools X N, |cappedPrefixStatistic T 0 z| ≤ 1 := by
intro z
by_cases hz : ∀ i, (z i).2 ≤ N i
· rw [cappedPrefixStatistic, dif_pos hz]
exact abs_le.mpr (hTmem _)
· rw [cappedPrefixStatistic, dif_neg hz]
norm_num
refine ⟨?_, ?_, ?_⟩
· fun_prop
· intro s
exact abs_le.mp (abs_kernelMean_le (independentPoissonCountKernel _)
hCb s)
· calc
_ ≤ sqRisk (independentPoissonPrefixLaw P (fun i => (N i : NNReal) / 8)) T theta +
∑ i, (poissonMeasure ((N i : NNReal) / 8)).real (Ioi (N i)) :=
zero_overflow_prefix_risk P _ N hT hTmem htheta
_ ≤ Ab + ∑ i, exp (-(N i : Real)) :=
add_le_add hA (Finset.sum_le_sum (fun i _ => eighth_pool_poisson_overflow (N i)))
2 supporting declarations (lemmas, instances)
-
zero_overflow_prefix_risktheorem — For a finite coordinate type, coordinatewise observation spaces, coordinatewise probability laws, Poisson intensities, fixed pool capacities, a prefix statistic, its measurability, its values between minus one and one, a target, and that target's membership between minus one and one, the squared risk of finite-prefix averaging with zero output on overflow is at most the Poissonized risk plus the sum of the marginal overflow probabilities.hypothesesI :∀ i, MeasurableSpace (X i)P :∀ i, Measure (X i)∀ i, IsProbabilityMeasure (P i)lambda :I → NNRealN :I → NatT :PrefixFamily X → RealhT :hTmem :∀ s, T s ∈ Icc (-1) 1theta :htheta :theta ∈ Icc (-1) 1conclusionsqRisk (fixedPoolsLaw P N) (prefixRaoBlackwellStatistic lambda T 0) theta≤ sqRisk (independentPoissonPrefixLaw P lambda) T thetaProof (Lean source)
theorem zero_overflow_prefix_risk {I : Type*} [Fintype I] {X : I → Type*} [∀ i, MeasurableSpace (X i)] (P : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (P i)] (lambda : I → NNReal) (N : I → Nat) {T : PrefixFamily X → Real} (hT : Measurable T) (hTmem : ∀ s, T s ∈ Icc (-1) 1) {theta : Real} (htheta : theta ∈ Icc (-1) 1) : sqRisk (fixedPoolsLaw P N) (prefixRaoBlackwellStatistic lambda T 0) theta ≤ sqRisk (independentPoissonPrefixLaw P lambda) T theta + ∑ i, (poissonMeasure (lambda i)).real (Ioi (N i)) := by classical have hTb : UniformlyBounded T := ⟨1, by norm_num, fun s => abs_le.mpr (hTmem s)⟩ have hCb : ∀ z : RandomizedPools X N, |cappedPrefixStatistic T 0 z| ≤ 1 := by intro z by_cases hz : ∀ i, (z i).2 ≤ N i · rw [cappedPrefixStatistic, dif_pos hz] exact abs_le.mpr (hTmem _) · rw [cappedPrefixStatistic, dif_neg hz] norm_num let mu := randomizedPoolsLaw P lambda N let : IsProbabilityMeasure mu := by dsimp [mu, randomizedPoolsLaw] infer_instance let good := nonoverflowSet (X := X) N have hgood : MeasurableSet good := measurableSet_nonoverflowSet N have hInt : Integrable (fun z => (cappedPrefixStatistic T 0 z - theta) ^ 2) mu := by apply Integrable.of_bound (((measurable_cappedPrefixStatistic hT 0).sub measurable_const).pow_const 2 ).aestronglyMeasurable 4 filter_upwards with z rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] have hdist : |cappedPrefixStatistic T 0 z - theta| ≤ 2 := (abs_sub _ _).trans (by have ht := abs_le.mpr htheta linarith [hCb z]) change (cappedPrefixStatistic T 0 z - theta) ^ 2 ≤ 4 nlinarith [sq_abs (cappedPrefixStatistic T 0 z - theta), abs_nonneg (cappedPrefixStatistic T 0 z - theta)] have hsplit : sqRisk mu (cappedPrefixStatistic T 0) theta = sqRisk (mu.restrict good) (cappedPrefixStatistic T 0) theta + sqRisk (mu.restrict goodᶜ) (cappedPrefixStatistic T 0) theta := by unfold sqRisk conv_lhs => rw [← Measure.restrict_add_restrict_compl (μ := mu) hgood, integral_add_measure hInt.restrict hInt.restrict] have hcomp : goodᶜ = overflowSet (X := X) N := by simp only [good, nonoverflowSet_eq_compl_overflowSet, compl_compl] have hbad : sqRisk (mu.restrict (overflowSet (X := X) N)) (cappedPrefixStatistic T 0) theta = theta ^ 2 * mu.real (overflowSet (X := X) N) := by unfold sqRisk have hae : ∀ᵐ z ∂mu.restrict (overflowSet (X := X) N), (cappedPrefixStatistic T 0 z - theta) ^ 2 = theta ^ 2 := by filter_upwards [ae_restrict_mem (measurableSet_overflowSet N)] with z hz obtain ⟨i, hi⟩ := hz rw [cappedPrefixStatistic, dif_neg (fun hz => (Nat.not_lt_of_ge (hz i)) hi)] ring rw [integral_congr_ae hae, integral_const] simp only [smul_eq_mul, measureReal_def, Measure.restrict_apply_univ] ring have hthetaSq : theta ^ 2 ≤ 1 := by have ht := abs_le.mpr htheta nlinarith [sq_abs theta, abs_nonneg theta] calc _ ≤ sqRisk mu (cappedPrefixStatistic T 0) theta := sqRisk_prefixRaoBlackwellStatistic_le_capped P lambda N hT hTmem (by norm_num) _ = sqRisk ((independentPoissonPrefixLaw P lambda).restrict {s : PrefixFamily X | ∀ i, (s i).count ≤ N i}) T theta + theta ^ 2 * mu.real (overflowSet (X := X) N) := by rw [hsplit, hcomp, hbad] rw [sqRisk_cappedPrefixStatistic_restrict_nonoverflow_eq P lambda N hT 0 theta] _ ≤ sqRisk (independentPoissonPrefixLaw P lambda) T theta + mu.real (overflowSet (X := X) N) := add_le_add (sqRisk_independentPoissonPrefixLaw_restrict_nonoverflow_le P lambda N hT hTb theta) (by simpa using (mul_le_mul_of_nonneg_right hthetaSq (by positivity : 0 ≤ mu.real (overflowSet (X := X) N)))) _ ≤ _ := add_le_add le_rfl (overflowSet_measureReal_le_sum_poisson_tails P lambda N) -
eighth_pool_poisson_overflowtheorem — For a pool capacity, a Poisson prefix whose mean is one eighth of that capacity has overflow probability at most the negative-capacity exponential.Proof (Lean source)
theorem eighth_pool_poisson_overflow (N : Nat) : (poissonMeasure ((N : NNReal) / 8)).real (Ioi N) ≤ exp (-(N : Real)) := by have htail := poisson_upper_tail_mul_exp_le ((N : NNReal) / 8) N (r := 7) (by norm_num) have hlog : 15 / 8 ≤ log 8 := by have hh : log (8 : Real) = 3 * log 2 := by rw [show (8 : Real) = 2 ^ 3 by norm_num, Real.log_pow] norm_num rw [hh] linarith [Real.log_two_gt_d9] have hmul : exp (-(N : Real)) * exp (-7 * (((N : NNReal) / 8 : NNReal) : Real)) = exp (-(15 / 8) * (N : Real)) := by rw [← Real.exp_add] congr 1 simp only [NNReal.coe_div, NNReal.coe_natCast, NNReal.coe_ofNat] ring apply (mul_le_mul_iff_left₀ (Real.exp_pos (-7 * (((N : NNReal) / 8 : NNReal) : Real)))).mp calc _ ≤ exp (-log (1 + 7) * (N : Real)) := htail _ ≤ exp (-(15 / 8) * (N : Real)) := by apply Real.exp_le_exp.mpr norm_num only at * nlinarith [(Nat.cast_nonneg N : (0 : Real) ≤ N)] _ = _ := hmul.symm