OAI/Geometry/CubicTorus/Estimates/CirclePeriodize.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_zero_curvature_not_preconnected line 13
  2. lemma OAI.CubicTorus.real_periodic_deriv line 87
  3. lemma OAI.CubicTorus.continuous_periodic_lift line 93
  4. theorem OAI.CubicTorus.integerCharacter_directional_variation line 98
  5. lemma OAI.CubicTorus.finite_integer_support_near line 181
  6. def OAI.CubicTorus.circlePeriodize line 207
  7. lemma OAI.CubicTorus.circlePeriodize_periodic line 209
  8. lemma OAI.CubicTorus.circlePeriodize_contDiff line 221
  9. lemma OAI.CubicTorus.circlePeriodize_eventuallyEq line 232
  10. lemma OAI.CubicTorus.circlePeriodize_unit_bounds line 263
  11. theorem OAI.CubicTorus.circle_positive_transition_lower_bound line 297
  12. theorem OAI.CubicTorus.circle_hat_calibration line 394
  13. theorem OAI.CubicTorus.circle_nontrivial_phase_lower_bound line 490
  14. lemma OAI.CubicTorus.integer_lattice_norm_ge_one line 556
  15. theorem OAI.CubicTorus.Periodic.isMinimizerAt_connected_or_unit_integer_phase line 570
  16. lemma OAI.CubicTorus.integer_lattice_norm_one_coordinate line 616
  17. theorem OAI.CubicTorus.Periodic.isMinimizerAt_connected_or_coordinate_phase line 661
  18. lemma OAI.CubicTorus.circlePeriodize_abs_le_one line 696
  19. theorem OAI.CubicTorus.circle_compact_calibration line 716
  20. theorem OAI.CubicTorus.circle_good_partition_variation line 754
  21. def OAI.CubicTorus.circlePhaseGood line 827
  22. lemma OAI.CubicTorus.circlePhaseGood_ae line 832
  23. theorem OAI.CubicTorus.circle_no_four_alternations line 843