OAI/Analysis/Daugavet/Clipping.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactModuli.scalarClip line 14

   Source documentation

   Scalar clipping, equivalently sign(a) * min(|a|,h) when h >= 0.

   def scalarClip (h a : ℝ) : ℝ := max (-h) (min h a)

2. lemma OAI.ExactModuli.scalarClip_bounds line 16
3. lemma OAI.ExactModuli.abs_scalarClip_le line 22
4. lemma OAI.ExactModuli.scalarClip_eq_of_mem line 25
5. lemma OAI.ExactModuli.abs_sub_scalarClip line 29
6. lemma OAI.ExactModuli.abs_scalarClip_eq_min line 46
7. lemma OAI.ExactModuli.scalarClip_mono line 61
8. lemma OAI.ExactModuli.scalarClip_sub_le line 65
9. lemma OAI.ExactModuli.abs_scalarClip_sub_le line 71
10. lemma OAI.ExactModuli.scalar_average_abs line 82
11. def OAI.ExactModuli.clip line 109

    Source documentation

    Clip at a nonnegative L1 height. Clips are not required to belong to E.

    def clip (h y : Lp ℝ 1 μ) : Lp ℝ 1 μ := (-h) ⊔ (h ⊓ y)

12. lemma OAI.ExactModuli.coeFn_clip line 111
13. lemma OAI.ExactModuli.norm_sub_clip line 117
14. lemma OAI.ExactModuli.cofinite_ker line 133
15. lemma OAI.ExactModuli.finite_norming_kernel line 142

    Source documentation

    The finite norming-functional step of the clipping argument. In L1 the functionals can be taken to be signs; Hahn--Banach gives the same estimate.

    lemma finite_norming_kernel (j : X →L[ℝ] Y) (s : Finset Y) :
        ∃ F : Submodule ℝ X, Cofinite F ∧
          ∀ y ∈ F, ∀ b ∈ s, ‖b‖ ≤ ‖b - j y‖ := by
    …

    Mentions: OAI.ExactModuli.Cofinite

16. lemma OAI.ExactModuli.half_mass_of_norming line 166

    Source documentation

    The quantitative half-mass estimate, before the net radius tends to zero.

    lemma half_mass_of_norming {Y : Type uY} [NormedAddCommGroup Y] [NormedSpace ℝ Y]
        {b c u : Y} {ε : ℝ}
        (hunit : ‖u‖ = 1) (hres : ‖u - c‖ = ‖u‖ - ‖c‖)
        (hnet : ‖c - b‖ < ε) (hker : ‖b‖ ≤ ‖b - u‖) :
        ‖c‖ < 1 / 2 + ε := by
    …

17. lemma OAI.ExactModuli.small_set_integral_norm line 183
18. lemma OAI.ExactModuli.measureDistance_threshold_nonempty line 202
19. lemma OAI.ExactModuli.measureDistance_nonneg line 207
20. lemma OAI.ExactModuli.tail_lt_of_measureDistance_lt line 211
21. lemma OAI.ExactModuli.scalarClip_diff_le_two line 220
22. lemma OAI.ExactModuli.clip_small_tail line 229

    Source documentation

    Uniform passage from the measure metric to the L1 norm on the clipped image. This proves the norm-precompactness step without needing to choose subsequences.

    lemma clip_small_tail [IsProbabilityMeasure μ] (h : Lp ℝ 1 μ) (hh : 0 ≤ h)
        {ε : ℝ} (hε : 0 < ε) :
        ∃ δ : ℝ, 0 < δ ∧ ∀ f g : Lp ℝ 1 μ,
          μ.real {ω | δ < |f ω - g ω|} < δ → ‖clip h f - clip h g‖ < ε := by
    …

    Mentions: OAI.ExactModuli.clip

23. lemma OAI.ExactModuli.finite_clip_net line 265
24. lemma OAI.ExactModuli.finite_cokernel_half_clip line 278
25. lemma OAI.ExactModuli.scalar_overlap line 293
26. def OAI.ExactModuli.clipHeight line 311
27. lemma OAI.ExactModuli.coeFn_clipHeight line 313
28. lemma OAI.ExactModuli.clipHeight_nonneg line 318
29. lemma OAI.ExactModuli.overlap_identity line 325