OAI/Analysis/TreePotential/RealModuli.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BoundedTreePotentials.ereal_coe_ciInf line 14

    Source documentation

    Coercion commutes with a bounded real infimum.

    lemma ereal_coe_ciInf {I : Type*} [Nonempty I] (f : I → ℝ)
    (hf : BddBelow (Set.range f)) :
    ((⨅ i,f i : ℝ) : EReal) = ⨅ i,(f i : EReal) := by
…
  2. lemma OAI.BoundedTreePotentials.ereal_coe_ciSup line 34
  3. lemma OAI.BoundedTreePotentials.ereal_coe_modulus_game line 54
  4. instance OAI.BoundedTreePotentials.(instance at line 80) line 80
  5. lemma OAI.BoundedTreePotentials.ClosedFiniteCodim.unit_exists line 83
  6. def OAI.BoundedTreePotentials.averagedModulusReal line 97

    Source documentation

    The real-valued averaged asymptotic modulus.

    Also declared: ComparatorChallenges/BoundedTreePotentials.lean:325 (same declaration text).

    def averagedModulusReal (t : ℝ) : ℝ :=
…
  7. def OAI.BoundedTreePotentials.oneSidedModulusReal line 102

    Also declared: ComparatorChallenges/BoundedTreePotentials.lean:330 (same declaration text).

  8. def OAI.BoundedTreePotentials.maximumModulusReal line 106
  9. def OAI.BoundedTreePotentials.IsAUCReal line 111

    Distinct definitions of this name: ComparatorChallenges/BoundedTreePotentials.lean:334 (same statement text; different proof or body). Qualify references as OAI.BoundedTreePotentials.IsAUCReal@path.

  10. lemma OAI.BoundedTreePotentials.unit_nonempty_of_infinite line 113
  11. lemma OAI.BoundedTreePotentials.unit_perturbation_bound line 118
  12. lemma OAI.BoundedTreePotentials.averagedModulusReal_coe line 124
  13. lemma OAI.BoundedTreePotentials.oneSidedModulusReal_coe line 140
  14. lemma OAI.BoundedTreePotentials.maximumModulusReal_coe line 156
  15. lemma OAI.BoundedTreePotentials.isAUCReal_iff line 173
  16. lemma OAI.BoundedTreePotentials.oneSidedModulus_eq_top_of_finite line 178
  17. lemma OAI.BoundedTreePotentials.infiniteDimensional_of_not_isAUC line 193
  18. lemma OAI.BoundedTreePotentials.not_isAUCReal_of_not_isAUC line 201