JointCycleIdentity.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

The joint-word cycle as a cocycle coboundary

The finite matrix cycle is W * φ^[n](W*), where W = ∑ tᵢ sᵢ*. This is a coboundary of W, not the product W φ(W) ⋯ φ^[n-1](W).

def OAI.WeakPureInfiniteness.finiteRowShiftIterate line 18
lemma OAI.WeakPureInfiniteness.finiteRowShift_support line 22
lemma OAI.WeakPureInfiniteness.finiteRowShiftIterate_right_support line 36
lemma OAI.WeakPureInfiniteness.finiteRowShift_mul_row line 45
lemma OAI.WeakPureInfiniteness.finiteRowShiftIterate_mul_jointWord line 59
lemma OAI.WeakPureInfiniteness.finiteRowCocycle_support line 76
lemma OAI.WeakPureInfiniteness.finiteRowShiftIterate_cocycle_star_mul_jointWord line 92
lemma OAI.WeakPureInfiniteness.finiteJointWord_move_target line 111
lemma OAI.WeakPureInfiniteness.finiteRowCocycle_mul_sourceWord line 131
lemma OAI.WeakPureInfiniteness.finiteCoordinateCycle_eq_snoc line 149
def OAI.WeakPureInfiniteness.finiteJointCycleCoboundary line 176
Source documentation
This is the degree-zero cycle coboundary, with its shifted adjoint tail.
```
def finiteJointCycleCoboundary (s t : I → E) (n : ℕ) : E :=
…
```
lemma OAI.WeakPureInfiniteness.finiteJointCycleCoboundary_mul_row line 179
lemma OAI.WeakPureInfiniteness.finiteRow_eq_of_mul_row_eq line 194
lemma OAI.WeakPureInfiniteness.finiteJointCycleCoboundary_eq_permutation line 204

lemma OAI.WeakPureInfiniteness.exists_controlled_jointCycleCoboundary_path line 231

Source documentation

The concrete coboundary has a path of speed at most 4π, uniformly in the iterate. This does not assert such a bound for products of W.

lemma exists_controlled_jointCycleCoboundary_path [Nontrivial E]
    (q : E) (s t : I → E) (hqstar : star q = q) (hqq : q * q = q)
    (hs : ∀ i j, star (s i) * s j = if i = j then q else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then q else 0)
    (hsum : (∑ i, s i * star (s i)) = q)
    (htsum : (∑ i, t i * star (t i)) = q)
    (hc : ∀ i j, Commute (s i) (t j)) (n : ℕ) :
    ∃ u : unitary E, (u : E) = finiteJointCycleCoboundary s t n + (1 - q) ∧
      ∃ p : Path (1 : unitary E) u,
        ∀ a b, ‖(p a : E) - p b‖ ≤ (4 * Real.pi) * |(a : ℝ) - b| := by
…

Mentions: OAI.WeakPureInfiniteness.finiteJointCycleCoboundary