OAI/Analysis/TreePotential/SegmentHeads.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Cutting needs only ancestry, so it applies to finite heads and whole components.

   def Initial (C : Set Node) : Prop := ∀ ⦃s t⦄, s ∈ C → Prefix t s → t ∈ C

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

2. lemma OAI.BoundedTreePotentials.Segments.initial_complement line 17
3. lemma OAI.BoundedTreePotentials.Segments.prefix_of_length_le line 20
4. lemma OAI.BoundedTreePotentials.Segments.prefix_equal_length line 24
5. lemma OAI.BoundedTreePotentials.Segments.Segment.head_restriction line 29
6. lemma OAI.BoundedTreePotentials.Segments.Segment.tail_restriction line 50
7. lemma OAI.BoundedTreePotentials.Segments.incomparable_image line 71
8. lemma OAI.BoundedTreePotentials.Segments.unit_subsegment_family line 86
9. lemma OAI.BoundedTreePotentials.Segments.unit_head line 95
10. lemma OAI.BoundedTreePotentials.Segments.unit_tail line 117
11. lemma OAI.BoundedTreePotentials.Segments.shortening_loss line 143

    Source documentation

    At the crucial shortening step the starts are unchanged. The squared increase is paid out of the unused unit-test budget, not an assumed tail bound.

    lemma shortening_loss {g : Node → ℝ} (hg : IsUnitTest g) {F : Finset Segment}
        (hF : Incomparable F) (R : Segment → Segment) (c : Segment → ℝ)
        (hstart : ∀ S ∈ F, (R S).start=S.start)
        (heval : ∀ S ∈ F, (R S).eval g=S.eval g-c S)
        (hopposite : ∀ S ∈ F, S.eval g*c S ≤ 0) :
        2*(∑ S ∈ F, |S.eval g*c S|) ≤ 1-(∑ S ∈ F, (S.eval g)^2) := by
    …

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

12. def OAI.BoundedTreePotentials.Segments.oppositeProduct line 163

    Source documentation

    This is the unsigned product only on genuinely opposite signs.

    def oppositeProduct (a b : ℝ) : ℝ := (|a*b|-a*b)/2

13. lemma OAI.BoundedTreePotentials.Segments.oppositeProduct_nonneg line 165
14. lemma OAI.BoundedTreePotentials.Segments.oppositeProduct_eq line 169
15. lemma OAI.BoundedTreePotentials.Segments.unsigned_energy_identity line 178
16. lemma OAI.BoundedTreePotentials.Segments.unsigned_energy_bound line 204

    Source documentation

    The independent-copy cancellation step. No independence or expectation identity is assumed: both expectations and their product are finite sums.

    lemma unsigned_energy_bound (p : I → ℝ) (hp : ∀ i, 0 ≤ p i) (hp1 : ∑ i, p i=1)
        (r : I → Q → ℝ) (d : I → ℝ)
        (hc : ∀ i j, (∑ q, oppositeProduct (r i q) (r j q)) ≤ d i+d j) :
        (∑ q, (∑ i, p i*|r i q|)^2) ≤
          (∑ q, (∑ i, p i*r i q)^2)+4*(∑ i, p i*d i) := by
    …

    Mentions: OAI.BoundedTreePotentials.Segments.oppositeProduct

17. lemma OAI.BoundedTreePotentials.Segments.weighted_sqrt_bound line 233

    Source documentation

    Jensen's square-root bound, in precisely the finite-state setting used in the atom mixtures.

    lemma weighted_sqrt_bound (p : I → ℝ) (hp : ∀ i, 0 ≤ p i) (hp1 : ∑ i, p i=1)
        (d : I → ℝ) (hd : ∀ i, 0 ≤ d i) :
        (∑ i, p i*Real.sqrt (d i)) ≤ Real.sqrt (∑ i, p i*d i) := by
    …

18. def OAI.BoundedTreePotentials.Segments.startCost line 257

    Source documentation

    The start-mass cost, literally the upward recursion, including infinite values. The field m is restricted by the remaining height of recursion.

    def startCost : ℕ → (List ℕ → ℝ≥0∞) → ℝ≥0∞
      | 0, m => m []
      | n+1, m => m [] + (∑' j : ℕ, (startCost n (fun s => m (j::s)))^2)^(1/2:ℝ)

19. lemma OAI.BoundedTreePotentials.Segments.startCost_mono line 261
20. lemma OAI.BoundedTreePotentials.Segments.startCost_zero line 272
21. lemma OAI.BoundedTreePotentials.Segments.initial_before line 280
22. lemma OAI.BoundedTreePotentials.Segments.Segment.shorten_before line 284
23. lemma OAI.BoundedTreePotentials.Segments.Segment.eval_to_exit line 309

    Source documentation

    Replacing an endpoint after an exit does not affect a headed test.

    lemma Segment.eval_to_exit {C : Set Node} (hC : Initial C) {g : Node → ℝ}
        (hg : ∀ v ∉ C, g v=0) (S : Segment) {q : Node} (hq : q ∈ S.nodes) (hqC : q ∉ C) :
        S.eval g=(Segment.mk S.start q ((S.mem_nodes q).mp hq).1).eval g := by
    …

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

24. lemma OAI.BoundedTreePotentials.Segments.Segment.shorten_at_exit line 328
25. def OAI.BoundedTreePotentials.Segments.IsExit line 345

    Source documentation

    Minimal nodes outside an initial set, including roots of unused components.

    def IsExit (C : Set Node) (q : Node) : Prop := q ∉ C ∧ ∀ s, Prefix s q → s ≠ q → s ∈ C

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

26. lemma OAI.BoundedTreePotentials.Segments.exits_incomparable line 347
27. lemma OAI.BoundedTreePotentials.Segments.Segment.tail_exit line 351