OAI/Geometry/PrescribedPotential/ParameterRegularity.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Parameter Regularity.

  1. def OAI.FrozenPoisson.ParameterRegularity.schwartzResolvent line 21
  2. lemma OAI.FrozenPoisson.ParameterRegularity.schwartzResolvent_distribution line 25
  3. lemma OAI.FrozenPoisson.ParameterRegularity.schwartzCoord_resolvent line 32
  4. lemma OAI.FrozenPoisson.ParameterRegularity.weak_deriv_resolvent line 40
  5. lemma OAI.FrozenPoisson.ParameterRegularity.schwartz_deriv_resolvent line 50
  6. lemma OAI.FrozenPoisson.ParameterRegularity.schwartz_word_resolvent line 58
  7. def OAI.FrozenPoisson.ParameterRegularity.schwartzNeumann line 69
  8. lemma OAI.FrozenPoisson.ParameterRegularity.schwartzResolvent_bound line 73
  9. lemma OAI.FrozenPoisson.ParameterRegularity.schwartzNeumann_bound line 82
  10. lemma OAI.FrozenPoisson.ParameterRegularity.schwartz_word_neumann line 95
  11. def OAI.FrozenPoisson.ParameterRegularity.schwartzIterate line 106
  12. lemma OAI.FrozenPoisson.ParameterRegularity.schwartzIterate_succ line 110
  13. lemma OAI.FrozenPoisson.ParameterRegularity.summable_norm_neumann_of line 115
  14. theorem OAI.FrozenPoisson.ParameterRegularity.neumann_summable_word line 125
  15. def OAI.FrozenPoisson.ParameterRegularity.neumannSum line 147
  16. lemma OAI.FrozenPoisson.ParameterRegularity.schwartzCoord_neumann line 151
  17. lemma OAI.FrozenPoisson.ParameterRegularity.neumannSum_fixed line 160
  18. lemma OAI.FrozenPoisson.ParameterRegularity.fixed_unique line 177
  19. lemma OAI.FrozenPoisson.ParameterRegularity.parameterLocal_fixed line 199
  20. lemma OAI.FrozenPoisson.ParameterRegularity.neumannSum_eq_local line 208
  21. theorem OAI.FrozenPoisson.ParameterRegularity.parameterLocal_schwartz_memSobolev line 224