OAI/Analysis/Daugavet/EquivalentNorm.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactModuli.equivalentNorm_pos line 14
2. lemma OAI.ExactModuli.seminorm_normalize line 19
3. lemma OAI.ExactModuli.cofinite_has_Nunit line 23
4. def OAI.ExactModuli.normOneSidedValues line 30
5. lemma OAI.ExactModuli.normOneSidedValues_bddBelow line 33
6. lemma OAI.ExactModuli.normOneSidedValues_nonempty line 39
7. lemma OAI.ExactModuli.normD_outer_bddAbove line 45
8. lemma OAI.ExactModuli.normD_ge_neg_one line 56
9. lemma OAI.ExactModuli.normD_centers_bddBelow line 64
10. lemma OAI.ExactModuli.seminorm_segment_le line 72

    Source documentation

    Seminorm convexity with an explicit common endpoint bound.

    lemma seminorm_segment_le (N : Seminorm ℝ X) {x y : X} {r M : ℝ}
        (hr : 0 ≤ r) (hr' : r ≤ 1) (hx : N x ≤ M) (hy : N y ≤ M) :
        N ((1 - r) • x + r • y) ≤ M := by
    …

11. lemma OAI.ExactModuli.equivalentNorm_supremum line 87
12. lemma OAI.ExactModuli.seminorm_normalized_segment line 124
13. lemma OAI.ExactModuli.normD_bound_at_original_unit line 148