OAI/Analysis/OInfinity/ClockFragmentation.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Controlled fragmentation on a joint cyclic partition

The clock-corrected quarter paths have a uniform sampled modulus, with an arbitrarily small additive error. The finite fragmentation operations below retain that modulus and the actual cell commutators. No continuity estimate for an arbitrary choice of a polar decomposition is used.

  1. structure OAI.WeakPureInfiniteness.ClockPathControl line 22

    Source documentation

    The two estimates needed when a finite path is sampled on the cyclic tower.

    structure ClockPathControl {u v : unitary E} (p : Path u v) (e : I → E)
    (L ρ C : ℝ) : Prop where
…
  2. lemma OAI.WeakPureInfiniteness.ClockPathControl.mono line 27
  3. lemma OAI.WeakPureInfiniteness.ClockPathControl.cast line 34
  4. lemma OAI.WeakPureInfiniteness.ClockPathControl.symm line 45
  5. lemma OAI.WeakPureInfiniteness.clock_product_commutator line 54

    Distinct definitions of this name: OAI/Analysis/OInfinity/ClockGram.lean:228 (different declaration text). Qualify references as OAI.WeakPureInfiniteness.clock_product_commutator@path.

  6. lemma OAI.WeakPureInfiniteness.ClockPathControl.mul line 67
  7. lemma OAI.WeakPureInfiniteness.clockPathControl_refl line 87
  8. lemma OAI.WeakPureInfiniteness.ClockPathControl.trans line 94

    Source documentation

    Concatenation doubles the mesh speed and adds at most two additive errors.

    lemma ClockPathControl.trans {u v w : unitary E} {p : Path u v} {q : Path v w}
    {e : I → E} {L ρ C : ℝ} (hρ : 0 ≤ ρ)
    (hp : ClockPathControl p e L ρ C) (hq : ClockPathControl q e L ρ C) :
    ClockPathControl (p.trans q) e (2 * L) (2 * ρ) C where
…

    Mentions: OAI.WeakPureInfiniteness.ClockPathControl

  9. lemma OAI.WeakPureInfiniteness.clock_fragment_isometry_norm line 144
  10. lemma OAI.WeakPureInfiniteness.clock_corner_commutator line 149
  11. lemma OAI.WeakPureInfiniteness.ClockPathControl.corner line 177
  12. lemma OAI.WeakPureInfiniteness.exists_joint_clocked_quarter_control line 190

    Source documentation

    The actual corrected angular paths, expressed on the unit interval with the two estimates used by fragmentation.

    lemma exists_joint_clocked_quarter_control [Nontrivial E] (s t : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (hsum : (∑ i, s i * star (s i)) = 1)
    (htsum : (∑ i, t i * star (t i)) = 1)
    (hcomm : bergRowsCommute s t) (m n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ e : ZMod (2 ^ m) → E,
      (∀ j, IsStarProjection (e j)) ∧ (∑ j, e j) = 1 ∧
      (∀ j l, j ≠ l → e j * e l = 0) ∧
      (∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ < ε) ∧
      (∀ j, ‖finiteRowShift t (e j) - e (j + 1)‖ < ε) ∧
      ∀ i r l : Fin 2, i ≠ l → ∃ p : Path
…

    Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.finiteRowShift

  13. lemma OAI.WeakPureInfiniteness.clock_fragment_product_transport line 234
  14. lemma OAI.WeakPureInfiniteness.exists_clocked_binaryQuarter line 256

    Source documentation

    The finite quarter-fragmentation step preserves cell commutators and an additive sampled modulus. Its cancellation paths are kept literal.

    lemma exists_clocked_binaryQuarter {N : ℕ} (e : ZMod N → E)
    (he : ∀ j, star (e j) = e j) (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)
    (u : unitary E) (L K ρ C δ : ℝ)
    (hL : 0 ≤ L) (hK : 0 ≤ K) (hρ : 0 ≤ ρ) (hC : 0 ≤ C) (hδ : 0 ≤ δ)
    (hu : ∀ j, ‖(u : E) * e j - e j * (u : E)‖ ≤ C)
    (haT : ∀ j, ‖a * e j - e (j + 1) * a‖ ≤ δ)
    (hAT : ∀ j, ‖A * e j - e (j + 1) * A‖ ≤ δ)
    (hBT : ∀ j, ‖B * e j - e (j + 1) * B‖ ≤ δ)
    (p : Path u (binaryCornerUnitary a ha u * binaryCornerUnitary b hb u))
    (hp : ClockPathControl p e L ρ C)
…

    Mentions: OAI.WeakPureInfiniteness.binaryCornerUnitary, OAI.WeakPureInfiniteness.ClockPathControl

  15. lemma OAI.WeakPureInfiniteness.exists_clocked_binaryFragmentation line 322

    Source documentation

    The complete finite binary fragmentation, with its actual supplied quarter paths and quantitative tower control.

    lemma exists_clocked_binaryFragmentation {N : ℕ} (s : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (e : ZMod N → E) (he : ∀ j, star (e j) = e j)
    (u : unitary E) (L K ρ C δ : ℝ)
    (hL : 0 ≤ L) (hK : 0 ≤ K) (hρ : 0 ≤ ρ) (hC : 0 ≤ C) (hδ : 0 ≤ δ)
    (hu : ∀ j, ‖(u : E) * e j - e j * (u : E)‖ ≤ C)
    (hT : ∀ i j, ‖s i * e j - e (j + 1) * s i‖ ≤ δ)
    (p : Path u (binaryCornerUnitary (s 0) (by simpa using hs 0 0) u *
      binaryCornerUnitary (s 1) (by simpa using hs 1 1) u))
    (hp : ClockPathControl p e L ρ C)
    (hc₁ : ∀ i j : Fin 2, i ≠ j → ∃ c : Path
      (binaryCornerUnitary (s i) (by simpa using hs i i) u *
…

    Mentions: OAI.WeakPureInfiniteness.binaryCornerUnitary, OAI.WeakPureInfiniteness.ClockPathControl

  16. lemma OAI.WeakPureInfiniteness.exists_balanced_clockCancellation line 415

    Source documentation

    Equal-degree cancellation needs no clock correction: its literal quarter rotation already almost commutes with the partition.

    lemma exists_balanced_clockCancellation {N : ℕ} (e : ZMod N → E)
    (he : ∀ j, star (e j) = e j) (a b : E) (u : unitary E)
    (ha : star a * a = 1) (hb : star b * b = 1) (hab : star a * b = 0)
    (d : ZMod N) (C δ : ℝ) (hC : 0 ≤ C) (hδ : 0 ≤ δ)
    (haT : ∀ j, ‖a * e j - e (j + d) * a‖ ≤ δ)
    (hbT : ∀ j, ‖b * e j - e (j + d) * b‖ ≤ δ)
    (hu : ∀ j, ‖(u : E) * e j - e j * (u : E)‖ ≤ C) :
    ∃ p : Path (binaryCornerUnitary a ha u * binaryCornerUnitary b hb (star u)) 1,
      ClockPathControl p e (2 * Real.pi) 0 (20 * (C + δ)) := by
…

    Mentions: OAI.WeakPureInfiniteness.binaryCornerUnitary, OAI.WeakPureInfiniteness.ClockPathControl

  17. lemma OAI.WeakPureInfiniteness.clock_jointWord_norm line 461
  18. lemma OAI.WeakPureInfiniteness.clock_jointWord_transport line 475
  19. lemma OAI.WeakPureInfiniteness.finiteJointPermutation_commutator_le line 518

    Source documentation

    Balanced finite matrix words commute approximately with the actual joint partition. This applies to each reflection in the cycle factorization.

    lemma finiteJointPermutation_commutator_le {N : ℕ} (s t : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (e : ZMod N → E) (he : ∀ j, star (e j) = e j) (η : ℝ) (hη : 0 ≤ η)
    (hS : ∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ ≤ η)
    (hT : ∀ j, ‖finiteRowShift t (e j) - e (j + 1)‖ ≤ η)
    (n : ℕ) (σ : Equiv.Perm (Fin (n + 1) → Fin 2)) (j : ZMod N) :
    ‖finiteRowPermutation (finiteJointWord s t n) σ * e j -
      e j * finiteRowPermutation (finiteJointWord s t n) σ‖ ≤
      (Fintype.card (Fin (n + 1) → Fin 2) : ℝ) * (5 * (((n : ℝ) + 1) * η)) := by
…

    Mentions: OAI.WeakPureInfiniteness.finiteRowShift, OAI.WeakPureInfiniteness.finiteRowPermutation, OAI.WeakPureInfiniteness.finiteJointWord

  20. lemma OAI.WeakPureInfiniteness.ClockPathControl.map_star line 549
  21. lemma OAI.WeakPureInfiniteness.exists_jointCycle_affine_control line 562

    Source documentation

    The literal two-reflection path for the splitting defect retains the finite joint-word commutator bound.

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

    Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.finiteRowShift, OAI.WeakPureInfiniteness.finiteJointCycleCoboundary, OAI.WeakPureInfiniteness.ClockPathControl

  22. lemma OAI.WeakPureInfiniteness.exists_joint_clocked_cocycle_path line 634

    Source documentation

    Actual cocycle contractions on an actual joint partition. The speed is uniform in the cocycle length; both additive sampling error and cell commutators can be made arbitrarily small. The source rows here are full coisometric binary rows.

    lemma exists_joint_clocked_cocycle_path [Nontrivial E] (s t : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (hsum : (∑ i, s i * star (s i)) = 1)
    (htsum : (∑ i, t i * star (t i)) = 1)
    (hcomm : bergRowsCommute s t) (m n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ e : ZMod (2 ^ m) → E,
      (∀ j, IsStarProjection (e j)) ∧ (∑ j, e j) = 1 ∧
      (∀ j l, j ≠ l → e j * e l = 0) ∧
      (∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ < ε) ∧
      (∀ j, ‖finiteRowShift t (e j) - e (j + 1)‖ < ε) ∧
      ∃ p : Path (binaryRowCocycleUnitary s t hs ht hsum htsum n) 1,
…

    Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.finiteRowShift, OAI.WeakPureInfiniteness.binaryRowCocycleUnitary