OAI/Geometry/CubicTorus/Variation/BVColumnMismatchMeasure.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.columnGraphMismatch_disagreement_volume_le line 15
  2. theorem OAI.CubicTorus.columnGraphMismatch_L1_le line 46
  3. lemma OAI.CubicTorus.characteristic_symmDiff_eq_abs line 91
  4. lemma OAI.CubicTorus.graphSublevelIndicator_column line 96
  5. lemma OAI.CubicTorus.cubeCenter_add_mem line 103
  6. lemma OAI.CubicTorus.torusGraphRegion_symmDiff_ball_le line 111
  7. lemma OAI.CubicTorus.columnPhase_abs_sub line 204
  8. lemma OAI.CubicTorus.integral_abs_columnPhase_sub line 212
  9. lemma OAI.CubicTorus.columnGraphMismatch_change_le line 224
  10. lemma OAI.CubicTorus.torusGraphRegion_symmDiff_change_le line 252
  11. lemma OAI.CubicTorus.torusGraphRegion_graphSmooth_difference_le line 272
  12. lemma OAI.CubicTorus.columnPhase_integral line 300
  13. lemma OAI.CubicTorus.normalColumnHeight_error_le_mismatch line 314
  14. lemma OAI.CubicTorus.columnGraphMismatch_bound line 331
  15. lemma OAI.CubicTorus.columnGraphMismatch_integrable_ball line 340
  16. lemma OAI.CubicTorus.columnGraphMismatch_integral_change_le line 351
  17. lemma OAI.CubicTorus.normalColumnHeight_integral_error_le line 366
  18. lemma OAI.CubicTorus.plane_ball_real_volume_scale line 391
  19. lemma OAI.CubicTorus.torusGraphRegion_symmDiff_real_ball_le line 397
  20. theorem OAI.CubicTorus.exists_physical_smooth_graph line 410
  21. theorem OAI.CubicTorus.normalMeasure_lipschitz_approximation_with_cones line 459
  22. theorem OAI.CubicTorus.isMinimizerAt_lipschitz_approximation_with_cones line 526
  23. lemma OAI.CubicTorus.clamp_height_bound line 581
  24. theorem OAI.CubicTorus.isMinimizerAt_trapped_graph_approximation line 586
  25. theorem OAI.CubicTorus.isMinimizerAt_tightly_trapped_graph_approximation line 696
  26. theorem OAI.CubicTorus.isMinimizerAt_smooth_trapped_approximation line 807