NormIdentities.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.BoundedTreePotentials.Segments.incomparable_iff_nodewise line 16
Source documentation
The start antichain convention is equivalent to nodewise incomparability, not merely disjointness of segments.
```
theorem incomparable_iff_nodewise (F : Finset Segment) :
    Incomparable F ↔ ∀ S ∈ F, ∀ T ∈ F, S ≠ T →
      ∀ s ∈ S.nodes, ∀ t ∈ T.nodes, ¬Prefix s t ∧ ¬Prefix t s := by
…
```
Mentions: OAI.BoundedTreePotentials.Segments.Segment, OAI.BoundedTreePotentials.Segments.Incomparable, OAI.BoundedTreePotentials.Segments.Prefix
def OAI.BoundedTreePotentials.Segments.completedSegmentEval line 27
Source documentation
Literal finite segment evaluation, with each coordinate extended to the completion by its proved continuous functional.
```
def completedSegmentEval (S : Segment) : Predual →L[ℝ] ℝ :=
…
```
Mentions: OAI.BoundedTreePotentials.Segments.Segment, OAI.BoundedTreePotentials.Segments.Predual
lemma OAI.BoundedTreePotentials.Segments.completedSegmentEval_coe line 30
lemma OAI.BoundedTreePotentials.Segments.completedAtomTest_eval line 34
lemma OAI.BoundedTreePotentials.Segments.completed_predual_family_energy line 45
theorem OAI.BoundedTreePotentials.Segments.predual_norm_formula line 56
Source documentation
The exact segment norm supremum on the full completion equals the atom-testing norm.
```
theorem predual_norm_formula (g : Predual) :
    ‖g‖=⨆ F : {F : Finset Segment // Incomparable F},
      Real.sqrt (∑ S ∈ F.val,(completedSegmentEval S g)^2) := by
…
```
Mentions: OAI.BoundedTreePotentials.Segments.Predual, OAI.BoundedTreePotentials.Segments.Segment, OAI.BoundedTreePotentials.Segments.Incomparable, OAI.BoundedTreePotentials.Segments.completedSegmentEval
theorem OAI.BoundedTreePotentials.Segments.predual_finite_norm_formula line 84
Source documentation
The exact original c00 norm used to form the predual completion.
```
theorem predual_finite_norm_formula (g : Node →₀ ℝ) :
    testNorm atomTests g=⨆ F : {F : Finset Segment // Incomparable F},
      Real.sqrt (∑ S ∈ F.val,(S.eval g)^2) := by
…
```
Mentions: OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.testNorm, OAI.BoundedTreePotentials.Segments.atomTests, OAI.BoundedTreePotentials.Segments.Segment, OAI.BoundedTreePotentials.Segments.Incomparable
def OAI.BoundedTreePotentials.linearOuterCoordinate line 97
Source documentation
Canonical coordinates in every finite-height component, including the last level (not only the shallower nodes used in the obstruction trees).
```
def linearOuterCoordinate (n : ℕ) (s : Tree (n+1)) : LinearOuter :=
…
```
Mentions: OAI.BoundedTreePotentials.Tree, OAI.BoundedTreePotentials.LinearOuter
def OAI.BoundedTreePotentials.linearOuterPath line 100
theorem OAI.BoundedTreePotentials.linearOuterCoordinate_norm line 103
theorem OAI.BoundedTreePotentials.linearOuterPath_norm line 109
theorem OAI.BoundedTreePotentials.linearOuter_children_weaklyNull line 115
theorem OAI.BoundedTreePotentials.Segments.incomparable_tail_head_zero line 125
Source documentation
The incomparable tail bound.
```
theorem incomparable_tail_head_zero {E : Finset Node} (hE : Initial (E : Set Node))
    (x y : Dual) (hx : dualHead E x=x) (hy : dualTail E y=y)
    (hp : ‖x+y‖≤1) (hm : ‖x-y‖≤1) :
    ‖y‖≤(Real.sqrt 2+Real.sqrt 6)*Real.sqrt (1-‖x‖) := by
…
```
Mentions: OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.Segments.Initial, OAI.BoundedTreePotentials.Segments.Dual, OAI.BoundedTreePotentials.Segments.dualHead, OAI.BoundedTreePotentials.Segments.dualTail
theorem OAI.BoundedTreePotentials.linearBlock_complete line 134
Source documentation
Completeness statements for the literal infimal-cost norm instances.
```
theorem linearBlock_complete (n : ℕ) : CompleteSpace (LinearBlock n) := inferInstance
```
Mentions: OAI.BoundedTreePotentials.LinearBlock
theorem OAI.BoundedTreePotentials.linearOuter_complete line 135
theorem OAI.BoundedTreePotentials.quadraticBlock_complete line 136
theorem OAI.BoundedTreePotentials.quadraticOuter_complete line 137
theorem OAI.BoundedTreePotentials.freeRoot_complete line 138

theorem OAI.BoundedTreePotentials.CostHeads.quadratic_uniform_sphere_infimum line 145

Source documentation

The exact real sphere-infimum formulation, with positive e_t chosen independently of the unit center.

theorem quadratic_uniform_sphere_infimum {t : ℝ} (ht : 0<t) :
    ∃ e : ℝ,0<e ∧ ∀ x : QuadraticOuter,‖x‖=1 →
      ∃ F : ClosedFiniteCodim QuadraticOuter,
        1+e≤⨅ u : {u : QuadraticOuter // u ∈ F.space ∧ ‖u‖=1},
          max ‖x+t • u.val‖ ‖x-t • u.val‖ := by
…

Mentions: OAI.BoundedTreePotentials.QuadraticOuter, OAI.BoundedTreePotentials.ClosedFiniteCodim

theorem OAI.BoundedTreePotentials.Segments.predualBlock_complete line 162
theorem OAI.BoundedTreePotentials.Segments.predual_complete line 163
theorem OAI.BoundedTreePotentials.Segments.incomparable_complete line 164
theorem OAI.BoundedTreePotentials.Segments.startBlock_complete line 165
theorem OAI.BoundedTreePotentials.Segments.start_complete line 166