Stat.Concentration.Hoeffding.Random­Design

@[fun_prop] theorem measurable_designVector {N : Nat} {Omega D : Type*} [MeasurableSpace Omega] [MeasurableSpace D] (design : Omega -> D) (hdesign : Measurable design) : Measurable (designVector (N := N) design) := by rw [measurable_pi_iff] intro i exact hdesign.comp (measurable_pi_apply i)

theorem product_weighted_centered_sq_integral_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 : forall omega, 0 <= Y omega) (hY_le_one : forall omega, 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) (hweight_sq : Integrable (fun z : Fin N -> Omega => ∑ i, (w (designVector design z) i) ^ 2) (Measure.pi (fun _ : Fin N => P))) (hsum_sq : Integrable (fun z : Fin N -> Omega => (weightedCenteredSum design Y mD w z) ^ 2) (Measure.pi (fun _ : Fin N => P))) : (∫ z : Fin N -> Omega, (weightedCenteredSum design Y mD w z) ^ 2 ∂(Measure.pi (fun _ : Fin N => P))) <= (1 / 4 : Real) * (∫ z : Fin N -> Omega, ∑ i, (w (designVector design z) i) ^ 2 ∂(Measure.pi (fun _ : Fin N => P))) := by cases N with | zero => simp [weightedCenteredSum] | succ n => let μN : Measure (Fin (n + 1) -> Omega) := Measure.pi fun _ : Fin (n + 1) => P let W : Fin (n + 1) -> (Fin (n + 1) -> Omega) -> Real := fun i z => w (designVector design z) i let R : Fin (n + 1) -> (Fin (n + 1) -> Omega) -> Real := fun i z => Y (z i) - mD (design (z i)) let X : Fin (n + 1) -> (Fin (n + 1) -> Omega) -> Real := fun i z => W i z * R i z have hdesignN : Measurable (designVector (N := n + 1) design) := measurable_designVector design hdesign have hWmeas (i : Fin (n + 1)) : Measurable (W i) := by exact (measurable_pi_apply i).comp (hw.comp hdesignN) have hRmeas (i : Fin (n + 1)) : Measurable (R i) := by exact (hY.comp (measurable_pi_apply i)).sub (hmD.comp (hdesign.comp (measurable_pi_apply i))) have hXmeas (i : Fin (n + 1)) : Measurable (X i) := (hWmeas i).mul (hRmeas i) have henergyMeas : Measurable (fun z : Fin (n + 1) -> Omega => ∑ i, (W i z) ^ 2) := Finset.measurable_sum _ fun i _ => (hWmeas i).pow_const 2 obtain ⟨hYInt, hmInt, hm_nonneg, hm_le_one, hcenter⟩ := residual_facts P design hdesign Y hY hY_nonneg hY_le_one mD hmD hcond have hRbound (i : Fin (n + 1)) : ∀ᵐ z ∂μN, ‖R i z‖ ≤ (2 : Real) := by have hmp := measurePreserving_eval (fun _ : Fin (n + 1) => P) i have hm0 := hmp.quasiMeasurePreserving.tendsto_ae.eventually hm_nonneg have hm1 := hmp.quasiMeasurePreserving.tendsto_ae.eventually hm_le_one filter_upwards [hm0, hm1] with z hz0 hz1 change 0 ≤ mD (design (z i)) at hz0 change mD (design (z i)) ≤ 1 at hz1 rw [Real.norm_eq_abs] apply abs_le.2 constructor <;> linarith [hY_nonneg (z i), hY_le_one (z i)] have hWiSq (i : Fin (n + 1)) : Integrable (fun z => (W i z) ^ 2) μN := by apply Integrable.mono hweight_sq ((hWmeas i).pow_const 2).aestronglyMeasurable filter_upwards with z rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _), Real.norm_eq_abs, abs_of_nonneg (Finset.sum_nonneg fun _ _ => sq_nonneg _)] exact Finset.single_le_sum (s := univ) (f := fun k : Fin (n + 1) => (W k z) ^ 2) (fun k _ => sq_nonneg (W k z)) (Finset.mem_univ i) have hXiSq (i : Fin (n + 1)) : Integrable (fun z => (X i z) ^ 2) μN := by apply (hWiSq i).const_mul 4 |>.mono' · exact (hXmeas i).pow_const 2 |>.aestronglyMeasurable · filter_upwards [hRbound i] with z hr change ‖(X i z) ^ 2‖ ≤ (4 : Real) * (W i z) ^ 2 rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] change (W i z * R i z) ^ 2 ≤ 4 * W i z ^ 2 rw [Real.norm_eq_abs] at hr have hrsq : (R i z) ^ 2 ≤ 4 := by rw [← sq_abs] have hs := (sq_le_sq₀ (abs_nonneg (R i z)) (by norm_num)).2 hr norm_num at hs ⊢ exact hs rw [mul_pow] calc W i z ^ 2 * R i z ^ 2 ≤ W i z ^ 2 * 4 := mul_le_mul_of_nonneg_left hrsq (sq_nonneg _) _ = 4 * W i z ^ 2 := by ring have hcrossInt (i j : Fin (n + 1)) : Integrable (fun z => X i z * X j z) μN := by apply (hXiSq i).add (hXiSq j) |>.mono' · exact (hXmeas i).mul (hXmeas j) |>.aestronglyMeasurable · filter_upwards with z rw [Real.norm_eq_abs] have ha : 0 ≤ |X i z| := abs_nonneg _ have hb : 0 ≤ |X j z| := abs_nonneg _ have hab : |X i z * X j z| = |X i z| * |X j z| := abs_mul _ _ rw [hab] have hsq := sq_nonneg (|X i z| - |X j z|) have hi : (X i z) ^ 2 = |X i z| ^ 2 := (sq_abs _).symm have hj : (X j z) ^ 2 = |X j z| ^ 2 := (sq_abs _).symm change |X i z| * |X j z| ≤ (X i z) ^ 2 + (X j z) ^ 2 rw [hi, hj] nlinarith [sq_nonneg |X i z|, sq_nonneg |X j z|] have hdiag (i : Fin (n + 1)) : (∫ z, (X i z) ^ 2 ∂μN) ≤ (1 / 4 : Real) * ∫ z, (W i z) ^ 2 ∂μN := by simpa [μN, X, W, R] using product_diag_integral_le P design hdesign Y hY hY_nonneg hY_le_one mD hmD hcond w hw i (hXiSq i) (hWiSq i) have hcross (i j : Fin (n + 1)) (hij : i ≠ j) : (∫ z, X i z * X j z ∂μN) = 0 := by simpa [μN, X, W, R] using product_cross_integral_eq_zero P design hdesign Y hY hY_nonneg hY_le_one mD hmD hcond w hw i j hij (hcrossInt i j) have hsquare (z : Fin (n + 1) -> Omega) : (weightedCenteredSum design Y mD w z) ^ 2 = ∑ i, ∑ j, X i z * X j z := by rw [pow_two] simp only [weightedCenteredSum, X, W, R] rw [Finset.sum_mul_sum] have hsumIntegral : (∫ z, (weightedCenteredSum design Y mD w z) ^ 2 ∂μN) = ∑ i, ∑ j, ∫ z, X i z * X j z ∂μN := by rw [integral_congr_ae (Filter.Eventually.of_forall hsquare)] rw [integral_finsetSum univ] · apply Finset.sum_congr rfl intro i hi rw [integral_finsetSum univ] intro j hj exact hcrossInt i j · intro i hi exact integrable_finsetSum univ fun j _ => hcrossInt i j have hcollapse (i : Fin (n + 1)) : (∑ j, ∫ z, X i z * X j z ∂μN) = ∫ z, (X i z) ^ 2 ∂μN := by rw [Finset.sum_eq_single i] · apply integral_congr_ae filter_upwards with z rw [pow_two] · intro j hj hji exact hcross i j (Ne.symm hji) · simp have henergyIntegral : (∫ z, ∑ i, (W i z) ^ 2 ∂μN) = ∑ i, ∫ z, (W i z) ^ 2 ∂μN := by exact integral_finsetSum univ fun i _ => hWiSq i change (∫ z, (weightedCenteredSum design Y mD w z) ^ 2 ∂μN) ≤ (1 / 4 : Real) * ∫ z, ∑ i, (W i z) ^ 2 ∂μN rw [hsumIntegral] simp_rw [hcollapse] rw [henergyIntegral, Finset.mul_sum] exact Finset.sum_le_sum fun i _ => hdiag i

@[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 Finset.measurable_sum intro i _ exact ((measurable_pi_apply i).comp hw).pow_const 2

@[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 Finset.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)))

@[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 Finset.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))))

@[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)

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

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

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) (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) : ∀ᵐ 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 Finset.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

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) (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) : ∀ᵐ 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 hmean hbound w] with d hd intro s have hmgf := hd.mgf_le s have henergy_nonneg : 0 <= realizedWeightEnergy w d := by exact Finset.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

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)

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 hmean hbound w, 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