OAI/Analysis/TreePotential/FiniteTree.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BoundedTreePotentials.Tree line 13

   Source documentation

   The countably branching, finite-height, root-inclusive tree.

   abbrev Tree (n : ℕ) := {s : List ℕ // s.length ≤ n}

2. abbrev OAI.BoundedTreePotentials.TreeHilbert line 14
3. def OAI.BoundedTreePotentials.root line 16
4. instance OAI.BoundedTreePotentials.(instance at line 17) line 17
5. def OAI.BoundedTreePotentials.prefixNode line 19
6. lemma OAI.BoundedTreePotentials.prefixNode_length line 22
7. lemma OAI.BoundedTreePotentials.prefixNode_injective line 27
8. def OAI.BoundedTreePotentials.pathNodes line 33
9. lemma OAI.BoundedTreePotentials.pathNodes_card line 36
10. lemma OAI.BoundedTreePotentials.mem_pathNodes_iff line 40
11. lemma OAI.BoundedTreePotentials.self_mem_pathNodes line 51
12. lemma OAI.BoundedTreePotentials.root_mem_pathNodes line 54
13. def OAI.BoundedTreePotentials.rootPath line 59

    Source documentation

    The root occurs in every path vector, including the root's own path.

    def rootPath {n : ℕ} (s : Tree n) : TreeHilbert n :=
    …

    Mentions: OAI.BoundedTreePotentials.Tree, OAI.BoundedTreePotentials.TreeHilbert

14. def OAI.BoundedTreePotentials.pathPotential line 62
15. lemma OAI.BoundedTreePotentials.rootPath_apply line 65
16. lemma OAI.BoundedTreePotentials.rootPath_norm_sq line 69
17. lemma OAI.BoundedTreePotentials.rootPath_norm_bound line 73
18. lemma OAI.BoundedTreePotentials.inner_rootPath line 78
19. def OAI.BoundedTreePotentials.pathSynthesis line 83

    Source documentation

    The map B_n is exactly the absolutely convergent signed sum of root paths.

    def pathSynthesis (n : ℕ) : L1Mass (Tree n) →L[ℝ] TreeHilbert n :=
    …

    Mentions: OAI.BoundedTreePotentials.L1Mass, OAI.BoundedTreePotentials.Tree, OAI.BoundedTreePotentials.TreeHilbert

20. lemma OAI.BoundedTreePotentials.pathSynthesis_apply line 86
21. lemma OAI.BoundedTreePotentials.pathSynthesis_bound line 89
22. def OAI.BoundedTreePotentials.linearBlockCost line 94

    Source documentation

    L_n, not Q_n: the two costs are added, not squared.

    def linearBlockCost (n : ℕ) (x : TreeHilbert n) : ℝ := linearCost (pathSynthesis n) x

    Mentions: OAI.BoundedTreePotentials.TreeHilbert, OAI.BoundedTreePotentials.linearCost, OAI.BoundedTreePotentials.pathSynthesis

23. def OAI.BoundedTreePotentials.linearPolar line 96
24. lemma OAI.BoundedTreePotentials.pathPotential_bound line 99
25. lemma OAI.BoundedTreePotentials.pathPotential_bddAbove line 105
26. lemma OAI.BoundedTreePotentials.linearPolar_le_one_iff line 109
27. theorem OAI.BoundedTreePotentials.linearBlockCost_duality line 115

    Source documentation

    Exact linear-cost duality with the root-potential norming set.

    theorem linearBlockCost_duality (n : ℕ) (x : TreeHilbert n) :
        linearBlockCost n x = sSup {r : ℝ | ∃ f : TreeHilbert n,
          linearPolar n f ≤ 1 ∧ r = inner ℝ f x} := by
    …

    Mentions: OAI.BoundedTreePotentials.TreeHilbert, OAI.BoundedTreePotentials.linearBlockCost, OAI.BoundedTreePotentials.linearPolar

28. theorem OAI.BoundedTreePotentials.linearBlockCost_comparison line 125

    Source documentation

    Both exact linear-cost norm comparison constants.

    theorem linearBlockCost_comparison (n : ℕ) (x : TreeHilbert n) :
        ‖x‖ / Real.sqrt (n + 1) ≤ linearBlockCost n x ∧ linearBlockCost n x ≤ ‖x‖ := by
    …

    Mentions: OAI.BoundedTreePotentials.TreeHilbert, OAI.BoundedTreePotentials.linearBlockCost

29. lemma OAI.BoundedTreePotentials.singleton_pathPotential line 134
30. lemma OAI.BoundedTreePotentials.singleton_polar_le_one line 139
31. lemma OAI.BoundedTreePotentials.linearBlockCost_eval_le line 148
32. lemma OAI.BoundedTreePotentials.linearBlockCost_abs_eval_le line 157
33. theorem OAI.BoundedTreePotentials.coordinate_le_linearBlockCost line 174

    Source documentation

    Every coordinate of a finite-height block is norm continuous, with bound 1.

    theorem coordinate_le_linearBlockCost {n : ℕ} (x : TreeHilbert n) (s : Tree n) :
        |x s| ≤ linearBlockCost n x := by
    …

    Mentions: OAI.BoundedTreePotentials.TreeHilbert, OAI.BoundedTreePotentials.Tree, OAI.BoundedTreePotentials.linearBlockCost

34. theorem OAI.BoundedTreePotentials.linearBlockCost_singleton line 179
35. theorem OAI.BoundedTreePotentials.linearBlockCost_rootPath line 185
36. def OAI.BoundedTreePotentials.LinearBlock line 197

    Source documentation

    A separate type is used for the infimal-cost norm. It is not silently identified with the original Hilbert norm.

    def LinearBlock (n : ℕ) := TreeHilbert n

    Mentions: OAI.BoundedTreePotentials.TreeHilbert

37. instance OAI.BoundedTreePotentials.(instance at line 198) line 198
38. instance OAI.BoundedTreePotentials.(instance at line 199) line 199
39. def OAI.BoundedTreePotentials.linearBlockEquiv line 200
40. instance OAI.BoundedTreePotentials.(instance at line 204) line 204
41. theorem OAI.BoundedTreePotentials.linearBlockCore line 206
42. instance OAI.BoundedTreePotentials.(instance at line 226) line 226
43. instance OAI.BoundedTreePotentials.(instance at line 227) line 227
44. lemma OAI.BoundedTreePotentials.norm_LinearBlock line 229
45. def OAI.BoundedTreePotentials.linearBlockHilbertEquiv line 233

    Source documentation

    Completeness is transported by equivalence of norms, with exactly the finite-height comparison constant sqrt(n+1).

    def linearBlockHilbertEquiv (n : ℕ) : LinearBlock n ≃L[ℝ] TreeHilbert n :=
    …

    Mentions: OAI.BoundedTreePotentials.LinearBlock, OAI.BoundedTreePotentials.TreeHilbert

46. def OAI.BoundedTreePotentials.linearBlockUniformEquiv line 242
47. instance OAI.BoundedTreePotentials.(instance at line 247) line 247
48. lemma OAI.BoundedTreePotentials.linearPolar_nonneg line 250
49. lemma OAI.BoundedTreePotentials.norm_le_linearPolar line 253
50. lemma OAI.BoundedTreePotentials.path_le_linearPolar line 255
51. lemma OAI.BoundedTreePotentials.pathPotential_smul line 259
52. lemma OAI.BoundedTreePotentials.linearBlockCost_abs_eval_scaled line 263
53. def OAI.BoundedTreePotentials.blockFunctional line 288

    Source documentation

    The functional with Hilbert coefficients f, acting on the L_n block.

    def blockFunctional (n : ℕ) (f : TreeHilbert n) : LinearBlock n →L[ℝ] ℝ :=
    …

    Mentions: OAI.BoundedTreePotentials.TreeHilbert, OAI.BoundedTreePotentials.LinearBlock

54. lemma OAI.BoundedTreePotentials.blockFunctional_apply line 291
55. lemma OAI.BoundedTreePotentials.block_inv_norm_le line 294
56. theorem OAI.BoundedTreePotentials.blockFunctional_norm line 302

    Source documentation

    The exact continuous-dual norm, not merely an equivalent norm.

    theorem blockFunctional_norm (n : ℕ) (f : TreeHilbert n) :
        ‖blockFunctional n f‖ = linearPolar n f := by
    …

    Mentions: OAI.BoundedTreePotentials.TreeHilbert, OAI.BoundedTreePotentials.blockFunctional, OAI.BoundedTreePotentials.linearPolar

57. theorem OAI.BoundedTreePotentials.blockFunctional_surjective line 330

    Source documentation

    Every bounded linear functional on X_n has Hilbert coefficients.

    theorem blockFunctional_surjective (n : ℕ) : Function.Surjective (blockFunctional n) := by
    …

    Mentions: OAI.BoundedTreePotentials.blockFunctional