OAI/Analysis/InterpolatedFactors/Diagonal.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.WeightedFock.annihilation_commute_diagonalInsert line 15
  2. theorem OAI.FreeGroupFactorMain.WeightedFock.Cstar_commute_diagonalInsert line 26
  3. theorem OAI.FreeGroupFactorMain.WeightedFock.fresh_C_edge_root line 32
  4. theorem OAI.FreeGroupFactorMain.WeightedFock.fresh_C_diagonal_edge line 40
  5. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonal_weightedDefect line 56
  6. theorem OAI.FreeGroupFactorMain.WeightedFock.weightedDefect_edge_root line 68
  7. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonal_filled_contraction line 78
  8. theorem OAI.FreeGroupFactorMain.WeightedFock.diagonal_filled_annihilation line 98
  9. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_trace_inner line 113
  10. theorem OAI.FreeGroupFactorMain.WeightedFock.supportedLeg_vertex line 123
  11. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_star_supportedLeg line 129
  12. theorem OAI.FreeGroupFactorMain.WeightedFock.supportedLeg_root_trace line 133
  13. def OAI.FreeGroupFactorMain.WeightedFock.transportedDiagonal line 142
  14. def OAI.FreeGroupFactorMain.WeightedFock.normalizedDiagonal line 145
  15. theorem OAI.FreeGroupFactorMain.WeightedFock.transportedDiagonal_filled_contraction line 148
  16. theorem OAI.FreeGroupFactorMain.WeightedFock.normalizedDiagonal_filled_covariance line 175