Main.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ForestSpace.main_theorem line 16
Source documentation
The space is the full continuous dual of the specified segment-norm completion, not the coordinate completion in place of that dual.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, Not, FiniteDimensional, Real, OAI.ForestSpace.FullDual, OAI.ForestSpace.Vertex, OAI.ForestSpace.J, OAI.ForestSpace.TestVector, RingHom.id, TopologicalSpace.SeparableSpace, OAI.ForestSpace.Reflexive, OAI.ForestSpace.EquivalentNorm, OAI.ForestSpace.IsAUC, Seminorm, OAI.ForestSpace.EquivalentNorm.N, LT.lt, OfNat.ofNat, LE.le, HSub.hSub, Real.sqrt and 9 more
Proof uses: And.intro, OAI.ForestSpace.infiniteDimensional_main_fullDual, OAI.ForestSpace.separable_main_fullDual, OAI.ForestSpace.reflexive_main_fullDual, OAI.ForestSpace.main_no_equivalent_AUC, OAI.ForestSpace.main_average_modulus, OAI.ForestSpace.main_diamond_distortion
204 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: ComparatorChallenges/ForestSpace.lean:453 (same statement text; different proof or body). Qualify references as OAI.ForestSpace.main_theorem@path.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem main_theorem :
    (¬FiniteDimensional ℝ (FullDual Vertex)) ∧
    TopologicalSpace.SeparableSpace (FullDual Vertex) ∧
    Reflexive (FullDual Vertex) ∧
    (∀ (α β : ℝ) (R : EquivalentNorm (FullDual Vertex) α β), ¬IsAUC R.N) ∧
    (∀ t : ℝ, 0 < t →
      Real.sqrt (1+t^2/12)-1 ≤ averageModulus (FullDual Vertex) norm t) ∧
    (∀ (k : ℕ) (f : (Diamond.diamond k).V → FullDual Vertex) (C : ℝ),
      Diamond.EmbeddingBound k f C → Real.sqrt (1+(k:ℝ)/12) ≤ C) := by
…
```
Mentions: OAI.ForestSpace.FullDual, OAI.ForestSpace.Vertex, OAI.ForestSpace.Reflexive, OAI.ForestSpace.EquivalentNorm, OAI.ForestSpace.IsAUC, OAI.ForestSpace.averageModulus, OAI.ForestSpace.Diamond.diamond, OAI.ForestSpace.Diamond.EmbeddingBound

theorem OAI.ForestSpace.general_forest_main line 32

Source documentation

The general-forest refinement. ForestOrder says that each ancestor set is a chain; finite ancestor sets provide the rooted-forest structure. No reflexivity or full-dual identification is assumed here.

theorem general_forest_main (V : Type) [PartialOrder V] [Countable V] [Infinite V]
    (hF : ForestOrder V) (hAnc : ∀ v : V, (Set.Iic v).Finite) :
    (∀ (H : Finset V) (hH : IsLowerSet (H : Set V)) (x y : X V),
      x = PX H hH x → y = QX H hH y →
      Real.sqrt (‖x‖^2+‖y‖^2/12) ≤ (‖x+y‖+‖x-y‖)/2) ∧
    (∀ (H : Finset V) (hH : IsLowerSet (H : Set V)) (x y : X V),
      x = PX H hH x → y = QX H hH y → ∀ (s t : ℝ), 0 < s → 0 < t →
      (‖x‖+s*t*‖y‖)/Real.sqrt (1+12*s^2) ≤ (‖x+t•y‖+‖x-t•y‖)/2) ∧
    (∀ t : ℝ, 0 < t → Real.sqrt (1+t^2/12)-1 ≤ averageModulus (X V) norm t) := by
…

Mentions: OAI.ForestSpace.ForestOrder, OAI.ForestSpace.X, OAI.ForestSpace.PX, OAI.ForestSpace.QX, OAI.ForestSpace.averageModulus

theorem OAI.ForestSpace.word_forest_main line 45
Source documentation
The last clause of the general-forest refinement, with exactly the scale alpha/(2 beta) and every equivalent norm.
```
theorem word_forest_main (α β : ℝ) (R : EquivalentNorm (X Word) α β) :
    aucModulus (X Word) R.N (α/(2*β)) = 0 :=
…
```
Mentions: OAI.ForestSpace.EquivalentNorm, OAI.ForestSpace.X, OAI.ForestSpace.Word, OAI.ForestSpace.aucModulus