OAI/Analysis/InterpolatedFactors/CornerGaussian.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.Amplification.subalgebraCorner line 13
  2. def OAI.FreeGroupFactorMain.Amplification.sandwiched line 27
  3. abbrev OAI.FreeGroupFactorMain.WeightedFock.PCorner line 41
  4. def OAI.FreeGroupFactorMain.WeightedFock.pFilled line 43
  5. def OAI.FreeGroupFactorMain.WeightedFock.filledOfCorner line 47
  6. def OAI.FreeGroupFactorMain.WeightedFock.pTrace line 50
  7. theorem OAI.FreeGroupFactorMain.WeightedFock.pTrace_tracial line 57
  8. theorem OAI.FreeGroupFactorMain.WeightedFock.P_mul_supportedLeg line 65
  9. def OAI.FreeGroupFactorMain.WeightedFock.pFresh line 71
  10. theorem OAI.FreeGroupFactorMain.WeightedFock.pFresh_val line 75
  11. def OAI.FreeGroupFactorMain.WeightedFock.pResidual line 78
  12. theorem OAI.FreeGroupFactorMain.WeightedFock.pResidual_val line 82
  13. def OAI.FreeGroupFactorMain.WeightedFock.pDiagonal line 85
  14. theorem OAI.FreeGroupFactorMain.WeightedFock.pDiagonal_val line 90
  15. theorem OAI.FreeGroupFactorMain.WeightedFock.P_mul_legSupport line 93
  16. theorem OAI.FreeGroupFactorMain.WeightedFock.legSupport_projection line 98
  17. def OAI.FreeGroupFactorMain.WeightedFock.pSupport line 103
  18. theorem OAI.FreeGroupFactorMain.WeightedFock.pSupport_projection line 112
  19. theorem OAI.FreeGroupFactorMain.WeightedFock.pSupport_false line 119
  20. theorem OAI.FreeGroupFactorMain.WeightedFock.pFresh_covariance line 121
  21. theorem OAI.FreeGroupFactorMain.WeightedFock.legSupport_mul_leg line 145
  22. theorem OAI.FreeGroupFactorMain.WeightedFock.pFresh_supported line 152
  23. def OAI.FreeGroupFactorMain.WeightedFock.freshAbsorptionData line 162
  24. def OAI.FreeGroupFactorMain.WeightedFock.pResidualSupport line 197
  25. theorem OAI.FreeGroupFactorMain.WeightedFock.pResidualSupport_val line 201
  26. theorem OAI.FreeGroupFactorMain.WeightedFock.pResidualSupport_projection line 205
  27. theorem OAI.FreeGroupFactorMain.WeightedFock.residualSupport_projection line 211
  28. theorem OAI.FreeGroupFactorMain.WeightedFock.residualSupport_mul_leg line 217
  29. theorem OAI.FreeGroupFactorMain.WeightedFock.pResidual_supported line 224
  30. theorem OAI.FreeGroupFactorMain.WeightedFock.pDiagonal_supported line 236
  31. theorem OAI.FreeGroupFactorMain.WeightedFock.pResidual_covariance line 246
  32. theorem OAI.FreeGroupFactorMain.WeightedFock.pDiagonal_covariance line 263
  33. theorem OAI.FreeGroupFactorMain.WeightedFock.pFresh_residual line 277
  34. theorem OAI.FreeGroupFactorMain.WeightedFock.pFresh_diagonal line 284
  35. theorem OAI.FreeGroupFactorMain.WeightedFock.pResidual_diagonal line 291