OAI/Analysis/OInfinity/AffineReflectionPath.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

An affine path for each finite reflection

A selfadjoint unitary has an explicit path in its two-dimensional linear span with the unit. Unlike a general short path, this formula preserves commutator control directly. The resulting joint-cycle path has controlled commutators.

  1. def OAI.WeakPureInfiniteness.reflectionPhase line 19
  2. lemma OAI.WeakPureInfiniteness.reflectionPhase_norm line 21
  3. lemma OAI.WeakPureInfiniteness.reflectionPhase_star_mul line 24
  4. lemma OAI.WeakPureInfiniteness.reflectionPhase_sub_norm_le line 28
  5. def OAI.WeakPureInfiniteness.reflectionProjection line 45
  6. lemma OAI.WeakPureInfiniteness.reflectionProjection_star line 47
  7. lemma OAI.WeakPureInfiniteness.reflectionProjection_sq line 51
  8. lemma OAI.WeakPureInfiniteness.projection_phase_product line 57
  9. lemma OAI.WeakPureInfiniteness.projection_phase_mem line 62
  10. def OAI.WeakPureInfiniteness.affineReflection line 78
  11. lemma OAI.WeakPureInfiniteness.affineReflection_mem line 81
  12. lemma OAI.WeakPureInfiniteness.affineReflection_zero line 87
  13. lemma OAI.WeakPureInfiniteness.affineReflection_pi line 91
  14. lemma OAI.WeakPureInfiniteness.affineReflection_continuous line 97
  15. lemma OAI.WeakPureInfiniteness.affineReflection_sub_norm_le line 101
  16. lemma OAI.WeakPureInfiniteness.affineReflection_commutator_bound line 113
  17. def OAI.WeakPureInfiniteness.affineReflectionPath line 131

    Source documentation

    This path has an explicit affine formula and retains every commutator bound of the reflection. Its speed is at most π.

    def affineReflectionPath (h : unitary E) (hh : star (h : E) = h) : Path (1 : unitary E) h where
…
  18. lemma OAI.WeakPureInfiniteness.affineReflectionPath_sub_norm_le line 144
  19. lemma OAI.WeakPureInfiniteness.affineReflectionPath_commutator_bound line 152