OAI/Geometry/CubicTorus/Profiles/PlanarWeakGradient.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.CenteredJacobiChart.weak_ground_state_equation line 13
  2. lemma OAI.CubicTorus.surfaceChartPullback_periodic line 120
  3. lemma OAI.CubicTorus.surfaceChartPullback_smoothJet_value line 142
  4. lemma OAI.CubicTorus.surfaceChartPullback_smoothJet_gradient line 151
  5. theorem OAI.CubicTorus.surfaceH1_chart_weak_chain_rule line 194
  6. def OAI.CubicTorus.HasPlanarWeakGradient line 306
  7. lemma OAI.CubicTorus.memLp_variable_clm_on_compact line 311
  8. theorem OAI.CubicTorus.surfaceH1_hasPlanarWeakGradient line 324
  9. lemma OAI.CubicTorus.memLp_scalar_pair_integrable line 362
  10. lemma OAI.CubicTorus.memLp_vector_pair_integrable line 370
  11. theorem OAI.CubicTorus.PlaneWeakGradient.vector_test line 377
  12. theorem OAI.CubicTorus.PlaneWeakGradient.mul_smooth line 421
  13. lemma OAI.CubicTorus.HasPlanarWeakGradient.extend_zero line 472
  14. lemma OAI.CubicTorus.HasPlanarWeakGradient.zero_extension_memLp line 486
  15. lemma OAI.CubicTorus.memLp_continuous_smul_zero_extension line 491
  16. lemma OAI.CubicTorus.memLp_zero_extension_smul_continuous line 506
  17. def OAI.CubicTorus.CenteredJacobiChart.parameter line 535
  18. lemma OAI.CubicTorus.CenteredJacobiChart.parameter_smooth line 538
  19. lemma OAI.CubicTorus.CenteredJacobiChart.parameter_measurable line 542
  20. def OAI.CubicTorus.CenteredJacobiChart.value line 546
  21. def OAI.CubicTorus.CenteredJacobiChart.ambientGradient line 550
  22. def OAI.CubicTorus.CenteredJacobiChart.planarGradient line 554
  23. def OAI.CubicTorus.CenteredJacobiChart.weight line 557
  24. lemma OAI.CubicTorus.CenteredJacobiChart.weight_smooth line 559
  25. def OAI.CubicTorus.CenteredJacobiChart.weightedValue line 562
  26. def OAI.CubicTorus.CenteredJacobiChart.weightedGradient line 565
  27. lemma OAI.CubicTorus.CenteredJacobiChart.hasPlanarWeakGradient line 569
  28. lemma OAI.CubicTorus.CenteredJacobiChart.weighted_weak_gradient line 581
  29. lemma OAI.CubicTorus.CenteredJacobiChart.representatives_ae line 597
  30. theorem OAI.CubicTorus.CenteredJacobiChart.weighted_divergence line 616
  31. theorem OAI.CubicTorus.cmc_weak_continuous_C1 line 662
  32. def OAI.CubicTorus.planeSlopeClamp line 707
  33. lemma OAI.CubicTorus.planeSlopeClamp_continuous line 709
  34. lemma OAI.CubicTorus.planeSlopeClamp_norm line 713
  35. lemma OAI.CubicTorus.planeSlopeClamp_eq line 718
  36. lemma OAI.CubicTorus.smooth_cmc_coefficient_lipschitz line 721
  37. theorem OAI.CubicTorus.CenteredJacobiChart.continuous_representative_C1 line 742
  38. lemma OAI.CubicTorus.sibling_continuous_indicator_positive_piece line 824