OAI/Geometry/CubicTorus/Reflection/BVTorusGraphFlux.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.plane_gradient_norm line 15
  2. lemma OAI.CubicTorus.graphAreaVector_norm_sq line 19
  3. lemma OAI.CubicTorus.graphAreaVector_norm_le line 25
  4. lemma OAI.CubicTorus.graph_trace_compactSupport line 31
  5. lemma OAI.CubicTorus.graph_trace_continuous line 44
  6. lemma OAI.CubicTorus.graphAreaVector_continuous line 50
  7. lemma OAI.CubicTorus.graph_trace_flux_integrable line 56
  8. theorem OAI.CubicTorus.integral_graphSublevel_divergence_le line 71
  9. theorem OAI.CubicTorus.cutoff_gluing_local_flux_le line 105
  10. def OAI.CubicTorus.torusGraphRegion line 198
  11. lemma OAI.CubicTorus.measurableSet_torusGraphRegion line 201
  12. lemma OAI.CubicTorus.characteristic_torusGraphRegion line 208
  13. lemma OAI.CubicTorus.latticePeriodize_mem_Icc line 214
  14. lemma OAI.CubicTorus.interior_cutoff_flux_eq line 222
  15. theorem OAI.CubicTorus.torusGraphRegion_cutoff_flux_le line 246
  16. theorem OAI.CubicTorus.perimeter_glued_local_flux_le line 274
  17. lemma OAI.CubicTorus.radialDensityWeight_cell_support line 348
  18. lemma OAI.CubicTorus.radialDensityWeight_periodize line 358
  19. lemma OAI.CubicTorus.graph_trace_energy_integrable line 380
  20. def OAI.CubicTorus.graphBallQuadraticArea line 389
  21. lemma OAI.CubicTorus.graphBallQuadraticArea_tendsto line 392
  22. lemma OAI.CubicTorus.normalMeasure_radial_sublevel line 443
  23. theorem OAI.CubicTorus.isMinimizerAt_graph_replacement line 456
  24. lemma OAI.CubicTorus.lipschitz_probability_average_integrable line 509
  25. lemma OAI.CubicTorus.lipschitz_probability_average_error line 523
  26. lemma OAI.CubicTorus.lipschitz_probability_average_hasFDerivAt line 543
  27. lemma OAI.CubicTorus.lipschitz_probability_average_gradient_sq line 568
  28. lemma OAI.CubicTorus.lipschitz_gradient_sq_integrable_ball line 600
  29. lemma OAI.CubicTorus.lipschitz_gradient_sq_shift_ball_le line 609
  30. theorem OAI.CubicTorus.lipschitz_probability_average_local_energy line 643
  31. def OAI.CubicTorus.graphSmoothingMeasure line 688
  32. instance OAI.CubicTorus.graphSmoothingMeasure_probability line 691
  33. lemma OAI.CubicTorus.graphSmoothingMeasure_ac line 699
  34. lemma OAI.CubicTorus.graphSmoothingMeasure_radius line 702
  35. def OAI.CubicTorus.graphSmooth line 713
  36. lemma OAI.CubicTorus.graphSmooth_eq_convolution line 716
  37. lemma OAI.CubicTorus.graphSmooth_contDiff line 725
  38. lemma OAI.CubicTorus.graphSmooth_error line 731
  39. lemma OAI.CubicTorus.graphSmooth_local_energy line 736
  40. lemma OAI.CubicTorus.normalGraph_norm_ge line 756
  41. lemma OAI.CubicTorus.graphBallQuadraticArea_le_disk line 762
  42. theorem OAI.CubicTorus.graphSmooth_ball_area_le line 787
  43. lemma OAI.CubicTorus.smooth_graph_energy_integrable line 808
  44. theorem OAI.CubicTorus.isMinimizerAt_graph_low_slice line 814