OAI/Geometry/CubicTorus/Curvature/LinearCMCEquation.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.exists_plane_test_cutoff line 13
  2. theorem OAI.CubicTorus.exists_C1_test_approximants line 29
  3. lemma OAI.CubicTorus.cmcFlux_norm_le line 103
  4. lemma OAI.CubicTorus.cmcFlux_difference_bound line 108
  5. lemma OAI.CubicTorus.cmcFlux_line_deriv line 119
  6. lemma OAI.CubicTorus.cmcFlux_strong_monotone line 127
  7. lemma OAI.CubicTorus.measurable_cmc_gradient line 158
  8. lemma OAI.CubicTorus.measurable_differential_apply line 162
  9. theorem OAI.CubicTorus.weak_flux_C1_test line 167
  10. theorem OAI.CubicTorus.WeakCMCGraph.test_C1 line 210
  11. lemma OAI.CubicTorus.integrable_differential_apply_of_bounded line 231
  12. lemma OAI.CubicTorus.translated_test_support line 245
  13. lemma OAI.CubicTorus.WeakCMCGraph.translated_test line 258
  14. theorem OAI.CubicTorus.WeakCMCGraph.difference_test line 275
  15. lemma OAI.CubicTorus.local_C1_cutoff_product line 311
  16. lemma OAI.CubicTorus.energyTest_tsupport line 322
  17. lemma OAI.CubicTorus.integrable_bounded_compact line 329
  18. lemma OAI.CubicTorus.cmc_energy_absorption line 340
  19. lemma OAI.CubicTorus.translated_difference_contDiffOn line 362
  20. lemma OAI.CubicTorus.translated_difference_fderiv line 373
  21. lemma OAI.CubicTorus.cmc_linear_energy_absorption line 402
  22. lemma OAI.CubicTorus.gradient_difference_norm_le line 442
  23. lemma OAI.CubicTorus.height_difference_norm_le line 449
  24. lemma OAI.CubicTorus.measurable_plane_gradient line 453
  25. lemma OAI.CubicTorus.cmc_cutoff_energies_integrable line 456
  26. theorem OAI.CubicTorus.WeakCMCGraph.caccioppoli line 496
  27. lemma OAI.CubicTorus.cmcJacobian_contDiff line 561
  28. lemma OAI.CubicTorus.cmcJacobian_symmetric line 566
  29. lemma OAI.CubicTorus.cmcFlux_quadratic_remainder line 573
  30. def OAI.CubicTorus.LinearCMCEquation line 609
  31. lemma OAI.CubicTorus.measurable_plane_clm_apply line 613
  32. lemma OAI.CubicTorus.linear_cmc_flux_measurable line 619
  33. lemma OAI.CubicTorus.linear_cmc_flux_bound line 624
  34. lemma OAI.CubicTorus.LinearCMCEquation.difference_test line 631
  35. lemma OAI.CubicTorus.compact_weighted_energy_integrable line 676
  36. theorem OAI.CubicTorus.LinearCMCEquation.caccioppoli line 693
  37. lemma OAI.CubicTorus.compact_derivative_square_integrable line 778
  38. theorem OAI.CubicTorus.WeakCMCGraph.local_gradient_energy line 792
  39. lemma OAI.CubicTorus.linear_cmc_difference_source_bound line 845