OAI/Analysis/BackwardIntertwiners/PolarDiagonals.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BackwardIntertwiners.betaSymbol line 19
  2. lemma OAI.BackwardIntertwiners.betaSymbol_apply line 24
  3. lemma OAI.BackwardIntertwiners.betaSymbol_star line 26
  4. def OAI.BackwardIntertwiners.polarDiagonal line 31
  5. lemma OAI.BackwardIntertwiners.polarDiagonal_ae line 32
  6. lemma OAI.BackwardIntertwiners.polarDiagonal_selfAdjoint line 35
  7. lemma OAI.BackwardIntertwiners.polarDiagonal_commute line 38
  8. def OAI.BackwardIntertwiners.projectionSymbol line 44
  9. lemma OAI.BackwardIntertwiners.projectionSymbol_apply line 48
  10. lemma OAI.BackwardIntertwiners.projectionSymbol_norm_le line 50
  11. lemma OAI.BackwardIntertwiners.projectionSymbol_star line 53
  12. lemma OAI.BackwardIntertwiners.projectionSymbol_idempotent line 59
  13. def OAI.BackwardIntertwiners.diagonalProjection line 66
  14. lemma OAI.BackwardIntertwiners.diagonalProjection_ae line 68
  15. lemma OAI.BackwardIntertwiners.diagonalProjection_isStarProjection line 74
  16. lemma OAI.BackwardIntertwiners.diagonalProjection_mul line 82
  17. lemma OAI.BackwardIntertwiners.diagonalProjection_compl line 93
  18. lemma OAI.BackwardIntertwiners.diagonalProjection_empty line 102
  19. lemma OAI.BackwardIntertwiners.diagonalProjection_univ line 106
  20. lemma OAI.BackwardIntertwiners.diagonalProjection_ext line 110
  21. lemma OAI.BackwardIntertwiners.diagonalProjection_nonzero line 121
  22. lemma OAI.BackwardIntertwiners.explicitBeta_le_one line 136
  23. def OAI.BackwardIntertwiners.levelProjection line 139
  24. lemma OAI.BackwardIntertwiners.peak_nonneg line 143
  25. lemma OAI.BackwardIntertwiners.peak_le_one line 147
  26. lemma OAI.BackwardIntertwiners.peak_lt_one line 148
  27. def OAI.BackwardIntertwiners.peakSymbol line 152
  28. lemma OAI.BackwardIntertwiners.peakSymbol_apply line 153
  29. lemma OAI.BackwardIntertwiners.peakSymbol_bound line 156
  30. lemma OAI.BackwardIntertwiners.peakSymbol_powers_tendsto line 161
  31. lemma OAI.BackwardIntertwiners.levelProjection_mem line 173
  32. def OAI.BackwardIntertwiners.baseProjection line 196
  33. lemma OAI.BackwardIntertwiners.baseProjection_ae line 198
  34. lemma OAI.BackwardIntertwiners.baseProjection_mem_full line 203
  35. lemma OAI.BackwardIntertwiners.diagonal_commute line 205
  36. lemma OAI.BackwardIntertwiners.fullMultiplier_commute line 208
  37. lemma OAI.BackwardIntertwiners.baseProjection_constant line 213
  38. lemma OAI.BackwardIntertwiners.L2_norm_sq line 221
  39. lemma OAI.BackwardIntertwiners.baseProjection_norm_sq line 223
  40. lemma OAI.BackwardIntertwiners.local_operator_energy_bound line 230
  41. lemma OAI.BackwardIntertwiners.sliceProjection_diagonal line 242
  42. lemma OAI.BackwardIntertwiners.sliceProjection_mem_full line 252
  43. def OAI.BackwardIntertwiners.columnSymbol line 257
  44. lemma OAI.BackwardIntertwiners.columnSymbol_ae line 265
  45. lemma OAI.BackwardIntertwiners.columnSymbol_basis line 276
  46. lemma OAI.BackwardIntertwiners.operators_equal_of_constantBasis line 293
  47. lemma OAI.BackwardIntertwiners.fullMultiplier_centralizer_eq line 320
  48. lemma OAI.BackwardIntertwiners.fullMultiplier_stronglyClosed line 337
  49. lemma OAI.BackwardIntertwiners.levelProjection_mem_all line 341