Mathlib.Probability.Sub­Gaussian

theorem dyadic_suffix_partition (N m : ℕ) (hm : 1 ≤ m) (f : Fin N → ℝ) : (∑ k : Fin N, if m ≤ k.val + 1 then f k else 0) = ∑ j ∈ range (N + 1), ∑ k : Fin N, if 2 ^ j * m ≤ k.val + 1 ∧ k.val + 1 < 2 * (2 ^ j * m) then f k else 0 := by classical rw [Finset.sum_comm] apply Finset.sum_congr rfl intro k _ let n := k.val + 1 let q := n / m have hm0 : 0 < m := hm by_cases hmn : m ≤ n · have hq : q ≠ 0 := (Nat.div_pos hmn hm0).ne' let j₀ := Nat.log 2 q have hj₀ : j₀ ∈ range (N + 1) := by apply Finset.mem_range.mpr have hle : j₀ ≤ n := (Nat.log_le_self 2 q).trans (Nat.div_le_self n m) have hn : n ≤ N := by dsimp [n] exact k.isLt omega have hblock : ∀ j : ℕ, (2 ^ j * m ≤ n ∧ n < 2 * (2 ^ j * m)) ↔ j = j₀ := by intro j constructor · rintro ⟨hlo, hhi⟩ have hlo' : 2 ^ j ≤ q := (Nat.le_div_iff_mul_le hm0).2 hlo have hhi' : q < 2 ^ (j + 1) := by apply (Nat.div_lt_iff_lt_mul hm0).2 simpa [pow_succ, mul_assoc, mul_comm, mul_left_comm] using hhi exact (Nat.log_eq_of_pow_le_of_lt_pow hlo' hhi').symm · intro hj subst j constructor · exact (Nat.le_div_iff_mul_le hm0).1 (Nat.pow_log_le_self 2 hq) · have hhi' := Nat.lt_pow_succ_log_self (by omega : 1 < 2) q have hhi'' := (Nat.div_lt_iff_lt_mul hm0).1 hhi' simpa [pow_succ, mul_assoc, mul_comm, mul_left_comm] using hhi'' rw [Finset.sum_eq_single_of_mem j₀ hj₀] · change (if m ≤ n then f k else 0) = (if 2 ^ j₀ * m ≤ n ∧ n < 2 * (2 ^ j₀ * m) then f k else 0) simp [hmn, (hblock j₀).2 rfl] · intro j _ hj have : ¬ (2 ^ j * m ≤ n ∧ n < 2 * (2 ^ j * m)) := by simpa only [hblock] using hj change (if 2 ^ j * m ≤ n ∧ n < 2 * (2 ^ j * m) then f k else 0) = 0 simp [this] · have hzero : ∀ j : ℕ, ¬ (2 ^ j * m ≤ n ∧ n < 2 * (2 ^ j * m)) := by intro j h have hpow : 0 < 2 ^ j := by positivity have : m ≤ 2 ^ j * m := by nlinarith omega change (if m ≤ n then f k else 0) = ∑ j ∈ range (N + 1), if 2 ^ j * m ≤ n ∧ n < 2 * (2 ^ j * m) then f k else 0 rw [if_neg hmn] symm apply Finset.sum_eq_zero intro j _ simp [hzero j]

theorem ordered_gaussian_tail_integral (α : ℝ) (hα : 0 < α) : ∃ Kα : ℝ, 0 < Kα ∧ ∀ (N : ℕ) (a b : ℝ), 0 < a → 0 < b → let g : ℝ → ℝ := fun t => min 1 (∑ k : Fin N, 2 * exp (-(t ^ 2) / (2 * min (a ^ 2) (b ^ 2 * (k.val + 1 : ℝ) ^ (-α))))) IntegrableOn g (Ioi (0 : ℝ)) volume ∧ ∫ t in Ioi (0 : ℝ), g t ≤ Kα * a * sqrt (1 + max 0 (log ((b / a) ^ (2 / α)))) := by obtain ⟨C, hC, hprefix⟩ := clipped_gaussian_integral obtain ⟨D, hD, hsuffix⟩ := decaying_gaussian_suffix_integral α hα refine ⟨2 * (C + D), by positivity, ?_⟩ intro N a b ha hb dsimp let R : ℝ := (b / a) ^ (2 / α) let m : ℕ := ⌈R⌉₊ have hR : 0 < R := by dsimp [R]; positivity have hm : 1 ≤ m := Nat.one_le_ceil_iff.mpr hR have hmpos : (0 : ℝ) < m := by exact_mod_cast (lt_of_lt_of_le Nat.zero_lt_one hm) have hRm : R ≤ (m : ℝ) := Nat.le_ceil R have hmR : (m : ℝ) ≤ 2 * max 1 R := by have hceil : (m : ℝ) < R + 1 := Nat.ceil_lt_add_one hR.le rcases le_total R 1 with h | h · rw [max_eq_left h] linarith · rw [max_eq_right h] linarith have hlogm : 1 + log (m : ℝ) ≤ 2 * (1 + max 0 (log R)) := by have hmax : (0 : ℝ) < max 1 R := lt_of_lt_of_le (by norm_num) (le_max_left _ _) have hlog : log (m : ℝ) ≤ log (2 * max 1 R) := Real.log_le_log hmpos hmR have hlogtwo : log (2 : ℝ) ≤ 1 := by have := Real.log_le_sub_one_of_pos (show (0 : ℝ) < 2 by norm_num) norm_num at this ⊢ exact this have hlogmax : log (max 1 R) = max 0 (log R) := by rcases le_total R 1 with h | h · rw [max_eq_left h, Real.log_one, max_eq_left] exact Real.log_nonpos (le_of_lt hR) h · rw [max_eq_right h, max_eq_right] exact Real.log_nonneg h rw [Real.log_mul (by norm_num : (2 : ℝ) ≠ 0) hmax.ne', hlogmax] at hlog have : 0 ≤ max 0 (log R) := le_max_left _ _ linarith have hsqrt : sqrt (1 + log (m : ℝ)) ≤ 2 * sqrt (1 + max 0 (log R)) := by have hnonneg : 0 ≤ 1 + log (m : ℝ) := by have : 0 ≤ log (m : ℝ) := Real.log_nonneg (by exact_mod_cast hm) linarith have harg : 0 ≤ 1 + max 0 (log R) := by have : 0 ≤ max 0 (log R) := le_max_left _ _ linarith have hs := Real.sqrt_le_sqrt hlogm have hsq : sqrt (2 * (1 + max 0 (log R))) ≤ 2 * sqrt (1 + max 0 (log R)) := by have h1 := Real.sq_sqrt harg have h2 := Real.sq_sqrt (show 0 ≤ 2 * (1 + max 0 (log R)) by positivity) nlinarith [Real.sqrt_nonneg (2 * (1 + max 0 (log R))), Real.sqrt_nonneg (1 + max 0 (log R))] exact hs.trans hsq have hRpow : R ^ α = (b / a) ^ (2 : ℕ) := by dsimp [R] rw [← Real.rpow_mul (div_pos hb ha).le] have he : (2 / α) * α = 2 := by field_simp rw [he] norm_cast have hba : b ^ 2 ≤ a ^ 2 * (m : ℝ) ^ α := by have hrpow := Real.rpow_le_rpow hR.le hRm hα.le have hdiv : (b / a) ^ (2 : ℕ) = b ^ 2 / a ^ 2 := by ring rw [hRpow, hdiv] at hrpow have ha2 : 0 < a ^ 2 := by positivity apply (div_le_iff₀ ha2).mp at hrpow nlinarith have hvar (k : Fin N) : b ^ 2 * (k.val + 1 : ℝ) ^ (-α) ≤ a ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α := by have hk : (0 : ℝ) < (k.val + 1 : ℝ) := by positivity rw [Real.div_rpow hmpos.le hk.le, Real.rpow_neg hk.le] have hpow : 0 ≤ ((k.val + 1 : ℝ) ^ α)⁻¹ := by positivity have hh := mul_le_mul_of_nonneg_right hba hpow have heq : a ^ 2 * (m : ℝ) ^ α * ((k.val + 1 : ℝ) ^ α)⁻¹ = a ^ 2 * ((m : ℝ) ^ α / (k.val + 1 : ℝ) ^ α) := by ring rw [heq] at hh exact hh let f (k : Fin N) (t : ℝ) : ℝ := 2 * exp (-(t ^ 2) / (2 * min (a ^ 2) (b ^ 2 * (k.val + 1 : ℝ) ^ (-α)))) let P (t : ℝ) : ℝ := min 1 (2 * (m : ℝ) * exp (-(t ^ 2) / (2 * a ^ 2))) let S (t : ℝ) : ℝ := min 1 (∑ k : Fin N, if m ≤ k.val + 1 then 2 * exp (-(t ^ 2) / (2 * a ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α)) else 0) let g (t : ℝ) : ℝ := min 1 (∑ k : Fin N, f k t) have hfpos (k : Fin N) : 0 < min (a ^ 2) (b ^ 2 * (k.val + 1 : ℝ) ^ (-α)) := by apply lt_min <;> positivity have hfint (k : Fin N) : Integrable (f k) volume := by have hh : 0 < (1 / (2 * min (a ^ 2) (b ^ 2 * (k.val + 1 : ℝ) ^ (-α))) : ℝ) := by positivity [hfpos k] have hi := (integrable_exp_neg_mul_sq hh).const_mul (2 : ℝ) convert hi using 1 ext t dsimp [f] congr 1 ring_nf have hgint : IntegrableOn g (Ioi (0 : ℝ)) volume := by have hraw : IntegrableOn (fun t : ℝ => ∑ k : Fin N, f k t) (Ioi (0 : ℝ)) volume := (integrable_finsetSum _ (fun k _ => hfint k)).integrableOn apply hraw.mono' · exact (aestronglyMeasurable_const.inf hraw.aestronglyMeasurable) · filter_upwards [] with t rw [Real.norm_eq_abs, abs_of_nonneg (by dsimp [g] apply le_min (by norm_num) exact Finset.sum_nonneg (fun k _ => by positivity [f]))] exact min_le_right _ _ obtain ⟨hPint, hPbound⟩ := hprefix m a hm ha obtain ⟨hSint, hSbound⟩ := hsuffix N m a hm ha have hPint' : IntegrableOn P (Ioi (0 : ℝ)) volume := hPint have hSint' : IntegrableOn S (Ioi (0 : ℝ)) volume := hSint let T : Finset (Fin N) := Finset.univ.filter (fun k => k.val + 1 < m) have hTcard : T.card ≤ m := by have hc : T.card ≤ (range m).card := by apply Finset.card_le_card_of_injOn (fun k : Fin N => k.val) · intro k hk have hkm : k.val + 1 < m := (Finset.mem_filter.mp hk).2 simpa using (show k.val < m by omega) · intro k _ j _ heq exact Fin.ext heq simpa using hc have hprefixTerm (k : Fin N) (t : ℝ) : f k t ≤ 2 * exp (-(t ^ 2) / (2 * a ^ 2)) := by have hd : 0 < 2 * min (a ^ 2) (b ^ 2 * (k.val + 1 : ℝ) ^ (-α)) := by positivity [hfpos k] have ha2 : 0 < 2 * a ^ 2 := by positivity have hden : 2 * min (a ^ 2) (b ^ 2 * (k.val + 1 : ℝ) ^ (-α)) ≤ 2 * a ^ 2 := by nlinarith [min_le_left (a ^ 2) (b ^ 2 * (k.val + 1 : ℝ) ^ (-α))] have he : -(t ^ 2) / (2 * min (a ^ 2) (b ^ 2 * (k.val + 1 : ℝ) ^ (-α))) ≤ -(t ^ 2) / (2 * a ^ 2) := by apply (div_le_div_iff₀ hd ha2).2 nlinarith [mul_nonneg (sq_nonneg t) (sub_nonneg.mpr hden)] exact mul_le_mul_of_nonneg_left (Real.exp_le_exp.mpr he) (by norm_num) have hprefixPoint (t : ℝ) : min 1 (∑ k : Fin N, if k.val + 1 < m then f k t else 0) ≤ P t := by have heq : (∑ k : Fin N, if k.val + 1 < m then f k t else 0) = ∑ k ∈ T, f k t := by simp [T, Finset.sum_filter] rw [heq] have hsum : (∑ k ∈ T, f k t) ≤ 2 * (m : ℝ) * exp (-(t ^ 2) / (2 * a ^ 2)) := by calc _ ≤ ∑ _k ∈ T, 2 * exp (-(t ^ 2) / (2 * a ^ 2)) := Finset.sum_le_sum (fun k _ => hprefixTerm k t) _ = (T.card : ℝ) * (2 * exp (-(t ^ 2) / (2 * a ^ 2))) := by simp _ ≤ 2 * (m : ℝ) * exp (-(t ^ 2) / (2 * a ^ 2)) := by have hc : (T.card : ℝ) ≤ m := by exact_mod_cast hTcard nlinarith [Real.exp_pos (-(t ^ 2) / (2 * a ^ 2))] exact min_le_min_left _ hsum have hsuffixTerm (k : Fin N) (t : ℝ) : f k t ≤ 2 * exp (-(t ^ 2) / (2 * a ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α)) := by have hd : 0 < 2 * min (a ^ 2) (b ^ 2 * (k.val + 1 : ℝ) ^ (-α)) := by positivity [hfpos k] have hd2 : 0 < 2 * a ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α := by positivity have hden : 2 * min (a ^ 2) (b ^ 2 * (k.val + 1 : ℝ) ^ (-α)) ≤ 2 * a ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α := by nlinarith [min_le_right (a ^ 2) (b ^ 2 * (k.val + 1 : ℝ) ^ (-α)), hvar k] have he : -(t ^ 2) / (2 * min (a ^ 2) (b ^ 2 * (k.val + 1 : ℝ) ^ (-α))) ≤ -(t ^ 2) / (2 * a ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α) := by apply (div_le_div_iff₀ hd hd2).2 nlinarith [mul_nonneg (sq_nonneg t) (sub_nonneg.mpr hden)] exact mul_le_mul_of_nonneg_left (Real.exp_le_exp.mpr he) (by norm_num) have hsuffixPoint (t : ℝ) : min 1 (∑ k : Fin N, if m ≤ k.val + 1 then f k t else 0) ≤ S t := by apply min_le_min_left apply Finset.sum_le_sum intro k _ split · exact hsuffixTerm k t · exact le_refl 0 have hpoint (t : ℝ) : g t ≤ P t + S t := by have hsplit : (∑ k : Fin N, f k t) = (∑ k : Fin N, if k.val + 1 < m then f k t else 0) + (∑ k : Fin N, if m ≤ k.val + 1 then f k t else 0) := by rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro k _ by_cases hk : k.val + 1 < m · have hnot : ¬m ≤ k.val + 1 := by omega simp [hk, hnot] · have hle : m ≤ k.val + 1 := by omega simp [hk, hle] dsimp [g] rw [hsplit] have hmin (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) : min 1 (x + y) ≤ min 1 x + min 1 y := by rcases le_total 1 x with h | h · rw [min_eq_left h, min_eq_left (by linarith : 1 ≤ x + y)] have : 0 ≤ min 1 y := le_min (by norm_num) hy linarith · rcases le_total 1 y with h' | h' · rw [min_eq_left h', min_eq_left (by linarith : 1 ≤ x + y)] have : 0 ≤ min 1 x := le_min (by norm_num) hx linarith · rw [min_eq_right h, min_eq_right h'] exact min_le_right _ _ have hx : 0 ≤ (∑ k : Fin N, if k.val + 1 < m then f k t else 0) := by apply Finset.sum_nonneg intro k _ split <;> positivity [f] have hy : 0 ≤ (∑ k : Fin N, if m ≤ k.val + 1 then f k t else 0) := by apply Finset.sum_nonneg intro k _ split <;> positivity [f] exact (hmin _ _ hx hy).trans (add_le_add (hprefixPoint t) (hsuffixPoint t)) -- … truncated; follow the source link for the rest …

theorem expected_max_le_tail_integral {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (N : ℕ) (Z : Fin N → Ω → ℝ) (g : ℝ → ℝ) (hInt : ∀ k : Fin N, ∀ t : ℝ, Integrable (fun ω => exp (t * Z k ω)) μ) (hg : IntegrableOn g (Ioi (0 : ℝ)) volume) (hTail : ∀ t : ℝ, 0 ≤ t → μ.real {ω | t < sSup ((fun k : Fin N => |Z k ω|) '' univ)} ≤ g t) : ∫ ω, sSup ((fun k : Fin N => |Z k ω|) '' univ) ∂μ ≤ ∫ t in Ioi (0 : ℝ), g t := by have hcoord : ∀ k : Fin N, Integrable (fun ω => |Z k ω|) μ := by intro k simpa using (integrable_pow_abs_of_integrable_exp_mul (μ := μ) (X := Z k) (t := (1 : ℝ)) one_ne_zero (hInt k 1) (hInt k (-1)) 1) have htail_int : IntegrableOn (fun t : ℝ => μ.real {ω | t < sSup ((fun k : Fin N => |Z k ω|) '' univ)}) (Ioi (0 : ℝ)) volume := by have hnonneg : 0 ≤ᵐ[volume.restrict (Ioi (0 : ℝ))] (fun t : ℝ => μ.real {ω | t < sSup ((fun k : Fin N => |Z k ω|) '' univ)}) := Filter.Eventually.of_forall (fun _ => ENNReal.toReal_nonneg) have hle : (fun t : ℝ => μ.real {ω | t < sSup ((fun k : Fin N => |Z k ω|) '' univ)}) ≤ᵐ[volume.restrict (Ioi (0 : ℝ))] g := by filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht exact hTail t ht.le have hmeas : Measurable (fun t : ℝ => μ.real {ω | t < sSup ((fun k : Fin N => |Z k ω|) '' univ)}) := by apply Measurable.ennreal_toReal exact Antitone.measurable (fun _ _ hst => measure_mono (fun _ h => lt_of_le_of_lt hst h)) exact Integrable.mono_nonneg hg hmeas.aestronglyMeasurable hnonneg hle by_cases hN : N = 0 · subst N have hzero : (fun ω => sSup ((fun k : Fin 0 => |Z k ω|) '' univ)) = (fun _ => (0 : ℝ)) := by funext ω simp rw [hzero, integral_zero] exact setIntegral_nonneg measurableSet_Ioi fun t ht => (ENNReal.toReal_nonneg).trans (hTail t ht.le) · have hU : (Finset.univ : Finset (Fin N)).Nonempty := ⟨Classical.choice (Fin.pos_iff_nonempty.mp (Nat.pos_of_ne_zero hN)), Finset.mem_univ _⟩ have hsup : Integrable (fun ω => (Finset.univ : Finset (Fin N)).sup' hU (fun k => |Z k ω|)) μ := by have aux : ∀ (s : Finset (Fin N)) (hs : s.Nonempty), Integrable (fun ω => s.sup' hs (fun k => |Z k ω|)) μ := by intro s hs induction hs using Finset.Nonempty.cons_induction with | singleton k => simpa using hcoord k | cons k s hk hs ih => convert (hcoord k).sup ih using 1 funext ω exact Finset.sup'_cons hs (fun j => abs (Z j ω)) exact aux _ hU have hmax : Integrable (fun ω => sSup ((fun k : Fin N => |Z k ω|) '' univ)) μ := by convert hsup using 1 funext ω rw [Finset.sup'_eq_csSup_image] simp have hnonneg : 0 ≤ᵐ[μ] (fun ω => sSup ((fun k : Fin N => |Z k ω|) '' univ)) := by apply Filter.Eventually.of_forall intro ω change 0 ≤ sSup ((fun k : Fin N => |Z k ω|) '' univ) let k : Fin N := choice (Fin.pos_iff_nonempty.mp (Nat.pos_of_ne_zero hN)) have hb : BddAbove ((fun k : Fin N => |Z k ω|) '' univ) := (Set.finite_univ.image _).bddAbove exact (abs_nonneg (Z k ω)).trans (le_csSup hb (Set.mem_image_of_mem _ (Set.mem_univ k))) rw [hmax.integral_eq_integral_meas_lt hnonneg] exact setIntegral_mono_on htail_int hg measurableSet_Ioi (fun t ht => hTail t ht.le)

theorem orderedSubGaussianMaximal (α : ℝ) (hα : 0 < α) : ∃ Kα : ℝ, 0 < Kα ∧ ∀ {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (N : ℕ) (Z : Fin N → Ω → ℝ) (a b : ℝ), 0 < a → 0 < b → (∀ k : Fin N, ∀ t : ℝ, Integrable (fun ω => exp (t * Z k ω)) μ) → (∀ k : Fin N, ∀ t : ℝ, mgf (Z k) μ t ≤ exp (min (a ^ 2) (b ^ 2 * (k.val + 1 : ℝ) ^ (-α)) * t ^ 2 / 2)) → ∫ ω, sSup ((fun k : Fin N => |Z k ω|) '' univ) ∂μ ≤ Kα * a * sqrt (1 + max 0 (log ((b / a) ^ (2 / α)))) := by obtain ⟨Kα, hKα, hbound⟩ := ordered_gaussian_tail_integral α hα refine ⟨Kα, hKα, ?_⟩ intro Ω _ μ _ N Z a b ha hb hInt hmgf let v : Fin N → ℝ := fun k => min (a ^ 2) (b ^ 2 * (k.val + 1 : ℝ) ^ (-α)) let g : ℝ → ℝ := fun t => min 1 (∑ k : Fin N, 2 * exp (-(t ^ 2) / (2 * v k))) have hv : ∀ k : Fin N, 0 < v k := by intro k dsimp [v] apply lt_min <;> positivity obtain ⟨hg, hgb⟩ := hbound N a b ha hb calc (∫ ω, sSup ((fun k : Fin N => |Z k ω|) '' univ) ∂μ) ≤ ∫ t in Ioi (0 : ℝ), g t := by apply expected_max_le_tail_integral μ N Z g hInt · exact hg · intro t ht exact finite_max_tail_le μ N Z v hv hInt hmgf t ht _ ≤ Kα * a * sqrt (1 + max 0 (log ((b / a) ^ (2 / α)))) := hgb

theorem clipped_gaussian_integral : ∃ C : ℝ, 0 < C ∧ ∀ (m : ℕ) (σ : ℝ), 1 ≤ m → 0 < σ → let g : ℝ → ℝ := fun t => min 1 (2 * (m : ℝ) * exp (-(t ^ 2) / (2 * σ ^ 2))) IntegrableOn g (Ioi (0 : ℝ)) volume ∧ ∫ t in Ioi (0 : ℝ), g t ≤ C * σ * sqrt (1 + log (m : ℝ)) := by refine ⟨Real.exp 4, Real.exp_pos _, ?_⟩ intro m σ hm hσ dsimp let s : ℝ := sqrt (1 + log (m : ℝ)) let r : ℝ := σ * s have hmreal : (1 : ℝ) ≤ m := by exact_mod_cast hm have hmpos : (0 : ℝ) < m := by linarith have hlog : 0 ≤ log (m : ℝ) := Real.log_nonneg hmreal have hsarg : 0 < 1 + log (m : ℝ) := by linarith have hs : 0 < s := Real.sqrt_pos.2 hsarg have hs2 : s ^ 2 = 1 + log (m : ℝ) := Real.sq_sqrt hsarg.le have hsge : 1 ≤ s ^ 2 := by rw [hs2]; linarith have hlogm : log (2 * (m : ℝ)) ≤ s ^ 2 := by rw [hs2, Real.log_mul (by norm_num : (2 : ℝ) ≠ 0) hmpos.ne'] have h2 := Real.log_le_sub_one_of_pos (show (0 : ℝ) < 2 by norm_num) linarith have hr : 0 < r := mul_pos hσ hs have hb : 0 < (1 / (2 * σ ^ 2) : ℝ) := by positivity have hi : IntegrableOn (fun t : ℝ => 2 * (m : ℝ) * exp (-(t ^ 2) / (2 * σ ^ 2))) (Ioi (0 : ℝ)) volume := by have hgauss : IntegrableOn (fun t : ℝ => 2 * (m : ℝ) * exp (-(1 / (2 * σ ^ 2)) * t ^ 2)) (Ioi (0 : ℝ)) volume := ((integrable_exp_neg_mul_sq hb).const_mul (2 * (m : ℝ))).integrableOn have hfun : (fun t : ℝ => 2 * (m : ℝ) * exp (-(1 / (2 * σ ^ 2)) * t ^ 2)) = (fun t : ℝ => 2 * (m : ℝ) * exp (-(t ^ 2) / (2 * σ ^ 2))) := by funext t congr 1 ring rw [hfun] at hgauss exact hgauss have hgi : IntegrableOn (fun t : ℝ => min 1 (2 * (m : ℝ) * exp (-(t ^ 2) / (2 * σ ^ 2)))) (Ioi (0 : ℝ)) volume := by apply hi.mono' · fun_prop · filter_upwards [] with t rw [Real.norm_eq_abs, abs_of_nonneg (by positivity)] exact min_le_right _ _ have ha : -(1 / r) < (0 : ℝ) := neg_lt_zero.mpr (by positivity) have heq : (fun t : ℝ => exp (4 - t / r)) = (fun t : ℝ => exp 4 * exp ((-(1 / r)) * t)) := by funext t rw [← Real.exp_add] congr 1 ring have hei : IntegrableOn (fun t : ℝ => exp (4 - t / r)) (Ioi (0 : ℝ)) volume := by rw [heq] exact (integrableOn_exp_mul_Ioi ha 0).const_mul _ have heval : (∫ t in Ioi (0 : ℝ), exp (4 - t / r)) = exp 4 * r := by rw [heq, integral_const_mul, integral_exp_mul_Ioi ha] simp have hpoint (t : ℝ) : min 1 (2 * (m : ℝ) * exp (-(t ^ 2) / (2 * σ ^ 2))) ≤ exp (4 - t / r) := by by_cases ht : t ≤ 4 * r · calc min 1 (2 * (m : ℝ) * exp (-(t ^ 2) / (2 * σ ^ 2))) ≤ 1 := min_le_left _ _ _ = exp 0 := by simp _ ≤ exp (4 - t / r) := Real.exp_le_exp.mpr (by have hdiv : t / r ≤ 4 := (div_le_iff₀ hr).2 (by nlinarith) linarith) · have hx : 4 ≤ t / r := (le_div_iff₀ hr).2 (by linarith) have hx2 : 0 ≤ (t / r) ^ 2 / 2 - 1 := by nlinarith have hprod : 0 ≤ (s ^ 2 - 1) * ((t / r) ^ 2 / 2 - 1) := mul_nonneg (by linarith) hx2 have hquad : s ^ 2 - s ^ 2 * (t / r) ^ 2 / 2 ≤ 4 - t / r := by nlinarith [sq_nonneg (t / r - 1)] have hid : t ^ 2 / (2 * σ ^ 2) = s ^ 2 * (t / r) ^ 2 / 2 := by dsimp [r] field_simp have hpos : 0 < 2 * (m : ℝ) := by positivity calc min 1 (2 * (m : ℝ) * exp (-(t ^ 2) / (2 * σ ^ 2))) ≤ 2 * (m : ℝ) * exp (-(t ^ 2) / (2 * σ ^ 2)) := min_le_right _ _ _ = exp (log (2 * (m : ℝ)) - t ^ 2 / (2 * σ ^ 2)) := by simp [Real.exp_sub, Real.exp_log hpos, Real.exp_neg, div_eq_mul_inv] _ ≤ exp (4 - t / r) := Real.exp_le_exp.mpr (by rw [hid]; linarith) refine ⟨hgi, ?_⟩ calc (∫ t in Ioi (0 : ℝ), min 1 (2 * (m : ℝ) * exp (-(t ^ 2) / (2 * σ ^ 2)))) ≤ ∫ t in Ioi (0 : ℝ), exp (4 - t / r) := setIntegral_mono_ae hgi hei (Filter.Eventually.of_forall hpoint) _ = exp 4 * σ * sqrt (1 + log (m : ℝ)) := by rw [heval] dsimp [r, s] ring

theorem weighted_dyadic_geometric_bound (α : ℝ) (hα : 0 < α) : ∃ Cα : ℝ, 0 < Cα ∧ ∀ J : ℕ, (∑ j ∈ range J, ((j : ℝ) + 1) * (exp (-(α * log 2 / 2))) ^ j) ≤ Cα := by let r : ℝ := exp (-(α * log 2 / 2)) have hr0 : 0 ≤ r := (Real.exp_pos _).le have hr1 : r < 1 := by dsimp [r] rw [Real.exp_lt_one_iff] have hlog : (0 : ℝ) < log 2 := Real.log_pos (by norm_num) have hpos : 0 < α * log 2 / 2 := by positivity linarith have hrnorm : ‖r‖ < 1 := by simpa [Real.norm_eq_abs, abs_of_nonneg hr0] using hr1 have hsum : Summable (fun j : ℕ => ((j : ℝ) + 1) * r ^ j) := by have hweighted : Summable (fun j : ℕ => (j : ℝ) * r ^ j) := by simpa using (summable_pow_mul_geometric_of_norm_lt_one (R := ℝ) 1 hrnorm) have hplain : Summable (fun j : ℕ => r ^ j) := summable_geometric_of_lt_one hr0 hr1 convert hweighted.add hplain using 1 ext j ring have hnonneg (j : ℕ) : 0 ≤ ((j : ℝ) + 1) * r ^ j := by positivity refine ⟨1 + ∑' j : ℕ, ((j : ℝ) + 1) * r ^ j, ?_, ?_⟩ · have htsum : 0 ≤ ∑' j : ℕ, ((j : ℝ) + 1) * r ^ j := tsum_nonneg hnonneg linarith · intro J change (∑ j ∈ range J, ((j : ℝ) + 1) * r ^ j) ≤ 1 + ∑' j : ℕ, ((j : ℝ) + 1) * r ^ j have hle := hsum.sum_le_tsum (range J) (fun j _ => hnonneg j) linarith

theorem decaying_gaussian_suffix_integral (α : ℝ) (hα : 0 < α) : ∃ Cα : ℝ, 0 < Cα ∧ ∀ (N m : ℕ) (σ : ℝ), 1 ≤ m → 0 < σ → let g : ℝ → ℝ := fun t => min 1 (∑ k : Fin N, if m ≤ k.val + 1 then 2 * exp (-(t ^ 2) / (2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α)) else 0) IntegrableOn g (Ioi (0 : ℝ)) volume ∧ ∫ t in Ioi (0 : ℝ), g t ≤ Cα * σ * sqrt (1 + log (m : ℝ)) := by obtain ⟨C, hC, hblock⟩ := gaussian_suffix_block_integral α hα obtain ⟨D, hD, hgeom⟩ := weighted_dyadic_geometric_bound α hα refine ⟨C * D, mul_pos hC hD, ?_⟩ intro N m σ hm hσ dsimp let f (k : Fin N) (t : ℝ) : ℝ := 2 * exp (-(t ^ 2) / (2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α)) let B (j : ℕ) (t : ℝ) : ℝ := ∑ k : Fin N, if 2 ^ j * m ≤ k.val + 1 ∧ k.val + 1 < 2 * (2 ^ j * m) then f k t else 0 let F (j : ℕ) (t : ℝ) : ℝ := min 1 (B j t) have hmreal : (1 : ℝ) ≤ m := by exact_mod_cast hm have hlogm : 0 ≤ log (m : ℝ) := Real.log_nonneg hmreal have hsqrt : 0 ≤ sqrt (1 + log (m : ℝ)) := Real.sqrt_nonneg _ have hBi (j : ℕ) : IntegrableOn (F j) (Ioi (0 : ℝ)) volume := by have hmL : m ≤ 2 ^ j * m := by have hp : 1 ≤ 2 ^ j := by exact Nat.one_le_pow j 2 (by omega) exact Nat.le_mul_of_pos_left m hp exact (hblock N m (2 ^ j * m) σ hm hmL hσ).1 have hBbound (j : ℕ) : (∫ t in Ioi (0 : ℝ), F j t) ≤ C * σ * ((m : ℝ) / (2 ^ j * m : ℝ)) ^ (α / 2) * sqrt (1 + log (2 ^ j * m : ℝ)) := by have hmL : m ≤ 2 ^ j * m := by have hp : 1 ≤ 2 ^ j := by exact Nat.one_le_pow j 2 (by omega) exact Nat.le_mul_of_pos_left m hp simpa only [F, B, f, Nat.cast_mul, Nat.cast_pow, Nat.cast_ofNat] using (hblock N m (2 ^ j * m) σ hm hmL hσ).2 have hscale (j : ℕ) : ((m : ℝ) / (2 ^ j * m : ℝ)) ^ (α / 2) = (exp (-(α * log 2 / 2))) ^ j := by have hmpos : (0 : ℝ) < m := by linarith have hp : (0 : ℝ) < (2 : ℝ) ^ j := by positivity have hcast : (2 ^ j * m : ℝ) = (2 : ℝ) ^ j * m := by norm_cast have hratio : (m : ℝ) / (2 ^ j * m : ℝ) = ((2 : ℝ) ^ j)⁻¹ := by rw [hcast] field_simp rw [hratio, Real.rpow_def_of_pos (inv_pos.mpr hp), Real.log_inv, Real.log_pow, ← Real.exp_nat_mul] congr 1 ring have hlogscale (j : ℕ) : sqrt (1 + log (2 ^ j * m : ℝ)) ≤ ((j : ℝ) + 1) * sqrt (1 + log (m : ℝ)) := by have hmpos : (0 : ℝ) < m := by linarith have hj : (0 : ℝ) ≤ j := Nat.cast_nonneg _ have hlog2 : log (2 : ℝ) ≤ 1 := by convert (Real.log_le_sub_one_of_pos (by norm_num : (0 : ℝ) < 2)) using 1 <;> norm_num have hlogeq : log (2 ^ j * m : ℝ) = (j : ℝ) * log 2 + log (m : ℝ) := by rw [Real.log_mul (by positivity) hmpos.ne', Real.log_pow] have harg : 0 ≤ 1 + log (2 ^ j * m : ℝ) := by rw [hlogeq] have : 0 ≤ log (2 : ℝ) := Real.log_nonneg (by norm_num) nlinarith have hsq : sqrt (1 + log (m : ℝ)) ^ 2 = 1 + log (m : ℝ) := Real.sq_sqrt (by linarith) have hsq' : sqrt (1 + log (2 ^ j * m : ℝ)) ^ 2 = 1 + log (2 ^ j * m : ℝ) := Real.sq_sqrt harg have hnonneg : 0 ≤ ((j : ℝ) + 1) * sqrt (1 + log (m : ℝ)) := by positivity nlinarith [mul_nonneg hj (sub_nonneg.mpr hlog2), mul_nonneg hj hlogm, sq_nonneg (j : ℝ)] have hpointNonneg (t : ℝ) (j : ℕ) : 0 ≤ B j t := by dsimp [B] apply Finset.sum_nonneg intro k _ split <;> positivity [f] have hminsum (t : ℝ) (s : Finset ℕ) : min 1 (∑ j ∈ s, B j t) ≤ ∑ j ∈ s, F j t := by classical induction s using Finset.induction_on with | empty => simp [F] | @insert j s hjs ih => simp only [Finset.sum_insert hjs] have ha := hpointNonneg t j have hb : 0 ≤ ∑ i ∈ s, B i t := by exact Finset.sum_nonneg (fun i _ => hpointNonneg t i) have hmin : min 1 (B j t + ∑ i ∈ s, B i t) ≤ min 1 (B j t) + min 1 (∑ i ∈ s, B i t) := by rcases le_total 1 (B j t) with h | h · have hc : 1 ≤ B j t + ∑ i ∈ s, B i t := by linarith rw [min_eq_left hc, min_eq_left h] have : 0 ≤ min 1 (∑ i ∈ s, B i t) := le_min (by norm_num) hb linarith · rcases le_total 1 (∑ i ∈ s, B i t) with h' | h' · have : 1 ≤ B j t + ∑ i ∈ s, B i t := by linarith rw [min_eq_left this, min_eq_left h'] have : 0 ≤ min 1 (B j t) := le_min (by norm_num) ha linarith · rw [min_eq_right h, min_eq_right h'] exact min_le_right _ _ dsimp [F] at ih ⊢ linarith have hpoint (t : ℝ) : min 1 (∑ k : Fin N, if m ≤ k.val + 1 then f k t else 0) ≤ ∑ j ∈ range (N + 1), F j t := by rw [dyadic_suffix_partition N m hm (fun k => f k t)] exact hminsum t (range (N + 1)) have hterm (k : Fin N) : Integrable (f k) volume := by have hb : 0 < (1 / (2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α) : ℝ) := by positivity have hi := (integrable_exp_neg_mul_sq hb).const_mul (2 : ℝ) convert hi using 1 ext t dsimp [f] congr 1 ring have hraw : IntegrableOn (fun t : ℝ => ∑ k : Fin N, if m ≤ k.val + 1 then f k t else 0) (Ioi (0 : ℝ)) volume := by apply Integrable.integrableOn apply integrable_finsetSum intro k _ split · exact hterm k · exact integrable_zero _ _ _ have hgi : IntegrableOn (fun t : ℝ => min 1 (∑ k : Fin N, if m ≤ k.val + 1 then f k t else 0)) (Ioi (0 : ℝ)) volume := by apply hraw.mono' · exact (aestronglyMeasurable_const.inf hraw.aestronglyMeasurable) · filter_upwards [] with t rw [Real.norm_eq_abs, abs_of_nonneg (by apply le_min (by norm_num) apply Finset.sum_nonneg intro k _ split <;> positivity [f])] exact min_le_right _ _ have hsumInt : IntegrableOn (fun t : ℝ => ∑ j ∈ range (N + 1), F j t) (Ioi (0 : ℝ)) volume := by apply integrable_finsetSum intro j _ exact hBi j refine ⟨hgi, ?_⟩ calc (∫ t in Ioi (0 : ℝ), min 1 (∑ k : Fin N, if m ≤ k.val + 1 then f k t else 0)) ≤ ∫ t in Ioi (0 : ℝ), ∑ j ∈ range (N + 1), F j t := setIntegral_mono_ae hgi hsumInt (Filter.Eventually.of_forall hpoint) _ = ∑ j ∈ range (N + 1), ∫ t in Ioi (0 : ℝ), F j t := by exact integral_finsetSum _ (fun j _ => hBi j) _ ≤ ∑ j ∈ range (N + 1), C * σ * (((j : ℝ) + 1) * (exp (-(α * log 2 / 2))) ^ j) * sqrt (1 + log (m : ℝ)) := by apply Finset.sum_le_sum intro j _ calc _ ≤ C * σ * ((m : ℝ) / (2 ^ j * m : ℝ)) ^ (α / 2) * sqrt (1 + log (2 ^ j * m : ℝ)) := hBbound j _ ≤ C * σ * (((j : ℝ) + 1) * (exp (-(α * log 2 / 2))) ^ j) * sqrt (1 + log (m : ℝ)) := by rw [hscale] have hp : 0 ≤ C * σ * (exp (-(α * log 2 / 2))) ^ j := by positivity nlinarith [hlogscale j] _ = C * σ * (∑ j ∈ range (N + 1), ((j : ℝ) + 1) * (exp (-(α * log 2 / 2))) ^ j) * sqrt (1 + log (m : ℝ)) := by rw [Finset.mul_sum, Finset.sum_mul] _ ≤ (C * D) * σ * sqrt (1 + log (m : ℝ)) := by have hp : 0 ≤ C * σ * sqrt (1 + log (m : ℝ)) := by positivity nlinarith [hgeom (N + 1)]

theorem gaussian_suffix_block_integral (α : ℝ) (hα : 0 < α) : ∃ C : ℝ, 0 < C ∧ ∀ (N m L : ℕ) (σ : ℝ), 1 ≤ m → m ≤ L → 0 < σ → let g : ℝ → ℝ := fun t => min 1 (∑ k : Fin N, if L ≤ k.val + 1 ∧ k.val + 1 < 2 * L then 2 * exp (-(t ^ 2) / (2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α)) else 0) IntegrableOn g (Ioi (0 : ℝ)) volume ∧ ∫ t in Ioi (0 : ℝ), g t ≤ C * σ * ((m : ℝ) / (L : ℝ)) ^ (α / 2) * sqrt (1 + log (L : ℝ)) := by obtain ⟨C, hC, hclip⟩ := clipped_gaussian_integral refine ⟨C, hC, ?_⟩ intro N m L σ hm hmL hσ dsimp let S : Finset (Fin N) := Finset.univ.filter (fun k => L ≤ k.val + 1 ∧ k.val + 1 < 2 * L) let a : ℝ := σ * ((m : ℝ) / (L : ℝ)) ^ (α / 2) have hL : 0 < L := lt_of_lt_of_le hm hmL have hLreal : (0 : ℝ) < L := by exact_mod_cast hL have hmreal : (0 : ℝ) < m := by exact_mod_cast (lt_of_lt_of_le Nat.zero_lt_one hm) have ha : 0 < a := by dsimp [a]; positivity have hcard : S.card ≤ L := by have hle : S.card ≤ (Ico L (2 * L)).card := by apply Finset.card_le_card_of_injOn (fun k : Fin N => k.val + 1) · intro k hk simpa [S, Finset.mem_Ico] using (Finset.mem_filter.mp hk).2 · intro k hk j hj heq apply Fin.ext exact Nat.add_right_cancel heq rw [Nat.card_Ico] at hle omega have hS (t : ℝ) : (∑ k : Fin N, if L ≤ k.val + 1 ∧ k.val + 1 < 2 * L then 2 * exp (-(t ^ 2) / (2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α)) else 0) = ∑ k ∈ S, 2 * exp (-(t ^ 2) / (2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α)) := by simp [S, Finset.sum_filter] have hterm (k : Fin N) : Integrable (fun t : ℝ => 2 * exp (-(t ^ 2) / (2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α))) volume := by have hb : 0 < (1 / (2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α) : ℝ) := by positivity have hi := (integrable_exp_neg_mul_sq hb).const_mul (2 : ℝ) convert hi using 1 ext t congr 1 ring have hsum : IntegrableOn (fun t : ℝ => ∑ k ∈ S, 2 * exp (-(t ^ 2) / (2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α))) (Ioi (0 : ℝ)) volume := by exact (integrable_finsetSum S (fun k _ => hterm k)).integrableOn have hgi : IntegrableOn (fun t : ℝ => min 1 (∑ k : Fin N, if L ≤ k.val + 1 ∧ k.val + 1 < 2 * L then 2 * exp (-(t ^ 2) / (2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α)) else 0)) (Ioi (0 : ℝ)) volume := by simp_rw [hS] apply hsum.mono' · fun_prop · filter_upwards [] with t rw [Real.norm_eq_abs, abs_of_nonneg (by positivity)] exact min_le_right _ _ have ha2 : a ^ 2 = σ ^ 2 * ((m : ℝ) / (L : ℝ)) ^ α := by dsimp [a] rw [mul_pow, ← Real.rpow_mul_natCast (le_of_lt (div_pos hmreal hLreal))] congr 1 ring have hpoint (t : ℝ) : min 1 (∑ k : Fin N, if L ≤ k.val + 1 ∧ k.val + 1 < 2 * L then 2 * exp (-(t ^ 2) / (2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α)) else 0) ≤ min 1 (2 * (L : ℝ) * exp (-(t ^ 2) / (2 * a ^ 2))) := by rw [hS] have hbound (k : Fin N) (hk : k ∈ S) : 2 * exp (-(t ^ 2) / (2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α)) ≤ 2 * exp (-(t ^ 2) / (2 * a ^ 2)) := by have hkL : L ≤ k.val + 1 := (Finset.mem_filter.mp hk).2.1 have hkreal : (0 : ℝ) < (k.val + 1 : ℝ) := by positivity have hfrac : (m : ℝ) / (k.val + 1 : ℝ) ≤ (m : ℝ) / (L : ℝ) := by apply (div_le_div_iff₀ hkreal hLreal).2 have hcast : (L : ℝ) ≤ (k.val + 1 : ℝ) := by exact_mod_cast hkL nlinarith have hq := Real.rpow_le_rpow (by positivity : 0 ≤ (m : ℝ) / (k.val + 1 : ℝ)) hfrac hα.le have hd1 : 0 < 2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α := by positivity have hd2 : 0 < 2 * a ^ 2 := by positivity have hden : 2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α ≤ 2 * a ^ 2 := by rw [ha2]; nlinarith [sq_nonneg σ] have hexp : -(t ^ 2) / (2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α) ≤ -(t ^ 2) / (2 * a ^ 2) := by apply (div_le_div_iff₀ hd1 hd2).2 nlinarith [mul_nonneg (sq_nonneg t) (sub_nonneg.mpr hden)] exact mul_le_mul_of_nonneg_left (Real.exp_le_exp.mpr hexp) (by norm_num) have hsumBound : (∑ k ∈ S, 2 * exp (-(t ^ 2) / (2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α))) ≤ 2 * (L : ℝ) * exp (-(t ^ 2) / (2 * a ^ 2)) := by calc _ ≤ ∑ _k ∈ S, 2 * exp (-(t ^ 2) / (2 * a ^ 2)) := Finset.sum_le_sum (fun k hk => hbound k hk) _ = (S.card : ℝ) * (2 * exp (-(t ^ 2) / (2 * a ^ 2))) := by simp _ ≤ 2 * (L : ℝ) * exp (-(t ^ 2) / (2 * a ^ 2)) := by have hc : (S.card : ℝ) ≤ (L : ℝ) := by exact_mod_cast hcard nlinarith [Real.exp_pos (-(t ^ 2) / (2 * a ^ 2))] exact min_le_min_left _ hsumBound obtain ⟨hclipi, hclipbound⟩ := hclip L a (lt_of_lt_of_le Nat.zero_lt_one hL) ha refine ⟨hgi, ?_⟩ calc (∫ t in Ioi (0 : ℝ), min 1 (∑ k : Fin N, if L ≤ k.val + 1 ∧ k.val + 1 < 2 * L then 2 * exp (-(t ^ 2) / (2 * σ ^ 2 * ((m : ℝ) / (k.val + 1 : ℝ)) ^ α)) else 0)) ≤ ∫ t in Ioi (0 : ℝ), min 1 (2 * (L : ℝ) * exp (-(t ^ 2) / (2 * a ^ 2))) := setIntegral_mono_ae hgi hclipi (Filter.Eventually.of_forall hpoint) _ ≤ C * a * sqrt (1 + log (L : ℝ)) := hclipbound _ = C * σ * ((m : ℝ) / (L : ℝ)) ^ (α / 2) * sqrt (1 + log (L : ℝ)) := by dsimp [a]; ring

theorem finite_max_tail_le {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (N : ℕ) (Z : Fin N → Ω → ℝ) (v : Fin N → ℝ) (hv : ∀ k, 0 < v k) (hInt : ∀ k : Fin N, ∀ t : ℝ, Integrable (fun ω => exp (t * Z k ω)) μ) (hmgf : ∀ k : Fin N, ∀ t : ℝ, mgf (Z k) μ t ≤ exp (v k * t ^ 2 / 2)) (t : ℝ) (ht : 0 ≤ t) : μ.real {ω | t < sSup ((fun k : Fin N => |Z k ω|) '' univ)} ≤ min 1 (∑ k : Fin N, 2 * exp (-(t ^ 2) / (2 * v k))) := by classical by_cases hN : N = 0 · subst N have hempty : {ω : Ω | t < 0} = ∅ := by ext ω simp [not_lt.mpr ht] simp [hempty] have hne : (Finset.univ : Finset (Fin N)).Nonempty := by simpa using Finset.univ_nonempty_iff.mpr (Fin.pos_iff_nonempty.mp (Nat.pos_of_ne_zero hN)) have hevent : {ω | t < sSup ((fun k : Fin N => |Z k ω|) '' univ)} = ⋃ k : Fin N, {ω | t < |Z k ω|} := by ext ω simp only [Set.mem_ofPred_eq, Set.mem_iUnion] have hsup : sSup ((fun k : Fin N => |Z k ω|) '' univ) = (Finset.univ : Finset (Fin N)).sup' hne (fun k => |Z k ω|) := by simpa using (Finset.sup'_eq_csSup_image Finset.univ hne (fun k : Fin N => |Z k ω|)).symm rw [hsup] simp only [Finset.lt_sup'_iff hne, Finset.mem_univ, true_and] have hcoord (k : Fin N) : μ.real {ω | t < |Z k ω|} ≤ 2 * exp (-(t ^ 2) / (2 * v k)) := by let c : NNReal := ⟨v k, le_of_lt (hv k)⟩ have hc : (c : ℝ) = v k := rfl have hk : HasSubgaussianMGF (Z k) c μ := by refine ⟨hInt k, ?_⟩ intro u simpa only [hc] using hmgf k u have hp := hk.measure_ge_le ht have hn := hk.neg.measure_ge_le ht have hs : {ω | t < |Z k ω|} ⊆ {ω | t ≤ Z k ω} ∪ {ω | t ≤ -(Z k ω)} := by intro ω hω simp only [Set.mem_ofPred_eq, Set.mem_union] at hω ⊢ rcases le_total 0 (Z k ω) with h | h · left simpa [abs_of_nonneg h] using le_of_lt hω · right simpa [abs_of_nonpos h] using le_of_lt hω calc μ.real {ω | t < |Z k ω|} ≤ μ.real ({ω | t ≤ Z k ω} ∪ {ω | t ≤ -(Z k ω)}) := measureReal_mono hs _ ≤ μ.real {ω | t ≤ Z k ω} + μ.real {ω | t ≤ -(Z k ω)} := measureReal_union_le _ _ _ ≤ 2 * exp (-(t ^ 2) / (2 * v k)) := by have hp' : μ.real {ω | t ≤ Z k ω} ≤ exp (-(t ^ 2) / (2 * v k)) := by simpa only [hc] using hp have hn' : μ.real {ω | t ≤ -(Z k ω)} ≤ exp (-(t ^ 2) / (2 * v k)) := by simpa only [hc, Pi.neg_apply] using hn linarith have hsum : μ.real {ω | t < sSup ((fun k : Fin N => |Z k ω|) '' univ)} ≤ ∑ k : Fin N, 2 * exp (-(t ^ 2) / (2 * v k)) := by rw [hevent] exact (measureReal_iUnion_fintype_le _).trans (Finset.sum_le_sum fun k _ => hcoord k) exact le_min (by simp) hsum