DualCoordinates.lean`

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.BoundedTreePotentials.ForestCoordinates.hilbertSumTree_separable line 18
Source documentation
Countability is used on node coordinates, not just on the block index. This also applies to each of the equivalent finite-height dual norms.
```
theorem hilbertSumTree_separable (e : ∀ n, E n ≃L[ℝ] TreeHilbert (n+1)) :
    TopologicalSpace.SeparableSpace (HilbertSum E) := by
…
```
Mentions: OAI.BoundedTreePotentials.TreeHilbert, OAI.BoundedTreePotentials.HilbertSum
def OAI.BoundedTreePotentials.blockDualHilbertEquiv line 58
Source documentation
Hilbert coefficients of every finite-height linear-cost dual functional, with its genuine continuous topology. Its norm is p_n, not the Hilbert norm.
```
def blockDualHilbertEquiv (n : ℕ) : StrongDual ℝ (LinearBlock n) ≃L[ℝ] TreeHilbert n :=
…
```
Mentions: OAI.BoundedTreePotentials.LinearBlock, OAI.BoundedTreePotentials.TreeHilbert
lemma OAI.BoundedTreePotentials.blockDualHilbertEquiv_symm line 62
lemma OAI.BoundedTreePotentials.blockDualHilbertEquiv_functional line 68
lemma OAI.BoundedTreePotentials.blockDualHilbertEquiv_norm line 72
abbrev OAI.BoundedTreePotentials.LinearDualPieces line 76
def OAI.BoundedTreePotentials.linearDualCoefficients line 78
theorem OAI.BoundedTreePotentials.linearOuterDual_pairing line 82
Source documentation
The full linear-cost dual and its exact Hilbert pairing.
```
theorem linearOuterDual_pairing (φ : StrongDual ℝ LinearOuter) (x : LinearOuter) :
    φ x=∑' n,inner ℝ (linearDualCoefficients φ n) (linearBlockEquiv (n+1) (x n)) := by
…
```
Mentions: OAI.BoundedTreePotentials.LinearOuter, OAI.BoundedTreePotentials.linearDualCoefficients, OAI.BoundedTreePotentials.linearBlockEquiv
lemma OAI.BoundedTreePotentials.dualPieces_norm_eq line 91
theorem OAI.BoundedTreePotentials.linearOuterDual_norm_sq line 97
Source documentation
The sum of p_n-squares, with no equivalence constants substituted.
```
theorem linearOuterDual_norm_sq (φ : StrongDual ℝ LinearOuter) :
    ‖φ‖^2=∑' n,(linearPolar (n+1) (linearDualCoefficients φ n))^2 := by
…
```
Mentions: OAI.BoundedTreePotentials.LinearOuter, OAI.BoundedTreePotentials.linearPolar, OAI.BoundedTreePotentials.linearDualCoefficients
theorem OAI.BoundedTreePotentials.linearOuterDual_all_coefficients line 109
Source documentation
Conversely every square-p_n-summable Hilbert coefficient family is a dual functional. Thus the displayed coefficient description is onto.
```
theorem linearOuterDual_all_coefficients (f : (n : ℕ) → TreeHilbert (n+1))
    (hf : Summable (fun n => (linearPolar (n+1) (f n))^2)) :
    ∃ φ : StrongDual ℝ LinearOuter,linearDualCoefficients φ=f := by
…
```
Mentions: OAI.BoundedTreePotentials.TreeHilbert, OAI.BoundedTreePotentials.linearPolar, OAI.BoundedTreePotentials.LinearOuter, OAI.BoundedTreePotentials.linearDualCoefficients
theorem OAI.BoundedTreePotentials.linearOuter_separable_dual line 124
Source documentation
Norm separability of the full continuous linear-cost dual.
```
theorem linearOuter_separable_dual : TopologicalSpace.SeparableSpace (StrongDual ℝ LinearOuter) := by
…
```
Mentions: OAI.BoundedTreePotentials.LinearOuter
theorem OAI.BoundedTreePotentials.Segments.start_component_coordinates_mem line 137
Source documentation
All component coordinates of a literal finite-cost forest vector belong to the full finite-height Hilbert coordinate set.
```
theorem start_component_coordinates_mem (x : StartSpace) (n : ℕ) :
    Memℓp (fun v : BlockNode n => x.val (componentEmbedding n v)) 2 := by
…
```
Mentions: OAI.BoundedTreePotentials.Segments.StartSpace, OAI.BoundedTreePotentials.Segments.BlockNode, OAI.BoundedTreePotentials.Segments.componentEmbedding
theorem OAI.BoundedTreePotentials.Segments.start_outer_norm_sq line 148
Source documentation
Equality of the literal forest infimum with the outer Hilbert norm of the literal finite-height infima, not merely equivalence of these norms.
```
theorem start_outer_norm_sq (x : StartSpace) :
    ‖x‖^2=∑' n,(literalBlockStartNorm n (fun v => x.val (componentEmbedding n v)))^2 := by
…
```
Mentions: OAI.BoundedTreePotentials.Segments.StartSpace, OAI.BoundedTreePotentials.Segments.literalBlockStartNorm, OAI.BoundedTreePotentials.Segments.componentEmbedding
theorem OAI.BoundedTreePotentials.Segments.start_coordinate_characterization line 165
Source documentation
The range of countable finite-cost segment representations is exactly the outer ℓ₂ sum of Hilbert coordinate sets equipped with their literal infimal component norms.
```
theorem start_coordinate_characterization (z : Node → ℝ) :
    (∃ x : StartSpace,x.val=z) ↔
      (∀ n,Memℓp (fun v : BlockNode n => z (componentEmbedding n v)) 2) ∧
      Summable (fun n => (literalBlockStartNorm n (fun v => z (componentEmbedding n v)))^2) := by
…
```
Mentions: OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.Segments.StartSpace, OAI.BoundedTreePotentials.Segments.BlockNode, OAI.BoundedTreePotentials.Segments.componentEmbedding, OAI.BoundedTreePotentials.Segments.literalBlockStartNorm
theorem OAI.BoundedTreePotentials.Segments.start_finite_support_dense line 203
Source documentation
Density refers to finite node support, not merely to finite block support.
```
theorem start_finite_support_dense : Dense {x : StartSpace | (Function.support x.val).Finite} := by
…
```
Mentions: OAI.BoundedTreePotentials.Segments.StartSpace