ClockedBands.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Clock correction of the actual cyclic bands

A clock which cycles the projection partition turns a band of degree d into a block diagonal element after multiplication by its inverse dth power. The clock and the partition can be constructed inside a prescribed closed row algebra. This does not assert the endpoint cocycle equation.

lemma OAI.WeakPureInfiniteness.clock_cycles_pow line 20
lemma OAI.WeakPureInfiniteness.clock_inverse_pow_cycles line 37

lemma OAI.WeakPureInfiniteness.clocked_band_diagonal line 44

Source documentation

Exact removal of the outer band degree. Coefficients remain literal.

lemma clocked_band_diagonal {N : ℕ} [NeZero N] (u : E) (e : ZMod N → E)
    (he : ∀ j, star (e j) = e j)
    (hc : ∀ j, u * e j = e (j + 1) * u) (d : ℕ) (x : ZMod N → E) :
    star (u ^ d) * towerBand e (Equiv.addRight (d : ZMod N)) x =
      ∑ j, e j * (star (u ^ d) * x j) * e j := by
…

Mentions: OAI.WeakPureInfiniteness.towerBand

lemma OAI.WeakPureInfiniteness.clocked_band_commute line 58

Source documentation

The inverse clock makes the band commute with every projection cell.

lemma clocked_band_commute {N : ℕ} [NeZero N] (u : E) (e : ZMod N → E)
    (he : ∀ j, IsStarProjection (e j))
    (ho : ∀ i j, i ≠ j → e i * e j = 0)
    (hc : ∀ j, u * e j = e (j + 1) * u) (d : ℕ) (x : ZMod N → E) (k : ZMod N) :
    Commute (star (u ^ d) * towerBand e (Equiv.addRight (d : ZMod N)) x) (e k) := by
…

Mentions: OAI.WeakPureInfiniteness.towerBand

lemma OAI.WeakPureInfiniteness.clocked_masked_band_commute line 88
lemma OAI.WeakPureInfiniteness.clocked_band_gram line 97
Source documentation
The norm and initial Gram are unchanged by multiplication by a unitary clock.
```
lemma clocked_band_gram (u x : E) (hu : u ∈ unitary E) (d : ℕ) :
    star (star (u ^ d) * x) * (star (u ^ d) * x) = star x * x := by
…
```
lemma OAI.WeakPureInfiniteness.clocked_band_norm line 105
lemma OAI.WeakPureInfiniteness.evenRohlinClock_cycles_mod line 109
lemma OAI.WeakPureInfiniteness.evenRohlinClock_transports line 127
lemma OAI.WeakPureInfiniteness.clock_small_sqrt line 137

lemma OAI.WeakPureInfiniteness.exists_even_clock_partition_in line 158

Source documentation

The clock and all cells are constructed in B; their row commutators and shift errors have an arbitrary prescribed tolerance.

lemma exists_even_clock_partition_in {n : ℕ} (B : StarSubalgebra ℂ E)
    [IsClosed (B : Set E)] (r : Fin 2 × Fin n → E)
    (hr : ∀ i j, star (r i) * r j = if i = j then 1 else 0)
    (hsum : (∑ i, r i * star (r i)) = 1) (hmem : ∀ i, r i ∈ B)
    (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ (u : E) (e : ZMod (2 ^ m) → E),
      u ∈ B ∧ u ∈ unitary E ∧ u ^ (2 ^ m) = 1 ∧
      (∀ j, e j ∈ B) ∧ (∀ j, IsStarProjection (e j)) ∧ (∑ j, e j) = 1 ∧
      (∀ i j, i ≠ j → e i * e j = 0) ∧
      (∀ j, u * e j = e (j + 1) * u) ∧
      ‖evenRowShift r u - u‖ < ε ∧
      (∀ i, ‖u * r i - r i * u‖ < ε) ∧
…

Mentions: OAI.WeakPureInfiniteness.evenRowShift

lemma OAI.WeakPureInfiniteness.exists_binary_clock_commuting line 241

Source documentation

In the two-row application the clock and source partition commute exactly with the opposite row, because they lie in the generated source algebra. The source-generator estimate is quantitative.

lemma exists_binary_clock_commuting (s t : 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)
    (hcomm : bergRowsCommute s t) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ (u : E) (e : ZMod (2 ^ m) → E),
      u ∈ unitary E ∧ u ^ (2 ^ m) = 1 ∧
      (∀ j, IsStarProjection (e j)) ∧ (∑ j, e j) = 1 ∧
      (∀ i j, i ≠ j → e i * e j = 0) ∧
      (∀ j, u * e j = e (j + 1) * u) ∧
      ‖finiteRowShift s u - u‖ < ε ∧
      (∀ i, ‖u * s i - s i * u‖ < ε) ∧
      (∀ i, Commute u (t i)) ∧ (∀ j i, Commute (e j) (t i)) ∧
…

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