OAI/Analysis/InterpolatedFactors/AmbientSystem.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.WeightedFock.vacuum_norm_one line 15
  2. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalGenerator_noAtoms line 24
  3. def OAI.FreeGroupFactorMain.WeightedFock.ambientUniform line 41
  4. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientUniform_mem line 46
  5. def OAI.FreeGroupFactorMain.WeightedFock.ambientUniformBase line 51
  6. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientUniform_state line 54
  7. def OAI.FreeGroupFactorMain.WeightedFock.diagonalAnnihilators line 64
  8. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalAnnihilators_sandwich line 70
  9. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientExtra_annihilator line 78
  10. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientRaw_annihilator line 85
  11. def OAI.FreeGroupFactorMain.WeightedFock.ambientCreation line 92
  12. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientCreation_annihilator line 94
  13. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientCreation_covariance line 98
  14. def OAI.FreeGroupFactorMain.WeightedFock.ambientSystem line 109
  15. theorem OAI.FreeGroupFactorMain.WeightedFock.path_closed_total line 127
  16. theorem OAI.FreeGroupFactorMain.WeightedFock.ambient_commutant_total line 141
  17. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalGenerator_mem_uniform line 155
  18. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalBase_le_uniform line 171
  19. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientExtra_pair_mem line 183
  20. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientOutput_pair_mem line 197
  21. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientSystem_le_ambient line 205
  22. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonalBase_le_system line 211
  23. theorem OAI.FreeGroupFactorMain.WeightedFock.ambient_generator_decomposition line 215
  24. theorem OAI.FreeGroupFactorMain.WeightedFock.ambient_le_ambientSystem line 227
  25. theorem OAI.FreeGroupFactorMain.WeightedFock.ambient_generated_eq line 250
  26. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientSystem_total line 253
  27. theorem OAI.FreeGroupFactorMain.WeightedFock.scalar_ambient_state line 266
  28. def OAI.FreeGroupFactorMain.WeightedFock.ambientGaussianIso line 272
  29. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientGaussianIso_normal line 278
  30. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientGaussianIso_trace line 285