OAI/Analysis/BackwardIntertwiners/SpectralProjections.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BackwardIntertwiners.polarAlgebra line 19
  2. lemma OAI.BackwardIntertwiners.polarDiagonal_mem line 20
  3. lemma OAI.BackwardIntertwiners.polarAlgebra_closed line 21
  4. lemma OAI.BackwardIntertwiners.polarAlgebra_le_full line 22
  5. lemma OAI.BackwardIntertwiners.polarAlgebra_commutative line 26
  6. lemma OAI.BackwardIntertwiners.halfExponent_eq_ten_iff line 30
  7. lemma OAI.BackwardIntertwiners.explicitBeta_central line 39
  8. lemma OAI.BackwardIntertwiners.sliceProjection_central line 52
  9. lemma OAI.BackwardIntertwiners.sliceProjection_mem_polar line 63
  10. def OAI.BackwardIntertwiners.rectangleProjection line 70
  11. lemma OAI.BackwardIntertwiners.rectangleProjection_univ line 72
  12. lemma OAI.BackwardIntertwiners.rectangleProjection_empty line 74
  13. lemma OAI.BackwardIntertwiners.rectangleProjection_ext line 79
  14. lemma OAI.BackwardIntertwiners.rectangleProjection_mul line 86
  15. lemma OAI.BackwardIntertwiners.rectangleProjection_compl line 93
  16. lemma OAI.BackwardIntertwiners.rectangleProjection_union line 103
  17. def OAI.BackwardIntertwiners.blockAnchor line 114
  18. lemma OAI.BackwardIntertwiners.blockAnchor_ne_zero line 115
  19. lemma OAI.BackwardIntertwiners.blockAnchor_block line 116
  20. def OAI.BackwardIntertwiners.residueEigenvalue line 119
  21. lemma OAI.BackwardIntertwiners.beta_anchor_residue line 121
  22. lemma OAI.BackwardIntertwiners.residue_rectangle_spectral line 134
  23. lemma OAI.BackwardIntertwiners.residue_rectangle_mem line 151
  24. lemma OAI.BackwardIntertwiners.borel_le_of_residue_measurable line 171
  25. lemma OAI.BackwardIntertwiners.rectangleProjection_finiteUnion_mem line 192
  26. lemma OAI.BackwardIntertwiners.rectangleProjection_iUnion_mem line 211
  27. def OAI.BackwardIntertwiners.polarProjectionMeasurableSpace line 242
  28. lemma OAI.BackwardIntertwiners.rectangleProjection_borel_mem line 254
  29. lemma OAI.BackwardIntertwiners.rectangleProjection_mem line 261
  30. lemma OAI.BackwardIntertwiners.DiagonalSymbol.sum_apply line 267
  31. def OAI.BackwardIntertwiners.simpleSliceSymbol line 274
  32. lemma OAI.BackwardIntertwiners.simpleSliceSymbol_apply line 278
  33. lemma OAI.BackwardIntertwiners.simpleSliceSymbol_mem line 289
  34. def OAI.BackwardIntertwiners.sliceSymbol line 297
  35. lemma OAI.BackwardIntertwiners.sliceSymbol_apply line 299
  36. lemma OAI.BackwardIntertwiners.sliceSymbol_norm_le line 302
  37. lemma OAI.BackwardIntertwiners.sliceSymbol_mem line 308
  38. lemma OAI.BackwardIntertwiners.finiteSliceSymbol_apply line 331
  39. lemma OAI.BackwardIntertwiners.diagonalOperator_mem_polar line 336
  40. theorem OAI.BackwardIntertwiners.polarAlgebra_eq_fullMultiplier line 360