OAI/Analysis/BackwardIntertwiners/PolarFactors.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BackwardIntertwiners.coordinateShift line 18
  2. lemma OAI.BackwardIntertwiners.coordinateShift_ae line 20
  3. lemma OAI.BackwardIntertwiners.coordinateShift_zero line 27
  4. lemma OAI.BackwardIntertwiners.coordinateShift_add line 33
  5. lemma OAI.BackwardIntertwiners.coordinateShift_norm_le line 42
  6. lemma OAI.BackwardIntertwiners.coordinateShift_norm line 49
  7. def OAI.BackwardIntertwiners.shiftIsometry line 58
  8. lemma OAI.BackwardIntertwiners.coordinateShift_star line 70
  9. def OAI.BackwardIntertwiners.shiftUnit line 80
  10. lemma OAI.BackwardIntertwiners.shiftUnit_zpow line 85
  11. lemma OAI.BackwardIntertwiners.forward_polar_factor line 91
  12. lemma OAI.BackwardIntertwiners.polarDiagonal_conjugate line 98
  13. def OAI.BackwardIntertwiners.betaRootSymbol line 109
  14. lemma OAI.BackwardIntertwiners.betaRootSymbol_star line 116
  15. lemma OAI.BackwardIntertwiners.betaRootSymbol_sq line 120
  16. lemma OAI.BackwardIntertwiners.polarDiagonal_nonneg line 125
  17. lemma OAI.BackwardIntertwiners.polar_modulus line 141
  18. lemma OAI.BackwardIntertwiners.polarDiagonal_injective line 147
  19. lemma OAI.BackwardIntertwiners.polarDiagonal_denseRange line 155