OAI/Analysis/InterpolatedFactors/WeightedCorner.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.FreeGroupFactorMain.WeightedFock.ambientClosed line 10
  2. def OAI.FreeGroupFactorMain.WeightedFock.ambientTopology line 13
  3. def OAI.FreeGroupFactorMain.WeightedFock.pAmbientTopology line 15
  4. theorem OAI.FreeGroupFactorMain.WeightedFock.pAmbientRepresentation_mem line 18
  5. def OAI.FreeGroupFactorMain.WeightedFock.pAmbientRepresentation line 23
  6. theorem OAI.FreeGroupFactorMain.WeightedFock.pAmbientRepresentation_normal line 33
  7. theorem OAI.FreeGroupFactorMain.WeightedFock.pAmbientRepresentation_symm_normal line 42
  8. def OAI.FreeGroupFactorMain.WeightedFock.representedGeneratedIso line 51
  9. theorem OAI.FreeGroupFactorMain.WeightedFock.representedGeneratedIso_normal line 62
  10. theorem OAI.FreeGroupFactorMain.WeightedFock.representedGeneratedIso_symm_normal line 71
  11. def OAI.FreeGroupFactorMain.WeightedFock.pAmbientGeneratedIso line 81
  12. def OAI.FreeGroupFactorMain.WeightedFock.pAmbientGaussianIso line 85
  13. theorem OAI.FreeGroupFactorMain.WeightedFock.pAmbientGaussianIso_normal line 88
  14. theorem OAI.FreeGroupFactorMain.WeightedFock.pAmbientGaussianIso_symm_normal line 102
  15. theorem OAI.FreeGroupFactorMain.WeightedFock.pAmbientGaussianIso_trace line 115
  16. def OAI.FreeGroupFactorMain.WeightedFock.ambientP line 121
  17. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientP_projection line 122
  18. def OAI.FreeGroupFactorMain.WeightedFock.ambientCornerGaussianIso line 125
  19. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientCornerGaussianIso_normal line 129
  20. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientCornerGaussianIso_symm_normal line 141
  21. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientCornerGaussianIso_trace line 155
  22. def OAI.FreeGroupFactorMain.WeightedFock.ambientScalarIso line 161
  23. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientScalarIso_normal line 165
  24. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientScalarIso_symm_normal line 176
  25. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientScalarIso_trace line 186