OAI/Analysis/ForestSpace/Moduli.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ForestSpace.Cofinite line 17

   Source documentation

   The closed finite-codimensional subspaces.

   Also declared: ComparatorChallenges/ForestSpace.lean:19 (same declaration text).

   def Cofinite : Type :=
   …

2. def OAI.ForestSpace.cofiniteTop line 20
3. def OAI.ForestSpace.aucValues line 24

   Source documentation

   The inner one-sided excess values and their infimum.

   Also declared: ComparatorChallenges/ForestSpace.lean:23 (same declaration text).

   def aucValues (N : E → ℝ) (t : ℝ) (x : E) (F : Cofinite E) : Set ℝ :=
   …

   Mentions: OAI.ForestSpace.Cofinite

4. def OAI.ForestSpace.aucInner line 27

   Also declared: ComparatorChallenges/ForestSpace.lean:26 (same declaration text).

5. def OAI.ForestSpace.aucCenter line 30

   Also declared: ComparatorChallenges/ForestSpace.lean:29 (same declaration text).

6. def OAI.ForestSpace.aucModulus line 35

   Source documentation

   The one-sided asymptotic uniform convexity modulus, with the order of infimum, supremum and infimum.

   Also declared: ComparatorChallenges/ForestSpace.lean:34 (same declaration text).

   noncomputable def aucModulus (N : E → ℝ) (t : ℝ) : ℝ :=
   …

7. def OAI.ForestSpace.averageValues line 39

   Source documentation

   The inner averaged signed excess; it is not replaced by a maximum.

   Also declared: ComparatorChallenges/ForestSpace.lean:38 (same declaration text).

   def averageValues (N : E → ℝ) (t : ℝ) (x : E) (F : Cofinite E) : Set ℝ :=
   …

   Mentions: OAI.ForestSpace.Cofinite

8. def OAI.ForestSpace.averageInner line 43

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

9. def OAI.ForestSpace.averageCenter line 46

   Also declared: ComparatorChallenges/ForestSpace.lean:45 (same declaration text).

10. def OAI.ForestSpace.averageModulus line 50

    Source documentation

    The averaged asymptotic midpoint modulus.

    Also declared: ComparatorChallenges/ForestSpace.lean:49 (same declaration text).

    noncomputable def averageModulus (N : E → ℝ) (t : ℝ) : ℝ :=
    …

11. structure OAI.ForestSpace.EquivalentNorm line 57

    Source documentation

    An equivalent norm is kept as its exact real seminorm, with explicit positive comparison constants. The lower inequality makes it a norm.

    Also declared: ComparatorChallenges/ForestSpace.lean:56 (same declaration text).

    structure EquivalentNorm (E : Type) [NormedAddCommGroup E] [NormedSpace ℝ E]
        (α β : ℝ) where
    …

12. def OAI.ForestSpace.Reflexive line 65

    Source documentation

    Canonical (not merely abstract) reflexivity.

    Also declared: ComparatorChallenges/ForestSpace.lean:65 (same declaration text).

    def Reflexive (E : Type) [NormedAddCommGroup E] [NormedSpace ℝ E] : Prop :=
    …

13. def OAI.ForestSpace.IsAUC line 68

    Source documentation

    AUC requires positivity at every strictly positive parameter.

    Also declared: ComparatorChallenges/ForestSpace.lean:69 (same declaration text).

    def IsAUC {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (N : E → ℝ) : Prop :=
    …