OAI/Analysis/Daugavet/Model.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactModuli.Cofinite line 16

   Source documentation

   Closed linear subspaces of finite codimension.

   Also declared: ComparatorChallenges/DaugavetModuli.lean:17 (same declaration text).

   def Cofinite (F : Submodule ℝ X) : Prop :=
   …

2. def OAI.ExactModuli.averagedIncrement line 20

   Source documentation

   Averaged increment for directions of norm at least one.

   Also declared: ComparatorChallenges/DaugavetModuli.lean:21 (same declaration text).

   def averagedIncrement (N : Seminorm ℝ X) (x : X) (t : ℝ) (y : X) : ℝ :=
   …

3. def OAI.ExactModuli.H line 23

   Also declared: ComparatorChallenges/DaugavetModuli.lean:24 (same declaration text).

4. def OAI.ExactModuli.D line 27

   Also declared: ComparatorChallenges/DaugavetModuli.lean:28 (same declaration text).

5. def OAI.ExactModuli.averagedModulus line 31

   Also declared: ComparatorChallenges/DaugavetModuli.lean:32 (same declaration text).

6. def OAI.ExactModuli.oneSidedModulus line 34

   Also declared: ComparatorChallenges/DaugavetModuli.lean:35 (same declaration text).

7. def OAI.ExactModuli.EquivalentNorm line 38

   Source documentation

   Two-sided comparison makes this seminorm a genuine norm equivalent to the original.

   Also declared: ComparatorChallenges/DaugavetModuli.lean:39 (same declaration text).

   def EquivalentNorm (N : Seminorm ℝ X) : Prop :=
   …

8. def OAI.ExactModuli.AUC line 41

   Also declared: ComparatorChallenges/DaugavetModuli.lean:42 (same declaration text).

9. def OAI.ExactModuli.Daugavet line 45

   Source documentation

   Every rank-one operator has the form ell.smulRight v.

   Also declared: ComparatorChallenges/DaugavetModuli.lean:46 (same declaration text).

   def Daugavet (X : Type uX) [NormedAddCommGroup X] [NormedSpace ℝ X] : Prop :=
   …

10. def OAI.ExactModuli.measureDistance line 52

    Source documentation

    Convergence-in-measure distance on L1 equivalence classes.

    Also declared: ComparatorChallenges/DaugavetModuli.lean:53 (same declaration text).

    def measureDistance (f g : Lp ℝ 1 μ) : ℝ :=
    …

11. def OAI.ExactModuli.MeasurePrecompactBall line 56

    Source documentation

    Finite covers of the entire unit ball in convergence-in-measure distance.

    Also declared: ComparatorChallenges/DaugavetModuli.lean:57 (same declaration text).

    def MeasurePrecompactBall (E : Submodule ℝ (Lp ℝ 1 μ)) : Prop :=
    …

12. def OAI.ExactModuli.UnitSliceProperty line 61

    Source documentation

    Every nonempty unit-ball slice contains an almost antipodal unit vector.

    Also declared: ComparatorChallenges/DaugavetModuli.lean:62 (same declaration text).

    def UnitSliceProperty (X : Type uX) [NormedAddCommGroup X] [NormedSpace ℝ X] : Prop :=
    …

13. abbrev OAI.ExactModuli.KWOmega line 67

    Source documentation

    The countable product of unit intervals.

    Also declared: ComparatorChallenges/DaugavetModuli.lean:68 (same declaration text).

    abbrev KWOmega := ℕ → unitInterval

14. def OAI.ExactModuli.kwMeasure line 69

    Also declared: ComparatorChallenges/DaugavetModuli.lean:70 (same declaration text).