OAI/Analysis/InterpolatedFactors/Recognition.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.GramSpatial.combination_inner line 16
  2. theorem OAI.FreeGroupFactorMain.GramSpatial.combination_norm line 24
  3. theorem OAI.FreeGroupFactorMain.GramSpatial.combination_dense line 34
  4. def OAI.FreeGroupFactorMain.GramSpatial.spatial line 42
  5. theorem OAI.FreeGroupFactorMain.GramSpatial.spatial_combination line 50
  6. theorem OAI.FreeGroupFactorMain.GramSpatial.spatial_family line 57
  7. theorem OAI.FreeGroupFactorMain.GramSpatial.spatial_intertwines line 65
  8. theorem OAI.FreeGroupFactorMain.GramSpatial.spatial_trace line 90
  9. abbrev OAI.FreeGroupFactorMain.GaussianRecognition.Operator line 106
  10. structure OAI.FreeGroupFactorMain.GaussianRecognition.System line 108
  11. abbrev OAI.FreeGroupFactorMain.GaussianRecognition.Word line 118
  12. def OAI.FreeGroupFactorMain.GaussianRecognition.System.normal line 122
  13. def OAI.FreeGroupFactorMain.GaussianRecognition.System.family line 126
  14. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.coeff_normal line 128
  15. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.create_normal line 134
  16. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.annihilate_normal_nil line 138
  17. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.annihilate_normal_cons line 141
  18. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.left_inner line 147
  19. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.old_left_inner line 158
  20. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.root_inner line 167
  21. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.normal_inner_eq line 176
  22. def OAI.FreeGroupFactorMain.GaussianRecognition.System.generator line 209
  23. def OAI.FreeGroupFactorMain.GaussianRecognition.System.generatorRule line 211
  24. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.generator_family line 219
  25. def OAI.FreeGroupFactorMain.GaussianRecognition.System.coeffRule line 233
  26. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.coeff_family line 237
  27. def OAI.FreeGroupFactorMain.GaussianRecognition.System.spatial line 247
  28. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.spatial_coeff line 251
  29. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.spatial_generator line 258
  30. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.spatial_root line 265
  31. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.spatial_trace line 270
  32. def OAI.FreeGroupFactorMain.GaussianRecognition.uniformCovariance line 285
  33. theorem OAI.FreeGroupFactorMain.WeightedFock.weightedUniformBase_rep line 292
  34. theorem OAI.FreeGroupFactorMain.WeightedFock.cornerAbsorption_trace line 296
  35. theorem OAI.FreeGroupFactorMain.WeightedFock.weightedUniformBase_trace line 299
  36. def OAI.FreeGroupFactorMain.WeightedFock.absorbedCreation line 305
  37. theorem OAI.FreeGroupFactorMain.WeightedFock.absorbedCreation_cov_diagonal line 309
  38. theorem OAI.FreeGroupFactorMain.WeightedFock.absorbedCreation_cov_off line 325
  39. theorem OAI.FreeGroupFactorMain.WeightedFock.absorbedCreation_annihilate line 339
  40. def OAI.FreeGroupFactorMain.WeightedFock.weightedSystem line 348