OAI/Analysis/BackwardIntertwiners/AtomicAlgebras.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BackwardIntertwiners.MinimalProjection line 22
  2. def OAI.BackwardIntertwiners.AtomicAlgebra line 26
  3. def OAI.BackwardIntertwiners.DiffuseAlgebra line 32
  4. lemma OAI.BackwardIntertwiners.selfAdjoint_commutes_rankOne line 35
  5. lemma OAI.BackwardIntertwiners.projection_reverse_mul line 45
  6. lemma OAI.BackwardIntertwiners.eigenspace_projection_minimal line 51
  7. def OAI.BackwardIntertwiners.halfExponentIndex line 95
  8. lemma OAI.BackwardIntertwiners.halfExponentIndex_cast line 97
  9. def OAI.BackwardIntertwiners.exponentIndex line 102
  10. lemma OAI.BackwardIntertwiners.exponentIndex_cast line 105
  11. lemma OAI.BackwardIntertwiners.explicitBeta_exponentIndex line 107
  12. lemma OAI.BackwardIntertwiners.exp_neg_int_injective line 111
  13. def OAI.BackwardIntertwiners.jointLevel line 117
  14. lemma OAI.BackwardIntertwiners.jointLevel_eq_iInter line 119
  15. lemma OAI.BackwardIntertwiners.jointLevel_measurable line 123
  16. lemma OAI.BackwardIntertwiners.jointLevel_partition line 126
  17. def OAI.BackwardIntertwiners.jointProjection line 132
  18. def OAI.BackwardIntertwiners.finitePolarAlgebra line 134
  19. lemma OAI.BackwardIntertwiners.finitePolarAlgebra_mem line 136
  20. lemma OAI.BackwardIntertwiners.DiagonalSymbol.prod_apply line 138
  21. lemma OAI.BackwardIntertwiners.diagonalRepresentation_prod_mem line 143
  22. lemma OAI.BackwardIntertwiners.projectionSymbol_prod line 151
  23. lemma OAI.BackwardIntertwiners.jointProjection_mem line 159
  24. lemma OAI.BackwardIntertwiners.jointProjection_isStarProjection line 171
  25. lemma OAI.BackwardIntertwiners.jointProjection_eigen line 173
  26. lemma OAI.BackwardIntertwiners.jointProjection_orthogonal line 186
  27. lemma OAI.BackwardIntertwiners.jointProjection_minimal line 196
  28. lemma OAI.BackwardIntertwiners.partitionProjection_hasSum line 209
  29. lemma OAI.BackwardIntertwiners.jointProjection_hasSum line 241
  30. theorem OAI.BackwardIntertwiners.finitePolarAlgebra_atomic line 245
  31. lemma OAI.BackwardIntertwiners.minimal_projection_dichotomy line 259
  32. lemma OAI.BackwardIntertwiners.rectangleProjection_coord line 273
  33. theorem OAI.BackwardIntertwiners.polarAlgebra_diffuse line 284
  34. def OAI.BackwardIntertwiners.PurePointResolution line 361
  35. lemma OAI.BackwardIntertwiners.polarDiagonal_purePoint line 366
  36. lemma OAI.BackwardIntertwiners.polarDiagonal_constantBasis_zero line 385
  37. lemma OAI.BackwardIntertwiners.polarDiagonal_not_commute line 396