OAI/Analysis/FreeGroupFactor/GlobalODE.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.global_solution_of_bounded_lipschitz line 16
  2. def OAI.FreeGroupFactorMain.radialClip line 85
  3. theorem OAI.FreeGroupFactorMain.radialClip_eq line 87
  4. theorem OAI.FreeGroupFactorMain.norm_radialClip_le line 90
  5. theorem OAI.FreeGroupFactorMain.radialClip_lipschitz line 95
  6. def OAI.FreeGroupFactorMain.BoundedLip line 148
  7. theorem OAI.FreeGroupFactorMain.BoundedLip.const line 154
  8. theorem OAI.FreeGroupFactorMain.BoundedLip.add line 159
  9. theorem OAI.FreeGroupFactorMain.BoundedLip.mul line 170
  10. theorem OAI.FreeGroupFactorMain.BoundedLip.star line 193
  11. theorem OAI.FreeGroupFactorMain.BoundedLip.sum line 200
  12. theorem OAI.FreeGroupFactorMain.BoundedLip.smul line 210
  13. theorem OAI.FreeGroupFactorMain.BoundedLip.pi line 214
  14. theorem OAI.FreeGroupFactorMain.BoundedLip.to_bounds line 232