OAI/Geometry/CubicTorus/Estimates/BVGraphRescaling.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.weakCMC_column_height_residual line 16
  2. lemma OAI.CubicTorus.integral_pairing_perturbation line 48
  3. lemma OAI.CubicTorus.norm_normalPlaneCoordinates_le line 81
  4. lemma OAI.CubicTorus.normalColumnTest_fderiv_le line 84
  5. theorem OAI.CubicTorus.weakCMC_column_residual_bound line 105
  6. lemma OAI.CubicTorus.integral_pairing_local_error line 199
  7. theorem OAI.CubicTorus.weakCMC_graph_residual_bound line 221
  8. lemma OAI.CubicTorus.laplacian_comp_smul line 290
  9. lemma OAI.CubicTorus.planar_scaled_laplacian_pairing line 311
  10. lemma OAI.CubicTorus.fderiv_comp_smul_eq line 328
  11. lemma OAI.CubicTorus.scaled_test_support line 336
  12. def OAI.CubicTorus.graphRescale line 361
  13. lemma OAI.CubicTorus.graphRescale_contDiff line 364
  14. lemma OAI.CubicTorus.graphRescale_fderiv line 368
  15. lemma OAI.CubicTorus.plane_integral_rescale_ball line 380
  16. lemma OAI.CubicTorus.graphRescale_relative_energy line 400
  17. lemma OAI.CubicTorus.graphRescale_blend line 409
  18. theorem OAI.CubicTorus.isMinimizerAt_scaled_graph_comparison line 428
  19. theorem OAI.CubicTorus.isMinimizerAt_sequential_oriented_decay line 508
  20. lemma OAI.CubicTorus.graphSmooth_integrable line 608
  21. lemma OAI.CubicTorus.graphSmooth_lipschitz line 613
  22. lemma OAI.CubicTorus.graphSmooth_affine line 630
  23. lemma OAI.CubicTorus.graphSmooth_affine_abs_le line 637
  24. theorem OAI.CubicTorus.exists_sharp_smooth_graph line 649
  25. def OAI.CubicTorus.columnPhase line 688
  26. def OAI.CubicTorus.columnGraphMismatch line 690
  27. lemma OAI.CubicTorus.columnPhase_measurable line 695
  28. lemma OAI.CubicTorus.columnPhase_difference_le line 698
  29. lemma OAI.CubicTorus.columnGraphMismatch_integrable line 703
  30. lemma OAI.CubicTorus.columnGraphMismatch_nonneg line 716
  31. lemma OAI.CubicTorus.measurable_columnGraphMismatch line 720
  32. lemma OAI.CubicTorus.good_column_characteristic line 734
  33. lemma OAI.CubicTorus.columnGraphMismatch_eq_zero_good line 761
  34. lemma OAI.CubicTorus.small_column_lift line 791
  35. lemma OAI.CubicTorus.trapped_column_phases line 809
  36. lemma OAI.CubicTorus.columnGraphMismatch_trapped_le line 827