OAI/Geometry/CubicTorus/Regularity/BVGraphNormalization.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.graphNormalize line 15
  2. lemma OAI.CubicTorus.graphNormalize_contDiff line 18
  3. lemma OAI.CubicTorus.graphRescale_normalize line 22
  4. lemma OAI.CubicTorus.graphNormalize_lipschitz line 29
  5. lemma OAI.CubicTorus.graphNormalize_energy line 44
  6. lemma OAI.CubicTorus.graphNormalize_height line 52
  7. lemma OAI.CubicTorus.planeSquare_subset_closedBall line 63
  8. lemma OAI.CubicTorus.ball_subset_planeSquare line 74
  9. lemma OAI.CubicTorus.planeSquare_mean_abs_le line 85
  10. theorem OAI.CubicTorus.smooth_graph_normalized_H1 line 98
  11. theorem OAI.CubicTorus.local_planar_H1_strong_harmonic_approximation line 151
  12. lemma OAI.CubicTorus.exists_planeSquare_cutoff line 229
  13. theorem OAI.CubicTorus.planeSquare_H1_strong_harmonic line 258
  14. theorem OAI.CubicTorus.weakCMC_normalized_graph_residual line 290
  15. lemma OAI.CubicTorus.integral_polar_tilt_ball line 359
  16. lemma OAI.CubicTorus.polar_tilt_integrable line 380
  17. lemma OAI.CubicTorus.cubeCenter_closedBall_interior line 388
  18. theorem OAI.CubicTorus.weakCMC_spatial_normalized_residual line 397
  19. lemma OAI.CubicTorus.smooth_compact_test_bounds line 445
  20. theorem OAI.CubicTorus.weakCMC_normalized_sequence_harmonic line 458
  21. lemma OAI.CubicTorus.exists_small_planeSquare line 510
  22. lemma OAI.CubicTorus.strongL2_restrict_ball line 522
  23. lemma OAI.CubicTorus.directionalFlux_congr_ae line 534
  24. theorem OAI.CubicTorus.isMinimizerAt_trapped_harmonic_graphs line 538
  25. lemma OAI.CubicTorus.norm_sub_sq_le_two line 628
  26. lemma OAI.CubicTorus.graph_relative_energy_bound line 634
  27. lemma OAI.CubicTorus.sublevelVolume_ae_left line 657
  28. lemma OAI.CubicTorus.symmDiff_ae_left line 662
  29. theorem OAI.CubicTorus.isMinimizerAt_trapped_sequential_decay line 677
  30. lemma OAI.CubicTorus.diagonal_strictMono line 766
  31. lemma OAI.CubicTorus.oscillation_le_scaled_tilt line 779
  32. theorem OAI.CubicTorus.isMinimizerAt_trapping_subsequence line 807