OAI/Analysis/InterpolatedFactors/Ultraweak.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.HilbertUltraweak.topology line 12
  2. def OAI.FreeGroupFactorMain.HilbertUltraweak.sequenceMap line 17
  3. theorem OAI.FreeGroupFactorMain.HilbertUltraweak.functional_continuous line 21
  4. theorem OAI.FreeGroupFactorMain.HilbertUltraweak.sandwich_continuous line 25
  5. theorem OAI.FreeGroupFactorMain.HilbertUltraweak.spatial_continuous line 43
  6. theorem OAI.FreeGroupFactorMain.HilbertUltraweak.add_continuous line 48
  7. theorem OAI.FreeGroupFactorMain.CornerRerouting.lift_commute_four line 71
  8. def OAI.FreeGroupFactorMain.FullReducingCorner.bicomm line 100
  9. def OAI.FreeGroupFactorMain.FullReducingCorner.compress line 103
  10. theorem OAI.FreeGroupFactorMain.FullReducingCorner.compress_star line 106
  11. def OAI.FreeGroupFactorMain.FullReducingCorner.compressedSet line 112
  12. theorem OAI.FreeGroupFactorMain.FullReducingCorner.supported_commutant line 117
  13. theorem OAI.FreeGroupFactorMain.FullReducingCorner.commutant_of_supported line 135
  14. theorem OAI.FreeGroupFactorMain.FullReducingCorner.compress_mem line 165
  15. theorem OAI.FreeGroupFactorMain.FullReducingCorner.lift_mem line 181
  16. theorem OAI.FreeGroupFactorMain.FullReducingCorner.lift_compress line 208
  17. theorem OAI.FreeGroupFactorMain.FullReducingCorner.compress_lift line 216
  18. def OAI.FreeGroupFactorMain.FullReducingCorner.iso line 222
  19. def OAI.FreeGroupFactorMain.ReducingSubspace.reduce line 255
  20. theorem OAI.FreeGroupFactorMain.ReducingSubspace.reduce_apply line 258
  21. theorem OAI.FreeGroupFactorMain.ReducingSubspace.reduce_one line 261
  22. theorem OAI.FreeGroupFactorMain.ReducingSubspace.reduce_add line 266
  23. theorem OAI.FreeGroupFactorMain.ReducingSubspace.reduce_smul line 271
  24. theorem OAI.FreeGroupFactorMain.ReducingSubspace.inner_reduce line 276
  25. theorem OAI.FreeGroupFactorMain.ReducingSubspace.reduce_star line 282
  26. theorem OAI.FreeGroupFactorMain.ReducingSubspace.reduce_mul line 292
  27. def OAI.FreeGroupFactorMain.GaussianRecognition.System.reducedCoeff line 306
  28. def OAI.FreeGroupFactorMain.GaussianRecognition.System.reducedSystem line 316
  29. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.reducedSystem_normal line 331
  30. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.reducedSystem_family line 343
  31. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.reducedSystem_state line 346
  32. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.reducedSystem_total line 350
  33. theorem OAI.FreeGroupFactorMain.WeightedFock.reduced_weighted_scalar_state line 369
  34. def OAI.FreeGroupFactorMain.WeightedFock.reducedGaussianIso line 376
  35. theorem OAI.FreeGroupFactorMain.WeightedFock.reducedGaussianIso_normal line 383
  36. theorem OAI.FreeGroupFactorMain.WeightedFock.reducedGaussianIso_trace line 390