OAI/Analysis/OInfinity/RowCocycleDefect.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual row cocycle and its finite splitting defect

The product cocycle V_n = W φ(W) ... φ^[n-1](W) is not a finite permutation. Its splitting defect is: V_n φ(V_n*) = ψ^[n](W*) W, where ψ = Ad(W) φ. For commuting binary Cuntz rows the right side is the adjoint of the joint-word cycle already constructed.

  1. def OAI.WeakPureInfiniteness.finiteGroupCocycle line 22
  2. lemma OAI.WeakPureInfiniteness.finiteGroupCocycle_splitting_defect line 26
  3. def OAI.WeakPureInfiniteness.binarySplitHom line 51
  4. lemma OAI.WeakPureInfiniteness.binarySplitHom_coe line 68
  5. def OAI.WeakPureInfiniteness.binaryRowUnitary line 81
  6. lemma OAI.WeakPureInfiniteness.finiteRowCocycle_conjugate_shift line 89
  7. lemma OAI.WeakPureInfiniteness.binarySplitHom_conjugacy line 105
  8. lemma OAI.WeakPureInfiniteness.binarySplitHom_iterate_coe line 123
  9. lemma OAI.WeakPureInfiniteness.finiteRowShift_star line 134
  10. lemma OAI.WeakPureInfiniteness.finiteRowShiftIterate_star line 138
  11. def OAI.WeakPureInfiniteness.binaryRowCocycleUnitary line 144
  12. lemma OAI.WeakPureInfiniteness.binaryRowCocycleUnitary_defect line 155

    Source documentation

    The splitting defect of the actual product cocycle, not the product itself, is the adjoint joint-word permutation.

    lemma binaryRowCocycleUnitary_defect (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 : ℕ) :
    ((binaryRowCocycleUnitary s t hs ht hsum htsum n : E) *
      star (binarySplitHom (s 0) (s 1) (by simpa using hs 0 0)
        (by simpa using hs 1 1) (by simpa using hs 0 1)
        (binaryRowCocycleUnitary s t hs ht hsum htsum n) : E)) =
      star (finiteJointCycleCoboundary t s n) := by
…

    Mentions: OAI.WeakPureInfiniteness.binaryRowCocycleUnitary, OAI.WeakPureInfiniteness.binarySplitHom, OAI.WeakPureInfiniteness.finiteJointCycleCoboundary

  13. lemma OAI.WeakPureInfiniteness.exists_uniform_binaryRowCocycle_path line 186

    Source documentation

    Uniform paths for the genuine binary product cocycles. The bound is independent of the number of factors. These are coisometric rows in the ambient unit; applying this in a proper corner requires corner transport.

    lemma exists_uniform_binaryRowCocycle_path [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 : ℕ) :
    ∃ p : Path (binaryRowCocycleUnitary s t hs ht hsum htsum n) 1,
      ∀ a b, ‖(p a : E) - p b‖ ≤ (192 * Real.pi) * |(a : ℝ) - b| := by
…

    Mentions: OAI.WeakPureInfiniteness.binaryRowCocycleUnitary