OAI/Analysis/OInfinity/CanonicalShift.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The finite permutation cocycle of the canonical binary shift

The one-step cocycle swaps the first two letters. Its iterates are the right cyclic permutations of finite words. This balanced finite-matrix formula is separate from the nonzero-gauge cocycles of incomplete rows.

  1. lemma OAI.WeakPureInfiniteness.finiteCoordinateCycle_inv_eq_cons line 20
  2. lemma OAI.WeakPureInfiniteness.finiteJointWord_right_cycle line 30
  3. def OAI.WeakPureInfiniteness.canonicalShiftCycle line 38

    Source documentation

    The right cycle on all words of length n+1.

    def canonicalShiftCycle (s : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hsum : (∑ i, s i * star (s i)) = 1) (n : ℕ) : unitary E :=
…
  4. lemma OAI.WeakPureInfiniteness.canonicalShiftCycle_mul_word line 46
  5. lemma OAI.WeakPureInfiniteness.canonicalShiftCycle_zero line 57
  6. lemma OAI.WeakPureInfiniteness.canonicalShiftCycle_one_mul line 68
  7. lemma OAI.WeakPureInfiniteness.canonicalShiftCycle_one_generator line 77
  8. lemma OAI.WeakPureInfiniteness.canonicalShiftCycle_succ line 88

    Source documentation

    The finite cyclic permutation is the actual group cocycle of the one-step flip, with its orientation retained.

    lemma canonicalShiftCycle_succ (s : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hsum : (∑ i, s i * star (s i)) = 1) (n : ℕ) :
    canonicalShiftCycle s hs hsum (n + 1) =
      canonicalShiftCycle s hs hsum 1 *
        binarySplitHom (s 0) (s 1) (by simpa using hs 0 0)
          (by simpa using hs 1 1) (by simpa using hs 0 1)
          (canonicalShiftCycle s hs hsum n) := by
…

    Mentions: OAI.WeakPureInfiniteness.canonicalShiftCycle, OAI.WeakPureInfiniteness.binarySplitHom

  9. lemma OAI.WeakPureInfiniteness.canonicalShiftCycle_eq_cocycle line 131
  10. lemma OAI.WeakPureInfiniteness.canonicalShiftCycle_control line 145

    Source documentation

    The two affine reflection paths stay inside the balanced word algebra, so a single-row cyclic partition controls every point of the path.

    lemma canonicalShiftCycle_control {N : ℕ} (s : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hsum : (∑ i, s i * star (s i)) = 1)
    (e : ZMod N → E) (he : ∀ j, star (e j) = e j)
    (η : ℝ) (hη : 0 ≤ η)
    (hS : ∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ ≤ η) (n : ℕ) :
    ∃ p : Path (1 : unitary E) (canonicalShiftCycle s hs hsum n),
      ClockPathControl p e (2 * Real.pi) 0
        (2 * (Fintype.card (Fin (n + 1) → Fin 2) : ℝ) * (5 * (((n : ℝ) + 1) * η))) := by
…

    Mentions: OAI.WeakPureInfiniteness.finiteRowShift, OAI.WeakPureInfiniteness.canonicalShiftCycle, OAI.WeakPureInfiniteness.ClockPathControl

  11. def OAI.WeakPureInfiniteness.canonicalShiftCost line 215
  12. lemma OAI.WeakPureInfiniteness.canonicalShiftCost_nonneg line 218
  13. lemma OAI.WeakPureInfiniteness.exists_canonicalShift_cocycle_family line 224

    Source documentation

    All finite cocycle paths use one actual cyclic partition. The height and finite family bound are chosen before the partition accuracy.

    lemma exists_canonicalShift_cocycle_family [Nontrivial E]
    (s : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hsum : (∑ i, s i * star (s i)) = 1)
    (m N : ℕ) (ε : ℝ) (hε : 0 < ε) :
    let α := binarySplitHom (s 0) (s 1) (by simpa using hs 0 0)
…

    Mentions: OAI.WeakPureInfiniteness.binarySplitHom

  14. lemma OAI.WeakPureInfiniteness.exists_canonicalShift_coboundary_at_height line 278

    Source documentation

    The actual canonical-shift cocycle has a connected approximate coboundary; its only height-dependent error is the finite mesh term.

    lemma exists_canonicalShift_coboundary_at_height [Nontrivial E]
    (s : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hsum : (∑ i, s i * star (s i)) = 1) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
      ‖(canonicalShiftCycle s hs hsum 1 : E) * finiteRowShift s u - u‖ ≤
        (2 * Real.pi) * Real.sqrt (2 ^ m : ℕ) / (2 ^ m : ℕ) + ε := by
…

    Mentions: OAI.WeakPureInfiniteness.canonicalShiftCycle, OAI.WeakPureInfiniteness.finiteRowShift

  15. lemma OAI.WeakPureInfiniteness.exists_connected_canonicalShift_conjugacy line 331

    Source documentation

    The canonical binary endomorphism is approximately inner through unitaries connected to one, on its actual two generating isometries.

    lemma exists_connected_canonicalShift_conjugacy [Nontrivial E]
    (s : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hsum : (∑ i, s i * star (s i)) = 1) (ε : ℝ) (hε : 0 < ε) :
    ∃ u : unitary E, Joined (1 : unitary E) u ∧
      ∀ i, ‖(u : E) * s i * star (u : E) - finiteRowShift s (s i)‖ < ε := by
…

    Mentions: OAI.WeakPureInfiniteness.finiteRowShift