OAI/GroupTheory/ArtinCAT0/SectorMetric.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArtinCAT0.SectorMetric.Point line 7
2. def OAI.ArtinCAT0.SectorMetric.vec line 9
3. lemma OAI.ArtinCAT0.SectorMetric.vec_zero line 12
4. lemma OAI.ArtinCAT0.SectorMetric.vec_add line 13
5. lemma OAI.ArtinCAT0.SectorMetric.vec_sub line 16
6. lemma OAI.ArtinCAT0.SectorMetric.vec_mul line 19
7. lemma OAI.ArtinCAT0.SectorMetric.vec_sq line 23
8. lemma OAI.ArtinCAT0.SectorMetric.vec_basis1 line 31
9. lemma OAI.ArtinCAT0.SectorMetric.vec_basis2 line 32
10. lemma OAI.ArtinCAT0.SectorMetric.vec_bound line 37
11. lemma OAI.ArtinCAT0.SectorMetric.vec_lipschitz line 46
12. def OAI.ArtinCAT0.SectorMetric.mixNorm line 53
13. def OAI.ArtinCAT0.SectorMetric.unit line 54
14. lemma OAI.ArtinCAT0.SectorMetric.mixNorm_bounds line 56
15. lemma OAI.ArtinCAT0.SectorMetric.unit_vec line 70
16. lemma OAI.ArtinCAT0.SectorMetric.unit_nonneg line 80
17. lemma OAI.ArtinCAT0.SectorMetric.unit_sum line 85
18. lemma OAI.ArtinCAT0.SectorMetric.unit_pairing1 line 95
19. lemma OAI.ArtinCAT0.SectorMetric.unit_pairing2 line 105
20. lemma OAI.ArtinCAT0.SectorMetric.detour_gap line 116

    Source documentation

    The short chord needed for the outside cap, with no trigonometry.

    lemma detour_gap {c : ℝ} (hc : 1/2 < c) (hc' : c ≤ 1) :
        ∃ r : ℝ, 0 < r ∧ r < 1 ∧ 0 < 1+r^2-2*c*r ∧
          2*Real.sqrt (1+r^2-2*c*r)+r < 2 := by
    …

21. lemma OAI.ArtinCAT0.SectorMetric.quotient_lipschitz line 129
22. lemma OAI.ArtinCAT0.SectorMetric.mixNorm_lipschitz line 147
23. lemma OAI.ArtinCAT0.SectorMetric.unit_lipschitz line 153
24. lemma OAI.ArtinCAT0.SectorMetric.unit_zero line 171
25. lemma OAI.ArtinCAT0.SectorMetric.unit_one line 172
26. lemma OAI.ArtinCAT0.SectorMetric.chord_axis1 line 175
27. lemma OAI.ArtinCAT0.SectorMetric.chord_axis2 line 184
28. lemma OAI.ArtinCAT0.lengthPairing_abs_le line 200
29. def OAI.ArtinCAT0.twoBraid line 222
30. lemma OAI.ArtinCAT0.twoBraid_relations line 223
31. lemma OAI.ArtinCAT0.braid_three_commute line 232
32. lemma OAI.ArtinCAT0.braid_three_pairing line 240
33. def OAI.ArtinCAT0.SixSector.ray line 258
34. lemma OAI.ArtinCAT0.SixSector.ray_even line 262
35. lemma OAI.ArtinCAT0.SixSector.ray_odd line 268
36. lemma OAI.ArtinCAT0.SixSector.ray_commute line 275
37. lemma OAI.ArtinCAT0.SixSector.generator_square_length_pos line 290
38. lemma OAI.ArtinCAT0.SixSector.adjacent_square_length line 300
39. def OAI.ArtinCAT0.SixSector.StrictRatios line 305
40. lemma OAI.ArtinCAT0.SixSector.ray_length_pos line 308
41. def OAI.ArtinCAT0.SixSector.cosine line 322
42. lemma OAI.ArtinCAT0.SixSector.cosine_lower line 325
43. lemma OAI.ArtinCAT0.SixSector.cosine_le_one line 375
44. lemma OAI.ArtinCAT0.SectorMetric.floor_error line 387
45. def OAI.ArtinCAT0.SectorMetric.lattice line 399
46. lemma OAI.ArtinCAT0.SectorMetric.lattice_origin line 402
47. lemma OAI.ArtinCAT0.SectorMetric.powers_difference line 405
48. lemma OAI.ArtinCAT0.SectorMetric.lattice_length line 413
49. theorem OAI.ArtinCAT0.SectorMetric.lattice_metric line 433

    Source documentation

    Rounding a flat-coordinate lattice introduces a bounded additive metric error, uniformly for all pairs of real points, not just a fixed finite net.

    theorem lattice_metric (hG : GeometricAction G X) (y : X) {g h : G}
        (hg : 0<stableLengthAt y g) (hh : 0<stableLengthAt y h) (hcomm : Commute g h)
        {c : ℝ} (hc : |c|≤1)
        (hp : lengthPairing y g h = c*stableLengthAt y g*stableLengthAt y h) :
        ∃ C : ℝ, 0 ≤ C ∧ ∀ p q : Point,
          |dist (lattice g h (stableLengthAt y g) (stableLengthAt y h) p • y)
              (lattice g h (stableLengthAt y g) (stableLengthAt y h) q • y) -
            ‖vec c (q.1-p.1,q.2-p.2)‖| ≤ C := by
    …

    Mentions: OAI.ArtinCAT0.stableLengthAt, OAI.ArtinCAT0.lengthPairing, OAI.ArtinCAT0.SectorMetric.Point, OAI.ArtinCAT0.SectorMetric.lattice, OAI.ArtinCAT0.SectorMetric.vec