OAI/Analysis/TreePotential/StartRepresentation.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   The literal output coefficient of a countable segment array. Equivalently this is the double sum over t≼v with t≼s≼v; Segment carries exactly that pair.

   def representationOutput (a : Segment → ℝ) (v : Node) : ℝ :=
   …

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

2. lemma OAI.BoundedTreePotentials.Segments.representationOutput_summable line 18
3. def OAI.BoundedTreePotentials.Segments.finiteRepresentationFunctional line 26
4. lemma OAI.BoundedTreePotentials.Segments.finiteRepresentationFunctional_norm line 31
5. def OAI.BoundedTreePotentials.Segments.representationFunctional line 37
6. lemma OAI.BoundedTreePotentials.Segments.representationFunctional_lift line 40
7. lemma OAI.BoundedTreePotentials.Segments.representationFunctional_norm line 45
8. def OAI.BoundedTreePotentials.Segments.representedCore line 55

   Source documentation

   Every finite-cost literal representation defines an element of the full incomparable dual through the core/full-dual equivalence.

   def representedCore (a : Segment → ℝ) (ha : representationCost a≠∞) : DualCore :=
   …

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

9. lemma OAI.BoundedTreePotentials.Segments.representedCore_norm line 58
10. lemma OAI.BoundedTreePotentials.Segments.representedCore_coordinate line 64
11. lemma OAI.BoundedTreePotentials.Segments.dual_coordinates_total line 79
12. lemma OAI.BoundedTreePotentials.Segments.core_coordinates_total line 94
13. lemma OAI.BoundedTreePotentials.Segments.representedCore_add line 102
14. lemma OAI.BoundedTreePotentials.Segments.representedCore_smul line 118
15. lemma OAI.BoundedTreePotentials.Segments.Atom.representedCore line 133
16. lemma OAI.BoundedTreePotentials.Segments.representationCost_entry line 154
17. def OAI.BoundedTreePotentials.Segments.CostDomain line 163

    Source documentation

    The domain consists of all literal arrays of finite upward start cost.

    def CostDomain : Submodule ℝ (Segment → ℝ) where
    …

    Mentions: OAI.BoundedTreePotentials.Segments.Segment

18. def OAI.BoundedTreePotentials.Segments.representationMap line 172
19. lemma OAI.BoundedTreePotentials.Segments.representationCost_finset_sum line 177
20. lemma OAI.BoundedTreePotentials.Segments.atom_mixture_cost line 185
21. lemma OAI.BoundedTreePotentials.Segments.atom_mixture_output line 197
22. lemma OAI.BoundedTreePotentials.Segments.exists_representation_approx line 212
23. lemma OAI.BoundedTreePotentials.Segments.representationCost_tsum line 241
24. lemma OAI.BoundedTreePotentials.Segments.representationOutput_energy line 258
25. lemma OAI.BoundedTreePotentials.Segments.representedCore_summable line 267
26. lemma OAI.BoundedTreePotentials.Segments.representationOutput_joint_summable line 276

    Source documentation

    Absolute joint-coordinate summability, before exchanging two series.

    lemma representationOutput_joint_summable {I : Type*} (a : I → Segment → ℝ)
        (hcost : (∑' i,representationCost (a i))≠∞) (v : Node) :
        Summable (fun q : I × Segment => if v ∈ q.2.nodes then a q.1 q.2 else 0) := by
    …

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

27. lemma OAI.BoundedTreePotentials.Segments.real_tsum_ite_comm line 283
28. lemma OAI.BoundedTreePotentials.Segments.representationOutput_tsum line 293

    Source documentation

    Combining identical segments preserves every output coordinate.

    lemma representationOutput_tsum {I : Type*} (a : I → Segment → ℝ)
        (hcost : (∑' i,representationCost (a i))≠∞) (v : Node) :
        representationOutput (fun S => ∑' i,a i S) v=∑' i,representationOutput (a i) v := by
    …

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

29. lemma OAI.BoundedTreePotentials.Segments.representedCore_tsum line 299

    Source documentation

    Countable finite-cost representations commute with summation.

    lemma representedCore_tsum {I : Type*} (a : I → Segment → ℝ)
        (hcost : (∑' i,representationCost (a i))≠∞)
        (ha : representationCost (fun S => ∑' i,a i S)≠∞) :
        representedCore (fun S => ∑' i,a i S) ha=
          ∑' i,representedCore (a i) (ENNReal.ne_top_of_tsum_ne_top hcost i) := by
    …

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