OAI/Analysis/TreePotential/Main.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundedTreePotentials.TreeCalculus.main_counterexample line 12

   Source documentation

   Every root convention and quadratic budget gives a complete separable infinite-dimensional space with a positive real averaged midpoint modulus, but no continuously linearly equivalent space has an AUC norm.

   Distinct definitions of this name: ComparatorChallenges/BoundedTreePotentials.lean:339 (different declaration text). Qualify references as OAI.BoundedTreePotentials.TreeCalculus.main_counterexample@path.

   theorem main_counterexample (r : Bool) (k : QuadraticKind) :
       (CompleteSpace (TestCompletion (treeTestFamily r k)) ∧
         TopologicalSpace.SeparableSpace (TestCompletion (treeTestFamily r k)) ∧
         ¬Module.Finite ℝ (TestCompletion (treeTestFamily r k))) ∧
       (∀ t : ℝ, 0 < t → t < 1 →
         Real.sqrt (1 + t ^ 2 / 4) - 1 ≤
           averagedModulusReal (TestCompletion (treeTestFamily r k)) t) ∧
       (∀ (Y : Type u) [NormedAddCommGroup Y] [NormedSpace ℝ Y],
         (TestCompletion (treeTestFamily r k) ≃L[ℝ] Y) → ¬IsAUCReal Y) := by
   …

   Mentions: OAI.BoundedTreePotentials.TreeCalculus.QuadraticKind, OAI.BoundedTreePotentials.TestCompletion, OAI.BoundedTreePotentials.TreeCalculus.treeTestFamily, OAI.BoundedTreePotentials.averagedModulusReal