Stat.FiniteRaoBlackwell.Poisson.IndependentPrefix
This roll-up module exports exact laws, capped implementations, conditional averaging, and depoissonization bounds for independent Poisson prefixes.
ProductPools 24 core · 26 supporting · 4 submodules 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 RandomScaleTransfer 22 core · 21 supporting · 7 submodules This roll-up module exports ordered retention for two unequal marked-Poisson pools with a shared random scale, prior-predictive count-failure bounds, bounded-loss decision transfer, and the resulting fuzzy-prior minimax
Basic 10 core · 7 supporting This module provides the measurable sample spaces and deterministic maps used to Poissonize two independent fixed iid pools. ★ map_totalizedPrefixPair_restrict_nonoverflow
Independent unequal Poisson prefixes
This module provides the measurable sample spaces and deterministic maps used to Poissonize two independent fixed iid pools. The pools may have different capacities and observation spaces. It also identifies the exact joint law of the two untruncated Poisson prefixes and the jointly nonoverflowing part of the capped construction.
abbrev FixedPools reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix
Given the first pool capacity and the second pool capacity, two fixed observation pools are given by ordered pools whose capacities may differ. They are represented by the product of the two ordered pools.
abbrev RandomizedPools reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix
Given the first pool capacity and the second pool capacity, the randomized two-pool experiment attaches an independent requested prefix length to each fixed pool. It is represented by the pair of pool-length pairs.
def fixedPoolsLaw reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix
Given a probability law for the first observations, a probability law for the second observations, the first pool capacity, and the second pool capacity, the independent fixed-pool law is the product of the two iid pool laws. It is given by their product measure.
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
P :
Q :
NX NY :
ℕ
def
def randomizedPoolsLaw reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix
Given probability laws for the first and second observations, the first Poisson intensity, the second Poisson intensity, the first pool capacity, and the second pool capacity, the randomized-pool law has independent iid pools and independent Poisson requested lengths. It is given by the product of both pool-count laws.
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
P :
Q :
lambdaX lambdaY :
ℝ≥0
NX NY :
ℕ
def
given by
((Measure.pi (fun _ : Fin NX ↦ P)).prod (poissonMeasure lambdaX)).prod ((Measure.pi (fun _ : Fin NY ↦ Q)).prod (poissonMeasure lambdaY))
def independentPoissonPrefixLaw reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix
Given a probability law for the first observations, a probability law for the second observations, the first Poisson intensity, and the second Poisson intensity, the independent Poisson-prefix law is the joint law of two untruncated iid prefixes. It is given by their product law.
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
P :
Q :
lambdaX lambdaY :
ℝ≥0
def
given by
def nonoverflowSet reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix
Given the first pool capacity and the second pool capacity, the joint nonoverflow event says that both requested prefixes fit in their respective pools. It is given by the conjunction of the two capacity bounds.
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
NX NY :
ℕ
def
given by
{z | z.1.2 ≤ NX ∧ z.2.2 ≤ NY}
def overflowSet reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix
Given the first pool capacity and the second pool capacity, the overflow event says that at least one requested prefix is too long. It is given by the union of the two marginal overflow events.
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
NX NY :
ℕ
def
given by
{z | NX < z.1.2} ∪ {z | NY < z.2.2}
def totalizedPrefixPair reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix
Given a fallback first prefix, a fallback second prefix, and a randomized two-pool outcome, the totalized prefix pair retains both requested prefixes when possible and uses the corresponding fallback otherwise. It is given by applying the one-pool totalization in each coordinate.
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
NX NY :
ℕ
overflowX :
overflowY :
z :
RandomizedPools (X := X) (Y := Y) NX NY
def
given by
(totalizedPrefix overflowX z.1.1 z.1.2, totalizedPrefix overflowY z.2.1 z.2.2)
def cappedPrefixStatistic reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix
Given a two-prefix statistic, a fallback value, and a randomized two-pool outcome, the capped-prefix statistic uses the genuine prefixes when both fit and the fallback when either overflows. It is given by the two capacity tests.
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
NX NY :
ℕ
T :
(FiniteSample X × FiniteSample Y) → ℝ
zOver :
ℝ
z :
RandomizedPools (X := X) (Y := Y) NX NY
def
cappedPrefixStatistic T zOver z :
ℝ
given by
if hX : z.1.2
≤ NX then if hY : z.2.2 ≤ NY then T (prefixOfLE z.1.1 z.1.2 hX, prefixOfLE z.2.1 z.2.2 hY) else zOver else zOver
theorem map_totalizedPrefixPair_restrict_nonoverflow reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix
Given probability laws for the first and second pools, the first and second Poisson intensities, the first and second pool capacities, and fallback first and second prefixes, mapping the jointly nonoverflowing fixed pools to their totalized prefixes gives the correspondingly restricted product Poisson-prefix law.
Formal statement
hypotheses
X :
Type uX
Y :
Type uY
P :
Q :
lambdaX lambdaY :
ℝ≥0
NX NY :
ℕ
overflowX :
overflowY :
conclusion
Measure.map (totalizedPrefixPair overflowX overflowY) ((randomizedPoolsLaw P Q lambdaX lambdaY NX NY).restrict (nonoverflowSet (X := X) (Y := Y) NX NY))
Proof (Lean source)
theorem map_totalizedPrefixPair_restrict_nonoverflow
(P : Measure X) [IsProbabilityMeasure P]
(Q : Measure Y) [IsProbabilityMeasure Q]
(lambdaX lambdaY : ℝ≥0) (NX NY : ℕ)
(overflowX : FiniteSample X) (overflowY : FiniteSample Y) :
Measure.map (totalizedPrefixPair overflowX overflowY)
((randomizedPoolsLaw P Q lambdaX lambdaY NX NY).restrict
(nonoverflowSet (X := X) (Y := Y) NX NY)) =
(independentPoissonPrefixLaw P Q lambdaX lambdaY).restrict
((FiniteSample.count ⁻¹' Iic NX) ×ˢ
(FiniteSample.count ⁻¹' Iic NY)) := by
-- Rewrite `nonoverflowSet` as the product of the two marginal good events,
-- commute product and restriction with `Measure.prod_restrict`, and use
-- `Measure.map_prod_map`. Each marginal map is then exactly
-- `map_totalizedPrefix_restrict_nonoverflow`; fold the target product
-- restriction back with the same product/restriction identity.
have hset : nonoverflowSet (X := X) (Y := Y) NX NY =
(snd ⁻¹' Iic NX) ×ˢ (snd ⁻¹' Iic NY) := by
ext z
simp [nonoverflowSet]
rw [hset]
unfold randomizedPoolsLaw independentPoissonPrefixLaw totalizedPrefixPair
rw [← Measure.prod_restrict]
change Measure.map
(map
(fun z : (Fin NX → X) × ℕ ↦ totalizedPrefix overflowX z.1 z.2)
(fun z : (Fin NY → Y) × ℕ ↦ totalizedPrefix overflowY z.1 z.2))
_ = _
rw [← Measure.map_prod_map _ _ (measurable_totalizedPrefix overflowX)
(measurable_totalizedPrefix overflowY)]
rw [map_totalizedPrefix_restrict_nonoverflow P lambdaX NX overflowX,
map_totalizedPrefix_restrict_nonoverflow Q lambdaY NY overflowY,
Measure.prod_restrict]
7 supporting declarations (lemmas, instances)
-
measurableSet_nonoverflowSettheorem — Given the first pool capacity and the second pool capacity, the joint nonoverflow event is measurable.hypothesesX :sharedType uXY :sharedType uYNX NY :ℕconclusionMeasurableSet (nonoverflowSet (X := X) (Y := Y) NX NY)Proof (Lean source)
theorem measurableSet_nonoverflowSet (NX NY : ℕ) : MeasurableSet (nonoverflowSet (X := X) (Y := Y) NX NY) := by change MeasurableSet (((fun z : RandomizedPools (X := X) (Y := Y) NX NY ↦ z.1.2) ⁻¹' Iic NX) ∩ ((fun z : RandomizedPools (X := X) (Y := Y) NX NY ↦ z.2.2) ⁻¹' Iic NY)) have hX : Measurable (fun z : RandomizedPools (X := X) (Y := Y) NX NY ↦ z.1.2) := by fun_prop have hY : Measurable (fun z : RandomizedPools (X := X) (Y := Y) NX NY ↦ z.2.2) := by fun_prop exact (hX measurableSet_Iic).inter (hY measurableSet_Iic) -
measurableSet_overflowSettheorem — Given the first pool capacity and the second pool capacity, the union of the two overflow events is measurable.hypothesesX :sharedType uXY :sharedType uYNX NY :ℕconclusionMeasurableSet (overflowSet (X := X) (Y := Y) NX NY)Proof (Lean source)
theorem measurableSet_overflowSet (NX NY : ℕ) : MeasurableSet (overflowSet (X := X) (Y := Y) NX NY) := by change MeasurableSet (((fun z : RandomizedPools (X := X) (Y := Y) NX NY ↦ z.1.2) ⁻¹' Ioi NX) ∪ ((fun z : RandomizedPools (X := X) (Y := Y) NX NY ↦ z.2.2) ⁻¹' Ioi NY)) have hX : Measurable (fun z : RandomizedPools (X := X) (Y := Y) NX NY ↦ z.1.2) := by fun_prop have hY : Measurable (fun z : RandomizedPools (X := X) (Y := Y) NX NY ↦ z.2.2) := by fun_prop exact (hX measurableSet_Ioi).union (hY measurableSet_Ioi) -
nonoverflowSet_eq_compl_overflowSettheorem — Given the first pool capacity and the second pool capacity, joint nonoverflow is exactly the complement of either marginal overflow.hypothesesX :sharedType uXY :sharedType uYNX NY :ℕconclusionnonoverflowSet (X := X) (Y := Y) NX NY = (overflowSet (X := X) (Y := Y) NX NY)ᶜProof (Lean source)
theorem nonoverflowSet_eq_compl_overflowSet (NX NY : ℕ) : nonoverflowSet (X := X) (Y := Y) NX NY = (overflowSet (X := X) (Y := Y) NX NY)ᶜ := by ext z simp [nonoverflowSet, overflowSet, not_lt] -
measurable_totalizedPrefixPairtheorem — Given a fallback first prefix and a fallback second prefix, the totalized prefix pair is measurable.hypothesesX :sharedType uXY :sharedType uYNX NY :ℕoverflowX :overflowY :conclusionMeasurable (totalizedPrefixPair (NX := NX) (NY := NY) overflowX overflowY)Proof (Lean source)
@[fun_prop] theorem measurable_totalizedPrefixPair {NX NY : ℕ} (overflowX : FiniteSample X) (overflowY : FiniteSample Y) : Measurable (totalizedPrefixPair (NX := NX) (NY := NY) overflowX overflowY) := by exact (measurable_totalizedPrefix overflowX).prodMap (measurable_totalizedPrefix overflowY) -
measurable_cappedPrefixStatistictheorem — Given a measurable two-prefix statistic and a fallback value, the capped-prefix statistic is measurable on the two fixed pools and their independent requested lengths.hypothesesX :sharedType uXY :sharedType uYNX NY :ℕT :(FiniteSample X × FiniteSample Y) → ℝhT :zOver :ℝconclusionMeasurable (cappedPrefixStatistic (NX := NX) (NY := NY) T zOver)Proof (Lean source)
@[fun_prop] theorem measurable_cappedPrefixStatistic {NX NY : ℕ} {T : (FiniteSample X × FiniteSample Y) → ℝ} (hT : Measurable T) (zOver : ℝ) : Measurable (cappedPrefixStatistic (NX := NX) (NY := NY) T zOver) := by -- First expose the two count coordinates using -- `measurable_from_prod_countable_left` (twice, after reassociation). -- For fixed counts, split on the two bounds; the genuine branch is `hT` -- composed with the product of the two `measurable_prefixOfLE` maps, while -- every overflow branch is constant. let g : ((((Fin NX → X) × ℕ) × (Fin NY → Y)) × ℕ) → ℝ := fun z ↦ cappedPrefixStatistic T zOver ((z.1.1.1, z.1.1.2), (z.1.2, z.2)) have hg : Measurable g := by apply measurable_from_prod_countable_left intro n let f : (((Fin NX → X) × (Fin NY → Y)) × ℕ) → ℝ := fun z ↦ cappedPrefixStatistic T zOver ((z.1.1, z.2), (z.1.2, n)) have hf : Measurable f := by apply measurable_from_prod_countable_left intro m by_cases hX : m ≤ NX · by_cases hY : n ≤ NY · rw [show (fun z ↦ f (z, m)) = T ∘ map (fun x ↦ prefixOfLE x m hX) (fun y ↦ prefixOfLE y n hY) by funext z simp only [f, cappedPrefixStatistic, hX, hY, dite_true, Function.comp_apply] congr] exact hT.comp ((measurable_prefixOfLE (X := X) hX).prodMap (measurable_prefixOfLE (X := Y) hY)) · simpa [f, cappedPrefixStatistic, hX, hY] using (measurable_const : Measurable (fun _ : (Fin NX → X) × (Fin NY → Y) ↦ zOver)) · simpa [f, cappedPrefixStatistic, hX] using (measurable_const : Measurable (fun _ : (Fin NX → X) × (Fin NY → Y) ↦ zOver)) exact hf.comp (((measurable_fst.comp measurable_fst).prodMk measurable_snd).prodMk (measurable_snd.comp measurable_fst)) exact hg.comp ((measurable_fst.prodMk (measurable_fst.comp measurable_snd)).prodMk (measurable_snd.comp measurable_snd)) -
cappedPrefixStatistic_eq_off_overflowtheorem — Given a two-prefix statistic, a fallback value, fallback first and second prefixes, a randomized two-pool outcome, and a certificate of no overflow, the capped statistic equals the statistic of the corresponding totalized prefixes.hypothesesX :sharedType uXY :sharedType uYNX NY :ℕT :(FiniteSample X × FiniteSample Y) → ℝzOver :ℝoverflowX :overflowY :z :RandomizedPools (X := X) (Y := Y) NX NYhz :z ∉ overflowSet (X := X) (Y := Y) NX NYconclusioncappedPrefixStatistic T zOver z = T (totalizedPrefixPair overflowX overflowY z)Proof (Lean source)
theorem cappedPrefixStatistic_eq_off_overflow {NX NY : ℕ} (T : (FiniteSample X × FiniteSample Y) → ℝ) (zOver : ℝ) (overflowX : FiniteSample X) (overflowY : FiniteSample Y) (z : RandomizedPools (X := X) (Y := Y) NX NY) (hz : z ∉ overflowSet (X := X) (Y := Y) NX NY) : cappedPrefixStatistic T zOver z = T (totalizedPrefixPair overflowX overflowY z) := by have hX : z.1.2 ≤ NX := by exact Nat.le_of_not_gt fun h ↦ hz (by simp [overflowSet, h]) have hY : z.2.2 ≤ NY := by exact Nat.le_of_not_gt fun h ↦ hz (by simp [overflowSet, h]) simp [cappedPrefixStatistic, totalizedPrefixPair, totalizedPrefix, cappedPrefix, hX, hY] -
map_independent_streams_eq_independentPoissonPrefixLawtheorem — Given a probability law for the first stream, a probability law for the second stream, the first Poisson intensity, and the second Poisson intensity, mapping independent iid streams to finite prefixes gives exactly the product untruncated-prefix law.hypothesesX :sharedType uXY :sharedType uYP :Q :lambdaX lambdaY :ℝ≥0conclusionMeasure.map (map streamToFiniteSample streamToFiniteSample) ((poissonIIDStreamLaw P lambdaX).prod (poissonIIDStreamLaw Q lambdaY))= independentPoissonPrefixLaw P Q lambdaX lambdaYProof (Lean source)
theorem map_independent_streams_eq_independentPoissonPrefixLaw (P : Measure X) [IsProbabilityMeasure P] (Q : Measure Y) [IsProbabilityMeasure Q] (lambdaX lambdaY : ℝ≥0) : Measure.map (map streamToFiniteSample streamToFiniteSample) ((poissonIIDStreamLaw P lambdaX).prod (poissonIIDStreamLaw Q lambdaY)) = independentPoissonPrefixLaw P Q lambdaX lambdaY := by unfold independentPoissonPrefixLaw finitePoissonSampleLaw rw [← MeasureTheory.Measure.map_prod_map _ _ measurable_streamToFiniteSample measurable_streamToFiniteSample]
Risk 3 core · 8 supporting This module randomizes two independent fixed iid pools by two independent Poisson counts, averages a bounded capped-prefix statistic over those counts, and proves the conditional Jensen contraction and the resulting depo ★ sqRisk_independentPrefixRaoBlackwellStatistic_le
Rao--Blackwell risk transfer for independent unequal prefixes
This module randomizes two independent fixed iid pools by two independent Poisson counts, averages a bounded capped-prefix statistic over those counts, and proves the conditional Jensen contraction and the resulting depoissonization risk bound. Neither the alphabets nor the pool capacities need agree.
def independentPoissonCountKernel reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix
Given the first Poisson intensity and the second Poisson intensity, the independent Poisson-count kernel keeps both fixed pools and independently attaches one requested length to each. It is given by the product Poisson mechanism with the output rearranged into pool-count pairs.
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
NX NY :
ℕ
lambdaX lambdaY :
ℝ≥0
def
independentPoissonCountKernel lambdaX lambdaY :
Kernel (FixedPools (X := X) (Y := Y) NX NY) (RandomizedPools (X := X) (Y := Y) NX NY)
given by
mechanismKernel ((poissonMeasure lambdaX).prod (poissonMeasure lambdaY)) (fun z ↦ ((z.1.1, z.2.1), (z.1.2, z.2.2)))
def independentPrefixRaoBlackwellStatistic reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix
Given the first Poisson intensity, the second Poisson intensity, a two-prefix statistic, and a fallback value, the independent-prefix Rao--Blackwell statistic averages the capped statistic over the two auxiliary Poisson counts conditional on the fixed pools. It is given by the kernel mean.
Definition (Lean source)
parameters
X :
Type uX
Y :
Type uY
NX NY :
ℕ
lambdaX lambdaY :
ℝ≥0
T :
(FiniteSample X × FiniteSample Y) → ℝ
zOver :
ℝ
def
independentPrefixRaoBlackwellStatistic lambdaX lambdaY T zOver :
FixedPools (X := X) (Y := Y) NX NY → ℝ
given by
kernelMean (independentPoissonCountKernel lambdaX lambdaY) (cappedPrefixStatistic T zOver)
theorem sqRisk_independentPrefixRaoBlackwellStatistic_le reviewed
⚑ flagged
Causalean.Stat.FiniteRaoBlackwell.IndependentPoissonPrefix
Given probability laws for the first and second observations, the first and second Poisson intensities, the first and second pool capacities, a measurable two-prefix statistic, an ordered outcome interval, a certificate that the statistic stays in that interval, a target in the interval, and a fallback in the interval, the fixed-pool Rao--Blackwell risk is bounded by the untruncated Poisson-prefix risk plus the squared interval diameter times the two upper tails.
Formal statement
hypotheses
X :
Type uX
Y :
Type uY
P :
Q :
lambdaX lambdaY :
ℝ≥0
NX NY :
ℕ
T :
(FiniteSample X × FiniteSample Y) → ℝ
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 Q NX NY) (independentPrefixRaoBlackwellStatistic lambdaX lambdaY T zOver) theta
≤ sqRisk (independentPoissonPrefixLaw P Q lambdaX lambdaY) T theta
Proof (Lean source)
theorem sqRisk_independentPrefixRaoBlackwellStatistic_le
(P : Measure X) [IsProbabilityMeasure P]
(Q : Measure Y) [IsProbabilityMeasure Q]
(lambdaX lambdaY : ℝ≥0) (NX NY : ℕ)
{T : (FiniteSample X × FiniteSample Y) → ℝ} (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 Q NX NY)
(independentPrefixRaoBlackwellStatistic lambdaX lambdaY T zOver) theta ≤
sqRisk (independentPoissonPrefixLaw P Q lambdaX lambdaY) T theta +
(b - a) ^ 2 *
((poissonMeasure lambdaX).real (Ioi NX) +
(poissonMeasure lambdaY).real (Ioi NY)) := by
-- Start with the conditional contraction and split randomized risk over
-- `nonoverflowSet` and its complement. Rewrite the good contribution with
-- the restricted-risk equality and bound it by untruncated risk. The bad
-- contribution is the constant fallback loss; bound that loss by the
-- squared interval diameter and its event probability by the union bound.
-- `measureReal_union_le` supplies the union bound. Product-event masses
-- reduce to the stated Poisson tails using `Measure.prod_apply` and the
-- probability-one masses of the iid-pool and opposite-arm laws. Follow the
-- decomposition in `sqRisk_raoBlackwellStatistic_le`, with
-- `overflowSet` replacing the one count event.
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 (NX := NX) (NY := NY) T zOver) := by
refine ⟨max |a| |b|, (abs_nonneg a).trans (le_max_left _ _), ?_⟩
intro z
by_cases hX : z.1.2 ≤ NX
· by_cases hY : z.2.2 ≤ NY
· simp only [cappedPrefixStatistic, hX, hY, dite_true]
exact abs_le_max_abs_abs (hTmem _).1 (hTmem _).2
· simp only [cappedPrefixStatistic, hX, hY, dite_true, dite_false]
exact abs_le_max_abs_abs hzOver.1 hzOver.2
· simp only [cappedPrefixStatistic, hX, dite_false]
exact abs_le_max_abs_abs hzOver.1 hzOver.2
let μ : Measure (RandomizedPools (X := X) (Y := Y) NX NY) :=
randomizedPoolsLaw P Q lambdaX lambdaY NX NY
letI : IsProbabilityMeasure μ := by
unfold μ randomizedPoolsLaw
infer_instance
let s : Set (RandomizedPools (X := X) (Y := Y) NX NY) :=
nonoverflowSet (X := X) (Y := Y) NX NY
have hs : MeasurableSet s := measurableSet_nonoverflowSet NX NY
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) (Y := Y) NX NY := 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) (Y := Y) NX NY))
(cappedPrefixStatistic T zOver) theta =
(zOver - theta) ^ 2 *
μ.real (overflowSet (X := X) (Y := Y) NX NY) := by
unfold sqRisk
have hae : ∀ᵐ z ∂μ.restrict (overflowSet (X := X) (Y := Y) NX NY),
(cappedPrefixStatistic T zOver z - theta) ^ 2 =
(zOver - theta) ^ 2 := by
filter_upwards [ae_restrict_mem (measurableSet_overflowSet NX NY)] with z hz
change NX < z.1.2 ∨ NY < z.2.2 at hz
rcases hz with hx | hy
· simp [cappedPrefixStatistic, not_le_of_gt hx]
· by_cases hx : z.1.2 ≤ NX
· simp [cappedPrefixStatistic, hx, not_le_of_gt hy]
· simp [cappedPrefixStatistic, hx]
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) (Y := Y) NX NY) ≤
(poissonMeasure lambdaX).real (Ioi NX) +
(poissonMeasure lambdaY).real (Ioi NY) := by
let eX : Set (RandomizedPools (X := X) (Y := Y) NX NY) :=
{z | NX < z.1.2}
let eY : Set (RandomizedPools (X := X) (Y := Y) NX NY) :=
{z | NY < z.2.2}
have hOverflow :
overflowSet (X := X) (Y := Y) NX NY = eX ∪ eY := by
rfl
have heXeq :
μ.real eX = (poissonMeasure lambdaX).real (Ioi NX) := by
have hset : eX =
((Set.univ : Set (Fin NX → X)) ×ˢ Ioi NX) ×ˢ
(Set.univ : Set ((Fin NY → Y) × ℕ)) := by
ext z
simp [eX]
simp [hset, μ, randomizedPoolsLaw]
have heYeq :
μ.real eY = (poissonMeasure lambdaY).real (Ioi NY) := by
have hset : eY =
(Set.univ : Set ((Fin NX → X) × ℕ)) ×ˢ
((Set.univ : Set (Fin NY → Y)) ×ˢ Ioi NY) := by
ext z
simp [eY]
simp [hset, μ, randomizedPoolsLaw]
rw [hOverflow]
exact (measureReal_union_le eX eY).trans_eq
(congrArg₂ (· + ·) heXeq heYeq)
have hbadLe :
sqRisk (μ.restrict (overflowSet (X := X) (Y := Y) NX NY))
(cappedPrefixStatistic T zOver) theta ≤
(b - a) ^ 2 *
((poissonMeasure lambdaX).real (Ioi NX) +
(poissonMeasure lambdaY).real (Ioi NY)) := by
rw [hbadEq]
calc
(zOver - theta) ^ 2 *
μ.real (overflowSet (X := X) (Y := Y) NX NY) ≤
(b - a) ^ 2 *
μ.real (overflowSet (X := X) (Y := Y) NX NY) :=
mul_le_mul_of_nonneg_right hoverflowSq (by positivity)
_ ≤ (b - a) ^ 2 *
((poissonMeasure lambdaX).real (Ioi NX) +
(poissonMeasure lambdaY).real (Ioi NY)) :=
mul_le_mul_of_nonneg_left hoverflowMass (sq_nonneg _)
calc
sqRisk (fixedPoolsLaw P Q NX NY)
(independentPrefixRaoBlackwellStatistic lambdaX lambdaY T zOver) theta ≤
sqRisk μ (cappedPrefixStatistic T zOver) theta := by
exact sqRisk_independentPrefixRaoBlackwellStatistic_le_capped
P Q lambdaX lambdaY NX NY hT hTmem hzOver
_ = sqRisk (μ.restrict s) (cappedPrefixStatistic T zOver) theta +
sqRisk (μ.restrict sᶜ) (cappedPrefixStatistic T zOver) theta := hsplit
_ = sqRisk
((independentPoissonPrefixLaw P Q lambdaX lambdaY).restrict
((FiniteSample.count ⁻¹' Iic NX) ×ˢ
(FiniteSample.count ⁻¹' Iic NY))) T theta +
sqRisk (μ.restrict (overflowSet (X := X) (Y := Y) NX NY))
(cappedPrefixStatistic T zOver) theta := by
rw [show μ.restrict s =
(randomizedPoolsLaw P Q lambdaX lambdaY NX NY).restrict
(nonoverflowSet (X := X) (Y := Y) NX NY) from rfl,
sqRisk_cappedPrefixStatistic_restrict_nonoverflow_eq
P Q lambdaX lambdaY NX NY hT zOver theta, hsc]
_ ≤ sqRisk (independentPoissonPrefixLaw P Q lambdaX lambdaY) T theta +
(b - a) ^ 2 *
((poissonMeasure lambdaX).real (Ioi NX) +
(poissonMeasure lambdaY).real (Ioi NY)) :=
add_le_add
(sqRisk_independentPoissonPrefixLaw_restrict_nonoverflow_le
P Q lambdaX lambdaY NX NY hT hTb theta)
hbadLe
8 supporting declarations (lemmas, instances)
-
isMarkovKernelinstance — Given the first Poisson intensity and the second Poisson intensity, the independent Poisson-count kernel is a Markov kernel.parametersX :sharedType uXY :sharedType uYNX NY :ℕlambdaX lambdaY :ℝ≥0instanceisMarkovKernel lambdaX lambdaY :IsMarkovKernel (independentPoissonCountKernel (X := X) (Y := Y) (NX := NX) (NY := NY) lambdaX lambdaY)given byby unfold independentPoissonCountKernel exact instIsMarkovKernelMechanismKernel _ (by fun_prop) -
independentPoissonCountKernel_comp_fixedPoolsLawtheorem — Given probability laws for the first and second pools, the first and second Poisson intensities, and the first and second pool capacities, mixing the independent count kernel over the fixed pools gives exactly the randomized-pool law.hypothesesX :sharedType uXY :sharedType uYP :Q :lambdaX lambdaY :ℝ≥0NX NY :ℕconclusionindependentPoissonCountKernel (X := X) (Y := Y) lambdaX lambdaY ∘ₘ fixedPoolsLaw P Q NX NY= randomizedPoolsLaw P Q lambdaX lambdaY NX NYProof (Lean source)
theorem independentPoissonCountKernel_comp_fixedPoolsLaw (P : Measure X) [IsProbabilityMeasure P] (Q : Measure Y) [IsProbabilityMeasure Q] (lambdaX lambdaY : ℝ≥0) (NX NY : ℕ) : independentPoissonCountKernel (X := X) (Y := Y) lambdaX lambdaY ∘ₘ fixedPoolsLaw P Q NX NY = randomizedPoolsLaw P Q lambdaX lambdaY NX NY := by -- Follow `auxPoissonCountKernel_comp_pi`: express the composition product -- as the graph push-forward of the fixed-pool/count product, then map by -- the measurable reassociation permutation. Product associativity and -- `Measure.map_prod_map` identify the result with `randomizedPoolsLaw`. let μX : Measure (Fin NX → X) := Measure.pi (fun _ : Fin NX ↦ P) let μY : Measure (Fin NY → Y) := Measure.pi (fun _ : Fin NY ↦ Q) let νX : Measure ℕ := poissonMeasure lambdaX let νY : Measure ℕ := poissonMeasure lambdaY letI : IsProbabilityMeasure (fixedPoolsLaw P Q NX NY) := by unfold fixedPoolsLaw infer_instance let Φ : ((Fin NX → X) × (Fin NY → Y)) × (ℕ × ℕ) → ((Fin NX → X) × ℕ) × ((Fin NY → Y) × ℕ) := fun z => ((z.1.1, z.2.1), (z.1.2, z.2.2)) have hΦ : Measurable Φ := by fun_prop have hgraph : Measure.map (fun p => (p.1, Φ p)) ((fixedPoolsLaw P Q NX NY).prod (νX.prod νY)) = (fixedPoolsLaw P Q NX NY).compProd (independentPoissonCountKernel lambdaX lambdaY) := by simpa [independentPoissonCountKernel, Φ, νX, νY] using (map_graph_prod_eq_compProd (fixedPoolsLaw P Q NX NY) (νX.prod νY) 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 Φ ((fixedPoolsLaw P Q NX NY).prod (νX.prod νY)) = ((fixedPoolsLaw P Q NX NY) ⊗ₘ independentPoissonCountKernel lambdaX lambdaY).snd at hsnd rw [Measure.snd_compProd] at hsnd have hperm : Measure.map Φ ((μX.prod μY).prod (νX.prod νY)) = (μX.prod νX).prod (μY.prod νY) := by have hInner : MeasurePreserving (fun p : (Fin NY → Y) × (ℕ × ℕ) => (p.2.1, (p.1, p.2.2))) (μY.prod (νX.prod νY)) (νX.prod (μY.prod νY)) := by have h₁ := (measurePreserving_prodAssoc μY νX νY).symm (MeasurableEquiv.prodAssoc : (((Fin NY → Y) × ℕ) × ℕ) ≃ᵐ ((Fin NY → Y) × (ℕ × ℕ))) have h₂ := (Measure.measurePreserving_swap (μ := μY) (ν := νX)).prod (MeasurePreserving.id νY) have h₃ := measurePreserving_prodAssoc νX μY νY simpa [Function.comp_def, MeasurableEquiv.prodAssoc, MeasurableEquiv.prodComm] using h₃.comp (h₂.comp h₁) have hOuter := (MeasurePreserving.id μX).prod hInner have hFinal := (measurePreserving_prodAssoc μX νX (μY.prod νY)).symm (MeasurableEquiv.prodAssoc : (((Fin NX → X) × ℕ) × ((Fin NY → Y) × ℕ)) ≃ᵐ ((Fin NX → X) × (ℕ × ((Fin NY → Y) × ℕ)))) have hAll := hFinal.comp (hOuter.comp (measurePreserving_prodAssoc μX μY (νX.prod νY))) simpa [Φ, Function.comp_def, MeasurableEquiv.prodAssoc, MeasurableEquiv.prodComm] using hAll.map_eq simpa [fixedPoolsLaw, randomizedPoolsLaw, μX, μY, νX, νY] using hsnd.symm.trans hperm -
measurable_independentPrefixRaoBlackwellStatistictheorem — Given the first and second Poisson intensities, a measurable two-prefix statistic, and a fallback value, the independent-prefix Rao--Blackwell statistic is measurable.hypothesesX :sharedType uXY :sharedType uYNX NY :ℕlambdaX lambdaY :ℝ≥0T :(FiniteSample X × FiniteSample Y) → ℝhT :zOver :ℝconclusionMeasurable (independentPrefixRaoBlackwellStatistic (NX := NX) (NY := NY) lambdaX lambdaY T zOver)Proof (Lean source)
@[fun_prop] theorem measurable_independentPrefixRaoBlackwellStatistic {NX NY : ℕ} (lambdaX lambdaY : ℝ≥0) {T : (FiniteSample X × FiniteSample Y) → ℝ} (hT : Measurable T) (zOver : ℝ) : Measurable (independentPrefixRaoBlackwellStatistic (NX := NX) (NY := NY) lambdaX lambdaY T zOver) := by exact measurable_kernelMean _ (measurable_cappedPrefixStatistic hT zOver) -
independentPrefixRaoBlackwellStatistic_eq_integraltheorem — Given the first and second Poisson intensities, a two-prefix statistic, a certificate that it is measurable, a fallback value, and fixed pools, the Rao--Blackwell statistic equals the integral of the capped statistic over the independent Poisson counts.hypothesesX :sharedType uXY :sharedType uYNX NY :ℕlambdaX lambdaY :ℝ≥0T :(FiniteSample X × FiniteSample Y) → ℝhT :zOver :ℝpools :FixedPools (X := X) (Y := Y) NX NYconclusionindependentPrefixRaoBlackwellStatistic lambdaX lambdaY T zOver pools= ∫ counts : ℕ × ℕ, cappedPrefixStatistic T zOver ((pools.1, counts.1), (pools.2, counts.2)) ∂((poissonMeasure lambdaX).prod (poissonMeasure lambdaY))Proof (Lean source)
theorem independentPrefixRaoBlackwellStatistic_eq_integral {NX NY : ℕ} (lambdaX lambdaY : ℝ≥0) (T : (FiniteSample X × FiniteSample Y) → ℝ) (hT : Measurable T) (zOver : ℝ) (pools : FixedPools (X := X) (Y := Y) NX NY) : independentPrefixRaoBlackwellStatistic lambdaX lambdaY T zOver pools = ∫ counts : ℕ × ℕ, cappedPrefixStatistic T zOver ((pools.1, counts.1), (pools.2, counts.2)) ∂((poissonMeasure lambdaX).prod (poissonMeasure lambdaY)) := by -- Unfold `kernelMean` and the mechanism kernel, rewrite its pointwise value -- with `mechanismKernel_apply`, then apply `integral_map`; measurability of -- the integrand is `measurable_cappedPrefixStatistic hT zOver`. unfold independentPrefixRaoBlackwellStatistic kernelMean independentPoissonCountKernel rw [mechanismKernel_apply _ (show Measurable (fun z : FixedPools (X := X) (Y := Y) NX NY × (ℕ × ℕ) => ((z.1.1, z.2.1), (z.1.2, z.2.2))) from by fun_prop) pools] exact integral_map (show Measurable (fun counts : ℕ × ℕ => ((pools.1, counts.1), (pools.2, counts.2))) from by fun_prop).aemeasurable (measurable_cappedPrefixStatistic hT zOver).aestronglyMeasurable -
sqRisk_independentPrefixRaoBlackwellStatistic_le_cappedtheorem — Given probability laws for the first and second observations, the first and second Poisson intensities, the first and second pool capacities, a measurable two-prefix statistic, a certificate that the statistic stays in an interval, and a fallback in that interval, conditional averaging cannot increase squared risk, for any target.hypothesesX :sharedType uXY :sharedType uYP :Q :lambdaX lambdaY :ℝ≥0NX NY :ℕT :(FiniteSample X × FiniteSample Y) → ℝhT :a b theta zOver :ℝhTmem :∀ s, T s ∈ Icc a bhzOver :zOver ∈ Icc a bconclusionsqRisk (fixedPoolsLaw P Q NX NY) (independentPrefixRaoBlackwellStatistic lambdaX lambdaY T zOver) theta≤ sqRisk (randomizedPoolsLaw P Q lambdaX lambdaY NX NY) (cappedPrefixStatistic T zOver) thetaProof (Lean source)
theorem sqRisk_independentPrefixRaoBlackwellStatistic_le_capped (P : Measure X) [IsProbabilityMeasure P] (Q : Measure Y) [IsProbabilityMeasure Q] (lambdaX lambdaY : ℝ≥0) (NX NY : ℕ) {T : (FiniteSample X × FiniteSample Y) → ℝ} (hT : Measurable T) {a b theta zOver : ℝ} (hTmem : ∀ s, T s ∈ Icc a b) (hzOver : zOver ∈ Icc a b) : sqRisk (fixedPoolsLaw P Q NX NY) (independentPrefixRaoBlackwellStatistic lambdaX lambdaY T zOver) theta ≤ sqRisk (randomizedPoolsLaw P Q lambdaX lambdaY NX NY) (cappedPrefixStatistic T zOver) theta := by -- The interval assumptions uniformly bound the capped statistic by -- `max |a| |b|`. Apply `sqRisk_kernelMean_le_comp` to the auxiliary -- Markov kernel and rewrite the composed measure using -- `independentPoissonCountKernel_comp_fixedPoolsLaw`. letI : IsProbabilityMeasure (fixedPoolsLaw P Q NX NY) := by unfold fixedPoolsLaw infer_instance have hCappedBound : UniformlyBounded (cappedPrefixStatistic (NX := NX) (NY := NY) T zOver) := by refine ⟨max |a| |b|, ?_, ?_⟩ · exact (abs_nonneg a).trans (le_max_left _ _) · intro z by_cases hX : z.1.2 ≤ NX · by_cases hY : z.2.2 ≤ NY · simp only [cappedPrefixStatistic, hX, hY, dite_true] exact abs_le_max_abs_abs (hTmem _).1 (hTmem _).2 · simp only [cappedPrefixStatistic, hX, hY, dite_true, dite_false] exact abs_le_max_abs_abs hzOver.1 hzOver.2 · simp only [cappedPrefixStatistic, hX, dite_false] exact abs_le_max_abs_abs hzOver.1 hzOver.2 calc sqRisk (fixedPoolsLaw P Q NX NY) (independentPrefixRaoBlackwellStatistic lambdaX lambdaY T zOver) theta ≤ sqRisk (independentPoissonCountKernel (X := X) (Y := Y) lambdaX lambdaY ∘ₘ fixedPoolsLaw P Q NX NY) (cappedPrefixStatistic T zOver) theta := by exact sqRisk_kernelMean_le_comp (fixedPoolsLaw P Q NX NY) (independentPoissonCountKernel lambdaX lambdaY) (measurable_cappedPrefixStatistic hT zOver) hCappedBound theta _ = sqRisk (randomizedPoolsLaw P Q lambdaX lambdaY NX NY) (cappedPrefixStatistic T zOver) theta := by rw [independentPoissonCountKernel_comp_fixedPoolsLaw] -
sqRisk_cappedPrefixStatistic_restrict_nonoverflow_eqtheorem — Given probability laws for the first and second pools, the first and second Poisson intensities, the first and second pool capacities, a measurable two-prefix statistic, a fallback value, and a target, the capped risk on the joint nonoverflow event equals the restricted untruncated-prefix risk.hypothesesX :sharedType uXY :sharedType uYP :Q :lambdaX lambdaY :ℝ≥0NX NY :ℕT :(FiniteSample X × FiniteSample Y) → ℝhT :zOver theta :ℝconclusionProof (Lean source)
theorem sqRisk_cappedPrefixStatistic_restrict_nonoverflow_eq (P : Measure X) [IsProbabilityMeasure P] (Q : Measure Y) [IsProbabilityMeasure Q] (lambdaX lambdaY : ℝ≥0) (NX NY : ℕ) {T : (FiniteSample X × FiniteSample Y) → ℝ} (hT : Measurable T) (zOver theta : ℝ) : sqRisk ((randomizedPoolsLaw P Q lambdaX lambdaY NX NY).restrict (nonoverflowSet (X := X) (Y := Y) NX NY)) (cappedPrefixStatistic T zOver) theta = sqRisk ((independentPoissonPrefixLaw P Q lambdaX lambdaY).restrict ((FiniteSample.count ⁻¹' Iic NX) ×ˢ (FiniteSample.count ⁻¹' Iic NY))) T theta := by -- Pull squared loss back along `totalizedPrefixPair` using `integral_map` -- and `map_totalizedPrefixPair_restrict_nonoverflow`. On the restricted -- source, `cappedPrefixStatistic_eq_off_overflow` gives pointwise equality; -- use `ae_restrict_mem`, `nonoverflowSet_eq_compl_overflowSet`, and -- `cappedPrefixStatistic_eq_off_overflow` to discharge membership. This is -- the product analogue of -- `sqRisk_cappedStatistic_restrict_nonoverflow_eq`. let overflowX : FiniteSample X := ⟨0, fun i => Fin.elim0 i⟩ let overflowY : FiniteSample Y := ⟨0, fun i => Fin.elim0 i⟩ unfold sqRisk rw [← map_totalizedPrefixPair_restrict_nonoverflow P Q lambdaX lambdaY NX NY overflowX overflowY] rw [integral_map (μ := (randomizedPoolsLaw P Q lambdaX lambdaY NX NY).restrict (nonoverflowSet (X := X) (Y := Y) NX NY)) (φ := totalizedPrefixPair overflowX overflowY) (f := fun s : FiniteSample X × FiniteSample Y ↦ (T s - theta) ^ 2) (measurable_totalizedPrefixPair overflowX overflowY).aemeasurable ((hT.sub measurable_const).pow_const 2).aestronglyMeasurable] apply integral_congr_ae filter_upwards [ae_restrict_mem (measurableSet_nonoverflowSet NX NY)] with z hz rw [nonoverflowSet_eq_compl_overflowSet] at hz rw [cappedPrefixStatistic_eq_off_overflow T zOver overflowX overflowY z hz] -
sqRisk_independentPoissonPrefixLaw_restrict_nonoverflow_letheorem — Given probability laws for the first and second prefixes, the first and second Poisson intensities, the first and second capacities, a measurable two-prefix statistic, a uniform bound for that statistic, and a target, restricting to jointly nonoverflowing prefix lengths cannot increase squared risk.hypothesesX :sharedType uXY :sharedType uYP :Q :lambdaX lambdaY :ℝ≥0NX NY :ℕT :(FiniteSample X × FiniteSample Y) → ℝhT :hTb :theta :ℝProof (Lean source)
theorem sqRisk_independentPoissonPrefixLaw_restrict_nonoverflow_le (P : Measure X) [IsProbabilityMeasure P] (Q : Measure Y) [IsProbabilityMeasure Q] (lambdaX lambdaY : ℝ≥0) (NX NY : ℕ) {T : (FiniteSample X × FiniteSample Y) → ℝ} (hT : Measurable T) (hTb : UniformlyBounded T) (theta : ℝ) : sqRisk ((independentPoissonPrefixLaw P Q lambdaX lambdaY).restrict ((FiniteSample.count ⁻¹' Iic NX) ×ˢ (FiniteSample.count ⁻¹' Iic NY))) T theta ≤ sqRisk (independentPoissonPrefixLaw P Q lambdaX lambdaY) T theta := by -- Uniform boundedness makes squared loss integrable. Split the full -- integral into the measurable joint-good restriction and its complement -- via `Measure.restrict_add_restrict_compl`, then discard the nonnegative -- complementary squared-loss integral. Equivalently, -- `MeasureTheory.setIntegral_le_integral` applies once integrability and -- nonnegativity are established; the one-pool template is -- `sqRisk_finitePoisson_restrict_nonoverflow_le`. obtain ⟨M, hM, hTb⟩ := hTb let μ : Measure (FiniteSample X × FiniteSample Y) := independentPoissonPrefixLaw P Q lambdaX lambdaY letI : IsProbabilityMeasure μ := by unfold μ independentPoissonPrefixLaw infer_instance let s : Set (FiniteSample X × FiniteSample Y) := (FiniteSample.count ⁻¹' Iic NX) ×ˢ (FiniteSample.count ⁻¹' Iic NY) have hs : MeasurableSet s := by exact (measurable_finiteSample_count measurableSet_Iic).prod (measurable_finiteSample_count 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)) -
finiteAlphabet_independentUnequalPrefix_risk_letheorem — Given finite measurable alphabets, probability laws for the two observations, the first and second Poisson intensities, the first and second pool capacities, a measurable two-prefix statistic, an ordered outcome interval, a certificate that the statistic stays in it, a target in it, and a fallback in it, the unequal-prefix risk transfer bound holds without coordinatewise pairing.hypothesesX :sharedType uXY :sharedType uYFintype XFintype YP :Q :lambdaX lambdaY :ℝ≥0NX NY :ℕT :(FiniteSample X × FiniteSample Y) → ℝhT :a b theta zOver :ℝhab :a ≤ bhTmem :∀ s, T s ∈ Icc a bhtheta :theta ∈ Icc a bhzOver :zOver ∈ Icc a bconclusionsqRisk (fixedPoolsLaw P Q NX NY) (independentPrefixRaoBlackwellStatistic lambdaX lambdaY T zOver) theta≤ sqRisk (independentPoissonPrefixLaw P Q lambdaX lambdaY) T thetaProof (Lean source)
theorem finiteAlphabet_independentUnequalPrefix_risk_le [Fintype X] [MeasurableSingletonClass X] [DecidableEq X] [Fintype Y] [MeasurableSingletonClass Y] [DecidableEq Y] (P : Measure X) [IsProbabilityMeasure P] (Q : Measure Y) [IsProbabilityMeasure Q] (lambdaX lambdaY : ℝ≥0) (NX NY : ℕ) {T : (FiniteSample X × FiniteSample Y) → ℝ} (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 Q NX NY) (independentPrefixRaoBlackwellStatistic lambdaX lambdaY T zOver) theta ≤ sqRisk (independentPoissonPrefixLaw P Q lambdaX lambdaY) T theta + (b - a) ^ 2 * ((poissonMeasure lambdaX).real (Ioi NX) + (poissonMeasure lambdaY).real (Ioi NY)) := by exact sqRisk_independentPrefixRaoBlackwellStatistic_le P Q lambdaX lambdaY NX NY hT hab hTmem htheta hzOver