CocycleCentrality.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Actual cocycle commutators with periodic source towers

The same source shift occurs in the cocycle and in the tower estimate. For elements fixed by the target row, the cocycle commutator equals the source-periodicity defect. In particular an N-cycle with step error η has cocycle commutator at most Nη. No centrality on source isometries is assumed.

lemma OAI.WeakPureInfiniteness.finiteGroupCocycle_inv line 22
lemma OAI.WeakPureInfiniteness.finiteRowShift_mul line 37
lemma OAI.WeakPureInfiniteness.finiteRowShift_fixed_of_commutes line 42
lemma OAI.WeakPureInfiniteness.finiteRowShiftIterate_fixed_of_commutes line 49
lemma OAI.WeakPureInfiniteness.binaryRowCocycle_coe_succ line 57
lemma OAI.WeakPureInfiniteness.finiteRowCocycle_shift_intertwining line 71

lemma OAI.WeakPureInfiniteness.binaryRowCocycle_iterate_intertwining line 86

Source documentation

Intertwining holds on every element, not just on generators.

lemma binaryRowCocycle_iterate_intertwining (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) (n : ℕ) (x : E) :
    (binaryRowCocycleUnitary s t hs ht hsum htsum n : E) * finiteRowShiftIterate s n x =
      finiteRowShiftIterate t n x * (binaryRowCocycleUnitary s t hs ht hsum htsum n : E) := by
…

Mentions: OAI.WeakPureInfiniteness.binaryRowCocycleUnitary, OAI.WeakPureInfiniteness.finiteRowShiftIterate

lemma OAI.WeakPureInfiniteness.binaryRowCocycle_star line 112

Source documentation

Reversing the rows gives exactly the adjoint product cocycle.

lemma binaryRowCocycle_star (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) (n : ℕ) :
    star (binaryRowCocycleUnitary s t hs ht hsum htsum n) =
      binaryRowCocycleUnitary t s ht hs htsum hsum n := by
…

Mentions: OAI.WeakPureInfiniteness.binaryRowCocycleUnitary

lemma OAI.WeakPureInfiniteness.binaryRowCocycle_commutator_norm line 132
lemma OAI.WeakPureInfiniteness.finiteRowShiftIterate_cycle_error line 148

lemma OAI.WeakPureInfiniteness.binaryRowCocycle_periodic_commutator_le line 170

Source documentation

A periodic source tower gives the actual cocycle commutator estimate.

lemma binaryRowCocycle_periodic_commutator_le (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)
    (x : ℕ → E) (N : ℕ) (η : ℝ) (hperiod : x N = x 0)
    (hstep : ∀ k < N, ‖finiteRowShift s (x k) - x (k + 1)‖ ≤ η)
    (hxt : ∀ i, Commute (t i) (x 0)) :
    ‖(binaryRowCocycleUnitary s t hs ht hsum htsum N : E) * x 0 -
        x 0 * (binaryRowCocycleUnitary s t hs ht hsum htsum N : E)‖ ≤ (N : ℝ) * η := by
…

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

lemma OAI.WeakPureInfiniteness.exists_binaryCocycleGrid line 185

Source documentation

Actual finite coefficients with uniform mesh error for the binary row cocycle. The endpoint equality is exact.

lemma exists_binaryCocycleGrid [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)
    (hc : ∀ i j, Commute (s i) (t j)) (N : ℕ) (hN : 0 < N) :
    ∃ v : Fin (N + 1) → unitary E,
      v 0 = v (Fin.last N) ∧
      ∀ k : Fin N, ‖finiteRowCocycle s t * finiteRowShift s (v k.castSucc) -
        (v k.succ : E)‖ ≤ (192 * Real.pi) / N := by
…

Mentions: OAI.WeakPureInfiniteness.finiteRowCocycle, OAI.WeakPureInfiniteness.finiteRowShift