OAI/Analysis/Daugavet/MeasureDistance.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactModuli.measureDistance_self line 15
2. lemma OAI.ExactModuli.measureDistance_symm line 22
3. lemma OAI.ExactModuli.measureDistance_triangle line 26
4. lemma OAI.ExactModuli.measureDistance_le_of_norm_sub_lt_sq line 50

   Source documentation

   Markov's norm-to-measure estimate, in a form avoiding an unnecessary metric instance.

   lemma measureDistance_le_of_norm_sub_lt_sq (f g : Lp ℝ 1 μ) {ε : ℝ} (hε : 0 < ε)
       (hfg : ‖f - g‖ < ε ^ 2) : measureDistance μ f g ≤ ε := by
   …

   Mentions: OAI.ExactModuli.measureDistance

5. lemma OAI.ExactModuli.KW.normalizeL1_approx line 70
6. lemma OAI.ExactModuli.KW.sphere_normalize_approx line 93