OAI/Analysis/TreePotential/HilbertCompletion.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BoundedTreePotentials.CoordinateHilbert line 17
  2. def OAI.BoundedTreePotentials.finiteHilbert line 19
  3. lemma OAI.BoundedTreePotentials.finiteHilbert_apply line 24
  4. lemma OAI.BoundedTreePotentials.finiteHilbert_norm_sq line 26
  5. lemma OAI.BoundedTreePotentials.finiteHilbert_single line 34
  6. lemma OAI.BoundedTreePotentials.finiteHilbert_dense line 39
  7. def OAI.BoundedTreePotentials.finiteHilbertMap line 50

    Source documentation

    A general completion comparison, using both actual inequalities on c00. No finite dimensionality of the index set is asserted.

    def finiteHilbertMap (K : TestFamily I) (C : ℝ)
    (hlower : ∀ g, ‖finiteHilbert g‖ ≤ C*testNorm K g) :
    TestVector K →L[ℝ] CoordinateHilbert I :=
…

    Mentions: OAI.BoundedTreePotentials.TestFamily, OAI.BoundedTreePotentials.finiteHilbert, OAI.BoundedTreePotentials.testNorm, OAI.BoundedTreePotentials.TestVector, OAI.BoundedTreePotentials.CoordinateHilbert

  8. def OAI.BoundedTreePotentials.completedHilbertMap line 56
  9. lemma OAI.BoundedTreePotentials.completedHilbertMap_coe line 61
  10. lemma OAI.BoundedTreePotentials.completedHilbertMap_lower line 67
  11. def OAI.BoundedTreePotentials.completionHilbertEquiv line 77
  12. abbrev OAI.BoundedTreePotentials.Segments.BlockNode line 107
  13. def OAI.BoundedTreePotentials.Segments.componentEmbedding line 108
  14. abbrev OAI.BoundedTreePotentials.Segments.blockTests line 109
  15. abbrev OAI.BoundedTreePotentials.Segments.PredualBlock line 110
  16. lemma OAI.BoundedTreePotentials.Segments.Segment.card_nodes line 112
  17. lemma OAI.BoundedTreePotentials.Segments.Atom.profile_sq line 116
  18. lemma OAI.BoundedTreePotentials.Segments.Atom.profile_energy line 131
  19. lemma OAI.BoundedTreePotentials.Segments.predual_hilbert_upper line 156
  20. lemma OAI.BoundedTreePotentials.Segments.level_incomparable line 177
  21. lemma OAI.BoundedTreePotentials.Segments.level_energy line 189
  22. lemma OAI.BoundedTreePotentials.Segments.predual_hilbert_lower line 204
  23. lemma OAI.BoundedTreePotentials.finiteHilbert_emb_norm line 231
  24. lemma OAI.BoundedTreePotentials.Segments.component_support line 239
  25. lemma OAI.BoundedTreePotentials.Segments.block_hilbert_comparisons line 246
  26. def OAI.BoundedTreePotentials.Segments.predualBlockHilbertEquiv line 253
  27. theorem OAI.BoundedTreePotentials.Segments.predualBlock_reflexive line 257