Stat.Concentration.Poisson

theorem poissonTable_pilot_cell_indicators_independent {J : Type*} [Fintype J] (evalRate : J → Fin 4 → ℝ≥0) (p : (J × Fin 4) → ℕ) (good : J → (Fin 4 → ℕ) → Bool) (φ : J → (Fin 4 → ℕ) → (Fin 4 → ℕ) → ℝ) (hφ : ∀ j, Measurable (φ j (poissonTableCell j p))) : iIndepFun (fun j (e : (J × Fin 4) → ℕ) => if good j (poissonTableCell j p) then φ j (poissonTableCell j p) (poissonTableCell j e) else 0) (poissonTableLaw (fun iz : J × Fin 4 => evalRate iz.1 iz.2)) := by apply poissonTable_pilot_cell_maps_independent evalRate p (fun j q w => if good j q then φ j q w else 0) intro j by_cases h : good j (poissonTableCell j p) <;> simp [h, hφ j]

theorem poisson_factorialLift_mixed (rate : NNReal) (m z : ℝ) (hm : m ≠ 0) (h t : ℕ) : (∫ N : ℕ, factorialLift m z N h * factorialLift m z N t ∂poissonMeasure rate) = ∑ r ∈ range (min h t + 1), (h.choose r : ℝ) * (t.choose r : ℝ) * (Nat.factorial r : ℝ) * ((rate : ℝ) / m ^ 2) ^ r * ((rate : ℝ) / m - z) ^ (h + t - 2 * r) := by exact (poisson_factorialLift_mixed_expansion rate m z hm h t).trans (factorialLift_mixed_finite_identity ((rate : ℝ) / m) ((rate : ℝ) / m ^ 2) z h t)

-- Use `integrable_prod_iff` after proving the outer integral of the absolute -- value is dominated by `bound`; nonnegativity identifies that absolute value -- with the conditional integral already bounded by `hsection_bound`. theorem poissonTable_cell_nonneg_integral_le_of_sections {J : Type*} [Fintype J] (pilotRate evalRate : J → Fin 4 → ℝ≥0) (j : J) (good : (Fin 4 → ℕ) → Bool) (hgood : Measurable good) (φ : (Fin 4 → ℕ) → (Fin 4 → ℕ) → ℝ) (hφ : Measurable (uncurry φ)) (hφ_nonneg : ∀ u v, 0 ≤ φ u v) (hsection_int : ∀ p : (J × Fin 4) → ℕ, Integrable (fun e : (J × Fin 4) → ℕ => if good (poissonTableCell j p) then φ (poissonTableCell j p) (poissonTableCell j e) else 0) (poissonTableLaw (fun iz : J × Fin 4 => evalRate iz.1 iz.2))) (bound : ((J × Fin 4) → ℕ) → ℝ) (hbound : Integrable bound (poissonTableLaw (fun iz : J × Fin 4 => pilotRate iz.1 iz.2))) (hsection_bound : ∀ p : (J × Fin 4) → ℕ, (∫ e : (J × Fin 4) → ℕ, (if good (poissonTableCell j p) then φ (poissonTableCell j p) (poissonTableCell j e) else 0) ∂poissonTableLaw (fun iz : J × Fin 4 => evalRate iz.1 iz.2)) ≤ bound p) : (∫ pe, (if good (poissonTableCell j pe.1) then φ (poissonTableCell j pe.1) (poissonTableCell j pe.2) else 0) ∂(poissonTableLaw (fun iz : J × Fin 4 => pilotRate iz.1 iz.2)).prod (poissonTableLaw (fun iz : J × Fin 4 => evalRate iz.1 iz.2))) ≤ ∫ p, bound p ∂poissonTableLaw (fun iz : J × Fin 4 => pilotRate iz.1 iz.2) := by let f : (((J × Fin 4) → ℕ) × ((J × Fin 4) → ℕ)) → ℝ := fun pe => if good (poissonTableCell j pe.1) then φ (poissonTableCell j pe.1) (poissonTableCell j pe.2) else 0 have hf_meas : Measurable f := poissonTable_cell_indicator_measurable j good hgood φ hφ have hf_nonneg : ∀ pe, 0 ≤ f pe := by intro pe dsimp [f] split_ifs <;> simp [hφ_nonneg] have hnorm : (fun p => ∫ e, ‖f (p, e)‖ ∂poissonTableLaw (fun iz : J × Fin 4 => evalRate iz.1 iz.2)) = (fun p => ∫ e, f (p, e) ∂poissonTableLaw (fun iz : J × Fin 4 => evalRate iz.1 iz.2)) := by funext p congr 1 funext e exact Real.norm_eq_abs (f (p, e)) ▸ abs_of_nonneg (hf_nonneg (p, e)) have houter : Integrable (fun p => ∫ e, ‖f (p, e)‖ ∂poissonTableLaw (fun iz : J × Fin 4 => evalRate iz.1 iz.2)) (poissonTableLaw (fun iz : J × Fin 4 => pilotRate iz.1 iz.2)) := by haveI : IsProbabilityMeasure (poissonTableLaw (fun iz : J × Fin 4 => pilotRate iz.1 iz.2)) := by unfold poissonTableLaw infer_instance rw [hnorm] apply integrable_of_le_of_le (g₁ := fun _ => (0 : ℝ)) (g₂ := bound) · exact hf_meas.stronglyMeasurable.integral_prod_right'.aestronglyMeasurable · filter_upwards [] with p exact integral_nonneg (fun e => hf_nonneg (p, e)) · exact Filter.Eventually.of_forall hsection_bound · exact integrable_const 0 · exact hbound have hf_int : Integrable f ((poissonTableLaw (fun iz : J × Fin 4 => pilotRate iz.1 iz.2)).prod (poissonTableLaw (fun iz : J × Fin 4 => evalRate iz.1 iz.2))) := (integrable_prod_iff hf_meas.aestronglyMeasurable).mpr ⟨Filter.Eventually.of_forall hsection_int, houter⟩ change (∫ pe, f pe ∂(poissonTableLaw (fun iz : J × Fin 4 => pilotRate iz.1 iz.2)).prod (poissonTableLaw (fun iz : J × Fin 4 => evalRate iz.1 iz.2))) ≤ _ rw [integral_prod f hf_int] exact integral_mono hf_int.integral_prod_left hbound hsection_bound

lemma tsum_le_one_of_le_poissonFactorial {I : Type*} [Fintype I] (rate : I → ℝ≥0) (f : (I → ℕ) → ℝ) (hf : ∀ counts, 0 ≤ f counts) (hdom : ∀ counts, f counts ≤ ∏ i : I, exp (-(rate i : ℝ)) * (rate i : ℝ) ^ counts i / (counts i).factorial) : (∑' counts, f counts) ≤ 1 := by have hg := summable_poissonFactorial_countVector rate have hfSummable : Summable f := Summable.of_nonneg_of_le hf hdom hg calc (∑' counts, f counts) ≤ ∑' counts : I → ℕ, ∏ i : I, exp (-(rate i : ℝ)) * (rate i : ℝ) ^ counts i / (counts i).factorial := Summable.tsum_le_tsum hdom hfSummable hg _ = 1 := poissonFactorial_countVector_tsum_one rate

theorem poisson_factorialLift_square_envelope (rate : NNReal) (m z R L : ℝ) (hm : 0 < m) (hR : 0 < R) (hL : 0 < L) (hcenter : |(rate : ℝ) / m - z| ≤ R) (hvariance : (rate : ℝ) / (m ^ 2 * R ^ 2) ≤ 1 / L) (h : ℕ) : (∫ N : ℕ, (factorialLift m z N h / R ^ h) ^ 2 ∂poissonMeasure rate) ≤ exp ((h : ℝ) ^ 2 / L) := by have hR0 : R ≠ 0 := ne_of_gt hR have hm0 : m ≠ 0 := ne_of_gt hm let c : ℝ := (rate : ℝ) / m - z let v : ℝ := (rate : ℝ) / m ^ 2 let x : ℝ := (h : ℝ) ^ 2 / L have hc2 : c ^ 2 ≤ R ^ 2 := by simpa only [c, sq_abs] using (pow_le_pow_left₀ (abs_nonneg ((rate : ℝ) / m - z)) hcenter 2) have hc : c ^ 2 / R ^ 2 ≤ 1 := (div_le_one (pow_pos hR 2)).mpr hc2 have hc0 : 0 ≤ c ^ 2 / R ^ 2 := by positivity have hv0 : 0 ≤ v / R ^ 2 := by dsimp [v]; positivity have hv : v / R ^ 2 ≤ 1 / L := by have heq : v / R ^ 2 = (rate : ℝ) / (m ^ 2 * R ^ 2) := by dsimp [v] ring rw [heq] exact hvariance have hx0 : 0 ≤ x := by dsimp [x]; positivity have hfirst : (∫ N : ℕ, (factorialLift m z N h / R ^ h) ^ 2 ∂poissonMeasure rate) = ∑ r ∈ range (h + 1), ((h.choose r : ℝ) ^ 2 * (Nat.factorial r : ℝ) * (v / R ^ 2) ^ r * (c ^ 2 / R ^ 2) ^ (h - r)) := by have hp (N : ℕ) : (factorialLift m z N h / R ^ h) ^ 2 = (R ^ h)⁻¹ ^ 2 * (factorialLift m z N h * factorialLift m z N h) := by rw [div_pow] field_simp simp_rw [hp] rw [integral_const_mul, poisson_factorialLift_mixed rate m z hm0 h h, Nat.min_self, Finset.mul_sum] apply Finset.sum_congr rfl intro r hr have hrh : r ≤ h := by have := Finset.mem_range.mp hr; omega have hex : h + h - 2 * r = 2 * (h - r) := by omega change (R ^ h)⁻¹ ^ 2 * ((h.choose r : ℝ) * (h.choose r : ℝ) * (Nat.factorial r : ℝ) * v ^ r * c ^ (h + h - 2 * r)) = (h.choose r : ℝ) ^ 2 * (Nat.factorial r : ℝ) * (v / R ^ 2) ^ r * (c ^ 2 / R ^ 2) ^ (h - r) generalize v = w, c = y rw [hex, show y ^ (2 * (h - r)) = (y ^ 2) ^ (h - r) by rw [pow_mul]] rw [show R ^ h = R ^ r * R ^ (h - r) by rw [← pow_add, Nat.add_sub_of_le hrh]] rw [div_pow, div_pow] field_simp [hR0] ring rw [hfirst] calc (∑ r ∈ range (h + 1), (h.choose r : ℝ) ^ 2 * (Nat.factorial r : ℝ) * (v / R ^ 2) ^ r * (c ^ 2 / R ^ 2) ^ (h - r)) ≤ ∑ r ∈ range (h + 1), x ^ r / (Nat.factorial r : ℝ) := by apply Finset.sum_le_sum intro r hr have hfac : 0 < (Nat.factorial r : ℝ) := by positivity have hchoose : (h.choose r : ℝ) ≤ (h : ℝ) ^ r / (Nat.factorial r : ℝ) := Nat.choose_le_pow_div r h have hcoeff : (h.choose r : ℝ) ^ 2 * (Nat.factorial r : ℝ) ≤ (h : ℝ) ^ (2 * r) / (Nat.factorial r : ℝ) := by have hs := pow_le_pow_left₀ (Nat.cast_nonneg _) hchoose 2 calc (h.choose r : ℝ) ^ 2 * (Nat.factorial r : ℝ) ≤ ((h : ℝ) ^ r / (Nat.factorial r : ℝ)) ^ 2 * (Nat.factorial r : ℝ) := mul_le_mul_of_nonneg_right hs hfac.le _ = (h : ℝ) ^ (2 * r) / (Nat.factorial r : ℝ) := by rw [mul_comm 2 r, pow_mul, div_pow] field_simp have hc_pow := pow_le_pow_left₀ hc0 hc (h - r) have hv_pow := pow_le_pow_left₀ hv0 hv r have hnonneg : 0 ≤ (h.choose r : ℝ) ^ 2 * (Nat.factorial r : ℝ) := by positivity calc _ ≤ (h.choose r : ℝ) ^ 2 * (Nat.factorial r : ℝ) * (v / R ^ 2) ^ r := by have := mul_le_mul_of_nonneg_left hc_pow (mul_nonneg hnonneg (pow_nonneg hv0 r)) simpa only [one_pow, mul_one] using this _ ≤ (h.choose r : ℝ) ^ 2 * (Nat.factorial r : ℝ) * (1 / L) ^ r := by exact mul_le_mul_of_nonneg_left hv_pow hnonneg _ ≤ ((h : ℝ) ^ (2 * r) / (Nat.factorial r : ℝ)) * (1 / L) ^ r := mul_le_mul_of_nonneg_right hcoeff (pow_nonneg (by positivity) r) _ = x ^ r / (Nat.factorial r : ℝ) := by dsimp [x] rw [div_pow, one_pow, mul_comm 2 r, pow_mul] ring _ ≤ exp x := Real.sum_le_exp_of_nonneg hx0 (h + 1)

theorem fourPoissonFactorialPath_sq_bound {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] {D : ℕ} (c : (Fin 4 → Fin (D + 1)) → Path) (hcBV : ∀ a, eVariationOn (c a) univ < ⊤) (W : Fin 4 → Ω → ℕ) (rate : Fin 4 → NNReal) (hWmeas : ∀ i, Measurable (W i)) (hWlaw : ∀ i, HasLaw (W i) (poissonMeasure (rate i)) μ) (hWindep : iIndepFun W μ) (m L : ℝ) (hm : 0 < m) (hL : 0 < L) (z R : Fin 4 → ℝ) (hR : ∀ i, 0 < R i) (hcenter : ∀ i, |(rate i : ℝ) / m - z i| ≤ R i) (hvariance : ∀ i, (rate i : ℝ) / (m ^ 2 * (R i) ^ 2) ≤ 1 / L) (cap : ℝ) (hcap : 0 ≤ cap) : Measurable (fourPoissonFactorialPath c W m z R cap) ∧ (∀ ω, eVariationOn (fourPoissonFactorialPath c W m z R cap ω) univ < ⊤) ∧ Integrable (fourPoissonFactorialPath c W m z R cap) μ ∧ Integrable (fun ω => (pathSize (fourPoissonFactorialPath c W m z R cap ω)) ^ 2) μ ∧ (∫ ω, (pathSize (fourPoissonFactorialPath c W m z R cap ω)) ^ 2 ∂μ) ≤ (∑ a, (pathSize (c a)) ^ 2) * ∑ _a : Fin 4 → Fin (D + 1), exp (4 * (D : ℝ) ^ 2 / L) := by let X (ω : Ω) (a : Fin 4 → Fin (D + 1)) : ℝ := fourFactorialMonomial W m z R a ω have hXmeas (a : Fin 4 → Fin (D + 1)) : Measurable (fun ω => X ω a) := by dsimp [X, fourFactorialMonomial, factorialProduct] apply Measurable.div_const apply Finset.measurable_prod intro i _ exact (Measurable.of_discrete : Measurable (fun N : ℕ => factorialLift m (z i) N (a i : ℕ))).comp (hWmeas i) have hraw (r : NNReal) (j k : ℕ) : Integrable (fun N : ℕ => (N.descFactorial j : ℝ) * (N.descFactorial k : ℝ)) (poissonMeasure r) := by have h := integrable_finsetSum (range (min j k + 1)) (fun t _ => (poisson_descFactorial_integrable r (j + k - t)).const_mul ((j.choose t : ℝ) * (k.choose t : ℝ) * (Nat.factorial t : ℝ))) have heq : (fun N : ℕ => (N.descFactorial j : ℝ) * (N.descFactorial k : ℝ)) = (fun N : ℕ => ∑ t ∈ range (min j k + 1), (j.choose t : ℝ) * (k.choose t : ℝ) * (Nat.factorial t : ℝ) * (N.descFactorial (j + k - t) : ℝ)) := by funext N exact descFactorial_mul N j k rw [heq] exact h have hlift (r : NNReal) (j : ℕ) (v : ℝ) : Integrable (fun N : ℕ => (factorialLift m v N j) ^ 2) (poissonMeasure r) := by have h := integrable_finsetSum (range (j + 1)) (fun p _ => integrable_finsetSum (range (j + 1)) (fun q _ => (hraw r p q).const_mul (((j.choose p : ℝ) * (-v) ^ (j - p) / m ^ p) * ((j.choose q : ℝ) * (-v) ^ (j - q) / m ^ q)))) have heq : (fun N : ℕ => (factorialLift m v N j) ^ 2) = (fun N : ℕ => ∑ p ∈ range (j + 1), ∑ q ∈ range (j + 1), (((j.choose p : ℝ) * (-v) ^ (j - p) / m ^ p) * ((j.choose q : ℝ) * (-v) ^ (j - q) / m ^ q)) * ((N.descFactorial p : ℝ) * (N.descFactorial q : ℝ))) := by funext N simp only [factorialLift, sq, Finset.sum_mul_sum] apply Finset.sum_congr rfl intro p _ apply Finset.sum_congr rfl intro q _ ring rw [heq] exact h have hXsq (a : Fin 4 → Fin (D + 1)) : Integrable (fun ω => (X ω a) ^ 2) μ := by let f (i : Fin 4) (N : ℕ) : ℝ := (factorialLift m (z i) N (a i : ℕ) / R i ^ (a i : ℕ)) ^ 2 have hf (i : Fin 4) : Integrable (f i) (poissonMeasure (rate i)) := by simpa only [f, div_pow] using (hlift (rate i) (a i : ℕ) (z i)).div_const ((R i ^ (a i : ℕ)) ^ 2) have hpi : Integrable (fun v : Fin 4 → ℕ => ∏ i, f i (v i)) (Measure.pi (fun i => poissonMeasure (rate i))) := Integrable.fintype_prod hf have hmap : μ.map (fun ω i => W i ω) = Measure.pi (fun i => poissonMeasure (rate i)) := by rw [hWindep.map_fun_eq_pi_map (fun i => (hWmeas i).aemeasurable)] congr 1 funext i exact (hWlaw i).map_eq have hcomp : Integrable (fun ω => ∏ i, f i (W i ω)) μ := by exact (hmap ▸ hpi).comp_measurable (measurable_pi_lambda _ hWmeas) convert hcomp using 1 funext ω simp only [X, fourFactorialMonomial, factorialProduct, f, ← Finset.prod_div_distrib, ← Finset.prod_pow] have hmeas : Measurable (fourPoissonFactorialPath c W m z R cap) := by let : BorelSpace Path := ⟨rfl⟩ exact measurable_clippedFinitePath c X hXmeas cap have hbv (ω : Ω) : eVariationOn (fourPoissonFactorialPath c W m z R cap ω) univ < ⊤ := by exact clippedFinitePath_bv c X cap hcBV ω have hsq := clippedFinitePath_sq_integral_le μ c X cap hcap hcBV hXmeas hXsq have hsize_meas : Measurable (fun ω => pathSize (fourPoissonFactorialPath c W m z R cap ω)) := by let : BorelSpace Path := ⟨rfl⟩ exact ((continuous_norm.measurable.comp hmeas).add (measurable_pathTV.comp hmeas)) have hsize_int : Integrable (fun ω => pathSize (fourPoissonFactorialPath c W m z R cap ω)) μ := by apply MeasureTheory.MemLp.integrable (q := 2) (by norm_num) exact (MeasureTheory.memLp_two_iff_integrable_sq hsize_meas.aestronglyMeasurable).2 hsq.1 have hpath_int : Integrable (fourPoissonFactorialPath c W m z R cap) μ := by let : BorelSpace Path := ⟨rfl⟩ apply Integrable.mono' hsize_int hmeas.aestronglyMeasurable filter_upwards [] with ω change ‖fourPoissonFactorialPath c W m z R cap ω‖ ≤ pathSize (fourPoissonFactorialPath c W m z R cap ω) unfold pathSize exact le_add_of_nonneg_right (pathTV_nonneg _) refine ⟨hmeas, hbv, hpath_int, hsq.1, ?_⟩ calc (∫ ω, (pathSize (fourPoissonFactorialPath c W m z R cap ω)) ^ 2 ∂μ) ≤ (∑ a, (pathSize (c a)) ^ 2) * ∑ a, (∫ ω, (X ω a) ^ 2 ∂μ) := hsq.2 _ ≤ (∑ a, (pathSize (c a)) ^ 2) * ∑ _a : Fin 4 → Fin (D + 1), exp (4 * (D : ℝ) ^ 2 / L) := by apply mul_le_mul_of_nonneg_left · apply Finset.sum_le_sum intro a _ exact factorialProduct_four_square_envelope μ W rate hWlaw hWindep m L hm hL z R hR hcenter hvariance (fun i => (a i : ℕ)) D (fun i => le_of_lt_succ (a i).isLt) · exact Finset.sum_nonneg (fun a _ => sq_nonneg _)

theorem factorialProduct_four_square_envelope {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (W : Fin 4 → Ω → ℕ) (rate : Fin 4 → NNReal) (hWlaw : ∀ i, HasLaw (W i) (poissonMeasure (rate i)) μ) (hWindep : iIndepFun W μ) (m L : ℝ) (hm : 0 < m) (hL : 0 < L) (z R : Fin 4 → ℝ) (hR : ∀ i, 0 < R i) (hcenter : ∀ i, |(rate i : ℝ) / m - z i| ≤ R i) (hvariance : ∀ i, (rate i : ℝ) / (m ^ 2 * (R i) ^ 2) ≤ 1 / L) (h : Fin 4 → ℕ) (D : ℕ) (hdegree : ∀ i, h i ≤ D) : (∫ ω, (factorialProduct W m z h ω / ∏ i, (R i) ^ (h i)) ^ 2 ∂μ) ≤ exp (4 * (D : ℝ) ^ 2 / L) := by have hs : (∑ i : Fin 4, (h i : ℝ) ^ 2) ≤ 4 * (D : ℝ) ^ 2 := by calc (∑ i : Fin 4, (h i : ℝ) ^ 2) ≤ ∑ _i : Fin 4, (D : ℝ) ^ 2 := by apply Finset.sum_le_sum intro i _ have hi : (h i : ℝ) ≤ D := by exact_mod_cast hdegree i have hnonneg : 0 ≤ (h i : ℝ) := by positivity nlinarith _ = 4 * (D : ℝ) ^ 2 := by norm_num exact (factorialProduct_square_envelope μ W rate hWlaw hWindep m L hm hL z R hR hcenter hvariance h).trans (Real.exp_le_exp.mpr (div_le_div_of_nonneg_right hs (le_of_lt hL)))

lemma poisson_power_moment_le (rate : NNReal) (r : ℕ) : (∫ k : ℕ, (k : ℝ) ^ r ∂poissonMeasure rate) ≤ ((rate : ℝ) + (r : ℝ)) ^ r := by rw [poisson_power_moment_eq, add_pow] apply Finset.sum_le_sum intro v hv have hvr : v ≤ r := by have := Finset.mem_range.mp hv; omega have hs : (Nat.stirlingSecond r v : ℝ) ≤ (r.choose v : ℝ) * (r : ℝ) ^ (r - v) := by exact_mod_cast stirlingSecond_le_choose_mul_pow (le_refl r) hvr have hh := mul_le_mul_of_nonneg_right hs (pow_nonneg rate.coe_nonneg v) convert hh using 1 ring

lemma poisson_upper_tail_mul_exp_le (lambda : NNReal) (k : Nat) {r : Real} (hr : 0 ≤ r) : (poissonMeasure lambda).real {w : Nat | k < w} * exp (-r * (lambda : Real)) ≤ exp (-log (1 + r) * (k : Real)) := by let theta := log (1 + r) have hone : 0 < 1 + r := by linarith have htheta : 0 ≤ theta := by dsimp [theta] exact Real.log_nonneg (by linarith) have hchernoff := measure_ge_le_exp_mul_mgf (X := fun w : Nat ↦ (w : Real)) (μ := poissonMeasure lambda) (k : Real) htheta (integrable_exp_natCast_poisson lambda theta) rw [mgf_natCast_poisson] at hchernoff have hexp : exp theta = 1 + r := by dsimp [theta] exact Real.exp_log hone have hsubset : {w : Nat | k < w} ⊆ {w : Nat | (k : Real) ≤ (w : Real)} := by intro w hw exact_mod_cast (le_of_lt hw) have hprob : (poissonMeasure lambda).real {w : Nat | k < w} ≤ exp (-theta * (k : Real)) * exp ((lambda : Real) * r) := by calc _ ≤ (poissonMeasure lambda).real {w : Nat | (k : Real) ≤ (w : Real)} := MeasureTheory.measureReal_mono hsubset (measure_ne_top _ _) _ ≤ _ := by simpa [hexp] using hchernoff calc _ ≤ (exp (-theta * (k : Real)) * exp ((lambda : Real) * r)) * exp (-r * (lambda : Real)) := by gcongr _ = exp (-log (1 + r) * (k : Real)) := by dsimp [theta] rw [← Real.exp_add, ← Real.exp_add] congr 1 ring

lemma poisson_lower_tail_of_two_mul_le (n : ℕ) (lambda : ℝ≥0) (hn : 1 ≤ n) (hlambda : (2 : ℝ) * n ≤ lambda) : (poissonMeasure lambda (Iio n)).toReal ≤ 8 / (n : ℝ) := by have hnR : (0 : ℝ) < n := by exact_mod_cast hn have hlambdaR : (2 : ℝ) * n ≤ (lambda : ℝ) := by exact hlambda have hlambdaPos : (0 : ℝ) < lambda := lt_of_lt_of_le (by positivity) hlambdaR have hsqrt : sqrt (2 * (lambda : ℝ) * ((n : ℝ) / 8)) ≤ (lambda : ℝ) / 2 := by rw [show 2 * (lambda : ℝ) * ((n : ℝ) / 8) = (lambda : ℝ) * (n : ℝ) / 4 by ring] apply (Real.sqrt_le_iff).2 constructor · positivity · nlinarith [mul_nonneg (show (0 : ℝ) ≤ lambda by positivity) (sub_nonneg.mpr (show (n : ℝ) ≤ lambda by linarith))] have hsubset : Iio n ⊆ {w : ℕ | (lambda : ℝ) - (w : ℝ) > sqrt (2 * (lambda : ℝ) * ((n : ℝ) / 8))} := by intro w hw have hwNat : w < n := hw have hwR : (w : ℝ) < n := by exact_mod_cast hwNat have : (lambda : ℝ) / 2 ≤ (lambda : ℝ) - (n : ℝ) := by linarith exact lt_of_le_of_lt hsqrt (lt_of_le_of_lt this (by linarith)) have hbern := poisson_lower_bernstein lambda (z := (n : ℝ) / 8) (by positivity) have hreal : (poissonMeasure lambda (Iio n)).toReal ≤ exp (-(n : ℝ) / 8) := by calc _ ≤ (ofReal (exp (-(n : ℝ) / 8))).toReal := ENNReal.toReal_mono ENNReal.ofReal_ne_top ((measure_mono hsubset).trans (by simpa [neg_div] using hbern)) _ = _ := ENNReal.toReal_ofReal (Real.exp_nonneg _) calc _ ≤ exp (-(n : ℝ) / 8) := hreal _ = 1 / exp ((n : ℝ) / 8) := by rw [show -(n : ℝ) / 8 = -((n : ℝ) / 8) by ring, Real.exp_neg, one_div] _ ≤ 1 / ((n : ℝ) / 8) := by apply one_div_le_one_div_of_le (by positivity) linarith [Real.add_one_le_exp ((n : ℝ) / 8)] _ = 8 / (n : ℝ) := by field_simp

lemma poisson_pilot_upper_tail (rate : NNReal) (B : ℝ) : (poissonMeasure rate).real {k : ℕ | B / 4 < (k : ℝ)} ≤ exp (3 * (rate : ℝ) - B * log 4 / 4) := by let theta : ℝ := log 4 have htheta : 0 ≤ theta := by dsimp [theta] exact (Real.log_pos (by norm_num)).le have hchernoff := measure_ge_le_exp_mul_mgf (X := fun k : ℕ => (k : ℝ)) (μ := poissonMeasure rate) (B / 4) htheta (integrable_exp_natCast_poisson rate theta) rw [mgf_natCast_poisson] at hchernoff have hexp : exp theta = 4 := by dsimp [theta] rw [Real.exp_log (by norm_num : (0 : ℝ) < 4)] have hsubset : {k : ℕ | B / 4 < (k : ℝ)} ⊆ {k : ℕ | B / 4 ≤ (k : ℝ)} := by intro k hk change B / 4 < (k : ℝ) at hk change B / 4 ≤ (k : ℝ) exact hk.le calc (poissonMeasure rate).real {k : ℕ | B / 4 < (k : ℝ)} ≤ (poissonMeasure rate).real {k : ℕ | B / 4 ≤ (k : ℝ)} := measureReal_mono hsubset (measure_ne_top _ _) _ ≤ exp (-theta * (B / 4)) * exp ((rate : ℝ) * (exp theta - 1)) := hchernoff _ = exp (3 * (rate : ℝ) - B * log 4 / 4) := by rw [hexp, ← Real.exp_add] dsimp [theta] congr 1 ring

-- Split on `M ω ≤ n` pointwise. On overflow the capped loss is `‖F‖² ≤ 1`. -- Integrate the pointwise comparison and transfer overflow probability using -- `hM.measureReal_eq` and `poisson_quarter_mean_cap_tail`. theorem poisson_cap_path_risk_le {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (n : ℕ) (M : Ω → ℕ) (hM : HasLaw M (poissonMeasure ((n : ℝ≥0) / 4)) μ) (Z : Ω → Path) (F : Path) (hF : ‖F‖ ≤ 1) (hZ : Integrable (fun ω => ‖Z ω - F‖ ^ 2) μ) (hcap : Integrable (fun ω => ‖(if M ω ≤ n then Z ω else 0) - F‖ ^ 2) μ) : (∫ ω, ‖(if M ω ≤ n then Z ω else 0) - F‖ ^ 2 ∂μ) ≤ (∫ ω, ‖Z ω - F‖ ^ 2 ∂μ) + exp (-(n : ℝ) / 2) := by let s : Set Ω := {ω | n < M ω} have hs : NullMeasurableSet s μ := by exact hM.aemeasurable.nullMeasurableSet_preimage (show MeasurableSet {w : ℕ | n < w} by simpa only [Ioi] using measurableSet_Ioi) have hind : Integrable (s.indicator (fun _ => (1 : ℝ))) μ := (integrable_const 1).indicator₀ hs have hpoint (ω : Ω) : ‖(if M ω ≤ n then Z ω else 0) - F‖ ^ 2 ≤ ‖Z ω - F‖ ^ 2 + s.indicator (fun _ => (1 : ℝ)) ω := by by_cases h : M ω ≤ n · simp [h, s] · have hF2 : ‖F‖ ^ 2 ≤ (1 : ℝ) := by nlinarith [norm_nonneg F] have hz2 : 0 ≤ ‖Z ω - F‖ ^ 2 := sq_nonneg _ simp only [if_neg h, zero_sub, norm_neg] rw [Set.indicator_of_mem (show ω ∈ s by simpa [s] using Nat.lt_of_not_ge h)] nlinarith have hmain := integral_mono hcap (hZ.add hind) hpoint have hint : (∫ ω, s.indicator (fun _ => (1 : ℝ)) ω ∂μ) = μ.real s := by rw [integral_indicator₀ hs, setIntegral_const] simp change _ ≤ ∫ ω, ‖Z ω - F‖ ^ 2 + s.indicator (fun _ => (1 : ℝ)) ω ∂μ at hmain rw [integral_add hZ hind, hint] at hmain have htail := poisson_quarter_mean_cap_tail n have htailReal : (poissonMeasure ((n : ℝ≥0) / 4)).real {w : ℕ | n < w} ≤ exp (-(n : ℝ) / 2) := (ENNReal.le_ofReal_iff_toReal_le (measure_ne_top _ _) (Real.exp_nonneg _)).mp htail have hsprob : μ.real s = (poissonMeasure ((n : ℝ≥0) / 4)).real {w : ℕ | n < w} := by simpa [s] using hM.measureReal_eq (p := fun w : ℕ => n < w) (show MeasurableSet {w : ℕ | n < w} by simpa only [Ioi] using measurableSet_Ioi) rw [hsprob] at hmain exact hmain.trans (add_le_add_right htailReal _)