OAI/Analysis/FreeGroupFactor/FiniteActive.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.FiniteActive.original_generators_mem line 19
  2. theorem OAI.FreeGroupFactorMain.FiniteActive.orbit_total line 44
  3. theorem OAI.FreeGroupFactorMain.FiniteActive.extension_at_time line 96
  4. theorem OAI.FreeGroupFactorMain.FiniteActive.basis_solution line 117
  5. theorem OAI.FreeGroupFactorMain.FiniteActive.automorphisms line 129
  6. theorem OAI.FreeGroupFactorMain.UnitaryEvaluation.hamiltonianLinear_mapDomain line 154
  7. theorem OAI.FreeGroupFactorMain.FiniteActive.flow_bound line 175
  8. theorem OAI.FreeGroupFactorMain.FiniteActive.bounded_solution line 195
  9. theorem OAI.FreeGroupFactorMain.FiniteActive.bounded_flow line 210
  10. theorem OAI.FreeGroupFactorMain.FiniteActive.wordHom_active line 238
  11. theorem OAI.FreeGroupFactorMain.FiniteActive.wordHom_tuple_active line 245
  12. theorem OAI.FreeGroupFactorMain.FiniteActive.displacements_from_bounds line 253
  13. theorem OAI.FreeGroupFactorMain.FiniteActive.displacement line 281
  14. theorem OAI.FreeGroupFactorMain.FiniteActive.one_step_from_laurent line 316
  15. theorem OAI.FreeGroupFactorMain.FiniteActive.one_step_of_coefficient_estimate line 369
  16. theorem OAI.FreeGroupFactorMain.FiniteActive.one_step line 388