Stat.Concentration.RandomDesignWeightedHoeffding
Random-design weighted Hoeffding concentration: conditional exponential-moment and self-normalized tail bounds for bounded marks whose weights depend measurably on the entire design vector.
Basic 4 core · 8 supporting This module proves conditional Hoeffding exponential-moment bounds for finite i.i.d. ★ product_weighted_centered_conditional_mgf_le
Conditional Hoeffding MGFs with random-design weights
This module proves conditional Hoeffding exponential-moment bounds for finite i.i.d. samples whose coefficient array is a measurable function of the complete design vector. It supplies a kernel-native formulation and a regular-conditional-distribution corollary, deriving rather than assuming conditional independence of the marks.
def realizedWeightEnergy reviewed
⚑ flagged
Causalean.Stat.Concentration.RandomDesignWeightedHoeffding
For a coefficient array determined by a complete design vector and a complete design vector, the realized weight energy is the sum of the squares of the coefficients selected by that design vector.
def weightedCenteredMarkSum reviewed
⚑ flagged
Causalean.Stat.Concentration.RandomDesignWeightedHoeffding
For a real-valued conditional mean function of a design value, a coefficient array determined by a complete design vector, a complete design vector, and a vector of real marks, the weighted centered mark sum is the sum over sample positions of the selected coefficient times the mark minus its conditional mean at the corresponding design value.
def selfNormalizedWeightedCenteredSum reviewed
⚑ flagged
Causalean.Stat.Concentration.RandomDesignWeightedHoeffding
For a design map, a real-valued outcome map, a real-valued conditional mean function of the design, a coefficient array determined by a complete design vector, and a finite vector of sampled units, the self-normalized weighted centered sum is the weighted centered sum divided by the square root of the realized weight energy of the sampled design vector; when that energy is zero, this value is zero.
theorem product_weighted_centered_conditional_mgf_le reviewed
⚑ flagged
Causalean.Stat.Concentration.RandomDesignWeightedHoeffding
A probability law P, measurable design, and measurable outcome that is almost surely in the unit interval, together with a measurable regression equal almost surely to the conditional expectation given the design and measurable complete-design weights, give the conditional Hoeffding exponential-moment bound on almost every complete design vector.
Formal statement
hypotheses
N :
Omega D :
P :
Measure Omega
design :
Omega -> D
hdesign :
Measurable design
Y :
Omega -> Real
hY :
hY_nonneg :
∀ᵐ omega ∂P, 0 <= Y omega
hY_le_one :
∀ᵐ omega ∂P, Y omega <= 1
mD :
D -> Real
hmD :
Measurable mD
hcond :
P[Y | comap design inferInstance] =ᵐ[P] mD ∘ design
hw :
conclusion
∀ᵐ d ∂Measure.pi (fun _ : Fin N => P.map design), ∀ s : Real, ∫ y, exp (s * weightedCenteredMarkSum mD w d y) ∂Causalean.Stat.finProductKernel N (condDistrib Y design P) d <
= exp (s ^ 2 * realizedWeightEnergy w d / 8)
Proof (Lean source)
theorem product_weighted_centered_conditional_mgf_le
{N : Nat} {Omega D : Type*} [MeasurableSpace Omega] [MeasurableSpace D]
(P : Measure Omega) [IsProbabilityMeasure P]
(design : Omega -> D) (hdesign : Measurable design)
(Y : Omega -> Real) (hY : Measurable Y)
(hY_nonneg : ∀ᵐ omega ∂P, 0 <= Y omega)
(hY_le_one : ∀ᵐ omega ∂P, Y omega <= 1)
(mD : D -> Real) (hmD : Measurable mD)
(hcond :
P[Y | comap design inferInstance] =ᵐ[P] mD ∘ design)
(w : (Fin N -> D) -> Fin N -> Real) (hw : Measurable w) :
∀ᵐ d ∂Measure.pi (fun _ : Fin N => P.map design), ∀ s : Real,
∫ y, exp (s * weightedCenteredMarkSum mD w d y)
∂Causalean.Stat.finProductKernel N (condDistrib Y design P) d <=
exp (s ^ 2 * realizedWeightEnergy w d / 8) := by
-- Derive the conditional-distribution mean and range from `hcond` and the ambient
-- bounds, then invoke the kernel-native product theorem. No conditional-independence
-- hypothesis is introduced here.
have hY_mem : ∀ᵐ omega ∂P, Y omega ∈ Icc (0 : ℝ) 1 :=
hY_nonneg.and hY_le_one
have hY_int : Integrable Y P :=
Integrable.of_mem_Icc 0 1 hY.aemeasurable hY_mem
have hmean_comp :
(fun omega => ∫ y, y ∂condDistrib Y design P (design omega)) =ᵐ[P]
mD ∘ design :=
(condExp_ae_eq_integral_condDistrib' hdesign hY_int).symm.trans hcond
have hmean :
∀ᵐ d ∂P.map design, ∫ y, y ∂condDistrib Y design P d = mD d := by
rw [ae_map_iff hdesign.aemeasurable]
· filter_upwards [hmean_comp] with x hx
exact hx
· exact measurableSet_eq_fun
(((stronglyMeasurable_id.comp_measurable measurable_snd).integral_condDistrib
(X := design) (Y := Y) (μ := P)).measurable)
hmD
have hpair :
∀ᵐ p ∂(P.map design ⊗ₘ condDistrib Y design P),
p.2 ∈ Icc (0 : ℝ) 1 := by
rw [compProd_map_condDistrib hY.aemeasurable]
rw [ae_map_iff (hdesign.prodMk hY).aemeasurable]
· simpa using hY_mem
· exact measurableSet_Icc.preimage measurable_snd
have hrange :
∀ᵐ d ∂P.map design,
∀ᵐ y ∂condDistrib Y design P d, y ∈ Icc (0 : ℝ) 1 :=
Measure.ae_ae_of_ae_compProd hpair
letI : IsProbabilityMeasure (P.map design) :=
Measure.isProbabilityMeasure_map hdesign.aemeasurable
exact product_weighted_centered_attachKernel_conditional_mgf_le
(P.map design) (condDistrib Y design P) mD hmD hmean hrange w hw
8 supporting declarations (lemmas, instances)
-
measurable_realizedWeightEnergytheorem — The sum of squared coefficients selected by a measurable complete-design weight array is itself measurable.hypothesesconclusionProof (Lean source)
@[fun_prop] theorem measurable_realizedWeightEnergy {N : Nat} {D : Type*} [MeasurableSpace D] {w : (Fin N -> D) -> Fin N -> Real} (hw : Measurable w) : Measurable (realizedWeightEnergy w) := by apply measurable_sum intro i _ exact ((measurable_pi_apply i).comp hw).pow_const 2 -
measurable_weightedCenteredMarkSumtheorem — A measurable regression and measurable complete-design weights make the weighted centered mark sum jointly measurable.Proof (Lean source)
@[fun_prop] theorem measurable_weightedCenteredMarkSum {N : Nat} {D : Type*} [MeasurableSpace D] {mD : D -> Real} (hmD : Measurable mD) {w : (Fin N -> D) -> Fin N -> Real} (hw : Measurable w) : Measurable (fun p : (Fin N -> D) × (Fin N -> Real) => weightedCenteredMarkSum mD w p.1 p.2) := by apply measurable_sum intro i _ exact ((measurable_pi_apply i).comp (hw.comp measurable_fst)).mul (((measurable_pi_apply i).comp measurable_snd).sub (hmD.comp ((measurable_pi_apply i).comp measurable_fst))) -
measurable_weightedCenteredSumtheorem — A measurable design, measurable outcome, measurable regression, and measurable complete-design weights make the finite-sample weighted centered sum measurable.hypothesesN :Omega D :hdesign :Measurable designY :Omega -> RealhY :mD :D -> RealhmD :Measurable mDhw :conclusionMeasurable (weightedCenteredSum design Y mD w)Proof (Lean source)
@[fun_prop] theorem measurable_weightedCenteredSum {N : Nat} {Omega D : Type*} [MeasurableSpace Omega] [MeasurableSpace D] {design : Omega -> D} (hdesign : Measurable design) {Y : Omega -> Real} (hY : Measurable Y) {mD : D -> Real} (hmD : Measurable mD) {w : (Fin N -> D) -> Fin N -> Real} (hw : Measurable w) : Measurable (weightedCenteredSum design Y mD w) := by apply measurable_sum intro i _ exact ((measurable_pi_apply i).comp (hw.comp (measurable_designVector design hdesign))).mul ((hY.comp (measurable_pi_apply i)).sub (hmD.comp (hdesign.comp (measurable_pi_apply i)))) -
measurable_selfNormalizedWeightedCenteredSumtheorem — A measurable design, measurable outcome, measurable regression, and measurable complete-design weights make the self-normalized weighted centered sum measurable, including at zero energy.hypothesesN :Omega D :hdesign :Measurable designY :Omega -> RealhY :mD :D -> RealhmD :Measurable mDhw :conclusionMeasurable (selfNormalizedWeightedCenteredSum design Y mD w)Proof (Lean source)
@[fun_prop] theorem measurable_selfNormalizedWeightedCenteredSum {N : Nat} {Omega D : Type*} [MeasurableSpace Omega] [MeasurableSpace D] {design : Omega -> D} (hdesign : Measurable design) {Y : Omega -> Real} (hY : Measurable Y) {mD : D -> Real} (hmD : Measurable mD) {w : (Fin N -> D) -> Fin N -> Real} (hw : Measurable w) : Measurable (selfNormalizedWeightedCenteredSum design Y mD w) := by exact (measurable_weightedCenteredSum hdesign hY hmD hw).div (((measurable_realizedWeightEnergy hw).comp (measurable_designVector design hdesign)).sqrt) -
measurableSet_selfNormalizedDeviationtheorem — A measurable design, measurable outcome, measurable regression, and measurable complete-design weights make the event that the absolute self-normalized sum exceeds the fixed threshold measurable.hypothesesN :Omega D :hdesign :Measurable designY :Omega -> RealhY :mD :D -> RealhmD :Measurable mDhw :t :conclusionProof (Lean source)
theorem measurableSet_selfNormalizedDeviation {N : Nat} {Omega D : Type*} [MeasurableSpace Omega] [MeasurableSpace D] {design : Omega -> D} (hdesign : Measurable design) {Y : Omega -> Real} (hY : Measurable Y) {mD : D -> Real} (hmD : Measurable mD) {w : (Fin N -> D) -> Fin N -> Real} (hw : Measurable w) (t : Real) : MeasurableSet {z : Fin N -> Omega | t <= |selfNormalizedWeightedCenteredSum design Y mD w z|} := by exact measurableSet_le measurable_const (measurable_selfNormalizedWeightedCenteredSum hdesign hY hmD hw).abs -
centered_condDistrib_mgf_letheorem — A probability law P, measurable design, and measurable outcome that is almost surely nonnegative and at most one, together with a measurable regression equal almost surely to its conditional expectation given the design, yield the conditional Hoeffding exponential-moment bound on almost every design fibre.hypothesesOmega D :P :Measure Omegadesign :Omega -> Dhdesign :Measurable designY :Omega -> RealhY :hY_nonneg :∀ᵐ omega ∂P, 0 <= Y omegahY_le_one :∀ᵐ omega ∂P, Y omega <= 1mD :D -> RealhmD :Measurable mDhcond :P[Y | comap design inferInstance] =ᵐ[P] mD ∘ designProof (Lean source)
theorem centered_condDistrib_mgf_le {Omega D : Type*} [MeasurableSpace Omega] [MeasurableSpace D] (P : Measure Omega) [IsProbabilityMeasure P] (design : Omega -> D) (hdesign : Measurable design) (Y : Omega -> Real) (hY : Measurable Y) (hY_nonneg : ∀ᵐ omega ∂P, 0 <= Y omega) (hY_le_one : ∀ᵐ omega ∂P, Y omega <= 1) (mD : D -> Real) (hmD : Measurable mD) (hcond : P[Y | comap design inferInstance] =ᵐ[P] mD ∘ design) : ∀ᵐ d ∂P.map design, ∀ s : Real, ∫ y, exp (s * (y - mD d)) ∂condDistrib Y design P d <= exp (s ^ 2 / 8) := by -- Proof route: boundedness gives `Integrable Y P`; identify the conditional fibre mean -- with `mD` using `condExp_ae_eq_integral_condDistrib'` and `hcond`, disintegrate the -- ambient interval bound with `compProd_map_condDistrib`, then apply Mathlib's -- `hasSubgaussianMGF_of_mem_Icc` on each good fibre (whose interval width is one). have hY_mem : ∀ᵐ omega ∂P, Y omega ∈ Icc (0 : ℝ) 1 := hY_nonneg.and hY_le_one have hY_int : Integrable Y P := Integrable.of_mem_Icc 0 1 hY.aemeasurable hY_mem have hmean_comp : (fun omega => ∫ y, y ∂condDistrib Y design P (design omega)) =ᵐ[P] mD ∘ design := (condExp_ae_eq_integral_condDistrib' hdesign hY_int).symm.trans hcond have hmean : ∀ᵐ d ∂P.map design, ∫ y, y ∂condDistrib Y design P d = mD d := by rw [ae_map_iff hdesign.aemeasurable] · filter_upwards [hmean_comp] with x hx exact hx · exact measurableSet_eq_fun (((stronglyMeasurable_id.comp_measurable measurable_snd).integral_condDistrib (X := design) (Y := Y) (μ := P)).measurable) hmD have hpair : ∀ᵐ p ∂(P.map design ⊗ₘ condDistrib Y design P), p.2 ∈ Icc (0 : ℝ) 1 := by rw [compProd_map_condDistrib hY.aemeasurable] rw [ae_map_iff (hdesign.prodMk hY).aemeasurable] · simpa using hY_mem · exact measurableSet_Icc.preimage measurable_snd have hrange : ∀ᵐ d ∂P.map design, ∀ᵐ y ∂condDistrib Y design P d, y ∈ Icc (0 : ℝ) 1 := Measure.ae_ae_of_ae_compProd hpair filter_upwards [hmean, hrange] with d hdmean hdrange intro s have hsub := hasSubgaussianMGF_of_mem_Icc (μ := condDistrib Y design P d) (X := id) measurable_id.aemeasurable hdrange have hmgf := hsub.mgf_le s simp only [mgf, id_eq, hdmean] at hmgf convert hmgf using 1 <;> norm_num <;> ring -
product_weighted_centered_attachKernel_hasSubgaussianMGFtheorem — Under a probability design law and Markov marking kernel whose conditional mean is the measurable regression, whose marks lie in the unit interval almost surely on almost every fibre, and whose complete-design weight array is measurable, the weighted centered mark sum is sub-Gaussian on almost every complete-design fibre with one quarter of its realized weight energy as variance proxy.hypothesesconclusion∀ᵐ d ∂Measure.pi (fun _ : Fin N => Q), HasSubgaussianMGF (weightedCenteredMarkSum mD w d) (toNNReal (realizedWeightEnergy w d / 4)) (finProductKernel N K d)Proof (Lean source)
theorem product_weighted_centered_attachKernel_hasSubgaussianMGF {N : Nat} {D : Type*} [MeasurableSpace D] (Q : Measure D) [IsProbabilityMeasure Q] (K : Kernel D Real) [IsMarkovKernel K] (mD : D -> Real) (hmD : Measurable mD) (hmean : ∀ᵐ d ∂Q, ∫ y, y ∂K d = mD d) (hbound : ∀ᵐ d ∂Q, ∀ᵐ y ∂K d, y ∈ Icc (0 : Real) 1) (w : (Fin N -> D) -> Fin N -> Real) (hw : Measurable w) : ∀ᵐ d ∂Measure.pi (fun _ : Fin N => Q), HasSubgaussianMGF (weightedCenteredMarkSum mD w d) (toNNReal (realizedWeightEnergy w d / 4)) (finProductKernel N K d) := by have hmeans : ∀ᵐ d ∂Measure.pi (fun _ : Fin N => Q), ∀ i, ∫ y, y ∂K (d i) = mD (d i) := by rw [ae_all_iff] intro i exact Measure.tendsto_eval_ae_ae (μ := fun _ : Fin N => Q) (i := i) |>.eventually hmean have hbounds : ∀ᵐ d ∂Measure.pi (fun _ : Fin N => Q), ∀ i, ∀ᵐ y ∂K (d i), y ∈ Icc (0 : ℝ) 1 := by rw [ae_all_iff] intro i exact Measure.tendsto_eval_ae_ae (μ := fun _ : Fin N => Q) (i := i) |>.eventually hbound filter_upwards [hmeans, hbounds] with d hdmean hdbound rw [finProductKernel_apply] let mu : Measure (Fin N -> ℝ) := Measure.pi (fun i : Fin N => K (d i)) let X : Fin N -> (Fin N -> ℝ) -> ℝ := fun i y => w d i * (y i - mD (d i)) let c : Fin N -> NNReal := fun i => ⟨(w d i) ^ 2, sq_nonneg _⟩ * ((‖(1 : ℝ) - 0‖₊ / 2) ^ 2) have hindep_eval : iIndepFun (fun i (y : Fin N -> ℝ) => y i) mu := iIndepFun_pi (X := fun _ => id) (fun _ => measurable_id.aemeasurable) have hindep : iIndepFun X mu := hindep_eval.comp (fun i y => w d i * (y - mD (d i))) (fun i => measurable_const.mul (measurable_id.sub measurable_const)) have hsub : ∀ i, HasSubgaussianMGF (X i) (c i) mu := by intro i have hbase := hasSubgaussianMGF_of_mem_Icc (μ := K (d i)) (X := id) measurable_id.aemeasurable (hdbound i) have hcentered : HasSubgaussianMGF (fun y : ℝ => y - mD (d i)) ((‖(1 : ℝ) - 0‖₊ / 2) ^ 2) (K (d i)) := by simpa [hdmean i] using hbase have hmap : Measure.map (fun y : Fin N -> ℝ => y i) mu = K (d i) := by simpa only [mu] using (measurePreserving_eval (fun j : Fin N => K (d j)) i).map_eq rw [← hmap] at hcentered have hbase' := HasSubgaussianMGF.of_map (μ := mu) (Y := fun y : Fin N -> ℝ => y i) (X := fun y : ℝ => y - mD (d i)) (measurable_pi_apply i).aemeasurable hcentered change HasSubgaussianMGF (fun y : Fin N -> ℝ => y i - mD (d i)) ((‖(1 : ℝ) - 0‖₊ / 2) ^ 2) mu at hbase' have hscaled := hbase'.const_mul (w d i) simpa only [X, c] using hscaled have hsum := HasSubgaussianMGF.sum_of_iIndepFun hindep (s := univ) (fun i _ => hsub i) have hc_sum : (↑(∑ i, c i) : ℝ) = realizedWeightEnergy w d / 4 := by rw [NNReal.coe_sum] simp only [c] norm_num [Real.norm_eq_abs] change (∑ i, (w d i) ^ 2 * (1 / 4)) = (∑ i, (w d i) ^ 2) / 4 rw [← Finset.sum_mul] ring have henergy_nonneg : 0 <= realizedWeightEnergy w d := by exact sum_nonneg fun i _ => sq_nonneg (w d i) have hc : (∑ i, c i) = toNNReal (realizedWeightEnergy w d / 4) := by apply NNReal.eq rw [hc_sum, Real.coe_toNNReal _ (div_nonneg henergy_nonneg (by norm_num))] rw [hc] at hsum change HasSubgaussianMGF (fun y : Fin N -> Real => ∑ i, w d i * (y i - mD (d i))) (toNNReal (realizedWeightEnergy w d / 4)) (Measure.pi (fun i : Fin N => K (d i))) simpa only [mu, X] using hsum -
product_weighted_centered_attachKernel_conditional_mgf_letheorem — Under a probability design law and Markov marking kernel whose conditional mean is the measurable regression, whose marks lie in the unit interval almost surely on almost every fibre, and whose complete-design weight array is measurable, the weighted centered sum has the conditional Hoeffding exponential-moment bound on almost every complete-design fibre.hypothesesconclusion∀ᵐ d ∂Measure.pi (fun _ : Fin N => Q), ∀ s : Real, ∫ y, exp (s * weightedCenteredMarkSum mD w d y) ∂Causalean.Stat.finProductKernel N K d <= exp (s ^ 2 * realizedWeightEnergy w d / 8)Proof (Lean source)
theorem product_weighted_centered_attachKernel_conditional_mgf_le {N : Nat} {D : Type*} [MeasurableSpace D] (Q : Measure D) [IsProbabilityMeasure Q] (K : Kernel D Real) [IsMarkovKernel K] (mD : D -> Real) (hmD : Measurable mD) (hmean : ∀ᵐ d ∂Q, ∫ y, y ∂K d = mD d) (hbound : ∀ᵐ d ∂Q, ∀ᵐ y ∂K d, y ∈ Icc (0 : Real) 1) (w : (Fin N -> D) -> Fin N -> Real) (hw : Measurable w) : ∀ᵐ d ∂Measure.pi (fun _ : Fin N => Q), ∀ s : Real, ∫ y, exp (s * weightedCenteredMarkSum mD w d y) ∂Causalean.Stat.finProductKernel N K d <= exp (s ^ 2 * realizedWeightEnergy w d / 8) := by filter_upwards [product_weighted_centered_attachKernel_hasSubgaussianMGF Q K mD hmD hmean hbound w hw] with d hd intro s have hmgf := hd.mgf_le s have henergy_nonneg : 0 <= realizedWeightEnergy w d := by exact sum_nonneg fun i _ => sq_nonneg (w d i) rw [Real.coe_toNNReal _ (div_nonneg henergy_nonneg (by norm_num))] at hmgf simp only [mgf] at hmgf convert hmgf using 1 congr 1 ring
Tail 1 core · 2 supporting This module transports the conditional random-design MGF bound to a retained-design law and then to an i.i.d. ★ product_weighted_centered_tail_le
Self-normalized random-design weighted Hoeffding tails
This module transports the conditional random-design MGF bound to a retained-design law and then to an i.i.d. observation product. It provides two-sided self-normalized Hoeffding tails for weights that depend measurably on every observed design coordinate.
theorem product_weighted_centered_tail_le reviewed
⚑ flagged
Causalean.Stat.Concentration.RandomDesignWeightedHoeffding
A probability law P, measurable design, and measurable outcome that is almost surely in the unit interval, together with a measurable regression equal almost surely to the conditional expectation given the design, measurable complete-design weights of positive realized energy almost surely, and a nonnegative threshold, yield the two-sided self-normalized Hoeffding tail bound for the finite i.i.d. sample.
Formal statement
hypotheses
N :
Omega D :
P :
Measure Omega
design :
Omega -> D
hdesign :
Measurable design
Y :
Omega -> Real
hY :
hY_nonneg :
∀ᵐ omega ∂P, 0 <= Y omega
hY_le_one :
∀ᵐ omega ∂P, Y omega <= 1
mD :
D -> Real
hmD :
Measurable mD
hcond :
P[Y | comap design inferInstance] =ᵐ[P] mD ∘ design
hw :
henergy :
t :
ht :
0 <= t
conclusion
(Measure.pi (fun _ : Fin N => P)).real {z | t * sqrt (realizedWeightEnergy w (designVector design z)) <= |weightedCenteredSum design Y mD w z|} <
= 2 * exp (-2 * t ^ 2)
Proof (Lean source)
theorem product_weighted_centered_tail_le
{N : Nat} {Omega D : Type*} [MeasurableSpace Omega] [MeasurableSpace D]
(P : Measure Omega) [IsProbabilityMeasure P]
(design : Omega -> D) (hdesign : Measurable design)
(Y : Omega -> Real) (hY : Measurable Y)
(hY_nonneg : ∀ᵐ omega ∂P, 0 <= Y omega)
(hY_le_one : ∀ᵐ omega ∂P, Y omega <= 1)
(mD : D -> Real) (hmD : Measurable mD)
(hcond :
P[Y | comap design inferInstance] =ᵐ[P] mD ∘ design)
(w : (Fin N -> D) -> Fin N -> Real) (hw : Measurable w)
(henergy : ∀ᵐ z ∂Measure.pi (fun _ : Fin N => P),
0 < realizedWeightEnergy w (designVector design z))
{t : Real} (ht : 0 <= t) :
(Measure.pi (fun _ : Fin N => P)).real
{z | t * sqrt
(realizedWeightEnergy w (designVector design z)) <=
|weightedCenteredSum design Y mD w z|} <=
2 * exp (-2 * t ^ 2) := by
have hY_mem : ∀ᵐ omega ∂P, Y omega ∈ Icc (0 : Real) 1 :=
hY_nonneg.and hY_le_one
have hY_int : Integrable Y P :=
Integrable.of_mem_Icc 0 1 hY.aemeasurable hY_mem
have hmean_comp :
(fun omega => ∫ y, y ∂condDistrib Y design P (design omega)) =ᵐ[P]
mD ∘ design :=
(condExp_ae_eq_integral_condDistrib' hdesign hY_int).symm.trans hcond
have hmean :
∀ᵐ d ∂P.map design, ∫ y, y ∂condDistrib Y design P d = mD d := by
rw [ae_map_iff hdesign.aemeasurable]
· filter_upwards [hmean_comp] with x hx
exact hx
· exact measurableSet_eq_fun
(((stronglyMeasurable_id.comp_measurable measurable_snd).integral_condDistrib
(X := design) (Y := Y) (μ := P)).measurable)
hmD
have hpair :
∀ᵐ p ∂(P.map design ⊗ₘ condDistrib Y design P),
p.2 ∈ Icc (0 : Real) 1 := by
rw [compProd_map_condDistrib hY.aemeasurable]
rw [ae_map_iff (hdesign.prodMk hY).aemeasurable]
· simpa using hY_mem
· exact measurableSet_Icc.preimage measurable_snd
have hrange :
∀ᵐ d ∂P.map design,
∀ᵐ y ∂condDistrib Y design P d, y ∈ Icc (0 : Real) 1 :=
Measure.ae_ae_of_ae_compProd hpair
let obsLaw : Measure (Fin N -> Omega) := Measure.pi (fun _ : Fin N => P)
let designLaw : Measure (Fin N -> D) :=
Measure.pi (fun _ : Fin N => P.map design)
let designVec : (Fin N -> Omega) -> (Fin N -> D) := designVector design
have hdesignVec : Measurable designVec := by
simpa only [designVec] using measurable_designVector design hdesign
have henergySet : MeasurableSet
{d : Fin N -> D | 0 < realizedWeightEnergy w d} :=
measurableSet_lt measurable_const (measurable_realizedWeightEnergy hw)
have hmapDesign : obsLaw.map designVec = designLaw := by
change (Measure.pi (fun _ : Fin N => P)).map
(fun z : Fin N -> Omega => fun i => design (z i)) =
Measure.pi (fun _ : Fin N => P.map design)
exact Causalean.Stat.map_pi_finCoordinatewise N P hdesign
have henergyDesign : ∀ᵐ d ∂designLaw, 0 < realizedWeightEnergy w d := by
rw [← hmapDesign, ae_map_iff hdesignVec.aemeasurable henergySet]
simpa only [obsLaw, designVec] using henergy
letI : IsProbabilityMeasure (P.map design) :=
Measure.isProbabilityMeasure_map hdesign.aemeasurable
have hattached := product_weighted_centered_attachKernel_tail_le
(N := N) (P.map design) (condDistrib Y design P) mD hmD hmean hrange w hw
henergyDesign ht
let jointMap : (Fin N -> Omega) -> (Fin N -> D) × (Fin N -> Real) :=
fun z => (designVector design z, fun i => Y (z i))
have hjointMap : Measurable jointMap := by
exact (measurable_designVector design hdesign).prodMk
(measurable_finCoordinatewise N hY)
let event : Set ((Fin N -> D) × (Fin N -> Real)) :=
{p | t * sqrt (realizedWeightEnergy w p.1) <=
|weightedCenteredMarkSum mD w p.1 p.2|}
have hevent : MeasurableSet event := by
exact measurableSet_le
(measurable_const.mul
((measurable_realizedWeightEnergy hw).comp measurable_fst).sqrt)
(measurable_weightedCenteredMarkSum hmD hw).abs
have hpull : jointMap ⁻¹' event =
{z | t * sqrt
(realizedWeightEnergy w (designVector design z)) <=
|weightedCenteredSum design Y mD w z|} := by
ext z
simp only [Set.mem_preimage, Set.mem_setOf_eq, jointMap, event]
change
t * sqrt (realizedWeightEnergy w (designVector design z)) <=
|∑ i, w (designVector design z) i *
(Y (z i) - mD (design (z i)))| ↔ _
rfl
have hlaw := product_observation_law_map_design_outcome
(N := N) P design hdesign Y hY
have hmapReal := map_measureReal_apply (μ := obsLaw) hjointMap hevent
rw [hlaw] at hmapReal
change obsLaw.real
{z | t * sqrt
(realizedWeightEnergy w (designVector design z)) <=
|weightedCenteredSum design Y mD w z|} <=
2 * exp (-2 * t ^ 2)
rw [← hpull, ← hmapReal]
simpa only [designLaw] using hattached
2 supporting declarations (lemmas, instances)
-
product_observation_law_map_design_outcometheorem — A probability law P, measurable design, and measurable outcome map an i.i.d. observation product to the retained-design law with the finite product of its one-observation conditional mark kernels.hypothesesN :Omega D :P :Measure Omegadesign :Omega -> Dhdesign :Measurable designY :Omega -> RealhY :conclusion= attachKernel (Measure.pi (fun _ : Fin N => P.map design)) (finProductKernel N (condDistrib Y design P))Proof (Lean source)
theorem product_observation_law_map_design_outcome {N : Nat} {Omega D : Type*} [MeasurableSpace Omega] [MeasurableSpace D] (P : Measure Omega) [IsProbabilityMeasure P] (design : Omega -> D) (hdesign : Measurable design) (Y : Omega -> Real) (hY : Measurable Y) : (Measure.pi (fun _ : Fin N => P)).map (fun z => (designVector design z, fun i => Y (z i))) = attachKernel (Measure.pi (fun _ : Fin N => P.map design)) (finProductKernel N (condDistrib Y design P)) := by -- First use `compProd_map_condDistrib` for one observation. Tensorize that equality -- with `map_pi_finCoordinatewise`, then split the vector of pairs into the pair of -- vectors; prove the resulting product-kernel identity on measurable rectangles. let pair : Omega → D × Real := fun omega => (design omega, Y omega) let split := MeasurableEquiv.arrowProdEquivProdArrow D Real (Fin N) have hpair : Measurable pair := hdesign.prodMk hY have hcoordinate := Causalean.Stat.map_pi_finCoordinatewise N P hpair have hdisintegrate : P.map pair = P.map design ⊗ₘ condDistrib Y design P := (compProd_map_condDistrib hY.aemeasurable).symm letI : IsProbabilityMeasure (P.map design) := Measure.isProbabilityMeasure_map hdesign.aemeasurable calc (Measure.pi (fun _ : Fin N => P)).map (fun z => (designVector design z, fun i => Y (z i))) = ((Measure.pi (fun _ : Fin N => P)).map (fun z => fun i => pair (z i))).map split := by rw [Measure.map_map split.measurable (measurable_finCoordinatewise N hpair)] rfl _ = (Measure.pi (fun _ : Fin N => P.map pair)).map split := by rw [hcoordinate] _ = (Measure.pi (fun _ : Fin N => P.map design ⊗ₘ condDistrib Y design P)).map split := by rw [hdisintegrate] _ = attachKernel (Measure.pi (fun _ : Fin N => P.map design)) (finProductKernel N (condDistrib Y design P)) := by exact map_pi_compProd_arrowProdEquivProdArrow (P.map design) (condDistrib Y design P) -
product_weighted_centered_attachKernel_tail_letheorem — Under a probability design law and Markov marking kernel whose conditional mean is the measurable regression, whose marks lie in the unit interval almost surely on almost every fibre, with measurable complete-design weights of positive realized energy almost surely, every nonnegative threshold obeys the two-sided self-normalized Hoeffding tail bound for the retained-design law.hypothesesN :D :Type*Q :K :mD :D -> RealhmD :Measurable mDhmean :∀ᵐ d ∂Q, ∫ y, y ∂K d = mD dhw :henergy :∀ᵐ d ∂Measure.pi (fun _ : Fin N => Q), 0 < realizedWeightEnergy w dt :ht :0 <= tconclusion(attachKernel (Measure.pi (fun _ : Fin N => Q)) (finProductKernel N K)).real {p | t * sqrt (realizedWeightEnergy w p.1) <= |weightedCenteredMarkSum mD w p.1 p.2|} <= 2 * exp (-2 * t ^ 2)Proof (Lean source)
theorem product_weighted_centered_attachKernel_tail_le {N : Nat} {D : Type*} [MeasurableSpace D] (Q : Measure D) [IsProbabilityMeasure Q] (K : Kernel D Real) [IsMarkovKernel K] (mD : D -> Real) (hmD : Measurable mD) (hmean : ∀ᵐ d ∂Q, ∫ y, y ∂K d = mD d) (hbound : ∀ᵐ d ∂Q, ∀ᵐ y ∂K d, y ∈ Icc (0 : Real) 1) (w : (Fin N -> D) -> Fin N -> Real) (hw : Measurable w) (henergy : ∀ᵐ d ∂Measure.pi (fun _ : Fin N => Q), 0 < realizedWeightEnergy w d) {t : Real} (ht : 0 <= t) : (attachKernel (Measure.pi (fun _ : Fin N => Q)) (Causalean.Stat.finProductKernel N K)).real {p | t * sqrt (realizedWeightEnergy w p.1) <= |weightedCenteredMarkSum mD w p.1 p.2|} <= 2 * exp (-2 * t ^ 2) := by let designLaw : Measure (Fin N -> D) := Measure.pi (fun _ : Fin N => Q) let markKernel := Causalean.Stat.finProductKernel N K let B : Real := 2 * exp (-2 * t ^ 2) have hB : 0 <= B := by positivity have hevent : MeasurableSet {p : (Fin N -> D) × (Fin N -> Real) | t * sqrt (realizedWeightEnergy w p.1) <= |weightedCenteredMarkSum mD w p.1 p.2|} := by exact measurableSet_le (measurable_const.mul ((measurable_realizedWeightEnergy hw).comp measurable_fst).sqrt) (measurable_weightedCenteredMarkSum hmD hw).abs have hfibre : ∀ᵐ d ∂designLaw, (markKernel d).real {y | t * sqrt (realizedWeightEnergy w d) <= |weightedCenteredMarkSum mD w d y|} <= B := by filter_upwards [product_weighted_centered_attachKernel_hasSubgaussianMGF Q K mD hmD hmean hbound w hw, henergy] with d hd hdenergy have henergy_nonneg : 0 <= realizedWeightEnergy w d := le_of_lt hdenergy have hepsilon : 0 <= t * sqrt (realizedWeightEnergy w d) := mul_nonneg ht (Real.sqrt_nonneg _) have hcoe : (toNNReal (realizedWeightEnergy w d / 4) : Real) = realizedWeightEnergy w d / 4 := Real.coe_toNNReal _ (div_nonneg henergy_nonneg (by norm_num)) have hexponent : -(t * sqrt (realizedWeightEnergy w d)) ^ 2 / (2 * (realizedWeightEnergy w d / 4)) = -2 * t ^ 2 := by rw [mul_pow, Real.sq_sqrt henergy_nonneg] field_simp [ne_of_gt hdenergy] ring have hup := hd.measure_ge_le hepsilon rw [hcoe, hexponent] at hup have hup' : (markKernel d).real {y | t * sqrt (realizedWeightEnergy w d) <= weightedCenteredMarkSum mD w d y - 0} <= exp (-2 * t ^ 2) := by simpa only [sub_zero, markKernel] using hup have hlow0 := hd.neg.measure_ge_le hepsilon rw [hcoe, hexponent] at hlow0 have hlow : (markKernel d).real {y | t * sqrt (realizedWeightEnergy w d) <= -weightedCenteredMarkSum mD w d y + 0} <= exp (-2 * t ^ 2) := by simpa only [Pi.neg_apply, add_zero] using hlow0 have htwo := measureReal_abs_dev_le_two_sided (μ := markKernel d) (weightedCenteredMarkSum mD w d) 0 (exp (-2 * t ^ 2)) (exp (-2 * t ^ 2)) (t * sqrt (realizedWeightEnergy w d)) hup' hlow simpa only [sub_zero, B, two_mul] using htwo have hfibreENN : ∀ᵐ d ∂designLaw, markKernel d (Prod.mk d ⁻¹' {p : (Fin N -> D) × (Fin N -> Real) | t * sqrt (realizedWeightEnergy w p.1) <= |weightedCenteredMarkSum mD w p.1 p.2|}) <= ofReal B := by filter_upwards [hfibre] with d hd have hd' : (markKernel d).real (Prod.mk d ⁻¹' {p : (Fin N -> D) × (Fin N -> Real) | t * sqrt (realizedWeightEnergy w p.1) <= |weightedCenteredMarkSum mD w p.1 p.2|}) <= B := by simpa only [Set.mem_setOf_eq, Set.preimage_setOf_eq, Function.comp_apply] using hd rw [measureReal_def] at hd' rw [← ENNReal.ofReal_toReal (measure_ne_top (markKernel d) _)] exact ENNReal.ofReal_le_ofReal hd' have hjoint : (designLaw ⊗ₘ markKernel) {p : (Fin N -> D) × (Fin N -> Real) | t * sqrt (realizedWeightEnergy w p.1) <= |weightedCenteredMarkSum mD w p.1 p.2|} <= ofReal B := by rw [Measure.compProd_apply hevent] calc (∫⁻ d, markKernel d (Prod.mk d ⁻¹' {p : (Fin N -> D) × (Fin N -> Real) | t * sqrt (realizedWeightEnergy w p.1) <= |weightedCenteredMarkSum mD w p.1 p.2|}) ∂designLaw) <= ∫⁻ _ : Fin N -> D, ofReal B ∂designLaw := lintegral_mono_ae hfibreENN _ = ofReal B := by simp [designLaw] change (designLaw ⊗ₘ markKernel).real {p | t * sqrt (realizedWeightEnergy w p.1) <= |weightedCenteredMarkSum mD w p.1 p.2|} <= B rw [measureReal_def] calc ((designLaw ⊗ₘ markKernel) {p | t * sqrt (realizedWeightEnergy w p.1) <= |weightedCenteredMarkSum mD w p.1 p.2|}).toReal <= (ofReal B).toReal := ENNReal.toReal_mono ENNReal.ofReal_ne_top hjoint _ = B := ENNReal.toReal_ofReal hB