Stat.Orthogonality

theorem IsBigOp.of_sqEnvelope {Xn : ℕ → Ω → ℝ} {cn : ℕ → Ω → ℝ} {rn : ℕ → ℝ} (hrn : ∀ n, 0 < rn n) (hbound : ∀ n, ∀ᵐ ω ∂μ, (Xn n ω) ^ 2 ≤ cn n ω) (hcn_BigOp : IsBigOp cn (fun n => (rn n) ^ 2) μ) : IsBigOp Xn rn μ := by intro ε hε rcases hcn_BigOp ε hε with ⟨K, hK⟩ let M : ℝ := max |K| 1 have hMpos : 0 < M := by dsimp [M] exact lt_of_lt_of_le zero_lt_one (le_max_right |K| 1) have hKleM2 : K ≤ M ^ 2 := by have hKle_abs : K ≤ |K| := le_abs_self K have habs_le_M : |K| ≤ M := by dsimp [M] exact le_max_left |K| 1 have hM_le_M2 : M ≤ M ^ 2 := by nlinarith [hMpos, (le_max_right |K| 1 : (1 : ℝ) ≤ M)] exact hKle_abs.trans (habs_le_M.trans hM_le_M2) have hpoint : ∀ n, μ {ω | M * rn n < |Xn n ω|} ≤ μ {ω | K * (rn n) ^ 2 < |cn n ω|} := by intro n apply MeasureTheory.measure_mono_ae filter_upwards [hbound n] with ω hb hω replace hω : M * rn n < |Xn n ω| := hω have hMr_pos : 0 < M * rn n := mul_pos hMpos (hrn n) have hsqX : (M * rn n) ^ 2 < (Xn n ω) ^ 2 := by rw [← sq_abs (Xn n ω), sq_lt_sq] simpa [abs_of_pos hMr_pos] using hω have hleft_le : K * (rn n) ^ 2 ≤ M ^ 2 * (rn n) ^ 2 := mul_le_mul_of_nonneg_right hKleM2 (sq_nonneg (rn n)) have hmul_sq : M ^ 2 * (rn n) ^ 2 = (M * rn n) ^ 2 := by ring have hlt_cn : K * (rn n) ^ 2 < cn n ω := by calc K * (rn n) ^ 2 ≤ M ^ 2 * (rn n) ^ 2 := hleft_le _ = (M * rn n) ^ 2 := hmul_sq _ < (Xn n ω) ^ 2 := hsqX _ ≤ cn n ω := hb exact hlt_cn.trans_le (le_abs_self (cn n ω)) refine ⟨M, ?_⟩ exact le_trans (Filter.limsup_le_limsup (Eventually.of_forall hpoint)) hK

theorem IsLittleOp.of_eq_on_asymptotic {Xn Yn : ℕ → Ω → ℝ} {rn : ℕ → ℝ} (h_diff_to_zero : Tendsto (fun n => μ {ω | Xn n ω ≠ Yn n ω}) atTop (𝓝 0)) (h_tilde : IsLittleOp Yn rn μ) : IsLittleOp Xn rn μ := by intro ε hε have hY := h_tilde ε hε have hpoint : ∀ n, μ {ω | ε * rn n < |Xn n ω|} ≤ μ {ω | Xn n ω ≠ Yn n ω} + μ {ω | ε * rn n < |Yn n ω|} := by intro n calc μ {ω | ε * rn n < |Xn n ω|} ≤ μ ({ω | Xn n ω ≠ Yn n ω} ∪ {ω | ε * rn n < |Yn n ω|}) := by apply measure_mono intro ω hω by_cases hxy : Xn n ω = Yn n ω · exact inr (by simpa [hxy] using hω) · exact inl hxy _ ≤ μ {ω | Xn n ω ≠ Yn n ω} + μ {ω | ε * rn n < |Yn n ω|} := MeasureTheory.measure_union_le _ _ have hsum : Tendsto (fun n => μ {ω | Xn n ω ≠ Yn n ω} + μ {ω | ε * rn n < |Yn n ω|}) atTop (𝓝 0) := by simpa using h_diff_to_zero.add hY rw [ENNReal.tendsto_nhds_zero] at hsum ⊢ intro δ hδ exact (hsum δ hδ).mono fun n hn => (hpoint n).trans hn

theorem lintegral_ofReal_tendsto_zero_of_bdd_isLittleOp [IsProbabilityMeasure μ] {Xn : ℕ → Ω → ℝ} {M : ℝ} (hM : 0 ≤ M) (hXn_meas : ∀ n, Measurable (Xn n)) (hXn_nonneg : ∀ n ω, 0 ≤ Xn n ω) (hXn_bdd : ∀ n ω, Xn n ω ≤ M) (hXn_op : IsLittleOp Xn (fun _ => (1 : ℝ)) μ) : Tendsto (fun n => ∫⁻ ω, ofReal (Xn n ω) ∂μ) atTop (𝓝 0) := by rw [ENNReal.tendsto_nhds_zero] intro δ hδ by_cases hδtop : δ = ⊤ · filter_upwards with n simp [hδtop] have hδreal_pos : 0 < δ.toReal := ENNReal.toReal_pos (ne_of_gt hδ) hδtop let η : ℝ := δ.toReal / 4 let α : ℝ := δ.toReal / (4 * (M + 1)) have hηpos : 0 < η := by dsimp [η] linarith have hαpos : 0 < α := by dsimp [α] exact div_pos hδreal_pos (mul_pos (by norm_num) (by linarith)) have hlintegral_le : ∀ n, ∫⁻ ω, ofReal (Xn n ω) ∂μ ≤ ofReal η + ofReal M * μ {ω | η * (1 : ℝ) < |Xn n ω|} := by intro n let A : Set Ω := {ω | Xn n ω ≤ η} have hA : MeasurableSet A := by dsimp [A] exact measurableSet_le (hXn_meas n) measurable_const have hsmall : ∫⁻ ω in A, ofReal (Xn n ω) ∂μ ≤ ofReal η := by calc ∫⁻ ω in A, ofReal (Xn n ω) ∂μ ≤ ∫⁻ ω in A, ofReal η ∂μ := by apply setLIntegral_mono measurable_const intro ω hω exact ENNReal.ofReal_le_ofReal hω _ = ofReal η * μ A := by rw [setLIntegral_const] _ ≤ ofReal η * μ univ := by exact mul_le_mul' le_rfl (measure_mono (Set.subset_univ A)) _ = ofReal η := by simp [MeasureTheory.measure_univ] have hlarge : ∫⁻ ω in Aᶜ, ofReal (Xn n ω) ∂μ ≤ ofReal M * μ {ω | η * (1 : ℝ) < |Xn n ω|} := by calc ∫⁻ ω in Aᶜ, ofReal (Xn n ω) ∂μ ≤ ∫⁻ ω in Aᶜ, ofReal M ∂μ := by apply setLIntegral_mono measurable_const intro ω hω exact ENNReal.ofReal_le_ofReal (hXn_bdd n ω) _ = ofReal M * μ Aᶜ := by rw [setLIntegral_const] _ ≤ ofReal M * μ {ω | η * (1 : ℝ) < |Xn n ω|} := by apply mul_le_mul' le_rfl apply measure_mono intro ω hω have hη_lt : η < Xn n ω := lt_of_not_ge hω simpa [abs_of_nonneg (hXn_nonneg n ω)] using hη_lt calc ∫⁻ ω, ofReal (Xn n ω) ∂μ = ∫⁻ ω in A, ofReal (Xn n ω) ∂μ + ∫⁻ ω in Aᶜ, ofReal (Xn n ω) ∂μ := by exact (lintegral_add_compl (μ := μ) (fun ω => ofReal (Xn n ω)) hA).symm _ ≤ ofReal η + ofReal M * μ {ω | η * (1 : ℝ) < |Xn n ω|} := add_le_add hsmall hlarge have hprob_event := (ENNReal.tendsto_nhds_zero.mp (hXn_op η hηpos)) (ofReal α) (ENNReal.ofReal_pos.mpr hαpos) filter_upwards [hprob_event] with n hn have hprod_le : ofReal M * μ {ω | η * (1 : ℝ) < |Xn n ω|} ≤ ofReal M * ofReal α := by exact mul_le_mul' le_rfl hn have hsum_eq : ofReal η + ofReal M * ofReal α = ofReal (η + M * α) := by rw [← ENNReal.ofReal_mul hM] rw [← ENNReal.ofReal_add (le_of_lt hηpos) (mul_nonneg hM (le_of_lt hαpos))] have hterm_le : M * α ≤ δ.toReal / 4 := by dsimp [α] field_simp [show (4 : ℝ) * (M + 1) ≠ 0 by nlinarith] nlinarith [mul_le_mul_of_nonneg_left (by linarith : M ≤ M + 1) (le_of_lt hδreal_pos)] have hsum_lt : ofReal (η + M * α) < δ := by rw [ENNReal.ofReal_lt_iff_lt_toReal] · dsimp [η] nlinarith · dsimp [η] nlinarith [le_of_lt hδreal_pos, hM, le_of_lt hαpos] · exact hδtop exact le_of_lt <| (hlintegral_le n).trans_lt <| lt_of_le_of_lt (add_le_add le_rfl hprod_le) <| hsum_eq.trans_lt hsum_lt

theorem abs_integral_le_eLpNorm_two [IsProbabilityMeasure ν] {f : X → ℝ} (hf : MemLp f 2 ν) : |∫ x, f x ∂ν| ≤ (eLpNorm f 2 ν).toReal := by have h_l1 : |∫ x, f x ∂ν| ≤ (eLpNorm f 1 ν).toReal := by calc |∫ x, f x ∂ν| ≤ ∫ x, |f x| ∂ν := MeasureTheory.abs_integral_le_integral_abs _ = (eLpNorm f 1 ν).toReal := by rw [MeasureTheory.eLpNorm_one_eq_lintegral_enorm] simpa [Real.norm_eq_abs] using MeasureTheory.integral_norm_eq_lintegral_enorm hf.1 exact h_l1.trans (ENNReal.toReal_mono hf.eLpNorm_ne_top (MeasureTheory.eLpNorm_le_eLpNorm_of_exponent_le (by norm_num) hf.1))

theorem integral_op_of_eLpNorm_op [IsProbabilityMeasure ν] {fn : ℕ → Ω → X → ℝ} (hfn_memLp : ∀ n ω, MemLp (fn n ω) 2 ν) {rn : ℕ → ℝ} (hrn : ∀ n, 0 < rn n) (hfn_rate : IsLittleOp (fun n ω => (eLpNorm (fn n ω) 2 ν).toReal) rn μ) : IsLittleOp (fun n ω => ∫ x, fn n ω x ∂ν) rn μ := by have _hrn := hrn intro ε hε have htarget := hfn_rate ε hε have hpoint : ∀ n, μ {ω | ε * rn n < |∫ x, fn n ω x ∂ν|} ≤ μ {ω | ε * rn n < |(eLpNorm (fn n ω) 2 ν).toReal|} := by intro n apply measure_mono intro ω hω exact (lt_of_lt_of_le hω (abs_integral_le_eLpNorm_two (hfn_memLp n ω))).trans_le (le_abs_self _) rw [ENNReal.tendsto_nhds_zero] at htarget ⊢ intro δ hδ exact (htarget δ hδ).mono fun n hn => (hpoint n).trans hn