OAI/Analysis/InterpolatedFactors/CornerGeneration.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.CornerRerouting.filled_edge_corner_generated line 13
  2. theorem OAI.FreeGroupFactorMain.WeightedFock.weightedDefect_semicircle_eq line 90
  3. theorem OAI.FreeGroupFactorMain.WeightedFock.filled_corner_mem_diffuseBase line 96
  4. theorem OAI.FreeGroupFactorMain.WeightedFock.pRepresentation_mem_bicommutant line 131
  5. theorem OAI.FreeGroupFactorMain.WeightedFock.representedBase_le_oldBase line 165
  6. theorem OAI.FreeGroupFactorMain.WeightedFock.oldBaseOp_mem_weightedUniform line 174
  7. theorem OAI.FreeGroupFactorMain.WeightedFock.representedBase_le_weightedUniform line 190
  8. theorem OAI.FreeGroupFactorMain.WeightedFock.absorbed_kind_recovery line 203
  9. theorem OAI.FreeGroupFactorMain.WeightedFock.absorbed_raw_recovery line 216
  10. theorem OAI.FreeGroupFactorMain.WeightedFock.absorbed_fresh_recovery line 227
  11. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_C_vertex line 239
  12. theorem OAI.FreeGroupFactorMain.WeightedFock.pDiagonal_eq_pFresh line 248
  13. def OAI.FreeGroupFactorMain.WeightedFock.blockCorner line 271
  14. theorem OAI.FreeGroupFactorMain.WeightedFock.blockCorner_normalized line 275
  15. def OAI.FreeGroupFactorMain.WeightedFock.residualBlockCorner line 284
  16. theorem OAI.FreeGroupFactorMain.WeightedFock.residualBlockCorner_normalized line 288
  17. theorem OAI.FreeGroupFactorMain.WeightedFock.blockCorner_zero_off line 298
  18. theorem OAI.FreeGroupFactorMain.WeightedFock.blockCorner_star line 306
  19. theorem OAI.FreeGroupFactorMain.WeightedFock.old_off_block_mem line 320
  20. theorem OAI.FreeGroupFactorMain.WeightedFock.absorbed_old_block_recovery line 328
  21. theorem OAI.FreeGroupFactorMain.WeightedFock.absorbed_residual_block_recovery line 340
  22. theorem OAI.FreeGroupFactorMain.WeightedFock.blockCorner_split_false_false line 353
  23. theorem OAI.FreeGroupFactorMain.WeightedFock.blockCorner_split_false_true line 363
  24. theorem OAI.FreeGroupFactorMain.WeightedFock.blockCorner_split_true_false line 372
  25. theorem OAI.FreeGroupFactorMain.WeightedFock.absorbed_filled_block_recovery line 381
  26. theorem OAI.FreeGroupFactorMain.WeightedFock.absorbed_block_recovery line 391
  27. theorem OAI.FreeGroupFactorMain.WeightedFock.full_corner_commutant line 402
  28. def OAI.FreeGroupFactorMain.WeightedFock.pAmbient line 415
  29. theorem OAI.FreeGroupFactorMain.WeightedFock.blockCorner_diagonal line 418
  30. theorem OAI.FreeGroupFactorMain.WeightedFock.blockCorner_off line 423
  31. theorem OAI.FreeGroupFactorMain.WeightedFock.blockCorner_remaining line 431
  32. theorem OAI.FreeGroupFactorMain.WeightedFock.pAmbient_recovered line 442