OAI/Analysis/OInfinity/FixedSparePath.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Finite stabilization inside a genuinely fixed spare corner

The first corner is the support of the original unitary. Additional equivalent corners lie in its fixed complement. A cyclic permutation of these corners turns a diagonal of path samples into adjacent increments. All finite corners and the uncovered complement are retained explicitly.

  1. def OAI.WeakPureInfiniteness.fixedSpareBlock line 21

    Source documentation

    A diagonal block sum in a row of partial isometries.

    def fixedSpareBlock (r : I → E) (x : I → E) : E := ∑ i, r i * x i * star (r i)
  2. def OAI.WeakPureInfiniteness.fixedSpareRange line 23
  3. lemma OAI.WeakPureInfiniteness.fixedSpareBlock_one line 26
  4. lemma OAI.WeakPureInfiniteness.fixedSpareBlock_star line 30
  5. lemma OAI.WeakPureInfiniteness.fixedSpareBlock_sub line 35
  6. lemma OAI.WeakPureInfiniteness.fixedSpareRow_right line 46
  7. lemma OAI.WeakPureInfiniteness.fixedSpareRow_star_left line 51
  8. lemma OAI.WeakPureInfiniteness.fixedSpareBlock_mul line 56
  9. lemma OAI.WeakPureInfiniteness.fixedSpareRange_star line 74
  10. lemma OAI.WeakPureInfiniteness.fixedSpareRange_sq line 78
  11. lemma OAI.WeakPureInfiniteness.fixedSpareBlock_range line 84
  12. lemma OAI.WeakPureInfiniteness.fixedSpareBlock_gram line 94
  13. def OAI.WeakPureInfiniteness.fixedSpareDiagonalUnitary line 110
  14. lemma OAI.WeakPureInfiniteness.fixedSpareDiagonalUnitary_mul line 120
  15. lemma OAI.WeakPureInfiniteness.fixedSpareRange_mul_row line 137
  16. lemma OAI.WeakPureInfiniteness.fixedSparePermutation_support line 142
  17. lemma OAI.WeakPureInfiniteness.fixedSparePermutation_gram line 151
  18. def OAI.WeakPureInfiniteness.fixedSparePermutationUnitary line 161
  19. lemma OAI.WeakPureInfiniteness.fixedSparePermutationUnitary_mul line 171
  20. lemma OAI.WeakPureInfiniteness.fixedSparePermutationUnitary_involution line 186
  21. lemma OAI.WeakPureInfiniteness.fixedSpareRow_norm_le line 200
  22. lemma OAI.WeakPureInfiniteness.fixedSpareBlock_sub_norm_le line 207
  23. lemma OAI.WeakPureInfiniteness.fixedSpareDiagonalUnitary_deviation line 234
  24. lemma OAI.WeakPureInfiniteness.fixedSparePermutationUnitary_mul_row line 243
  25. lemma OAI.WeakPureInfiniteness.fixedSparePermutation_conjugate_block line 250
  26. def OAI.WeakPureInfiniteness.fixedSpareReflection line 278
  27. lemma OAI.WeakPureInfiniteness.fixedSpareReflection_sq line 280
  28. lemma OAI.WeakPureInfiniteness.fixedSpareCycle_factor line 286
  29. lemma OAI.WeakPureInfiniteness.exists_fixedSpareCycle_path line 294

    Source documentation

    The cycle of arbitrary equivalent corners, including its uncovered complement, has a path whose bound is independent of the number of corners.

    lemma exists_fixedSpareCycle_path [NeZero N] [Nontrivial E]
    (q : E) (r : ZMod N → E) (hqstar : star q = q) (hqq : q * q = q)
    (hr : ∀ i j, star (r i) * r j = if i = j then q else 0) :
    ∃ p : Path (1 : unitary E)
        (fixedSparePermutationUnitary q r hqstar hqq hr (Equiv.addRight (1 : ZMod N))),
      ∀ a b, ‖(p a : E) - p b‖ ≤ (4 * Real.pi) * |(a : ℝ) - b| := by
…

    Mentions: OAI.WeakPureInfiniteness.fixedSparePermutationUnitary

  30. lemma OAI.WeakPureInfiniteness.exists_controlled_path_of_near_commutator line 319

    Source documentation

    A near-identity finite stabilization gives a path for the original unitary. Only the cycle path contributes to the bound; the diagonal does not.

    lemma exists_controlled_path_of_near_commutator (u d c : unitary E) (L : ℝ)
    (p : Path (1 : unitary E) c)
    (hp : ∀ a b, ‖(p a : E) - p b‖ ≤ L * |(a : ℝ) - b|)
    (hnear : ‖((u * (d * c * star d * star c) : unitary E) : E) - 1‖ < 2) :
    ∃ q : Path (1 : unitary E) u,
      ∀ a b, ‖(q a : E) - q b‖ ≤ (Real.pi + 2 * L) * |(a : ℝ) - b| := by
…