JointRohlin.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Joint source-target cyclic partitions

Convolving two commuting cyclic projection partitions produces one partition approximately shifted by both endomorphisms. This is the joint phase needed to control the row cocycle. The coefficient-path commutators are a separate requirement; no degree-zero property of the fragmentation path is asserted.

def OAI.WeakPureInfiniteness.jointRohlinProjection line 20
lemma OAI.WeakPureInfiniteness.jointRohlinProjection_star line 23
lemma OAI.WeakPureInfiniteness.jointRohlinProjection_mul line 33
lemma OAI.WeakPureInfiniteness.jointRohlinProjection_isStarProjection line 55
lemma OAI.WeakPureInfiniteness.jointRohlinProjection_orthogonal line 65
lemma OAI.WeakPureInfiniteness.jointRohlinProjection_sum line 80
lemma OAI.WeakPureInfiniteness.jointRohlinProjection_shift_left line 91
lemma OAI.WeakPureInfiniteness.jointRohlinProjection_shift_left_le line 107
lemma OAI.WeakPureInfiniteness.jointRohlinProjection_comm line 126
lemma OAI.WeakPureInfiniteness.jointRohlinProjection_shift_right_le line 136
lemma OAI.WeakPureInfiniteness.finiteRowShiftIterate_cyclic_error line 147

lemma OAI.WeakPureInfiniteness.binaryRowCocycle_joint_commutator_le line 163

Source documentation

A common cyclic shift for both rows controls every actual cocycle product. Unlike a source-only tower, this estimates all finite products.

lemma binaryRowCocycle_joint_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)
    (e : ZMod N → E) (ηs ηt : ℝ)
    (hshiftS : ∀ k, ‖finiteRowShift s (e k) - e (k + 1)‖ ≤ ηs)
    (hshiftT : ∀ k, ‖finiteRowShift t (e k) - e (k + 1)‖ ≤ ηt)
    (k : ZMod N) (n : ℕ) :
    ‖(binaryRowCocycleUnitary s t hs ht hsum htsum n : E) * e k -
      e k * (binaryRowCocycleUnitary s t hs ht hsum htsum n : E)‖ ≤
        (n : ℝ) * (ηs + ηt) := by
…

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

lemma OAI.WeakPureInfiniteness.binaryRowCocycle_jointRohlin_commutator_le line 200