OAI/Analysis/TreePotential/FiniteHeads.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundedTreePotentials.coordinateFunctional line 14
2. lemma OAI.BoundedTreePotentials.coordinateFunctional_coe line 17
3. def OAI.BoundedTreePotentials.coordinateVector line 23
4. lemma OAI.BoundedTreePotentials.norm_coordinateVector line 26
5. lemma OAI.BoundedTreePotentials.coordinateFunctional_vector line 30
6. def OAI.BoundedTreePotentials.completedHead line 35
7. lemma OAI.BoundedTreePotentials.completedHead_apply line 38
8. lemma OAI.BoundedTreePotentials.coordinate_completedHead line 42
9. lemma OAI.BoundedTreePotentials.finiteHead_eq_sum line 48
10. lemma OAI.BoundedTreePotentials.completedHead_coe line 55
11. def OAI.BoundedTreePotentials.headCoordinates line 65
12. def OAI.BoundedTreePotentials.coordinateTail line 70

    Source documentation

    Closed finite-codimensional coordinate tail, with no topological assumption on an arbitrary algebraic complement.

    def coordinateTail (K : TestFamily I) (B : Finset I) : Submodule ℝ (TestCompletion K) :=
    …

    Mentions: OAI.BoundedTreePotentials.TestFamily, OAI.BoundedTreePotentials.TestCompletion

13. lemma OAI.BoundedTreePotentials.mem_coordinateTail line 73
14. lemma OAI.BoundedTreePotentials.coordinateTail_closed line 78
15. instance OAI.BoundedTreePotentials.coordinateTail_finiteCodim line 82
16. def OAI.BoundedTreePotentials.completedTail line 86
17. lemma OAI.BoundedTreePotentials.completedTail_apply line 89
18. lemma OAI.BoundedTreePotentials.completedTail_mem line 92
19. lemma OAI.BoundedTreePotentials.completedTail_eq_self line 98
20. lemma OAI.BoundedTreePotentials.completedTail_coe line 106
21. lemma OAI.BoundedTreePotentials.completion_norm_pair_bound line 113

    Source documentation

    Density transfer with a continuous tail projection.

    lemma completion_norm_pair_bound (K : TestFamily I)
        (P : TestCompletion K →L[ℝ] TestCompletion K) (x : TestVector K) (a b t : ℝ)
        (h : ∀ w : TestVector K, a * ‖x‖ + b * ‖P (w : TestCompletion K)‖ ≤
          (‖(x : TestCompletion K) + t • P (w : TestCompletion K)‖ +
            ‖(x : TestCompletion K) - t • P (w : TestCompletion K)‖) / 2)
        (z : TestCompletion K) :
        a * ‖x‖ + b * ‖P z‖ ≤
          (‖(x : TestCompletion K) + t • P z‖ + ‖(x : TestCompletion K) - t • P z‖) / 2 := by
    …

    Mentions: OAI.BoundedTreePotentials.TestFamily, OAI.BoundedTreePotentials.TestCompletion, OAI.BoundedTreePotentials.TestVector

22. def OAI.BoundedTreePotentials.TreeCalculus.coordinateHead line 135
23. lemma OAI.BoundedTreePotentials.TreeCalculus.mem_coordinateHead line 138
24. def OAI.BoundedTreePotentials.TreeCalculus.initialHull line 141
25. lemma OAI.BoundedTreePotentials.TreeCalculus.root_mem_initialHull line 144
26. lemma OAI.BoundedTreePotentials.TreeCalculus.support_mem_initialHull line 147
27. lemma OAI.BoundedTreePotentials.TreeCalculus.initialHull_initial line 153
28. lemma OAI.BoundedTreePotentials.TreeCalculus.paired_vector_inequality line 168
29. lemma OAI.BoundedTreePotentials.TreeCalculus.paired_projected_inequality line 179
30. theorem OAI.BoundedTreePotentials.TreeCalculus.paired_completed_inequality line 201

    Source documentation

    The paired inequality on the actual completion. Finite tails are obtained by applying a continuous finite-coordinate tail projection to dense arrays.

    theorem paired_completed_inequality {r : Bool} {k : QuadraticKind} {D : Finset Node}
        (hD : Initial (D : Set Node)) (hroot : [] ∈ D)
        (x : TestVector (treeTestFamily r k)) (y : TestCompletion (treeTestFamily r k))
        (hx : ∀ s, (testVectorEquiv _ x) s ≠ 0 → s.val ∈ D)
        (hy : y ∈ coordinateTail (treeTestFamily r k) (coordinateHead r D))
        {a θ t : ℝ} (ha : 0 ≤ a) (ha1 : a ≤ 1) (hθ : 0 ≤ θ) (hθ1 : θ ≤ 1/2)
        (ht : 0 ≤ t) (hsquare : a^2 + θ^2 ≤ 1) :
        a * ‖x‖ + (t * θ / 2) * ‖y‖ ≤
          (‖(x : TestCompletion (treeTestFamily r k)) + t • y‖ +
            ‖(x : TestCompletion (treeTestFamily r k)) - t • y‖) / 2 := by
    …

    Mentions: OAI.BoundedTreePotentials.TreeCalculus.QuadraticKind, OAI.BoundedTreePotentials.TreeCalculus.Node, OAI.BoundedTreePotentials.TreeCalculus.Initial, OAI.BoundedTreePotentials.TestVector, OAI.BoundedTreePotentials.TreeCalculus.treeTestFamily, OAI.BoundedTreePotentials.TestCompletion, OAI.BoundedTreePotentials.testVectorEquiv, OAI.BoundedTreePotentials.coordinateTail, OAI.BoundedTreePotentials.TreeCalculus.coordinateHead