OAI/Geometry/CubicTorus/Estimates/CoordinatePlaneRays.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_centered_normal_product line 13
  2. def OAI.CubicTorus.coordinatePlaneLift line 68
  3. def OAI.CubicTorus.coordinateSectionPoint line 72
  4. lemma OAI.CubicTorus.coordinatePlaneLift_apply line 75
  5. lemma OAI.CubicTorus.coordinateSectionPoint_apply line 79
  6. lemma OAI.CubicTorus.coordinateSectionPoint_contDiff line 83
  7. lemma OAI.CubicTorus.coordinateSectionPoint_segment line 87
  8. lemma OAI.CubicTorus.coordinateSectionPoint_fold line 93
  9. lemma OAI.CubicTorus.coordinateSectionPoint_mem_box line 104
  10. theorem OAI.CubicTorus.isMinimizerAt_coordinate_plane_transverse line 117
  11. theorem OAI.CubicTorus.continuous_path_exit line 172
  12. theorem OAI.CubicTorus.isMinimizerAt_chamber_continuous_exit line 212
  13. lemma OAI.CubicTorus.coordinateSine_chamber_endpoint line 254
  14. theorem OAI.CubicTorus.isMinimizerAt_chamber_critical_interior line 264
  15. theorem OAI.CubicTorus.isMinimizerAt_chamber_critical_collar line 288
  16. lemma OAI.CubicTorus.coordinateSine_zero_reflection_iff line 328
  17. lemma OAI.CubicTorus.chamber_endpoint_of_coordinateSine_zero line 338
  18. lemma OAI.CubicTorus.chamberFoldLift_seam_iff line 361
  19. lemma OAI.CubicTorus.isMinimizerAt_frontier_nonempty line 369
  20. theorem OAI.CubicTorus.isMinimizerAt_boundary_meets_seam line 382
  21. theorem OAI.CubicTorus.isMinimizerAt_no_face_vertex_pattern line 412
  22. lemma OAI.CubicTorus.exists_periodic_primitive line 457
  23. lemma OAI.CubicTorus.periodic_normalized_primitive line 469
  24. lemma OAI.CubicTorus.fderiv_axial_function line 494
  25. lemma OAI.CubicTorus.axial_function_periodic line 501
  26. lemma OAI.CubicTorus.tangentialDivergence_axial line 506
  27. lemma OAI.CubicTorus.divergence_axial line 516
  28. theorem OAI.CubicTorus.axial_flux_derivative line 523
  29. def OAI.CubicTorus.axialNormalWeight line 552
  30. lemma OAI.CubicTorus.continuous_axialNormalWeight line 554
  31. lemma OAI.CubicTorus.integrable_axialNormalWeight line 558
  32. theorem OAI.CubicTorus.axial_flux_moment line 563
  33. theorem OAI.CubicTorus.isMinimizerAt_axial_flux_moments line 597
  34. lemma OAI.CubicTorus.axialNormalWeight_nonneg line 624
  35. lemma OAI.CubicTorus.axialNormalWeight_le_one line 634
  36. lemma OAI.CubicTorus.sum_axialNormalWeight line 639
  37. def OAI.CubicTorus.axialFluxWeight line 649
  38. lemma OAI.CubicTorus.axialFluxWeight_nonneg line 652
  39. lemma OAI.CubicTorus.axialFluxWeight_le_one line 656
  40. lemma OAI.CubicTorus.sum_axialFluxWeight line 664
  41. theorem OAI.CubicTorus.axialFluxWeight_lt_one_iff line 674
  42. def OAI.CubicTorus.scalarMollifier line 736
  43. lemma OAI.CubicTorus.scalarMollifier_tendsto line 742
  44. def OAI.CubicTorus.scalarMollification line 747
  45. lemma OAI.CubicTorus.scalarMollification_contDiff line 750
  46. lemma OAI.CubicTorus.scalarMollification_periodic line 755
  47. lemma OAI.CubicTorus.scalarMollification_bound line 764
  48. lemma OAI.CubicTorus.scalarMollification_tendsto line 776
  49. theorem OAI.CubicTorus.circle_measure_ext_smooth line 780