OAI/Geometry/PrescribedPotential/VariablePoisson.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Variable Poisson.

  1. def OAI.SobolevChart.secondH2Symbol line 20
  2. lemma OAI.SobolevChart.secondH2Symbol_temperate line 24
  3. lemma OAI.SobolevChart.secondH2Symbol_bound line 29
  4. def OAI.SobolevChart.secondH2SymbolBCF line 49
  5. lemma OAI.SobolevChart.secondH2SymbolBCF_norm line 54
  6. def OAI.SobolevChart.secondH2 line 60
  7. lemma OAI.SobolevChart.secondH2_bound line 62
  8. lemma OAI.SobolevChart.secondH2_distribution line 67
  9. def OAI.SobolevChart.perturbation line 84
  10. def OAI.SobolevChart.perturbationBound line 87
  11. lemma OAI.SobolevChart.perturbationBound_nonneg line 91
  12. lemma OAI.SobolevChart.perturbation_bound line 96
  13. lemma OAI.SobolevChart.perturbation_distribution line 112
  14. lemma OAI.FrozenPoisson.perturbation_resolvent_bound line 132
  15. def OAI.FrozenPoisson.localResolvent line 147
  16. lemma OAI.FrozenPoisson.localResolvent_equation line 156
  17. lemma OAI.FrozenPoisson.fixed_for_perturbed line 180
  18. lemma OAI.FrozenPoisson.perturbed_unique line 195
  19. lemma OAI.FrozenPoisson.localResolvent_bound line 221
  20. theorem OAI.FrozenPoisson.variable_sobolev_resolvent line 243