OAI/Analysis/InterpolatedFactors/CornerRange.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.WeightedFock.oldAnnihilators line 12
  2. theorem OAI.FreeGroupFactorMain.WeightedFock.oldAnnihilators_sandwich line 24
  3. theorem OAI.FreeGroupFactorMain.WeightedFock.kindCreator_annihilator line 33
  4. theorem OAI.FreeGroupFactorMain.WeightedFock.rawReservoir_annihilator line 43
  5. theorem OAI.FreeGroupFactorMain.WeightedFock.cornerAbsorption_annihilator line 49
  6. def OAI.FreeGroupFactorMain.Amplification.cornerEqualityEquiv line 59
  7. theorem OAI.FreeGroupFactorMain.Amplification.cornerEqualityEquiv_val line 64
  8. theorem OAI.FreeGroupFactorMain.Amplification.projectionRange_starProjection line 73
  9. def OAI.FreeGroupFactorMain.Amplification.projectionRepresentation line 76
  10. theorem OAI.FreeGroupFactorMain.Amplification.projectionRepresentation_apply line 80
  11. abbrev OAI.FreeGroupFactorMain.WeightedFock.PRange line 95
  12. instance OAI.FreeGroupFactorMain.WeightedFock.pRange_complete line 96
  13. def OAI.FreeGroupFactorMain.WeightedFock.pRoot line 100
  14. theorem OAI.FreeGroupFactorMain.WeightedFock.pRoot_norm line 102
  15. instance OAI.FreeGroupFactorMain.WeightedFock.pRange_nontrivial line 106
  16. abbrev OAI.FreeGroupFactorMain.WeightedFock.pRepresentation line 113
  17. theorem OAI.FreeGroupFactorMain.WeightedFock.pRepresentation_apply line 116
  18. def OAI.FreeGroupFactorMain.WeightedFock.pProject line 120
  19. theorem OAI.FreeGroupFactorMain.WeightedFock.pProject_val line 122
  20. theorem OAI.FreeGroupFactorMain.WeightedFock.pProject_coe line 126
  21. theorem OAI.FreeGroupFactorMain.WeightedFock.pRange_total line 129
  22. def OAI.FreeGroupFactorMain.WeightedFock.oldBaseCorner line 147
  23. def OAI.FreeGroupFactorMain.WeightedFock.oldBaseOp line 150
  24. theorem OAI.FreeGroupFactorMain.WeightedFock.oldBaseCorner_selfAdjoint line 152
  25. theorem OAI.FreeGroupFactorMain.WeightedFock.oldBaseOp_selfAdjoint line 155
  26. theorem OAI.FreeGroupFactorMain.WeightedFock.oldBaseOp_eigen_root_zero line 161
  27. def OAI.FreeGroupFactorMain.WeightedFock.pSandwich line 173
  28. theorem OAI.FreeGroupFactorMain.WeightedFock.pSandwich_commute line 179
  29. theorem OAI.FreeGroupFactorMain.WeightedFock.pRoot_vacuum line 191
  30. theorem OAI.FreeGroupFactorMain.WeightedFock.pSandwich_basis line 194
  31. theorem OAI.FreeGroupFactorMain.WeightedFock.centralizer_bicommutant line 207
  32. theorem OAI.FreeGroupFactorMain.WeightedFock.oldBaseOp_commutant_total line 215