OAI/Geometry/PrescribedPotential/StrongSobolevEmbedding.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Strong Sobolev Embedding.

  1. def OAI.SobolevChart.boundedToLinfLinear line 20
  2. lemma OAI.SobolevChart.boundedToLinf_norm line 25
  3. def OAI.SobolevChart.boundedToLinf line 31
  4. lemma OAI.SobolevChart.boundedToLinf_injective line 34
  5. def OAI.SobolevChart.boundedDistributionCLM line 42
  6. lemma OAI.SobolevChart.boundedDistributionCLM_apply line 45
  7. lemma OAI.SobolevChart.boundedDistribution_injective line 48
  8. lemma OAI.SobolevChart.strong_representation line 52
  9. def OAI.SobolevChart.strongRepresentative line 58
  10. lemma OAI.SobolevChart.strongRepresentative_distribution line 61
  11. def OAI.SobolevChart.strongRepresentativeLinear line 65
  12. def OAI.SobolevChart.strongEmbedding line 76
  13. lemma OAI.SobolevChart.strongEmbedding_distribution line 90
  14. lemma OAI.SobolevChart.strongEmbedding_norm line 94