Normalization.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.BoundedTreePotentials.rootPath_root line 14
theorem OAI.BoundedTreePotentials.quadraticBlockCost_root line 21
Source documentation
The sharp root normalization for the quadratic cost, distinct from L_n.
```
theorem quadraticBlockCost_root (n : ℕ) :
    quadraticBlockCost n (lp.single 2 (root n) (1:ℝ))=1/Real.sqrt 2 := by
…
```
Mentions: OAI.BoundedTreePotentials.quadraticBlockCost, OAI.BoundedTreePotentials.root
theorem OAI.BoundedTreePotentials.quadratic_finite_support_dense line 45
theorem OAI.BoundedTreePotentials.TreeCalculus.four_completed_space line 53
Source documentation
Completeness, separability and infinite dimension for every literal test-norm completion.
```
theorem four_completed_space (r : Bool) (k : QuadraticKind) :
    CompleteSpace (TestCompletion (treeTestFamily r k)) ∧
    TopologicalSpace.SeparableSpace (TestCompletion (treeTestFamily r k)) ∧
    ¬Module.Finite ℝ (TestCompletion (treeTestFamily r k)) := by
…
```
Mentions: OAI.BoundedTreePotentials.TreeCalculus.QuadraticKind, OAI.BoundedTreePotentials.TestCompletion, OAI.BoundedTreePotentials.TreeCalculus.treeTestFamily
theorem OAI.BoundedTreePotentials.CostHeads.quadratic_uniform_maximum line 66
Source documentation
A uniform positive e_t independent of the unit center; the finite-codimensional tail may depend on the center.
```
theorem quadratic_uniform_maximum {t : ℝ} (ht : 0< t) :
    ∃ e : ℝ,0< e ∧ ∀ x : QuadraticOuter,‖x‖=1 →
      ∃ F : ClosedFiniteCodim QuadraticOuter,∀ u : QuadraticOuter,
        u ∈ F.space → ‖u‖=1 → 1+e ≤ max ‖x+t • u‖ ‖x-t • u‖ := by
…
```
Mentions: OAI.BoundedTreePotentials.QuadraticOuter, OAI.BoundedTreePotentials.ClosedFiniteCodim

theorem OAI.BoundedTreePotentials.Segments.start_unit_sphere_bound line 90

Source documentation

The segment-start midpoint consequence.

theorem start_unit_sphere_bound (x : StartSpace) (hx : ‖x‖=1)
    {t ε : ℝ} (ht : 0< t) (hε : 0<ε) :
    ∃ F : ClosedFiniteCodim StartSpace,
      ((Real.sqrt (1+t^2/64)-ε : ℝ) : EReal) ≤
        ⨅ y : {y : StartSpace // y ∈ F.space ∧ ‖y‖=1},
          ((max ‖x+t • y.val‖ ‖x-t • y.val‖ : ℝ) : EReal) := by
…

Mentions: OAI.BoundedTreePotentials.Segments.StartSpace, OAI.BoundedTreePotentials.ClosedFiniteCodim