OAI/Analysis/TreePotential/StartQuotient.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BoundedTreePotentials.Segments.exists_costDomain_approx line 13
  2. theorem OAI.BoundedTreePotentials.Segments.exists_representation_near_norm line 22

    Source documentation

    Reverse literal representation theorem. The geometric residual expansion is a single countable signed segment array with the original recursive cost; no attained infimum or finite-support restriction is assumed.

    theorem exists_representation_near_norm (x : DualCore) {e : ℝ} (he : 0< e) :
    ∃ (a : Segment → ℝ) (ha : representationCost a≠∞),
      representedCore a ha=x ∧ (representationCost a).toReal<‖x‖+e := by
…

    Mentions: OAI.BoundedTreePotentials.Segments.DualCore, OAI.BoundedTreePotentials.Segments.Segment, OAI.BoundedTreePotentials.Segments.representationCost, OAI.BoundedTreePotentials.Segments.representedCore

  3. def OAI.BoundedTreePotentials.Segments.coreCoordinates line 80
  4. lemma OAI.BoundedTreePotentials.Segments.coreCoordinates_injective line 85
  5. def OAI.BoundedTreePotentials.Segments.representationOutputMap line 95

    Source documentation

    The linear output of literal arrays, with absolute convergence proved for every finite-cost array.

    def representationOutputMap : CostDomain →ₗ[ℝ] (Node → ℝ) := coreCoordinates.comp representationMap

    Mentions: OAI.BoundedTreePotentials.Segments.CostDomain, OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.Segments.representationMap

  6. lemma OAI.BoundedTreePotentials.Segments.representationOutputMap_apply line 97
  7. def OAI.BoundedTreePotentials.Segments.StartSpace line 104

    Source documentation

    The segment-start space consists of coordinate fields represented by finite-cost countable signed segment arrays. Its norm equals the infimum over exactly these representations.

    def StartSpace := ↥(LinearMap.range representationOutputMap)

    Mentions: OAI.BoundedTreePotentials.Segments.representationOutputMap

  8. instance OAI.BoundedTreePotentials.Segments.(instance at line 106) line 106
  9. instance OAI.BoundedTreePotentials.Segments.(instance at line 107) line 107
  10. lemma OAI.BoundedTreePotentials.Segments.coreCoordinates_representable line 109
  11. def OAI.BoundedTreePotentials.Segments.coreStartMap line 115
  12. lemma OAI.BoundedTreePotentials.Segments.coreStartMap_bijective line 120
  13. def OAI.BoundedTreePotentials.Segments.coreStartEquiv line 128
  14. def OAI.BoundedTreePotentials.Segments.startCoreEquiv line 130
  15. instance OAI.BoundedTreePotentials.Segments.(instance at line 132) line 132
  16. theorem OAI.BoundedTreePotentials.Segments.startNormCore line 134
  17. instance OAI.BoundedTreePotentials.Segments.(instance at line 143) line 143
  18. instance OAI.BoundedTreePotentials.Segments.(instance at line 144) line 144
  19. def OAI.BoundedTreePotentials.Segments.startCoreIsometry line 146
  20. instance OAI.BoundedTreePotentials.Segments.(instance at line 148) line 148
  21. theorem OAI.BoundedTreePotentials.Segments.start_reflexive line 150
  22. lemma OAI.BoundedTreePotentials.Segments.startCore_coordinate line 152
  23. lemma OAI.BoundedTreePotentials.Segments.representedCore_eq_startCore line 157
  24. def OAI.BoundedTreePotentials.Segments.literalStartNorm line 169

    Source documentation

    Exactly the original infimal forest representation formula, including all finite-cost countable arrays and the original signed coordinate output.

    def literalStartNorm (x : Node → ℝ) : ℝ :=
…

    Mentions: OAI.BoundedTreePotentials.Segments.Node

  25. theorem OAI.BoundedTreePotentials.Segments.start_norm_eq_infimum line 172