OAI/Analysis/TreePotential/Coordinates.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BoundedTreePotentials.ForestNode line 10
  2. def OAI.BoundedTreePotentials.FiniteOuterHead.subtreeEmbedding line 15
  3. def OAI.BoundedTreePotentials.FiniteOuterHead.ancestors line 19
  4. def OAI.BoundedTreePotentials.FiniteOuterHead.hull line 22
  5. lemma OAI.BoundedTreePotentials.FiniteOuterHead.mem_ancestors_same line 24
  6. lemma OAI.BoundedTreePotentials.FiniteOuterHead.hull_contains line 35
  7. lemma OAI.BoundedTreePotentials.FiniteOuterHead.hull_initial line 39
  8. def OAI.BoundedTreePotentials.FiniteOuterHead.ofFinset line 54
  9. lemma OAI.BoundedTreePotentials.FiniteOuterHead.ofFinset_contains line 74
  10. def OAI.BoundedTreePotentials.ForestCoordinates.coefficient line 84
  11. def OAI.BoundedTreePotentials.ForestCoordinates.coefficientCLM line 86
  12. lemma OAI.BoundedTreePotentials.ForestCoordinates.coefficientCLM_apply line 89
  13. lemma OAI.BoundedTreePotentials.ForestCoordinates.coefficient_add line 92
  14. lemma OAI.BoundedTreePotentials.ForestCoordinates.coefficient_smul line 94
  15. lemma OAI.BoundedTreePotentials.ForestCoordinates.coefficient_zero line 96
  16. lemma OAI.BoundedTreePotentials.ForestCoordinates.coefficient_ext line 98
  17. def OAI.BoundedTreePotentials.ForestCoordinates.finiteNodeSpace line 107

    Source documentation

    The actual finite node support, not only finite component support.

    def finiteNodeSpace : Submodule ℝ (HilbertSum E) where
…

    Mentions: OAI.BoundedTreePotentials.HilbertSum

  18. lemma OAI.BoundedTreePotentials.ForestCoordinates.finiteNodeSpace_single line 127
  19. lemma OAI.BoundedTreePotentials.ForestCoordinates.dense_finiteNodeSpace line 143
  20. lemma OAI.BoundedTreePotentials.ForestCoordinates.finiteNodeSpace_head line 164
  21. lemma OAI.BoundedTreePotentials.ForestCoordinates.exists_finite_head_approx line 174
  22. def OAI.BoundedTreePotentials.ForestCoordinates.finiteCoordinates line 181
  23. def OAI.BoundedTreePotentials.ForestCoordinates.coordinateTail line 185
  24. lemma OAI.BoundedTreePotentials.ForestCoordinates.mem_coordinateTail line 190