OAI/Analysis/OInfinity/BinaryFragmentation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Binary fragmentation and cancellation of localized unitaries

This is the finite path calculation underlying Brin's baker-map fragmentation argument (2009, Lemma 1, steps 4--5). The binary row here is coisometric in its unit. It is not the incomplete canonical row in O∞.

  1. def OAI.WeakPureInfiniteness.binaryCornerUnitary line 19
  2. lemma OAI.WeakPureInfiniteness.binaryCornerUnitary_one line 23
  3. lemma OAI.WeakPureInfiniteness.binaryCornerUnitary_mul line 28
  4. lemma OAI.WeakPureInfiniteness.binaryCornerUnitary_star line 34
  5. lemma OAI.WeakPureInfiniteness.binaryCornerUnitary_continuous line 39
  6. lemma OAI.WeakPureInfiniteness.binaryCornerUnitary_sub_norm_le line 45
  7. def OAI.WeakPureInfiniteness.binaryCornerPath line 70
  8. lemma OAI.WeakPureInfiniteness.binaryCornerPath_sub_norm_le line 74
  9. lemma OAI.WeakPureInfiniteness.binaryCornerUnitary_comp line 81
  10. lemma OAI.WeakPureInfiniteness.binaryProduct_isometry line 90
  11. lemma OAI.WeakPureInfiniteness.binaryCornerUnitary_commute line 97
  12. lemma OAI.WeakPureInfiniteness.exists_binaryCornerCancellation line 110

    Source documentation

    Cancelling two disjoint copies has a fixed path cost, independent of u.

    lemma exists_binaryCornerCancellation (a b : E)
    (ha : star a * a = 1) (hb : star b * b = 1) (hab : star a * b = 0)
    (u : unitary E) :
    ∃ p : Path (binaryCornerUnitary a ha u * binaryCornerUnitary b hb (star u)) 1,
      ∀ t s, ‖(p t : E) - p s‖ ≤ (2 * Real.pi) * |(t : ℝ) - s| := by
…

    Mentions: OAI.WeakPureInfiniteness.binaryCornerUnitary

  13. lemma OAI.WeakPureInfiniteness.binaryPath_mul_const_sub_norm_le line 128

    Source documentation

    A constant multiplier changes neither the speed nor endpoints' precision.

    lemma binaryPath_mul_const_sub_norm_le {u v : unitary E} (p : Path u v)
    (c : unitary E) (L : ℝ)
    (hp : ∀ t s, ‖(p t : E) - p s‖ ≤ L * |(t : ℝ) - s|) (t s : unitInterval) :
    ‖((p.mul (Path.refl c)) t : E) - (p.mul (Path.refl c)) s‖ ≤
      L * |(t : ℝ) - s| := by
…
  14. lemma OAI.WeakPureInfiniteness.binaryPath_symm_sub_norm_le line 137
  15. lemma OAI.WeakPureInfiniteness.exists_binaryQuarter_path line 151

    Source documentation

    One proper localized copy contracts using the splitting path in its parent and two disjoint-copy cancellations. No approximate commutation is needed. This is the finite content of Brin's small-rectangle argument.

    lemma exists_binaryQuarter_path (a b A B : E)
    (ha : star a * a = 1) (hb : star b * b = 1)
    (hA : star A * A = 1) (hB : star B * B = 1) (hAB : star A * B = 0)
    (u : unitary E) (L : ℝ) (hL : 0 ≤ L)
    (p : Path u (binaryCornerUnitary a ha u * binaryCornerUnitary b hb u))
    (hp : ∀ t s, ‖(p t : E) - p s‖ ≤ L * |(t : ℝ) - s|) :
    ∃ r : Path (binaryCornerUnitary (A * a) (binaryProduct_isometry A a hA ha) u) 1,
      ∀ t s, ‖(r t : E) - r s‖ ≤ (4 * (L + 2 * Real.pi)) * |(t : ℝ) - s| := by
…

    Mentions: OAI.WeakPureInfiniteness.binaryCornerUnitary, OAI.WeakPureInfiniteness.binaryProduct_isometry

  16. lemma OAI.WeakPureInfiniteness.exists_binaryFragmentation_path line 215

    Source documentation

    Binary fragmentation reduces a splitting path to a contraction with a uniform linear bound on its speed. The only input path is from the unitary to its two compressed copies.

    lemma exists_binaryFragmentation_path (a b : E)
    (ha : star a * a = 1) (hb : star b * b = 1) (hab : star a * b = 0)
    (u : unitary E) (L : ℝ) (hL : 0 ≤ L)
    (p : Path u (binaryCornerUnitary a ha u * binaryCornerUnitary b hb u))
    (hp : ∀ t s, ‖(p t : E) - p s‖ ≤ L * |(t : ℝ) - s|) :
    ∃ r : Path u 1,
      ∀ t s, ‖(r t : E) - r s‖ ≤ (32 * (L + 2 * Real.pi)) * |(t : ℝ) - s| := by
…

    Mentions: OAI.WeakPureInfiniteness.binaryCornerUnitary

  17. lemma OAI.WeakPureInfiniteness.exists_binaryFragmentation_of_defect_path line 291

    Source documentation

    A short path for the actual splitting defect gives the splitting path needed above, with the same speed.

    lemma exists_binaryFragmentation_of_defect_path (a b : E)
    (ha : star a * a = 1) (hb : star b * b = 1) (hab : star a * b = 0)
    (u : unitary E) (L : ℝ) (hL : 0 ≤ L)
    (p : Path (1 : unitary E)
      (u * star (binaryCornerUnitary a ha u * binaryCornerUnitary b hb u)))
    (hp : ∀ t s, ‖(p t : E) - p s‖ ≤ L * |(t : ℝ) - s|) :
    ∃ r : Path u 1,
      ∀ t s, ‖(r t : E) - r s‖ ≤ (32 * (L + 2 * Real.pi)) * |(t : ℝ) - s| := by
…

    Mentions: OAI.WeakPureInfiniteness.binaryCornerUnitary