OAI/Analysis/TreePotential/SegmentMidpoint.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundedTreePotentials.Segments.treeNode line 13
2. def OAI.BoundedTreePotentials.Segments.rootSegment line 15
3. lemma OAI.BoundedTreePotentials.Segments.rootSegment_mem line 18
4. lemma OAI.BoundedTreePotentials.Segments.treeNode_child_injective line 27
5. lemma OAI.BoundedTreePotentials.Segments.treeNode_child_prefix line 34
6. lemma OAI.BoundedTreePotentials.Segments.segmentVector_root_child line 39
7. def OAI.BoundedTreePotentials.Segments.boundedPath line 67
8. lemma OAI.BoundedTreePotentials.Segments.boundedPath_norm line 69
9. lemma OAI.BoundedTreePotentials.Segments.boundedPath_increment line 73
10. lemma OAI.BoundedTreePotentials.Segments.core_child_hilbert_upper line 79
11. lemma OAI.BoundedTreePotentials.Segments.core_children_weaklyNull line 121
12. theorem OAI.BoundedTreePotentials.Segments.incomparable_core_renorming_obstruction line 125
13. theorem OAI.BoundedTreePotentials.Segments.incomparable_renorming_obstruction line 143
14. theorem OAI.BoundedTreePotentials.Segments.incomparable_no_equivalent_AUC line 152
15. lemma OAI.BoundedTreePotentials.Segments.core_head_approx line 161
16. lemma OAI.BoundedTreePotentials.Segments.incomparable_squared_core line 184
17. theorem OAI.BoundedTreePotentials.Segments.incomparable_separated_core line 225

    Source documentation

    The separated-midpoint estimate on the isometric core, without finite-support assumptions on the center or sequence.

    theorem incomparable_separated_core (x : DualCore) (u : ℕ → DualCore)
        {c : ℝ} (hc : 0 < c) (hc1 : c ≤ 1)
        (hp : ∀ j, ‖x+u j‖ ≤ 1) (hm : ∀ j, ‖x-u j‖ ≤ 1)
        (hsep : ∀ i j, i ≠ j → 2*c ≤ ‖u i-u j‖) :
        ‖x‖ ≤ 1-(c/(Real.sqrt 2+Real.sqrt 6))^2 ∧ 1-(c/(Real.sqrt 2+Real.sqrt 6))^2 < 1 := by
    …

    Mentions: OAI.BoundedTreePotentials.Segments.DualCore

18. theorem OAI.BoundedTreePotentials.Segments.incomparable_separated_midpoints line 299