CancellationTransport.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Actual tower transport for the cancellation path

Two row words move a cyclic tower by their respective degrees. If the unitary coefficient almost commutes with that tower, the explicit cancellation path has three transported components, with a uniform error independent of the tower height. No gauge action on the ambient algebra is assumed.

lemma OAI.WeakPureInfiniteness.transport_product_bound line 22
lemma OAI.WeakPureInfiniteness.tower_adjoint_transport line 30

lemma OAI.WeakPureInfiniteness.tower_sandwich_transport line 44

Source documentation

A word, a nearly central coefficient, and an adjoint word transport by the difference of the two word degrees.

lemma tower_sandwich_transport {N : ℕ} (e : ZMod N → E)
    (he : ∀ k, star (e k) = e k) (a b v : E) (da db : ZMod N)
    (δ : ℝ) (hδ : 0 ≤ δ)
    (han : ‖a‖ ≤ 1) (hbn : ‖b‖ ≤ 1) (hvn : ‖v‖ ≤ 2)
    (ha : ∀ k, ‖a * e k - e (k + da) * a‖ ≤ δ)
    (hb : ∀ k, ‖b * e k - e (k + db) * b‖ ≤ δ)
    (hv : ∀ k, ‖v * e k - e k * v‖ ≤ δ) (k : ZMod N) :
    ‖a * v * star b * e k - e (k + da - db) * (a * v * star b)‖ ≤ 5 * δ := by
…

lemma OAI.WeakPureInfiniteness.transport_unitary_norm_le line 76
lemma OAI.WeakPureInfiniteness.tower_unitary_sub_one line 83

lemma OAI.WeakPureInfiniteness.cornerCancellationPath_tower_transport line 99

Source documentation

The three components of the genuine cancellation path move the cyclic indices by 0, da-db, and db-da, with error at most 20δ. All premises concern the supplied tower and the actual input words.

lemma cornerCancellationPath_tower_transport {N : ℕ} (e : ZMod N → E)
    (he : ∀ k, star (e k) = e k) (a b : E) (u : unitary E)
    (haa : star a * a = 1) (hbb : star b * b = 1) (hab : star a * b = 0)
    (da db : ZMod N) (δ : ℝ) (hδ : 0 ≤ δ)
    (ha : ∀ k, ‖a * e k - e (k + da) * a‖ ≤ δ)
    (hb : ∀ k, ‖b * e k - e (k + db) * b‖ ≤ δ)
    (hu : ∀ k, ‖(u : E) * e k - e k * u‖ ≤ δ) (θ : ℝ) (k : ZMod N) :
    ‖cornerCancellationPath a b u θ * e k -
      (e k * (1 + (Real.cos θ ^ 2) •
          (a * ((u : E) - 1) * star a + b * (star (u : E) - 1) * star b)) +
        e (k + da - db) * ((Real.sin θ * Real.cos θ) •
          (a * ((u : E) - 1) * star b)) -
…

Mentions: OAI.WeakPureInfiniteness.cornerCancellationPath