OAI/Analysis/Daugavet/TailEstimates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactModuli.KW.measurable_real_tail line 16
2. lemma OAI.ExactModuli.KW.integral_min_abs_sq line 22

   Source documentation

   The bounded weighted layer-cake identity used for truncation variances.

   lemma integral_min_abs_sq {X : Ω → ℝ} (hX : Measurable X) {u : ℝ} (hu : 0 < u) :
       ∫ ω, (min |X ω| u) ^ 2 ∂μ =
         ∫ t in Ioc 0 u, 2 * t * μ.real {ω | t < |X ω|} := by
   …

3. lemma OAI.ExactModuli.KW.integral_min_sq_tail_bound line 75

   Source documentation

   A truncated symmetric summand has second moment controlled using its tail.

   lemma integral_min_sq_tail_bound {X : Ω → ℝ} (hX : Measurable X)
       {p C u : ℝ} (_hp : 0 < p) (hp2 : p < 2) (_hC : 0 ≤ C) (hu : 0 < u)
       (htail : ∀ t : ℝ, 0 < t → μ.real {ω | t < |X ω|} ≤ C * t ^ (-p)) :
       ∫ ω, (min |X ω| u) ^ 2 ∂μ ≤ (2 * C / (2 - p)) * u ^ (2 - p) := by
   …

4. def OAI.ExactModuli.KW.hardTruncate line 102
5. lemma OAI.ExactModuli.KW.measurable_hardTruncate line 104
6. lemma OAI.ExactModuli.KW.hardTruncate_neg line 107
7. lemma OAI.ExactModuli.KW.abs_hardTruncate_le line 111
8. lemma OAI.ExactModuli.KW.hardTruncate_sq_le_min_sq line 117
9. lemma OAI.ExactModuli.KW.integral_hardTruncate_zero line 126
10. lemma OAI.ExactModuli.KW.hardTruncate_memLp line 135
11. lemma OAI.ExactModuli.KW.hardTruncate_variance_bound line 140
12. lemma OAI.ExactModuli.KW.independent_symmetric_sum_tail line 157

    Source documentation

    Truncation, the union bound, and Chebyshev, uniformly in the number of summands.

    lemma independent_symmetric_sum_tail {ι : Type uIota} [Fintype ι]
        (X : ι → Ω → ℝ) (hX : ∀ j, Measurable (X j)) (hind : iIndepFun X μ)
        (hsym : ∀ j, IdentDistrib (X j) (fun ω => -X j ω) μ μ)
        {p : ℝ} (hp : 0 < p) (hp2 : p < 2) (C : ι → ℝ) (hC : ∀ j, 0 ≤ C j)
        (htail : ∀ j t, 0 < t → μ.real {ω | t < |X j ω|} ≤ C j * t ^ (-p))
        {u : ℝ} (hu : 0 < u) :
        μ.real {ω | u < |∑ j, X j ω|} ≤
          (1 + 2 / (2 - p)) * (∑ j, C j) * u ^ (-p) := by
    …