OAI/Geometry/CubicTorus/Estimates/PlaneWeakGradient.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.differential_integral_restrict line 13
  2. theorem OAI.CubicTorus.WeakCMCGraph.linearized_equation line 20
  3. theorem OAI.CubicTorus.LinearCMCEquation.weak_derivative line 104
  4. lemma OAI.CubicTorus.C1_gradient_continuous line 211
  5. lemma OAI.CubicTorus.plane_gradient_support line 215
  6. lemma OAI.CubicTorus.plane_gradient_compact line 219
  7. lemma OAI.CubicTorus.compact_C1_gradient_memLp line 223
  8. lemma OAI.CubicTorus.compact_test_poincare line 227
  9. def OAI.CubicTorus.PlaneWeakGradient line 272
  10. lemma OAI.CubicTorus.PlaneWeakGradient.congr line 276
  11. lemma OAI.CubicTorus.compact_C1_weak_gradient line 287
  12. lemma OAI.CubicTorus.L2_pair_scalar_test line 303
  13. lemma OAI.CubicTorus.L2_pair_vector_test line 311
  14. lemma OAI.CubicTorus.PlaneWeakGradient.L2_limit line 324
  15. lemma OAI.CubicTorus.continuous_local_scalar_product line 358
  16. lemma OAI.CubicTorus.C1_local_integration_by_parts line 369
  17. lemma OAI.CubicTorus.C1_mixed_test_identity line 387
  18. lemma OAI.CubicTorus.indicator_inner_test_integral line 421
  19. lemma OAI.CubicTorus.indicator_differential_integral line 429
  20. theorem OAI.CubicTorus.WeakCMCGraph.scalar_linearized_equation line 438
  21. theorem OAI.CubicTorus.LinearCMCEquation.scalar_derivative line 512
  22. lemma OAI.CubicTorus.C1_gradient_add line 593
  23. lemma OAI.CubicTorus.C1_gradient_smul line 599
  24. lemma OAI.CubicTorus.C1_gradient_sub line 605
  25. def OAI.CubicTorus.smoothGradientSpace line 611
  26. def OAI.CubicTorus.zeroBoundaryGradientSpace line 659
  27. lemma OAI.CubicTorus.zeroBoundaryGradientSpace_isClosed line 662
  28. lemma OAI.CubicTorus.zeroBoundaryGradientSpace_approximation line 666
  29. lemma OAI.CubicTorus.compact_test_poincare_difference line 692
  30. lemma OAI.CubicTorus.cauchySeq_of_distance_comparison line 709
  31. theorem OAI.CubicTorus.zeroBoundaryGradientSpace_primitive line 723
  32. theorem OAI.CubicTorus.plane_harmonic_replacement line 763
  33. lemma OAI.CubicTorus.L2_pair_gradient_test line 779
  34. lemma OAI.CubicTorus.harmonic_replacement_test line 788
  35. lemma OAI.CubicTorus.L2_scalar_test_integrable line 811
  36. lemma OAI.CubicTorus.L2_vector_test_integrable line 818
  37. lemma OAI.CubicTorus.PlaneWeakGradient.Lp_sub line 824