OAI/Geometry/CubicTorus/Regularity/WeightedPerimeter.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.bv_isoperimetric_small_of_measurable line 16
  2. theorem OAI.CubicTorus.bv_isoperimetric_small line 59
  3. theorem OAI.CubicTorus.bv_isoperimetric line 70
  4. lemma OAI.CubicTorus.normalTest_le_one line 97
  5. theorem OAI.CubicTorus.normalMeasure_weighted_saturation line 103
  6. def OAI.CubicTorus.weightedPerimeter line 162
  7. lemma OAI.CubicTorus.normalMeasure_weighted_flux line 167
  8. theorem OAI.CubicTorus.normalMeasure_weightedPerimeter line 187
  9. lemma OAI.CubicTorus.exists_admissible_flux_gt line 223
  10. lemma OAI.CubicTorus.normalMeasure_approx_error line 237
  11. lemma OAI.CubicTorus.tendstoInMeasure_of_integral_norm_sq line 265
  12. theorem OAI.CubicTorus.normalMeasure_exists_approximating_fields line 287
  13. theorem OAI.CubicTorus.normalMeasure_exists_polar line 311
  14. def OAI.CubicTorus.IsPerimeterRepresentation line 334
  15. theorem OAI.CubicTorus.exists_perimeterRepresentation line 341
  16. def OAI.CubicTorus.regionDistance line 380
  17. lemma OAI.CubicTorus.regionDistance_nonneg line 383
  18. lemma OAI.CubicTorus.abs_realVolume_sub_le_regionDistance line 386
  19. lemma OAI.CubicTorus.regionDistance_translation line 394
  20. lemma OAI.CubicTorus.characteristic_mul_eq_indicator line 408
  21. lemma OAI.CubicTorus.abs_weighted_characteristic_sub_le line 413
  22. lemma OAI.CubicTorus.directionalFlux_eq_pairing line 440
  23. lemma OAI.CubicTorus.WallVariation.directionalDeriv_bound line 450
  24. lemma OAI.CubicTorus.WallVariation.flux_lipschitz line 457
  25. lemma OAI.CubicTorus.positive_flux_nearby line 472
  26. theorem OAI.CubicTorus.local_comparison_of_positive_flux line 485
  27. lemma OAI.CubicTorus.regionDistance_congr_ae line 554
  28. theorem OAI.CubicTorus.isMinimizerAt_local_quasiminimal line 563
  29. lemma OAI.CubicTorus.divergence_add_fields line 605
  30. lemma OAI.CubicTorus.admissible_convex_cutoff line 612
  31. lemma OAI.CubicTorus.cutoff_partition_flux_le line 633
  32. lemma OAI.CubicTorus.smoothTransition_deriv_zero_of_nonpos line 695
  33. lemma OAI.CubicTorus.smoothTransition_deriv_zero_of_one_le line 703
  34. lemma OAI.CubicTorus.smoothTransition_exists_deriv_bound line 711
  35. def OAI.CubicTorus.sublevelCutoff line 727
  36. lemma OAI.CubicTorus.sublevelCutoff_contDiff line 730
  37. lemma OAI.CubicTorus.sublevelCutoff_periodic line 735
  38. lemma OAI.CubicTorus.sublevelCutoff_mem_Icc line 741
  39. lemma OAI.CubicTorus.fderiv_sublevelCutoff line 745
  40. lemma OAI.CubicTorus.norm_gradient_eq_norm_fderiv line 763
  41. lemma OAI.CubicTorus.sublevelCutoff_gradient_bound line 767
  42. lemma OAI.CubicTorus.sublevelCutoff_gradient_zero line 777
  43. lemma OAI.CubicTorus.perimeter_partition_le_of_flux_bound line 796
  44. lemma OAI.CubicTorus.partition_flux_tendsto line 825
  45. def OAI.CubicTorus.sublevelRegion line 885
  46. def OAI.CubicTorus.sublevelVolume line 888
  47. lemma OAI.CubicTorus.measurableSet_sublevelRegion line 891
  48. lemma OAI.CubicTorus.mem_sublevelRegion_quotient line 895
  49. lemma OAI.CubicTorus.sublevelRegion_mono line 900
  50. lemma OAI.CubicTorus.sublevelVolume_mono line 904
  51. lemma OAI.CubicTorus.sublevelCutoff_gradient_integral_le line 909
  52. lemma OAI.CubicTorus.sublevelCutoff_tendsto line 969
  53. lemma OAI.CubicTorus.tendsto_backward_quotient_of_hasDerivAt line 994
  54. theorem OAI.CubicTorus.perimeter_sublevel_partition line 1009
  55. lemma OAI.CubicTorus.regionDistance_sdiff line 1051
  56. theorem OAI.CubicTorus.isMinimizerAt_sublevel_comparison line 1062
  57. theorem OAI.CubicTorus.isMinimizerAt_sublevel_density_inequality line 1081