OAI/Analysis/Daugavet/Recovery.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ExactModuli.KW.infiniteCube line 13
2. abbrev OAI.ExactModuli.KW.infiniteCubeMeasure line 14
3. lemma OAI.ExactModuli.KW.infinite_coordinate_mp line 17
4. lemma OAI.ExactModuli.KW.finite_coordinates_mp line 21
5. lemma OAI.ExactModuli.KW.multiplier_averages line 28

   Source documentation

   The number of copies can be chosen arbitrarily late, after the whole-ball parameters. This is Mathlib's L1 strong law, applied to the exact Pareto multiplier.

   lemma multiplier_averages {p h : ℝ} (hp : 1 < p) (hh : 0 < h) :
       ∃ n : ℕ, 0 < n ∧
         (∫ v : cube (Fin n), |(n : ℝ)⁻¹ * (∑ j, multiplier p (v j)) - 1|
           ∂cubeMeasure (Fin n)) < h := by
   …

   Mentions: OAI.ExactModuli.KW.cube, OAI.ExactModuli.KW.multiplier, OAI.ExactModuli.KW.cubeMeasure