OAI/Geometry/PrescribedPotential/SmoothDistributions.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Smooth Distributions.

  1. lemma OAI.SobolevChart.temperate_fderiv line 20
  2. def OAI.SobolevChart.directionDerivative line 25
  3. lemma OAI.SobolevChart.temperate_directionDerivative line 28
  4. lemma OAI.SobolevChart.temperateDistribution_eq_smul_volume line 34
  5. lemma OAI.SobolevChart.temperateDistribution_sub line 42
  6. lemma OAI.SobolevChart.temperateDistribution_schwartz line 50
  7. lemma OAI.SobolevChart.temperateDistribution_bounded line 55
  8. lemma OAI.SobolevChart.temperate_schwartz_integrable line 60
  9. lemma OAI.SobolevChart.temperateDistribution_derivative line 67
  10. lemma OAI.SobolevChart.temperateDistribution_eq_zero_iff line 85
  11. lemma OAI.SobolevChart.temperateDistribution_injective line 102