OAI/Analysis/FreeGroupFactor/FiniteMoments.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.source_laurent_moments_bounded line 16
  2. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.signedTrajectory_coordinate_ode line 51
  3. theorem OAI.FreeGroupFactorMain.encodedField_finite_range line 104
  4. theorem OAI.FreeGroupFactorMain.source_laurent_moments_finite line 134
  5. theorem OAI.FreeGroupFactorMain.laurent_flow_coordinate_moments line 160
  6. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.wordHom_map line 221
  7. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.hamiltonian_map line 229
  8. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.solution_coordinate_deriv line 241
  9. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.solution_coordinate_smooth line 247
  10. abbrev OAI.FreeGroupFactorMain.FiniteActive.Ambient line 260
  11. instance OAI.FreeGroupFactorMain.FiniteActive.ambientMulActionReal line 262
  12. instance OAI.FreeGroupFactorMain.FiniteActive.ambientContinuousSMulReal line 265
  13. def OAI.FreeGroupFactorMain.FiniteActive.coefficients line 269
  14. def OAI.FreeGroupFactorMain.FiniteActive.tuple line 272
  15. theorem OAI.FreeGroupFactorMain.FiniteActive.tuple_unitary line 275
  16. theorem OAI.FreeGroupFactorMain.FiniteActive.field_inl line 282
  17. theorem OAI.FreeGroupFactorMain.FiniteActive.field_inr line 293
  18. theorem OAI.FreeGroupFactorMain.FiniteActive.moments line 302
  19. theorem OAI.FreeGroupFactorMain.canonical_total_of_reducing line 345