OAI/Analysis/InterpolatedFactors/ScalarGeneration.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.FreeFock.appendEmbedding line 15
  2. def OAI.FreeGroupFactorMain.FreeFock.rightCreation line 18
  3. theorem OAI.FreeGroupFactorMain.FreeFock.rightCreation_single line 21
  4. theorem OAI.FreeGroupFactorMain.FreeFock.creation_rightCreation line 25
  5. def OAI.FreeGroupFactorMain.FreeFock.vacuumProjection line 31
  6. theorem OAI.FreeGroupFactorMain.FreeFock.vacuumProjection_nil line 33
  7. theorem OAI.FreeGroupFactorMain.FreeFock.vacuumProjection_cons line 40
  8. theorem OAI.FreeGroupFactorMain.FreeFock.annihilation_rightCreation line 44
  9. theorem OAI.FreeGroupFactorMain.FreeFock.vacuumProjection_selfAdjoint line 64
  10. theorem OAI.FreeGroupFactorMain.FreeFock.creation_rightAnnihilation line 67
  11. def OAI.FreeGroupFactorMain.FreeFock.rightSemicircular line 78
  12. theorem OAI.FreeGroupFactorMain.FreeFock.semicircular_rightSemicircular line 80
  13. def OAI.FreeGroupFactorMain.FreeFock.reverseEmbedding line 96
  14. def OAI.FreeGroupFactorMain.FreeFock.reverseIsometry line 97
  15. def OAI.FreeGroupFactorMain.FreeFock.reverseOperator line 98
  16. theorem OAI.FreeGroupFactorMain.FreeFock.reverseOperator_single line 100
  17. theorem OAI.FreeGroupFactorMain.FreeFock.reverseOperator_square line 104
  18. theorem OAI.FreeGroupFactorMain.FreeFock.reverseOperator_involutive line 109
  19. def OAI.FreeGroupFactorMain.FreeFock.reverseEquiv line 114
  20. theorem OAI.FreeGroupFactorMain.FreeFock.reverseEquiv_apply line 118
  21. theorem OAI.FreeGroupFactorMain.FreeFock.reverseEquiv_symm_apply line 119
  22. theorem OAI.FreeGroupFactorMain.FreeFock.reverse_conj_creation line 123
  23. theorem OAI.FreeGroupFactorMain.FreeFock.reverse_conj_semicircular line 131
  24. theorem OAI.FreeGroupFactorMain.FreeFock.wick_mem_any line 135
  25. def OAI.FreeGroupFactorMain.FreeFock.gaussianCommutant line 154
  26. def OAI.FreeGroupFactorMain.FreeFock.gaussianAlgebra line 157
  27. theorem OAI.FreeGroupFactorMain.FreeFock.rightSemicircular_mem line 160
  28. def OAI.FreeGroupFactorMain.FreeFock.rightWick line 168
  29. theorem OAI.FreeGroupFactorMain.FreeFock.rightWick_mem line 170
  30. theorem OAI.FreeGroupFactorMain.FreeFock.rightWick_vacuum line 177
  31. theorem OAI.FreeGroupFactorMain.FreeFock.rightWick_star line 183
  32. theorem OAI.FreeGroupFactorMain.FreeFock.gaussian_commute_rightWick line 186
  33. theorem OAI.FreeGroupFactorMain.FreeFock.gaussian_separating line 190
  34. theorem OAI.FreeGroupFactorMain.FreeFock.gaussian_star_vector line 199
  35. theorem OAI.FreeGroupFactorMain.FreeFock.gaussian_trace_mul line 216
  36. theorem OAI.FreeGroupFactorMain.FreeFock.fock_closed_total line 241
  37. theorem OAI.FreeGroupFactorMain.FreeFock.gaussian_commutant_total line 255
  38. theorem OAI.FreeGroupFactorMain.FreeFock.semicircular_mem_uniform_bicommutant line 269
  39. def OAI.FreeGroupFactorMain.FreeFock.scalarFlip line 286
  40. theorem OAI.FreeGroupFactorMain.FreeFock.scalarCoeff_mem_gaussian line 288
  41. theorem OAI.FreeGroupFactorMain.FreeFock.scalarGenerator_mem_gaussian line 295
  42. theorem OAI.FreeGroupFactorMain.FreeFock.scalar_semicircular_mem_generated line 301
  43. theorem OAI.FreeGroupFactorMain.FreeFock.scalar_generated_eq_gaussian line 312
  44. theorem OAI.FreeGroupFactorMain.FreeFock.scalarSystem_total line 322
  45. theorem OAI.FreeGroupFactorMain.WeightedFock.pRep_add line 338
  46. theorem OAI.FreeGroupFactorMain.WeightedFock.pRep_star line 341
  47. def OAI.FreeGroupFactorMain.WeightedFock.representedAmbient line 344
  48. theorem OAI.FreeGroupFactorMain.WeightedFock.pFilled_le_pAmbient line 347
  49. theorem OAI.FreeGroupFactorMain.WeightedFock.kindPair_mem_pAmbient line 350
  50. theorem OAI.FreeGroupFactorMain.WeightedFock.outputPair_mem_pAmbient line 360
  51. theorem OAI.FreeGroupFactorMain.WeightedFock.representedAmbient_saturated line 374
  52. theorem OAI.FreeGroupFactorMain.WeightedFock.weighted_generated_le_ambient line 394
  53. theorem OAI.FreeGroupFactorMain.WeightedFock.representedAmbient_le_weightedGenerated line 405
  54. theorem OAI.FreeGroupFactorMain.WeightedFock.weighted_generated_eq_ambient line 431