OAI/Analysis/IntegralMeans/LevelCurve.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Brennan.periodicLoop line 21
  2. lemma OAI.Brennan.periodicLoop_closed line 24
  3. lemma OAI.Brennan.periodicLoop_range line 30
  4. lemma OAI.Brennan.loopIndex_periodic_shift line 39
  5. lemma OAI.Brennan.transverse_displacement_not_mem line 52
  6. lemma OAI.Brennan.winding_jump line 69
  7. lemma OAI.Brennan.loopIndex_zero_of_re_lt line 92
  8. lemma OAI.Brennan.winding_leftmost_normal line 99
  9. lemma OAI.Brennan.isMIntegralCurve_iff_hasDerivAt line 121
  10. lemma OAI.Brennan.exists_global_curve line 133
  11. def OAI.Brennan.transverseCoordinate line 157
  12. def OAI.Brennan.levelChartDerivative line 160
  13. lemma OAI.Brennan.realFunctional_decomposition line 163
  14. lemma OAI.Brennan.levelChartDerivative_det line 170
  15. lemma OAI.Brennan.levelChartDerivative_det_pos line 176
  16. lemma OAI.Brennan.exists_regular_level_chart line 190
  17. lemma OAI.Brennan.curve_local_level_cover line 218
  18. lemma OAI.Brennan.integral_curve_contDiff_one line 266
  19. lemma OAI.Brennan.integral_curve_first_integral line 276
  20. lemma OAI.Brennan.integral_curves_shift_eq line 285
  21. lemma OAI.Brennan.curve_isOpenMap_level line 298
  22. lemma OAI.Brennan.compact_regular_level_periodic line 316
  23. lemma OAI.Brennan.curve_locally_injective line 368
  24. lemma OAI.Brennan.integral_curve_simple_period line 388
  25. lemma OAI.Brennan.integral_curves_range_eq line 433
  26. lemma OAI.Brennan.compact_regular_level_finite_curves line 448
  27. lemma OAI.Brennan.integral_curve_contDiff_two line 503