OAI/Geometry/CubicTorus/Regularity/NormalFirstVariation.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.normalFirstVariation line 18
  2. lemma OAI.CubicTorus.integrable_normalFirstVariation line 22
  3. lemma OAI.CubicTorus.integral_inner_doubleVelocity_zero line 30
  4. lemma OAI.CubicTorus.integrable_doublePerturbation line 40
  5. lemma OAI.CubicTorus.doubleVelocityCoefficient_eventually_bounded line 51
  6. theorem OAI.CubicTorus.hasDerivAt_doubleNormalArea line 66
  7. lemma OAI.CubicTorus.doubleNormalArea_zero line 83
  8. def OAI.CubicTorus.volumeCorrectionCoefficient line 90
  9. lemma OAI.CubicTorus.continuousAt_volumeCorrectionCoefficient line 93
  10. lemma OAI.CubicTorus.volume_doubleRegion_corrected line 99
  11. theorem OAI.CubicTorus.isMinimizerAt_mixed_stationary line 131
  12. theorem OAI.CubicTorus.isMinimizerAt_exists_coordinate_multiplier line 159
  13. lemma OAI.CubicTorus.fderiv_component line 177
  14. lemma OAI.CubicTorus.flux_sum_components line 185
  15. lemma OAI.CubicTorus.exists_positive_directionalFlux line 195
  16. def OAI.CubicTorus.wallCutoff line 215
  17. lemma OAI.CubicTorus.wallCutoff_contDiff line 217
  18. lemma OAI.CubicTorus.wallCutoff_periodic line 221
  19. lemma OAI.CubicTorus.wallCutoff_face line 229
  20. lemma OAI.CubicTorus.wallCutoff_halfShift line 233
  21. lemma OAI.CubicTorus.smooth_flux_translation line 243
  22. lemma OAI.CubicTorus.directionalFlux_translation line 274
  23. theorem OAI.CubicTorus.exists_positive_wallVariation line 296
  24. theorem OAI.CubicTorus.isMinimizerAt_exists_weakCMC line 351
  25. def OAI.CubicTorus.tangentialDivergence line 371
  26. lemma OAI.CubicTorus.inner_coordinateNormalVelocity line 374
  27. lemma OAI.CubicTorus.tangentialDivergence_eq_sum line 384
  28. lemma OAI.CubicTorus.continuous_tangentialDivergence line 393
  29. lemma OAI.CubicTorus.integral_tangentialDivergence_eq_sum line 402
  30. theorem OAI.CubicTorus.tangent_firstVariation_of_coordinate line 417
  31. theorem OAI.CubicTorus.weakCMC_identity line 439
  32. lemma OAI.CubicTorus.weakCMC_firstVariation_bound line 459
  33. lemma OAI.CubicTorus.latticeVector_add line 489
  34. lemma OAI.CubicTorus.latticeVector_zero line 493
  35. lemma OAI.CubicTorus.finite_lattice_support_near line 497
  36. def OAI.CubicTorus.latticePeriodize line 531
  37. lemma OAI.CubicTorus.latticePeriodize_periodic line 534
  38. lemma OAI.CubicTorus.latticePeriodize_contDiff line 547
  39. lemma OAI.CubicTorus.translate_not_mem_tsupport line 563
  40. lemma OAI.CubicTorus.latticePeriodize_eventuallyEq line 579
  41. lemma OAI.CubicTorus.compactCell_coordinates line 610
  42. lemma OAI.CubicTorus.latticePeriodize_wall line 616
  43. theorem OAI.CubicTorus.weakCMC_local_identity line 640
  44. def OAI.CubicTorus.coordinateBox line 660
  45. lemma OAI.CubicTorus.measurableSet_coordinateBox line 663
  46. lemma OAI.CubicTorus.coordinateBox_mono line 670
  47. lemma OAI.CubicTorus.coordinateBox_zero line 674
  48. lemma OAI.CubicTorus.coordinateBox_lift_preimage line 680
  49. lemma OAI.CubicTorus.volume_coordinateBox line 699
  50. lemma OAI.CubicTorus.integral_divergence_coordinateBox line 710
  51. lemma OAI.CubicTorus.box_face_flux_bound line 743
  52. theorem OAI.CubicTorus.perimeter_coordinateBox_le line 755
  53. theorem OAI.CubicTorus.finitePerimeter_coordinateBox line 772
  54. lemma OAI.CubicTorus.representative_norm_le_box line 782
  55. theorem OAI.CubicTorus.bv_cubical_isoperimetric line 799