IteratedBandTransport.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Actual endomorphism iterates on cyclic tower bands

Transport through a finite iterate costs the two endpoint tower errors. The adjacent-depth row identity is exact. In particular, mixed-depth orthogonality involves the inner letter of a two-letter word; it cannot be replaced by the same-depth outer-letter condition.

lemma OAI.WeakPureInfiniteness.binaryRowIterate_mul line 20
lemma OAI.WeakPureInfiniteness.binaryRowIterate_sub_norm_le line 29
lemma OAI.WeakPureInfiniteness.binaryRowIterate_norm_le line 38

lemma OAI.WeakPureInfiniteness.binaryRowIterate_adjacent line 46

Source documentation

The concrete intertwining relation between adjacent endomorphism depths.

lemma binaryRowIterate_adjacent (s : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (n : ℕ) (x : E) (i : Fin 2) :
    finiteRowShiftIterate s (n + 1) x * finiteRowShiftIterate s n (s i) =
      finiteRowShiftIterate s n (s i * x) := by
…

Mentions: OAI.WeakPureInfiniteness.finiteRowShiftIterate

lemma OAI.WeakPureInfiniteness.binaryRow_adjoint_left line 59

lemma OAI.WeakPureInfiniteness.binaryRowIterate_mixed_gram line 67

Source documentation

At neighboring depths the final letter, rather than the first letter, determines orthogonality.

lemma binaryRowIterate_mixed_gram (s : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (n : ℕ) (i r l : Fin 2) :
    star (finiteRowShiftIterate s n (s i * s r)) *
        finiteRowShiftIterate s (n + 1) (s l) =
      if r = l then finiteRowShiftIterate s n (star (s i)) else 0 := by
…

Mentions: OAI.WeakPureInfiniteness.finiteRowShiftIterate

lemma OAI.WeakPureInfiniteness.binaryRowIterate_band_transport line 88

Source documentation

An iterate of a degree-d coefficient still transports by d; the additional error is exactly the two endpoint tower errors.

lemma binaryRowIterate_band_transport {N : ℕ} (s : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (e : ZMod N → E) (η : ℝ) (hη : 0 ≤ η)
    (hshift : ∀ j, ‖finiteRowShift s (e j) - e (j + 1)‖ ≤ η)
    (x : E) (d : ZMod N) (δ : ℝ)
    (hx : ∀ j, ‖x * e j - e (j + d) * x‖ ≤ δ)
    (n : ℕ) (j : ZMod N) :
    ‖finiteRowShiftIterate s n x * e j -
        e (j + d) * finiteRowShiftIterate s n x‖ ≤
      δ + 2 * (n : ℝ) * η * ‖x‖ := by
…

Mentions: OAI.WeakPureInfiniteness.finiteRowShift, OAI.WeakPureInfiniteness.finiteRowShiftIterate