OAI/Analysis/TreePotential/StartMass.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundedTreePotentials.Segments.startArray line 15

    Source documentation

    Start masses indexed by the literal (component,prefix) array. There is one entry per actual segment, not one entry per path or per chain.

    def startArray (w : Segment → ℝ≥0∞) (n : ℕ) (s : List ℕ) : ℝ≥0∞ :=
…

    Mentions: OAI.BoundedTreePotentials.Segments.Segment

  2. lemma OAI.BoundedTreePotentials.Segments.startArray_mono line 18
  3. lemma OAI.BoundedTreePotentials.Segments.startArray_add line 26
  4. lemma OAI.BoundedTreePotentials.Segments.startArray_mul line 35
  5. lemma OAI.BoundedTreePotentials.Segments.startArray_tsum line 40
  6. lemma OAI.BoundedTreePotentials.Segments.startArray_zero line 50
  7. lemma OAI.BoundedTreePotentials.Segments.forest_treeSum_startArray line 52
  8. lemma OAI.BoundedTreePotentials.Segments.representation_test_energy line 82
  9. def OAI.BoundedTreePotentials.Segments.representationCost line 99

    Source documentation

    The start cost of a signed segment representation.

    def representationCost (a : Segment → ℝ) : ℝ≥0∞ :=
…

    Mentions: OAI.BoundedTreePotentials.Segments.Segment

  10. lemma OAI.BoundedTreePotentials.Segments.representationCost_add line 102
  11. lemma OAI.BoundedTreePotentials.Segments.representationCost_smul line 114
  12. lemma OAI.BoundedTreePotentials.Segments.representationCost_zero line 119
  13. lemma OAI.BoundedTreePotentials.Segments.startArray_nonzero line 128
  14. def OAI.BoundedTreePotentials.Segments.Atom.representation line 141
  15. lemma OAI.BoundedTreePotentials.Segments.Atom.representation_apply line 143
  16. lemma OAI.BoundedTreePotentials.Segments.Atom.start_injective line 147
  17. lemma OAI.BoundedTreePotentials.Segments.Atom.mass_antichain line 152
  18. lemma OAI.BoundedTreePotentials.Segments.Atom.mass_at_start line 169
  19. lemma OAI.BoundedTreePotentials.Segments.Atom.representation_cost line 190
  20. lemma OAI.BoundedTreePotentials.Segments.representation_finite_energy line 217
  21. lemma OAI.BoundedTreePotentials.Segments.real_series_bound line 249
  22. lemma OAI.BoundedTreePotentials.Segments.representation_series_bound line 263
  23. def OAI.BoundedTreePotentials.Segments.representationPairing line 272

    Source documentation

    The absolutely convergent countable representation pairing on finitely supported tests.

    def representationPairing (a : Segment → ℝ) (ha : representationCost a≠∞) : (Node →₀ ℝ) →ₗ[ℝ] ℝ where
…

    Mentions: OAI.BoundedTreePotentials.Segments.Segment, OAI.BoundedTreePotentials.Segments.representationCost, OAI.BoundedTreePotentials.Segments.Node