OAI/Analysis/InterpolatedFactors/Jacobi.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.JacobiNonatom.invariant line 12
  2. theorem OAI.FreeGroupFactorMain.JacobiNonatom.invariant_step line 15
  3. theorem OAI.FreeGroupFactorMain.JacobiNonatom.invariant_constant line 26
  4. theorem OAI.FreeGroupFactorMain.JacobiNonatom.invariant_zero line 33
  5. theorem OAI.FreeGroupFactorMain.JacobiNonatom.nonzero_eigenvector_zero line 51
  6. def OAI.FreeGroupFactorMain.WeightedFock.jacobiList line 87
  7. def OAI.FreeGroupFactorMain.WeightedFock.jacobiPath line 91
  8. def OAI.FreeGroupFactorMain.WeightedFock.oddJacobiPath line 92
  9. def OAI.FreeGroupFactorMain.WeightedFock.jacobiBasis line 93
  10. def OAI.FreeGroupFactorMain.WeightedFock.oddJacobiBasis line 94
  11. theorem OAI.FreeGroupFactorMain.WeightedFock.jacobiList_length line 97
  12. theorem OAI.FreeGroupFactorMain.WeightedFock.jacobiPath_injective line 103
  13. theorem OAI.FreeGroupFactorMain.WeightedFock.jacobiPath_start line 110
  14. theorem OAI.FreeGroupFactorMain.WeightedFock.oddJacobiPath_start line 113
  15. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_jacobi_zero line 115
  16. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonal_jacobi_succ line 122
  17. theorem OAI.FreeGroupFactorMain.WeightedFock.offDiagonalStar_oddJacobi line 129
  18. def OAI.FreeGroupFactorMain.WeightedFock.edgeSquare line 138
  19. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeSquare_selfAdjoint line 140
  20. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeSquare_jacobi_zero line 143
  21. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeSquare_jacobi_succ line 149
  22. theorem OAI.FreeGroupFactorMain.WeightedFock.jacobi_coordinates_decay line 160
  23. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeSquare_eigen_coordinates line 170
  24. theorem OAI.FreeGroupFactorMain.WeightedFock.edgeSquare_eigen_root_zero line 194
  25. def OAI.FreeGroupFactorMain.WeightedFock.flipPath line 208
  26. theorem OAI.FreeGroupFactorMain.WeightedFock.flipPath_apply line 220
  27. theorem OAI.FreeGroupFactorMain.WeightedFock.flipPath_involutive line 222
  28. theorem OAI.FreeGroupFactorMain.WeightedFock.flipPath_symm line 227
  29. theorem OAI.FreeGroupFactorMain.WeightedFock.start_flipPath line 231
  30. def OAI.FreeGroupFactorMain.WeightedFock.flipSpatial line 235
  31. theorem OAI.FreeGroupFactorMain.WeightedFock.flipSpatial_apply line 237
  32. theorem OAI.FreeGroupFactorMain.WeightedFock.flipSpatial_single line 242
  33. theorem OAI.FreeGroupFactorMain.WeightedFock.flipSpatial_vertex_intertwines line 255
  34. theorem OAI.FreeGroupFactorMain.WeightedFock.flipSpatial_conjugates_vertex line 266
  35. theorem OAI.FreeGroupFactorMain.WeightedFock.flipSpatial_creation_intertwines line 272
  36. theorem OAI.FreeGroupFactorMain.WeightedFock.flipSpatial_conjugates_creation line 282
  37. theorem OAI.FreeGroupFactorMain.WeightedFock.flipSpatial_conjugates_edgeCreation line 288
  38. theorem OAI.FreeGroupFactorMain.WeightedFock.flipSpatial_conjugates_offDiagonal line 293
  39. theorem OAI.FreeGroupFactorMain.WeightedFock.flipSpatial_conjugates_edgeSquare line 299
  40. theorem OAI.FreeGroupFactorMain.WeightedFock.leftEdgeSquare_eigen_root_zero line 303
  41. def OAI.FreeGroupFactorMain.WeightedFock.leftModulus line 324
  42. theorem OAI.FreeGroupFactorMain.WeightedFock.leftModulus_selfAdjoint line 326
  43. theorem OAI.FreeGroupFactorMain.WeightedFock.leftModulus_square line 329
  44. theorem OAI.FreeGroupFactorMain.WeightedFock.leftModulus_mul_range line 339
  45. theorem OAI.FreeGroupFactorMain.WeightedFock.range_mul_leftModulus line 344
  46. theorem OAI.FreeGroupFactorMain.WeightedFock.starPolar_mul_leftModulus line 349
  47. theorem OAI.FreeGroupFactorMain.WeightedFock.range_zero_of_starEdge_zero line 356
  48. theorem OAI.FreeGroupFactorMain.WeightedFock.leftModulus_eigen_root_zero line 363