OAI/GroupTheory/Hyperbolic/ThinTriangles.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Release075.Discrete.GeodesicSpace line 8
2. def OAI.Release075.Discrete.shortPath line 10
3. theorem OAI.Release075.Discrete.shortPath_geodesic line 12
4. theorem OAI.Release075.Discrete.shortPath_length line 15
5. def OAI.Release075.Discrete.Path.Outside line 21
6. theorem OAI.Release075.Discrete.Path.Outside.append line 23
7. theorem OAI.Release075.Discrete.Path.Outside.reverse line 30
8. theorem OAI.Release075.Discrete.Path.Outside.sub line 35
9. theorem OAI.Release075.Discrete.Path.outside_of_start line 41
10. theorem OAI.Release075.Discrete.Path.outside_of_end line 49
11. theorem OAI.Release075.Discrete.Path.triangle_lengths line 57
12. theorem OAI.Release075.Discrete.Path.shortBypass_arm line 72

    Source documentation

    Localization in a long arm of the comparison tripod.

    theorem shortBypass_arm (hgeo : GeodesicSpace M)
        {p : Path M a b} {q : Path M b c} {s : Path M a c}
        (hp : p.Geodesic) (hq : q.Geodesic) (hs : s.Geodesic)
        {T R t : ℕ} (hR : 4*T+2 ≤ R) (ht : t ≤ p.length)
        (hthin : SideNear T p q s)
        (hfar : ∀ x, q.Mem x ∨ s.Mem x → T ≤ M.dist (p.point t) x)
        (harm : t+4*R < (p.length+s.length-q.length)/2) :
        ShortBypass M T (p.point t) (10*R) := by
    …

    Mentions: OAI.Release075.Discrete.GeodesicSpace, OAI.Release075.Discrete.Path, OAI.Release075.Discrete.Path.SideNear, OAI.Release075.Discrete.ShortBypass

13. theorem OAI.Release075.Discrete.Path.shortBypass_center line 131

    Source documentation

    Localization near the three-pronged center of the comparison tripod.

    theorem shortBypass_center (hgeo : GeodesicSpace M)
        {p : Path M a b} {q : Path M b c} {s : Path M a c}
        (hp : p.Geodesic) (hq : q.Geodesic) (hs : s.Geodesic)
        {T R t : ℕ} (hR : 4*T+2 ≤ R) (ht : t ≤ p.length)
        (hthin : TriangleNear T p q s)
        (hfar : ∀ x, q.Mem x ∨ s.Mem x → T ≤ M.dist (p.point t) x)
        (hcenter₁ : (p.length+s.length-q.length)/2 ≤ t+4*R)
        (hcenter₂ : (p.length+q.length-s.length)/2 ≤ p.length-t+4*R) :
        ShortBypass M T (p.point t) (60*R) := by
    …

    Mentions: OAI.Release075.Discrete.GeodesicSpace, OAI.Release075.Discrete.Path, OAI.Release075.Discrete.Path.TriangleNear, OAI.Release075.Discrete.ShortBypass

14. theorem OAI.Release075.Discrete.Path.shortBypass_triangle line 244

    Source documentation

    A maximally fat point of a T-thin triangle has a bypass of length at most 1000(T+1).

    theorem shortBypass_triangle (hgeo : GeodesicSpace M)
        {p : Path M a b} {q : Path M b c} {s : Path M a c}
        (hp : p.Geodesic) (hq : q.Geodesic) (hs : s.Geodesic)
        {T : ℕ} (hthin : TriangleNear T p q s) {o : V} (ho : p.Mem o)
        (hfar : ∀ x, q.Mem x ∨ s.Mem x → T ≤ M.dist o x) :
        ShortBypass M T o (1000*(T+1)) := by
    …

    Mentions: OAI.Release075.Discrete.GeodesicSpace, OAI.Release075.Discrete.Path, OAI.Release075.Discrete.Path.TriangleNear, OAI.Release075.Discrete.ShortBypass

15. theorem OAI.Release075.Discrete.quadratic_bound line 276
16. theorem OAI.Release075.Discrete.Path.SideNear.mono line 294
17. theorem OAI.Release075.Discrete.Path.sideNear_shrink line 300
18. theorem OAI.Release075.Discrete.Path.triangleNear_shrink line 316
19. theorem OAI.Release075.Discrete.Path.triangleNear_of_cochainBound line 341

    Source documentation

    Discrete linear filling implies genuine uniform thinness of geodesic triangles.

    theorem triangleNear_of_cochainBound (hgeo : GeodesicSpace M) {B : ℕ}
        (hB : CochainBound M B) {p : Path M a b} {q : Path M b c} {s : Path M a c}
        (hp : p.Geodesic) (hq : q.Geodesic) (hs : s.Geodesic) :
        TriangleNear (10000*(B+1)) p q s := by
    …

    Mentions: OAI.Release075.Discrete.GeodesicSpace, OAI.Release075.Discrete.CochainBound, OAI.Release075.Discrete.Path, OAI.Release075.Discrete.Path.TriangleNear