OAI/Analysis/OInfinity/FinitePermutation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Finite row permutations

Permutations of a coisometric finite row give genuine unitaries after adding the ambient complement. Coordinate cycles factor into two reflections, so these cycle unitaries have uniform controlled paths. This applies to finite block permutations, not to the original nonzero-gauge row cocycle itself.

  1. def OAI.WeakPureInfiniteness.finiteRowPermutation line 20
  2. lemma OAI.WeakPureInfiniteness.finiteRowPermutation_star line 24
  3. lemma OAI.WeakPureInfiniteness.finiteRowPermutation_mul_row line 31
  4. lemma OAI.WeakPureInfiniteness.finiteRowPermutation_mul line 46
  5. lemma OAI.WeakPureInfiniteness.finiteRowPermutation_one line 57
  6. lemma OAI.WeakPureInfiniteness.finiteRowPermutation_support line 61
  7. lemma OAI.WeakPureInfiniteness.finiteRowPermutation_gram line 75
  8. def OAI.WeakPureInfiniteness.finiteRowPermutationUnitary line 87
  9. lemma OAI.WeakPureInfiniteness.finiteRowPermutationUnitary_mul line 98
  10. lemma OAI.WeakPureInfiniteness.finiteRowPermutationUnitary_involution line 113
  11. lemma OAI.WeakPureInfiniteness.exists_controlled_selfadjoint_unitary_path line 127

    Source documentation

    A selfadjoint unitary has a two-piece path with a fixed speed bound.

    lemma exists_controlled_selfadjoint_unitary_path [Nontrivial E] (u : unitary E)
    (hu : star (u : E) = (u : E)) :
    ∃ p : Path (1 : unitary E) u,
      ∀ t s, ‖(p t : E) - p s‖ ≤ (2 * Real.pi) * |(t : ℝ) - s| := by
…
  12. def OAI.WeakPureInfiniteness.finiteCoordinateReflection line 162

    Source documentation

    Reflection of the coordinate positions of a finite word.

    def finiteCoordinateReflection (m : ℕ) (c : ZMod m) : Equiv.Perm (ZMod m → I) where
…
  13. def OAI.WeakPureInfiniteness.finiteCoordinateCycle line 168
  14. lemma OAI.WeakPureInfiniteness.finiteCoordinateReflection_sq line 175
  15. lemma OAI.WeakPureInfiniteness.finiteCoordinateCycle_factor line 183
  16. lemma OAI.WeakPureInfiniteness.exists_controlled_coordinateCycle_path line 193

    Source documentation

    The cycle on a finite word row is a product of two actual selfadjoint row-permutation unitaries, so its path bound is independent of word length.

    lemma exists_controlled_coordinateCycle_path [Nontrivial E] (m : ℕ) [NeZero m]
    (q : E) (r : (ZMod m → I) → E) (hqstar : star q = q) (hqq : q * q = q)
    (hr : ∀ i j, star (r i) * r j = if i = j then q else 0)
    (hsum : (∑ i, r i * star (r i)) = q) :
    ∃ p : Path (1 : unitary E)
        (finiteRowPermutationUnitary q r hqstar hqq hr hsum (finiteCoordinateCycle m)),
      ∀ t s, ‖(p t : E) - p s‖ ≤ (4 * Real.pi) * |(t : ℝ) - s| := by
…

    Mentions: OAI.WeakPureInfiniteness.finiteRowPermutationUnitary, OAI.WeakPureInfiniteness.finiteCoordinateCycle