Stat.Concentration.Poisson­Self­Normalized

theorem integrable_radius (lambda : ℝ≥0) (L : ℝ) (hL : 0 ≤ L) : Integrable (radius L) (poissonMeasure lambda) := by have hlin : Integrable (fun w : ℕ => (w : ℝ) * L) (poissonMeasure lambda) := (integrable_natCast_poisson lambda).mul_const L have hc : Integrable (fun _ : ℕ => (1 + L : ℝ)) (poissonMeasure lambda) := integrable_const _ have hg := hlin.add hc refine hg.mono' (measurable_radius L).aestronglyMeasurable (Filter.Eventually.of_forall fun w => ?_) have hx : 0 ≤ (w : ℝ) * L := mul_nonneg (Nat.cast_nonneg _) hL have hsqrt : sqrt ((w : ℝ) * L) ≤ (w : ℝ) * L + 1 := by have hs := Real.sq_sqrt hx have hsq := sq_nonneg (sqrt ((w : ℝ) * L) - 1) nlinarith change ‖Real.sqrt ((w : ℝ) * L) + L‖ ≤ (w : ℝ) * L + (1 + L) rw [Real.norm_eq_abs, abs_of_nonneg] · linarith · exact add_nonneg (Real.sqrt_nonneg _) hL

-- Proof route: dominate `1_{BadAny}` by the sum of coordinate bad-event -- indicators and use `pow_sum_le_card_mul_sum_pow` on the nonnegative scores. -- This reduces the integral to terms `E[score_i^t 1_{Bad_j}]`. For `i = j`, -- transfer `poisson_weighted_bad_moment` through `HasLaw.integral_comp`. For -- `i != j`, use `hWindep.indepFun` (followed by measurable composition) and -- `IndepFun.integral_mul` to factor the term into an untruncated score moment -- and a bad-event probability. Transfer `poisson_score_moment` and -- `poisson_badEvent_probability_eighty` through the coordinate laws. Finally -- bound `sum_i localScale (lambda i) L` by a cardinality-dependent multiple of -- `sqrt ((sum_i lambda_i) * L) + L` using Cauchy--Schwarz for the square-root -- sum, and absorb all powers of `r` and scalar constants into -- `productMomentConstant`. Split off the empty-index/r=0 case before using -- positive cardinality inequalities, and eliminate the three values of `t` -- from `ht` explicitly. theorem independent_poisson_badAny_moment {ι Ω : Type*} [Fintype ι] [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (W : ι → Ω → ℕ) (lambda : ι → ℝ≥0) (hWmeas : ∀ i, Measurable (W i)) (hWlaw : ∀ i, HasLaw (W i) (poissonMeasure (lambda i)) μ) (hWindep : iIndepFun W μ) {r t : ℕ} (hcard : Fintype.card ι ≤ r) (ht : t = 1 ∨ t = 2 ∨ t = 4) {L : ℝ} (hL : 1 ≤ L) : ∫ ω, (badAny W universalH L lambda).indicator (fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω ∂μ ≤ productMomentConstant r t * exp (-20 * L) * (sqrt ((∑ i, (lambda i : ℝ)) * L) + L) ^ t := by classical by_cases hι : Nonempty ι · letI := hι have ht4 : t ≤ 4 := by rcases ht with rfl | rfl | rfl <;> norm_num let K : ℝ := scalarBadMomentConstant t + 2 * scalarMomentConstant t let A : ℝ := sqrt ((∑ i, (lambda i : ℝ)) * L) + L let n : ℝ := Fintype.card ι let F : ι → ι → Ω → ℝ := fun j i ω => (badEvent universalH L (lambda j)).indicator (fun _ => (score universalH L (lambda i) (W i ω)) ^ t) (W j ω) have hn0 : 0 ≤ n := by dsimp [n]; positivity have hn1 : 1 ≤ n := by dsimp [n] exact_mod_cast Fintype.card_pos have hK0 : 0 ≤ K := by dsimp [K] exact add_nonneg (scalarBadMomentConstant_pos t).le (mul_nonneg (by norm_num) (scalarMomentConstant_pos t).le) have hA0 : 0 ≤ A := by dsimp [A] exact add_nonneg (Real.sqrt_nonneg _) (by linarith) have hscore0 (i : ι) (ω : Ω) : 0 ≤ score universalH L (lambda i) (W i ω) := score_nonneg_product (lambda i) hL (W i ω) have hF0 (j i : ι) (ω : Ω) : 0 ≤ F j i ω := by dsimp [F] by_cases hω : W j ω ∈ badEvent universalH L (lambda j) · simp [hω, pow_nonneg (hscore0 i ω) t] · simp [hω] have hFint (j i : ι) : Integrable (F j i) μ := by have hi := (integrable_score_pow_comp μ (W i) (lambda i) (hWlaw i) hL ht4).indicator ((measurableSet_badEvent universalH L (lambda j)).preimage (hWmeas j)) change Integrable ((W j ⁻¹' badEvent universalH L (lambda j)).indicator (fun ω => (score universalH L (lambda i) (W i ω)) ^ t)) μ at hi have heq : F j i = (W j ⁻¹' badEvent universalH L (lambda j)).indicator (fun ω => (score universalH L (lambda i) (W i ω)) ^ t) := by funext ω by_cases hω : W j ω ∈ badEvent universalH L (lambda j) <;> simp [F, hω] rw [heq] exact hi have haggregate_pow (ω : Ω) : (aggregateScore W universalH L lambda ω) ^ t ≤ n ^ (t - 1) * ∑ i, (score universalH L (lambda i) (W i ω)) ^ t := by unfold aggregateScore rcases ht with rfl | rfl | rfl · simpa [n] using (pow_sum_le_card_mul_sum_pow (s := (Finset.univ : Finset ι)) (f := fun i => score universalH L (lambda i) (W i ω)) (fun i _ => hscore0 i ω) 0) · simpa [n] using (pow_sum_le_card_mul_sum_pow (s := (Finset.univ : Finset ι)) (f := fun i => score universalH L (lambda i) (W i ω)) (fun i _ => hscore0 i ω) 1) · simpa [n] using (pow_sum_le_card_mul_sum_pow (s := (Finset.univ : Finset ι)) (f := fun i => score universalH L (lambda i) (W i ω)) (fun i _ => hscore0 i ω) 3) have hpoint (ω : Ω) : (badAny W universalH L lambda).indicator (fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω ≤ n ^ (t - 1) * ∑ j, ∑ i, F j i ω := by by_cases hbad : ω ∈ badAny W universalH L lambda · rw [Set.indicator_of_mem hbad] rcases hbad with ⟨j, hj⟩ have hselected : ∑ i, (score universalH L (lambda i) (W i ω)) ^ t = ∑ i, F j i ω := by apply Finset.sum_congr rfl intro i _ simp [F, hj] have hinner : ∑ i, (score universalH L (lambda i) (W i ω)) ^ t ≤ ∑ j, ∑ i, F j i ω := by rw [hselected] exact Finset.single_le_sum (fun k _ => sum_nonneg fun i _ => hF0 k i ω) (Finset.mem_univ j) exact haggregate_pow ω |>.trans (mul_le_mul_of_nonneg_left hinner (pow_nonneg hn0 _)) · rw [Set.indicator_of_notMem hbad] exact mul_nonneg (pow_nonneg hn0 _) (sum_nonneg fun j _ => sum_nonneg fun i _ => hF0 j i ω) have hlhs0 : 0 ≤ᵐ[μ] fun ω => (badAny W universalH L lambda).indicator (fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω := by filter_upwards [] with ω by_cases hbad : ω ∈ badAny W universalH L lambda · rw [Set.indicator_of_mem hbad] apply pow_nonneg unfold aggregateScore exact sum_nonneg fun i _ => hscore0 i ω · simp [hbad] have hsumInt : Integrable (fun ω => ∑ j, ∑ i, F j i ω) μ := integrable_finsetSum _ fun j _ => integrable_finsetSum _ fun i _ => hFint j i have hdomInt : Integrable (fun ω => n ^ (t - 1) * ∑ j, ∑ i, F j i ω) μ := hsumInt.const_mul _ have hintegral : ∫ ω, (badAny W universalH L lambda).indicator (fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω ∂μ ≤ n ^ (t - 1) * ∑ j, ∑ i, ∫ ω, F j i ω ∂μ := by calc _ ≤ ∫ ω, n ^ (t - 1) * ∑ j, ∑ i, F j i ω ∂μ := integral_mono_of_nonneg hlhs0 hdomInt (Filter.Eventually.of_forall hpoint) _ = n ^ (t - 1) * ∫ ω, ∑ j, ∑ i, F j i ω ∂μ := integral_const_mul _ _ _ = n ^ (t - 1) * ∑ j, ∫ ω, ∑ i, F j i ω ∂μ := by congr 1 exact integral_finsetSum Finset.univ fun j _ => integrable_finsetSum _ fun i _ => hFint j i _ = n ^ (t - 1) * ∑ j, ∑ i, ∫ ω, F j i ω ∂μ := by congr 1 apply Finset.sum_congr rfl intro j _ exact integral_finsetSum Finset.univ fun i _ => hFint j i have hcross (j i : ι) : ∫ ω, F j i ω ∂μ ≤ K * exp (-(40 * L)) * (localScale (lambda i) L) ^ t := by exact coordinate_cross_moment μ W lambda hWmeas hWlaw hWindep hL ht i j have hcrossSum : ∑ j, ∑ i, ∫ ω, F j i ω ∂μ ≤ n * (K * exp (-(40 * L)) * ∑ i, (localScale (lambda i) L) ^ t) := by calc _ ≤ ∑ _j : ι, ∑ i, K * exp (-(40 * L)) * (localScale (lambda i) L) ^ t := by exact Finset.sum_le_sum fun j _ => Finset.sum_le_sum fun i _ => hcross j i _ = n * (K * exp (-(40 * L)) * ∑ i, (localScale (lambda i) L) ^ t) := by simp [n, Finset.mul_sum] have hpowSum := sum_localScale_pow_le_card_mul_pow_sum lambda hL t have hscale := sum_localScale_le_card_mul lambda hL have hscalePow : (∑ i, localScale (lambda i) L) ^ t ≤ (n * A) ^ t := by exact pow_le_pow_left₀ (sum_nonneg fun i _ => by unfold localScale positivity) (by simpa [n, A] using hscale) t have hncard : n ≤ (r : ℝ) := by dsimp [n] exact_mod_cast hcard have hcoeff : n ^ (2 * t + 1) * K ≤ productMomentConstant r t := by calc n ^ (2 * t + 1) * K ≤ (r : ℝ) ^ (2 * t + 1) * K := by exact mul_le_mul_of_nonneg_right (pow_le_pow_left₀ hn0 hncard _) hK0 _ ≤ productMomentConstant r t := product_coefficient_bound calc ∫ ω, (badAny W universalH L lambda).indicator (fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω ∂μ ≤ n ^ (t - 1) * ∑ j, ∑ i, ∫ ω, F j i ω ∂μ := hintegral _ ≤ n ^ (t - 1) * (n * (K * exp (-(40 * L)) * ∑ i, (localScale (lambda i) L) ^ t)) := mul_le_mul_of_nonneg_left hcrossSum (pow_nonneg hn0 _) _ ≤ n ^ (t - 1) * (n * (K * exp (-(40 * L)) * (n * (∑ i, localScale (lambda i) L) ^ t))) := by gcongr _ ≤ n ^ (t - 1) * (n * (K * exp (-(40 * L)) * (n * (n * A) ^ t))) := by gcongr _ = (n ^ (2 * t + 1) * K) * exp (-(40 * L)) * A ^ t := by rcases ht with rfl | rfl | rfl <;> ring _ ≤ productMomentConstant r t * exp (-(40 * L)) * A ^ t := by gcongr _ ≤ productMomentConstant r t * exp (-20 * L) * A ^ t := by apply mul_le_mul_of_nonneg_right · exact mul_le_mul_of_nonneg_left (Real.exp_le_exp.mpr (by nlinarith)) (productMomentConstant_pos r t).le · exact pow_nonneg hA0 t _ = productMomentConstant r t * exp (-20 * L) * (sqrt ((∑ i, (lambda i : ℝ)) * L) + L) ^ t := rfl · letI : IsEmpty ι := not_nonempty_iff.mp hι simp [badAny, aggregateScore] exact mul_nonneg (mul_nonneg (productMomentConstant_pos r t).le (Real.exp_nonneg _)) (pow_nonneg (by linarith) t)

-- Proof strategy: rewrite `deviation`, split the absolute-value event into -- upper and lower deviations, apply `measure_union_le`, and use the preceding -- one-sided bounds. The lower event with the larger displayed threshold is -- contained in the lower Bernstein event with threshold `sqrt (2 lambda z)`. theorem poisson_abs_bernstein (lambda : ℝ≥0) {z : ℝ} (hz : 0 ≤ z) : poissonMeasure lambda {w : ℕ | deviation lambda w > sqrt (2 * (lambda : ℝ) * z) + 2 * z} ≤ 2 * ofReal (exp (-z)) := by let s : ℝ := sqrt (2 * (lambda : ℝ) * z) let T : ℝ := s + 2 * z have hs_nonneg : 0 ≤ s := Real.sqrt_nonneg _ have hT_nonneg : 0 ≤ T := by dsimp [T] positivity have hsubset : {w : ℕ | deviation lambda w > sqrt (2 * (lambda : ℝ) * z) + 2 * z} ⊆ {w : ℕ | (w : ℝ) - (lambda : ℝ) > sqrt (2 * (lambda : ℝ) * z) + 2 * z} ∪ {w : ℕ | (lambda : ℝ) - (w : ℝ) > sqrt (2 * (lambda : ℝ) * z)} := by intro w hw simp only [Set.mem_ofPred_eq, Set.mem_union] at hw ⊢ change |(w : ℝ) - (lambda : ℝ)| > T at hw by_cases hu : (w : ℝ) - (lambda : ℝ) > T · left exact hu · right change (lambda : ℝ) - (w : ℝ) > s by_contra hl have hl' : (lambda : ℝ) - (w : ℝ) ≤ s := le_of_not_gt hl have hu' : (w : ℝ) - (lambda : ℝ) ≤ T := le_of_not_gt hu have hlower : -T ≤ (w : ℝ) - (lambda : ℝ) := by dsimp [T] linarith have habs : |(w : ℝ) - (lambda : ℝ)| ≤ T := (abs_le.mpr ⟨hlower, hu'⟩) linarith calc poissonMeasure lambda {w : ℕ | deviation lambda w > sqrt (2 * (lambda : ℝ) * z) + 2 * z} ≤ poissonMeasure lambda ({w : ℕ | (w : ℝ) - (lambda : ℝ) > sqrt (2 * (lambda : ℝ) * z) + 2 * z} ∪ {w : ℕ | (lambda : ℝ) - (w : ℝ) > sqrt (2 * (lambda : ℝ) * z)}) := measure_mono hsubset _ ≤ poissonMeasure lambda {w : ℕ | (w : ℝ) - (lambda : ℝ) > sqrt (2 * (lambda : ℝ) * z) + 2 * z} + poissonMeasure lambda {w : ℕ | (lambda : ℝ) - (w : ℝ) > sqrt (2 * (lambda : ℝ) * z)} := measure_union_le _ _ _ ≤ ofReal (exp (-z)) + ofReal (exp (-z)) := add_le_add (poisson_upper_bernstein lambda hz) (poisson_lower_bernstein lambda hz) _ = 2 * ofReal (exp (-z)) := by ring

theorem poisson_quarter_overflow_le_exp (n : ℕ) (hn : 0 < n) : (poissonMeasure ((n : ℝ≥0) / 4)).real (Ioi n) ≤ exp (-(n : ℝ) / 8) := by have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hsqrt : sqrt (2 * (((n : ℝ≥0) / 4 : ℝ≥0) : ℝ) * ((n : ℝ) / 8)) = (n : ℝ) / 4 := by rw [show 2 * (((n : ℝ≥0) / 4 : ℝ≥0) : ℝ) * ((n : ℝ) / 8) = ((n : ℝ) / 4) ^ 2 by norm_num; ring] rw [Real.sqrt_sq_eq_abs, abs_of_nonneg] positivity have hsubset : Ioi n ⊆ {w : ℕ | (w : ℝ) - (((n : ℝ≥0) / 4 : ℝ≥0) : ℝ) > sqrt (2 * (((n : ℝ≥0) / 4 : ℝ≥0) : ℝ) * ((n : ℝ) / 8)) + 2 * ((n : ℝ) / 8)} := by intro w hw simp only [Set.mem_Ioi] at hw ⊢ have hwR : (n : ℝ) < (w : ℝ) := by exact_mod_cast hw rw [hsqrt] norm_num nlinarith have hbern := poisson_upper_bernstein ((n : ℝ≥0) / 4) (z := (n : ℝ) / 8) (by positivity) have hmono : poissonMeasure ((n : ℝ≥0) / 4) (Ioi n) ≤ poissonMeasure ((n : ℝ≥0) / 4) {w : ℕ | (w : ℝ) - (((n : ℝ≥0) / 4 : ℝ≥0) : ℝ) > sqrt (2 * (((n : ℝ≥0) / 4 : ℝ≥0) : ℝ) * ((n : ℝ) / 8)) + 2 * ((n : ℝ) / 8)} := measure_mono hsubset simpa only [Measure.real_def, ENNReal.toReal_ofReal (Real.exp_pos _).le, neg_div] using ENNReal.toReal_mono ENNReal.ofReal_ne_top (hmono.trans hbern)

-- A convenient discrete-tail route is to partition by integer Bernstein -- levels `z = 40*L+n`. On each shell, the deterministic inequalities used -- in `badEvent_subset_remote_bernstein` bound `score^t` by a fixed multiple -- of `(localScale + n)^t`; `poisson_abs_bernstein` bounds the shell by -- `2*exp (-(40*L+n))`. Sum the resulting degree-at-most-four polynomial -- times geometric series, absorb its `L^t` factor into `localScale^t` -- (`localScale ≥ L`), and discharge the three allowed values of `t` -- separately. The very large declared constant leaves ample slack. theorem poisson_weighted_bad_moment (lambda : ℝ≥0) {L : ℝ} (hL : 1 ≤ L) {t : ℕ} (ht : t = 1 ∨ t = 2 ∨ t = 4) : ∫ w : ℕ, (badEvent universalH L lambda).indicator (fun w => (score universalH L lambda w) ^ t) w ∂poissonMeasure lambda ≤ scalarBadMomentConstant t * exp (-(scalarDecay * L)) * (localScale lambda L) ^ t := by let B := badEvent universalH L lambda let S := localScale lambda L let X : ℕ → ℝ := fun w => (score universalH L lambda w) ^ t let a : ℝ := exp (-(40 * L)) * (S ^ t)⁻¹ have hS : 0 < S := lt_of_lt_of_le zero_lt_one (localScale_one_le lambda hL) have ha : 0 < a := by positivity have ht8 : 2 * t ≤ 8 := by rcases ht with rfl | rfl | rfl <;> norm_num have hX : Integrable X (poissonMeasure lambda) := by exact integrable_score_pow_aux lambda hL t have hXsq : Integrable (fun w => (X w) ^ 2) (poissonMeasure lambda) := by simpa only [X, ← pow_mul, mul_comm] using integrable_score_pow_aux lambda hL (2 * t) have hB : MeasurableSet B := by exact measurableSet_badEvent universalH L lambda have hprobReal : (poissonMeasure lambda).real B ≤ 2 * exp (-(80 * L)) := by have hp := poisson_badEvent_probability_eighty lambda hL have hto := (ENNReal.toReal_le_toReal (by finiteness) (by finiteness)).mpr hp simpa [B, measureReal_def, ENNReal.toReal_mul, Real.exp_nonneg] using hto have hmoment : ∫ w : ℕ, (X w) ^ 2 ∂poissonMeasure lambda ≤ 10 ^ (8 * t + 4) * S ^ (2 * t) := by have heq : 4 * (2 * t) + 4 = 8 * t + 4 := by omega rw [← heq] simpa only [X, S, pow_two, ← pow_add, two_mul] using poisson_score_moment_aux lambda hL ht8 have hyoung (w : ℕ) : B.indicator X w ≤ (a * (X w) ^ 2 + a⁻¹ * B.indicator (fun _ => (1 : ℝ)) w) / 2 := by by_cases hw : w ∈ B · rw [Set.indicator_of_mem hw, Set.indicator_of_mem hw] have hsquare := sq_nonneg (a * X w - 1) have ha0 : a ≠ 0 := ne_of_gt ha field_simp [ha0] nlinarith · simp [Set.indicator_of_notMem hw] positivity have hleft : Integrable (B.indicator X) (poissonMeasure lambda) := hX.indicator hB have hright : Integrable (fun w => (a * (X w) ^ 2 + a⁻¹ * B.indicator (fun _ => (1 : ℝ)) w) / 2) (poissonMeasure lambda) := by apply Integrable.div_const apply Integrable.add · exact hXsq.const_mul a · exact (integrable_const (1 : ℝ)).indicator hB |>.const_mul a⁻¹ have hintegral : ∫ w : ℕ, B.indicator X w ∂poissonMeasure lambda ≤ (a * ∫ w : ℕ, (X w) ^ 2 ∂poissonMeasure lambda + a⁻¹ * (poissonMeasure lambda).real B) / 2 := by calc ∫ w : ℕ, B.indicator X w ∂poissonMeasure lambda ≤ ∫ w : ℕ, (a * (X w) ^ 2 + a⁻¹ * B.indicator (fun _ => (1 : ℝ)) w) / 2 ∂poissonMeasure lambda := integral_mono hleft hright hyoung _ = (a * ∫ w : ℕ, (X w) ^ 2 ∂poissonMeasure lambda + a⁻¹ * (poissonMeasure lambda).real B) / 2 := by rw [integral_div, integral_add, integral_const_mul, integral_const_mul, integral_indicator_const (1 : ℝ) hB] simp · exact hXsq.const_mul a · exact (integrable_const (1 : ℝ)).indicator hB |>.const_mul a⁻¹ have hterm1 : a * ∫ w : ℕ, (X w) ^ 2 ∂poissonMeasure lambda ≤ 10 ^ (8 * t + 4) * exp (-(40 * L)) * S ^ t := by calc a * ∫ w : ℕ, (X w) ^ 2 ∂poissonMeasure lambda ≤ a * (10 ^ (8 * t + 4) * S ^ (2 * t)) := mul_le_mul_of_nonneg_left hmoment ha.le _ = 10 ^ (8 * t + 4) * exp (-(40 * L)) * S ^ t := by dsimp [a] rw [pow_mul] field_simp ring have hterm2 : a⁻¹ * (poissonMeasure lambda).real B ≤ 2 * exp (-(40 * L)) * S ^ t := by calc a⁻¹ * (poissonMeasure lambda).real B ≤ a⁻¹ * (2 * exp (-(80 * L))) := mul_le_mul_of_nonneg_left hprobReal (inv_nonneg.mpr ha.le) _ = 2 * exp (-(40 * L)) * S ^ t := by dsimp [a] rw [mul_inv_rev, inv_inv, ← Real.exp_neg] field_simp [Real.exp_ne_zero, ne_of_gt hS] rw [← Real.exp_add] ring_nf calc ∫ w : ℕ, (badEvent universalH L lambda).indicator (fun w => (score universalH L lambda w) ^ t) w ∂poissonMeasure lambda = ∫ w : ℕ, B.indicator X w ∂poissonMeasure lambda := by rfl _ ≤ (a * ∫ w : ℕ, (X w) ^ 2 ∂poissonMeasure lambda + a⁻¹ * (poissonMeasure lambda).real B) / 2 := hintegral _ ≤ (10 ^ (8 * t + 4) * exp (-(40 * L)) * S ^ t + 2 * exp (-(40 * L)) * S ^ t) / 2 := by gcongr _ ≤ scalarBadMomentConstant t * exp (-(scalarDecay * L)) * (localScale lambda L) ^ t := by dsimp [scalarBadMomentConstant, scalarDecay, S] have hcoeff : (10 ^ (8 * t + 4) + 2 : ℝ) / 2 ≤ 10 ^ (8 * t + 8) := by rcases ht with rfl | rfl | rfl <;> norm_num calc (10 ^ (8 * t + 4) * exp (-(40 * L)) * localScale lambda L ^ t + 2 * exp (-(40 * L)) * localScale lambda L ^ t) / 2 = ((10 ^ (8 * t + 4) + 2 : ℝ) / 2) * (exp (-(40 * L)) * localScale lambda L ^ t) := by ring _ ≤ 10 ^ (8 * t + 8) * (exp (-(40 * L)) * localScale lambda L ^ t) := mul_le_mul_of_nonneg_right hcoeff (by positivity) _ = 10 ^ (8 * t + 8) * exp (-(40 * L)) * localScale lambda L ^ t := by ring

-- Proof route after `Product` is closed: for `m > 0`, prove pointwise -- `normalizedDeviation m q w = deviation (m*q) w / m` and -- `normalizedRadius m L w = radius L w / m` (use `Real.sqrt_div` and -- `Real.sqrt_sq_eq_abs`). Hence the normalized bad set is the unnormalized -- bad set at mean `m*q`, and the aggregate score is the corresponding score -- divided by `m`. Apply `independent_poisson_badAny_moment`, pull the positive -- constant `m^(-t)` through the indicator and integral, rewrite -- `sum_i (m*q_i)` as `m * sum_i q_i`, and identify the divided local scale -- with `sqrt (((sum_i q_i) * L) / m) + L/m`. theorem independent_poisson_normalized_badAny_moment {ι Ω : Type*} [Fintype ι] [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (W : ι → Ω → ℕ) (q : ι → ℝ≥0) (m : ℝ≥0) (hm : 0 < m) (hWmeas : ∀ i, Measurable (W i)) (hWlaw : ∀ i, HasLaw (W i) (poissonMeasure (m * q i)) μ) (hWindep : iIndepFun W μ) {r t : ℕ} (hcard : card ι ≤ r) (ht : t = 1 ∨ t = 2 ∨ t = 4) {L : ℝ} (hL : 1 ≤ L) : ∫ ω, (normalizedBadAny W universalH L m q).indicator (fun ω => (normalizedAggregateScore W universalH L m q ω) ^ t) ω ∂μ ≤ productMomentConstant r t * exp (-20 * L) * (sqrt (((∑ i, (q i : ℝ)) * L) / (m : ℝ)) + L / (m : ℝ)) ^ t := by classical have hmR : 0 < (m : ℝ) := NNReal.coe_pos.mpr hm let lambda : ι → ℝ≥0 := fun i => m * q i have hbad : normalizedBadAny W universalH L m q = badAny W universalH L lambda := by ext ω simp only [normalizedBadAny, badAny, Set.mem_ofPred_eq] apply exists_congr intro i rw [normalizedDeviation_eq_div m (q i) hm, normalizedRadius_eq_div m hm] change deviation (lambda i) (W i ω) / (m : ℝ) > (universalH / 4) * (radius L (W i ω) / (m : ℝ)) ↔ _ rw [show (universalH / 4) * (radius L (W i ω) / (m : ℝ)) = ((universalH / 4) * radius L (W i ω)) / (m : ℝ) by ring] exact div_lt_div_iff_of_pos_right hmR have hagg (ω : Ω) : normalizedAggregateScore W universalH L m q ω = aggregateScore W universalH L lambda ω / (m : ℝ) := by unfold normalizedAggregateScore aggregateScore rw [Finset.sum_div] apply Finset.sum_congr rfl intro i _ rw [normalizedDeviation_eq_div m (q i) hm, normalizedRadius_eq_div m hm] change deviation (lambda i) (W i ω) / (m : ℝ) + universalH * (radius L (W i ω) / (m : ℝ)) = score universalH L (lambda i) (W i ω) / (m : ℝ) unfold score ring have hind (ω : Ω) : (badAny W universalH L lambda).indicator (fun ω => (normalizedAggregateScore W universalH L m q ω) ^ t) ω = (badAny W universalH L lambda).indicator (fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω / (m : ℝ) ^ t := by by_cases hω : ω ∈ badAny W universalH L lambda <;> simp [hω, hagg, div_pow] have hlhs : (∫ ω, (normalizedBadAny W universalH L m q).indicator (fun ω => (normalizedAggregateScore W universalH L m q ω) ^ t) ω ∂μ) = (∫ ω, (badAny W universalH L lambda).indicator (fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω ∂μ) / (m : ℝ) ^ t := by rw [hbad, ← integral_div] exact integral_congr_ae (Filter.Eventually.of_forall hind) have hprod := independent_poisson_badAny_moment μ W lambda hWmeas (by simpa [lambda] using hWlaw) hWindep hcard ht hL have hdiv := (div_le_div_iff_of_pos_right (pow_pos hmR t)).2 hprod rw [hlhs] calc (∫ ω, (badAny W universalH L lambda).indicator (fun ω => (aggregateScore W universalH L lambda ω) ^ t) ω ∂μ) / (m : ℝ) ^ t ≤ (productMomentConstant r t * exp (-20 * L) * (sqrt ((∑ i, (lambda i : ℝ)) * L) + L) ^ t) / (m : ℝ) ^ t := hdiv _ = productMomentConstant r t * exp (-20 * L) * (sqrt (((∑ i, (q i : ℝ)) * L) / (m : ℝ)) + L / (m : ℝ)) ^ t := by have hsum : ∑ i, (lambda i : ℝ) = (m : ℝ) * ∑ i, (q i : ℝ) := by simp [lambda, Finset.mul_sum] rw [hsum] have hq0 : 0 ≤ ∑ i, (q i : ℝ) := sum_nonneg fun i _ => (q i).coe_nonneg have hL0 : 0 ≤ L := by linarith have hsqrt : sqrt (((m : ℝ) * (∑ i, (q i : ℝ))) * L) / (m : ℝ) = sqrt (((∑ i, (q i : ℝ)) * L) / (m : ℝ)) := by symm calc sqrt (((∑ i, (q i : ℝ)) * L) / (m : ℝ)) = sqrt ((((m : ℝ) * (∑ i, (q i : ℝ))) * L) / ((m : ℝ) ^ 2)) := by congr 1 field_simp _ = sqrt (((m : ℝ) * (∑ i, (q i : ℝ))) * L) / sqrt ((m : ℝ) ^ 2) := by rw [Real.sqrt_div] positivity _ = sqrt (((m : ℝ) * (∑ i, (q i : ℝ))) * L) / (m : ℝ) := by rw [Real.sqrt_sq_eq_abs, abs_of_pos hmR] have hscale : (sqrt (((m : ℝ) * (∑ i, (q i : ℝ))) * L) + L) / (m : ℝ) = sqrt (((∑ i, (q i : ℝ)) * L) / (m : ℝ)) + L / (m : ℝ) := by rw [add_div, hsqrt] calc productMomentConstant r t * exp (-20 * L) * (sqrt (((m : ℝ) * ∑ i, (q i : ℝ)) * L) + L) ^ t / (m : ℝ) ^ t = productMomentConstant r t * exp (-20 * L) * ((sqrt (((m : ℝ) * ∑ i, (q i : ℝ)) * L) + L) / (m : ℝ)) ^ t := by rw [div_pow]; ring _ = _ := by rw [hscale]