OAI/Geometry/CubicTorus/Estimates/UnitAngle.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.periodic_wirtinger line 21
  2. theorem OAI.CubicTorus.mean_zero_curve_area_energy line 71
  3. theorem OAI.CubicTorus.closed_curve_area_energy line 101
  4. theorem OAI.CubicTorus.positive_periodic_primitive_inverse line 157
  5. theorem OAI.CubicTorus.positive_periodic_arclength_parameter line 175
  6. lemma OAI.CubicTorus.continuous_memLp_two_Ioc line 219
  7. theorem OAI.CubicTorus.planar_curve_isoperimetric line 224
  8. def OAI.CubicTorus.unitAngle line 281
  9. lemma OAI.CubicTorus.unitAngle_norm line 283
  10. lemma OAI.CubicTorus.unitAngle_periodic line 285
  11. lemma OAI.CubicTorus.unitAngle_deriv line 292
  12. lemma OAI.CubicTorus.unitAngle_continuous line 298
  13. def OAI.CubicTorus.radialCurve line 301
  14. def OAI.CubicTorus.radialVelocity line 303
  15. lemma OAI.CubicTorus.radialCurve_deriv line 306
  16. lemma OAI.CubicTorus.radialVelocity_norm_sq line 312
  17. lemma OAI.CubicTorus.radialCurve_area_integrand line 317
  18. theorem OAI.CubicTorus.radial_curve_isoperimetric line 334
  19. def OAI.CubicTorus.complexSquareGauge line 375
  20. def OAI.CubicTorus.complexFold line 376
  21. def OAI.CubicTorus.unitSquareScale line 377
  22. def OAI.CubicTorus.unitSquareEnd line 378
  23. lemma OAI.CubicTorus.complexSquareGauge_pos line 380
  24. lemma OAI.CubicTorus.unitAngle_ne_zero line 387
  25. lemma OAI.CubicTorus.unitSquareScale_pos line 392
  26. lemma OAI.CubicTorus.complexSquareGauge_continuous line 395
  27. lemma OAI.CubicTorus.complexFold_continuous line 398
  28. lemma OAI.CubicTorus.unitSquareScale_continuous line 401
  29. lemma OAI.CubicTorus.unitSquareEnd_continuous line 405
  30. lemma OAI.CubicTorus.unitSquareScale_periodic line 408
  31. lemma OAI.CubicTorus.unitSquareEnd_periodic line 412
  32. lemma OAI.CubicTorus.complexFold_smul line 416
  33. lemma OAI.CubicTorus.complexSquareGauge_smul line 419
  34. lemma OAI.CubicTorus.unitSquareEnd_gauge line 424
  35. lemma OAI.CubicTorus.unitSquareEnd_coordinates line 431
  36. lemma OAI.CubicTorus.integral_square_le_mass line 473
  37. lemma OAI.CubicTorus.lipschitz_deriv_sq_integrableOn line 502
  38. lemma OAI.CubicTorus.lipschitz_sq_sub_le_interval_energy line 513
  39. lemma OAI.CubicTorus.integrable_square_sub_const line 528
  40. lemma OAI.CubicTorus.square_sub_average_le line 537
  41. lemma OAI.CubicTorus.lipschitz_sq_sub_le_common_interval_energy line 563
  42. lemma OAI.CubicTorus.lipschitz_interval_poincare line 578
  43. lemma OAI.CubicTorus.variance_le_separated_pairwise line 620
  44. lemma OAI.CubicTorus.lipschitz_product_partial_measurable line 650
  45. lemma OAI.CubicTorus.lipschitz_product_partial_integrable line 659
  46. theorem OAI.CubicTorus.lipschitz_box_poincare line 682
  47. lemma OAI.CubicTorus.differentiableAt_partial_sq_le line 745
  48. lemma OAI.CubicTorus.lipschitz_fderiv_sq_integrable line 763
  49. theorem OAI.CubicTorus.lipschitz_box_poincare_fderiv line 774