OAI/Analysis/InterpolatedFactors/Splitting.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.GaussianSplit.cut line 16
  2. theorem OAI.FreeGroupFactorMain.GaussianSplit.cut_star line 19
  3. theorem OAI.FreeGroupFactorMain.GaussianSplit.cut_d line 23
  4. theorem OAI.FreeGroupFactorMain.GaussianSplit.cut_false_a_d line 27
  5. def OAI.FreeGroupFactorMain.GaussianSplit.block line 31
  6. def OAI.FreeGroupFactorMain.GaussianSplit.D line 33
  7. def OAI.FreeGroupFactorMain.GaussianSplit.covariance line 35
  8. theorem OAI.FreeGroupFactorMain.GaussianSplit.D_contraction line 38
  9. theorem OAI.FreeGroupFactorMain.GaussianSplit.D_annihilation line 50
  10. theorem OAI.FreeGroupFactorMain.GaussianSplit.block_contraction line 58
  11. theorem OAI.FreeGroupFactorMain.GaussianSplit.block_annihilation line 80
  12. theorem OAI.FreeGroupFactorMain.GaussianSplit.block_D line 89
  13. def OAI.FreeGroupFactorMain.GaussianSplit.filled line 113
  14. theorem OAI.FreeGroupFactorMain.GaussianSplit.residual_covariance line 119
  15. theorem OAI.FreeGroupFactorMain.GaussianSplit.residual_annihilation line 137
  16. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeDefect_commute line 151
  17. def OAI.FreeGroupFactorMain.WeightedFock.defectAsEdge line 162
  18. theorem OAI.FreeGroupFactorMain.WeightedFock.defectAsEdge_projection line 165
  19. theorem OAI.FreeGroupFactorMain.WeightedFock.defectAsEdge_central line 172
  20. theorem OAI.FreeGroupFactorMain.WeightedFock.fresh_C_edge_contraction line 175
  21. theorem OAI.FreeGroupFactorMain.WeightedFock.fresh_C_edge_annihilation line 182
  22. def OAI.FreeGroupFactorMain.WeightedFock.splitCut line 187
  23. def OAI.FreeGroupFactorMain.WeightedFock.splitBlock line 190
  24. theorem OAI.FreeGroupFactorMain.WeightedFock.splitBlock_filled_covariance line 193
  25. theorem OAI.FreeGroupFactorMain.WeightedFock.splitBlock_filled_annihilation line 205
  26. theorem OAI.FreeGroupFactorMain.WeightedFock.splitCut_mem_edge line 213
  27. theorem OAI.FreeGroupFactorMain.WeightedFock.splitCut_selfAdjoint line 216
  28. def OAI.FreeGroupFactorMain.WeightedFock.splitPair line 220
  29. theorem OAI.FreeGroupFactorMain.WeightedFock.splitPair_eq line 223
  30. theorem OAI.FreeGroupFactorMain.WeightedFock.splitPair_mem_ambient line 230
  31. theorem OAI.FreeGroupFactorMain.WeightedFock.splitPair_reconstruct line 236
  32. def OAI.FreeGroupFactorMain.WeightedFock.residualLeg line 252
  33. def OAI.FreeGroupFactorMain.WeightedFock.residualSupport line 257
  34. def OAI.FreeGroupFactorMain.WeightedFock.residualCut line 261
  35. theorem OAI.FreeGroupFactorMain.WeightedFock.residualLeg_mem_edge line 265
  36. theorem OAI.FreeGroupFactorMain.WeightedFock.P_mul_residualLeg line 273
  37. theorem OAI.FreeGroupFactorMain.WeightedFock.edgePolar_mul_defect line 281
  38. theorem OAI.FreeGroupFactorMain.WeightedFock.edgePolar_mul_range line 284
  39. theorem OAI.FreeGroupFactorMain.WeightedFock.defect_mul_star_edgePolar line 287
  40. theorem OAI.FreeGroupFactorMain.WeightedFock.range_mul_star_edgePolar line 292
  41. theorem OAI.FreeGroupFactorMain.WeightedFock.residualLeg_mul_star line 297
  42. theorem OAI.FreeGroupFactorMain.WeightedFock.residualLeg_cut line 315
  43. theorem OAI.FreeGroupFactorMain.WeightedFock.cut_star_residualLeg line 324
  44. theorem OAI.FreeGroupFactorMain.WeightedFock.residualLeg_trace_covariance line 329
  45. def OAI.FreeGroupFactorMain.WeightedFock.residualCreation line 343
  46. theorem OAI.FreeGroupFactorMain.WeightedFock.residualCreation_split line 346
  47. theorem OAI.FreeGroupFactorMain.WeightedFock.residual_allowed line 356
  48. theorem OAI.FreeGroupFactorMain.WeightedFock.residualCreation_filled_covariance line 360