OAI/Analysis/InterpolatedFactors/UniformSpectral.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FreeGroupFactorMain.CyclicSpectral.UniformAlgebra line 15
  2. def OAI.FreeGroupFactorMain.CyclicSpectral.cdfMap line 17
  3. def OAI.FreeGroupFactorMain.CyclicSpectral.uniformHom line 22
  4. def OAI.FreeGroupFactorMain.CyclicSpectral.uniformState line 25
  5. theorem OAI.FreeGroupFactorMain.CyclicSpectral.uniformHom_state line 28
  6. def OAI.FreeGroupFactorMain.CyclicSpectral.uniformPhase line 51
  7. theorem OAI.FreeGroupFactorMain.CyclicSpectral.uniformHom_phase line 54
  8. theorem OAI.FreeGroupFactorMain.CyclicSpectral.uniformHom_mem line 56
  9. def OAI.FreeGroupFactorMain.CyclicSpectral.evaluate line 72
  10. theorem OAI.FreeGroupFactorMain.CyclicSpectral.evaluate_norm line 75
  11. def OAI.FreeGroupFactorMain.CyclicSpectral.realize line 89
  12. theorem OAI.FreeGroupFactorMain.CyclicSpectral.realize_continuous line 92
  13. theorem OAI.FreeGroupFactorMain.CyclicSpectral.realize_norm line 100
  14. def OAI.FreeGroupFactorMain.CyclicSpectral.isometry line 108
  15. theorem OAI.FreeGroupFactorMain.CyclicSpectral.mul_memLp line 119
  16. def OAI.FreeGroupFactorMain.CyclicSpectral.multiply line 125
  17. theorem OAI.FreeGroupFactorMain.CyclicSpectral.multiply_ae line 152
  18. theorem OAI.FreeGroupFactorMain.CyclicSpectral.multiply_continuous line 156
  19. theorem OAI.FreeGroupFactorMain.CyclicSpectral.realize_multiply line 166
  20. theorem OAI.FreeGroupFactorMain.CyclicSpectral.realize_coordinate line 174
  21. def OAI.FreeGroupFactorMain.CyclicSpectral.atom line 185
  22. theorem OAI.FreeGroupFactorMain.CyclicSpectral.atom_ae line 188
  23. theorem OAI.FreeGroupFactorMain.CyclicSpectral.multiply_atom line 192
  24. theorem OAI.FreeGroupFactorMain.CyclicSpectral.realize_atom_eigen line 206
  25. theorem OAI.FreeGroupFactorMain.CyclicSpectral.realize_one line 210
  26. theorem OAI.FreeGroupFactorMain.CyclicSpectral.realize_atom_inner line 213
  27. theorem OAI.FreeGroupFactorMain.CyclicSpectral.singleton_eq_zero line 230
  28. theorem OAI.FreeGroupFactorMain.CyclicSpectral.noAtoms line 236
  29. instance OAI.FreeGroupFactorMain.WeightedFock.oldBaseOp_probability line 251
  30. theorem OAI.FreeGroupFactorMain.WeightedFock.oldBaseOp_noAtoms line 255
  31. def OAI.FreeGroupFactorMain.WeightedFock.weightedUniform line 273
  32. def OAI.FreeGroupFactorMain.WeightedFock.representedBase line 277
  33. theorem OAI.FreeGroupFactorMain.WeightedFock.pRepresentation_symm_val line 280
  34. theorem OAI.FreeGroupFactorMain.WeightedFock.pRepresentation_symm_coe_continuous line 290
  35. theorem OAI.FreeGroupFactorMain.WeightedFock.representedBase_closed line 295
  36. theorem OAI.FreeGroupFactorMain.WeightedFock.oldBaseOp_mem_representedBase line 299
  37. theorem OAI.FreeGroupFactorMain.WeightedFock.weightedUniform_mem line 304
  38. def OAI.FreeGroupFactorMain.WeightedFock.weightedUniformBase line 308
  39. theorem OAI.FreeGroupFactorMain.WeightedFock.weightedUniform_state line 314
  40. theorem OAI.FreeGroupFactorMain.WeightedFock.pRepresentation_vacuumTrace line 324
  41. theorem OAI.FreeGroupFactorMain.WeightedFock.pAnnihilator_root line 342