OAI/Analysis/InterpolatedFactors/Fresh.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.WeightedFock.P_mem_old line 15
  2. theorem OAI.FreeGroupFactorMain.WeightedFock.S_mem_old line 18
  3. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_mem_old line 21
  4. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeAlgebra_le_old line 27
  5. def OAI.FreeGroupFactorMain.WeightedFock.weightedDefectCreation line 36
  6. def OAI.FreeGroupFactorMain.WeightedFock.defectCovariance line 39
  7. theorem OAI.FreeGroupFactorMain.WeightedFock.weightedDefect_contraction line 43
  8. theorem OAI.FreeGroupFactorMain.WeightedFock.weightedDefect_annihilates_edge line 61
  9. theorem OAI.FreeGroupFactorMain.WeightedFock.fresh_C_weightedDefect line 71
  10. def OAI.FreeGroupFactorMain.WeightedFock.filledEdgeAlgebra line 85
  11. theorem OAI.FreeGroupFactorMain.WeightedFock.fresh_C_filled_contraction line 89
  12. theorem OAI.FreeGroupFactorMain.WeightedFock.fresh_C_filled_annihilation line 110
  13. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeAlgebra_le_ambient line 124
  14. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeAlgebra_le_filled line 132
  15. theorem OAI.FreeGroupFactorMain.WeightedFock.weightedDefect_semicircle_mem_filled line 135
  16. theorem OAI.FreeGroupFactorMain.WeightedFock.filledEdgeAlgebra_le_ambient line 139
  17. theorem OAI.FreeGroupFactorMain.WeightedFock.weightedDefectCreation_eq line 151
  18. theorem OAI.FreeGroupFactorMain.WeightedFock.defectSemicircle_mem_filled line 162
  19. theorem OAI.FreeGroupFactorMain.WeightedFock.diffuseBase_le_filled line 172
  20. theorem OAI.FreeGroupFactorMain.WeightedFock.edgePolar_mul_P line 191
  21. theorem OAI.FreeGroupFactorMain.WeightedFock.P_mul_star_edgePolar line 194
  22. def OAI.FreeGroupFactorMain.WeightedFock.supportedLeg line 197
  23. def OAI.FreeGroupFactorMain.WeightedFock.legSupport line 200
  24. theorem OAI.FreeGroupFactorMain.WeightedFock.supportedLeg_mem_edge line 203
  25. theorem OAI.FreeGroupFactorMain.WeightedFock.supportedLeg_mem_ambient line 209
  26. theorem OAI.FreeGroupFactorMain.WeightedFock.supportedLeg_mul_star line 213
  27. theorem OAI.FreeGroupFactorMain.WeightedFock.supportedLeg_trace_covariance line 221
  28. def OAI.FreeGroupFactorMain.WeightedFock.supportedCreation line 236
  29. theorem OAI.FreeGroupFactorMain.WeightedFock.supportedCreation_filled_covariance line 239
  30. theorem OAI.FreeGroupFactorMain.WeightedFock.supportedCreation_filled_annihilation line 267
  31. def OAI.FreeGroupFactorMain.WeightedFock.pVacuumTrace line 279
  32. def OAI.FreeGroupFactorMain.WeightedFock.normalizedCreation line 281
  33. theorem OAI.FreeGroupFactorMain.WeightedFock.normalizedCreation_filled_covariance line 284
  34. theorem OAI.FreeGroupFactorMain.WeightedFock.supportedCreation_paired line 295
  35. theorem OAI.FreeGroupFactorMain.WeightedFock.normalizedCreation_paired_mem line 300