OAI/Analysis/InterpolatedFactors/RelativeClosure.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.Amplification.compress_mul_corner line 12
  2. theorem OAI.FreeGroupFactorMain.Amplification.corner_mul_compress line 16
  3. theorem OAI.FreeGroupFactorMain.Amplification.relative_corner_bicommutant line 23
  4. def OAI.FreeGroupFactorMain.FreeFock.creationWord line 68
  5. theorem OAI.FreeGroupFactorMain.FreeFock.creationWord_nil line 72
  6. theorem OAI.FreeGroupFactorMain.FreeFock.creationWord_cons line 73
  7. theorem OAI.FreeGroupFactorMain.FreeFock.creationWord_append line 76
  8. theorem OAI.FreeGroupFactorMain.FreeFock.creationWord_vacuum line 82
  9. theorem OAI.FreeGroupFactorMain.FreeFock.creationWord_star_vacuum line 89
  10. def OAI.FreeGroupFactorMain.FreeFock.wick line 98
  11. theorem OAI.FreeGroupFactorMain.FreeFock.wick_nil line 101
  12. theorem OAI.FreeGroupFactorMain.FreeFock.wick_star line 103
  13. theorem OAI.FreeGroupFactorMain.FreeFock.wick_vacuum line 119
  14. theorem OAI.FreeGroupFactorMain.FreeFock.wick_creation_formula line 141
  15. theorem OAI.FreeGroupFactorMain.FreeFock.wick_semicircular_cons line 154
  16. def OAI.FreeGroupFactorMain.FreeFock.runSpan line 177
  17. def OAI.FreeGroupFactorMain.FreeFock.positiveRunSpan line 180
  18. theorem OAI.FreeGroupFactorMain.FreeFock.run_mem line 183
  19. theorem OAI.FreeGroupFactorMain.FreeFock.semicircular_mul_runSpan line 186
  20. theorem OAI.FreeGroupFactorMain.FreeFock.run_mul_runSpan line 204
  21. def OAI.FreeGroupFactorMain.FreeFock.runAlgebra line 223
  22. theorem OAI.FreeGroupFactorMain.FreeFock.vacuumTrace_linear line 250
  23. theorem OAI.FreeGroupFactorMain.FreeFock.vacuumTrace_continuous line 254
  24. theorem OAI.FreeGroupFactorMain.FreeFock.vacuumTrace_run line 257
  25. theorem OAI.FreeGroupFactorMain.FreeFock.run_star_creation line 269
  26. theorem OAI.FreeGroupFactorMain.FreeFock.run_creation line 273
  27. theorem OAI.FreeGroupFactorMain.FreeFock.run_coarse_covariance line 288
  28. theorem OAI.FreeGroupFactorMain.FreeFock.polynomial_coarse_covariance line 299
  29. theorem OAI.FreeGroupFactorMain.FreeFock.closed_coarse_covariance line 311
  30. theorem OAI.FreeGroupFactorMain.FreeFock.closed_coefficient_annihilation line 318