OAI/Geometry/CubicTorus/Estimates/DifferenceStep.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.LinearCMCEquation.local_gradient_energy line 13
  2. theorem OAI.CubicTorus.hilbert_bounded_weak_subsequence line 87
  3. lemma OAI.CubicTorus.continuous_difference_quotient_pairing line 121
  4. theorem OAI.CubicTorus.continuous_difference_quotient_test_limit line 141
  5. theorem OAI.CubicTorus.continuous_L2_weak_directional_derivative line 168
  6. lemma OAI.CubicTorus.continuous_local_cutoff line 246
  7. lemma OAI.CubicTorus.C1_gradient_continuousOn line 257
  8. theorem OAI.CubicTorus.WeakCMCGraph.weak_hessian line 262
  9. def OAI.CubicTorus.differenceStep line 345
  10. def OAI.CubicTorus.vectorDifference line 346
  11. lemma OAI.CubicTorus.differenceStep_mem line 349
  12. lemma OAI.CubicTorus.differenceStep_tendsto line 356
  13. lemma OAI.CubicTorus.L2_vector_norm_sq_integral line 362
  14. lemma OAI.CubicTorus.vectorDifference_memLp line 367
  15. theorem OAI.CubicTorus.vector_L2_difference_subsequence line 378
  16. lemma OAI.CubicTorus.continuous_local_vector_cutoff line 420
  17. theorem OAI.CubicTorus.WeakCMCGraph.gradient_difference_data line 431
  18. theorem OAI.CubicTorus.LinearCMCEquation.gradient_difference_data line 484
  19. lemma OAI.CubicTorus.lipschitz_vector_quotient_bound line 539
  20. lemma OAI.CubicTorus.differentiable_vector_quotient_limit line 549
  21. lemma OAI.CubicTorus.linear_source_difference_limit line 555
  22. theorem OAI.CubicTorus.vector_weak_quotient_derivative line 606
  23. lemma OAI.CubicTorus.weak_linear_cmc_pairing line 653
  24. lemma OAI.CubicTorus.Lp.cmc_differential_integrable line 691
  25. theorem OAI.CubicTorus.weak_L2_linear_cmc_chain line 714
  26. theorem OAI.CubicTorus.weak_L2_cmc_chain line 769