OAI/Geometry/CubicTorus/Estimates/BVTriangleRegion.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.coordinateTriangle line 15
  2. lemma OAI.CubicTorus.measurableSet_coordinateTriangle line 18
  3. lemma OAI.CubicTorus.integralOn_coordinateTriangle line 23
  4. lemma OAI.CubicTorus.integral_coordinateTriangle line 51
  5. theorem OAI.CubicTorus.integral_coordinateTriangle_divergence line 57
  6. abbrev OAI.CubicTorus.PrismCoordinates line 86
  7. def OAI.CubicTorus.prismCoordinateDivergence line 88
  8. def OAI.CubicTorus.coordinatePrism line 91
  9. lemma OAI.CubicTorus.hasDerivAt_prism_axial line 94
  10. lemma OAI.CubicTorus.prism_planar_coordinate_derivatives line 101
  11. lemma OAI.CubicTorus.compact_support_prism_slice line 112
  12. theorem OAI.CubicTorus.integral_coordinatePrism_divergence line 121
  13. lemma OAI.CubicTorus.coordinateTriangle_subset_box line 194
  14. lemma OAI.CubicTorus.coordinateTriangle_measure_lt_top line 208
  15. theorem OAI.CubicTorus.volume_real_coordinateTriangle line 213
  16. lemma OAI.CubicTorus.abs_planar_normal_flux line 224
  17. lemma OAI.CubicTorus.abs_planar_second_flux line 233
  18. theorem OAI.CubicTorus.abs_integral_coordinateTriangle_divergence_le line 236
  19. theorem OAI.CubicTorus.triangular_chord_margin_pos line 262
  20. def OAI.CubicTorus.prismRadialFlux line 284
  21. def OAI.CubicTorus.prismClosingFlux line 288
  22. lemma OAI.CubicTorus.integral_coordinatePrism_divergence_split line 292
  23. theorem OAI.CubicTorus.abs_prismClosingFlux_le line 309
  24. theorem OAI.CubicTorus.exists_strict_prism_replacement_scale line 334
  25. lemma OAI.CubicTorus.small_oscillation_boundary_flat line 369
  26. theorem OAI.CubicTorus.isMinimizerAt_quantitative_trapping line 409
  27. lemma OAI.CubicTorus.characteristic_symmDiff_abs line 473
  28. theorem OAI.CubicTorus.cutoff_gluing_flux_le line 479
  29. def OAI.CubicTorus.gluedRegion line 579
  30. lemma OAI.CubicTorus.measurableSet_gluedRegion line 581
  31. lemma OAI.CubicTorus.characteristic_gluedRegion line 585
  32. lemma OAI.CubicTorus.cutoff_gluing_flux_tendsto line 592
  33. lemma OAI.CubicTorus.normalMeasure_sublevelCutoff_tendsto line 634
  34. lemma OAI.CubicTorus.normalMeasure_integral_one line 660
  35. theorem OAI.CubicTorus.perimeter_glued_sublevel_le line 665
  36. lemma OAI.CubicTorus.regionDistance_gluedRegion line 724
  37. theorem OAI.CubicTorus.isMinimizerAt_local_replacement line 737
  38. lemma OAI.CubicTorus.BoundaryFlatAt.exists_small_cone line 774
  39. lemma OAI.CubicTorus.BoundaryFlatAt.hasFDerivWithinAt_inner_zero line 792
  40. lemma OAI.CubicTorus.lipschitz_boundary_parameter_tangent line 835
  41. lemma OAI.CubicTorus.normalGraph_hasFDerivAt line 857
  42. lemma OAI.CubicTorus.normalGraph_tangent_ae line 864