OAI/Analysis/Daugavet/LowerBounds.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactModuli.cofinite_top line 14
2. lemma OAI.ExactModuli.cofinite_nontrivial line 18
3. lemma OAI.ExactModuli.cofinite_has_unit line 25
4. lemma OAI.ExactModuli.norm_average_scale_le line 31
5. lemma OAI.ExactModuli.increment_normalize_le line 47
6. lemma OAI.ExactModuli.averagedIncrement_nonneg line 56
7. lemma OAI.ExactModuli.averagedIncrement_le line 65
8. lemma OAI.ExactModuli.averagedIncrement_ge_t_sub_one line 73
9. def OAI.ExactModuli.averageValues line 87

   Source documentation

   Inner sets are kept explicit to make nonemptiness and conditional completeness visible.

   def averageValues (x : X) (t : ℝ) (F : Submodule ℝ X) : Set ℝ :=
   …

10. def OAI.ExactModuli.oneSidedValues line 90
11. lemma OAI.ExactModuli.averageValues_nonempty line 93
12. lemma OAI.ExactModuli.averageValues_bddBelow line 98
13. lemma OAI.ExactModuli.oneSidedValues_nonempty line 105
14. lemma OAI.ExactModuli.oneSidedValues_bddBelow line 110
15. lemma OAI.ExactModuli.H_outer_bddAbove line 116
16. lemma OAI.ExactModuli.D_outer_bddAbove line 125
17. lemma OAI.ExactModuli.le_H_of_cofinite line 136
18. lemma OAI.ExactModuli.le_D_of_cofinite line 146
19. lemma OAI.ExactModuli.H_ge_t_sub_one line 156
20. lemma OAI.ExactModuli.H_ge_half line 164

    Source documentation

    The sharp half-mass lower estimate from the measure-precompactness hypothesis.

    lemma H_ge_half [IsProbabilityMeasure μ] (E : Submodule ℝ (Lp ℝ 1 μ))
        (hinf : ¬ FiniteDimensional ℝ E) (hpre : MeasurePrecompactBall μ E)
        {x : E} (hx : ‖x‖ = 1) {t : ℝ} (ht : 0 < t) :
        t / 2 ≤ H (normSeminorm ℝ E) x t := by
    …

    Mentions: OAI.ExactModuli.MeasurePrecompactBall, OAI.ExactModuli.H

21. theorem OAI.ExactModuli.clipping_lower_bound line 194
22. lemma OAI.ExactModuli.norm_ray_ge_t_sub_one line 205
23. theorem OAI.ExactModuli.oneSided_lower_bound line 213

    Source documentation

    The one-sided lower estimate needs only a norming functional.

    theorem oneSided_lower_bound (hinf : ¬ FiniteDimensional ℝ X) {x : X} (hx : ‖x‖ = 1)
        {t : ℝ} (ht : 0 ≤ t) : max 0 (t - 2) ≤ D (normSeminorm ℝ X) x t := by
    …

    Mentions: OAI.ExactModuli.D

24. lemma OAI.ExactModuli.norm_ray_endpoint_bound line 229

    Source documentation

    A single almost antipodal endpoint controls all radii, including the corner t=2.

    lemma norm_ray_endpoint_bound {x y : X} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1)
        {L ε t : ℝ} (hL : 0 < L) (hε : 0 ≤ ε) (ht : 0 ≤ t)
        (hend : ‖x + L • y‖ ≤ 1 + ε) :
        ‖x + t • y‖ ≤ 1 + ε + max 0 (t - L) := by
    …