OAI/Geometry/PrescribedPotential/LocalRegularity.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Local Regularity.

  1. lemma OAI.SobolevChart.schwartz_distribution_injective line 21
  2. def OAI.SobolevChart.schwartzCoord line 30
  3. lemma OAI.SobolevChart.realize_schwartzCoord line 33
  4. lemma OAI.SobolevChart.schwartzCoord_add line 37
  5. lemma OAI.SobolevChart.schwartzCoord_sum line 42
  6. lemma OAI.SobolevChart.weak_deriv_comm line 48
  7. lemma OAI.SobolevChart.schwartz_deriv_comm line 55
  8. lemma OAI.SobolevChart.summable_of_contracting_recurrence line 66
  9. def OAI.FrozenPoisson.schwartzResolvent line 91
  10. lemma OAI.FrozenPoisson.schwartzResolvent_distribution line 95
  11. lemma OAI.FrozenPoisson.schwartzCoord_resolvent line 101
  12. lemma OAI.FrozenPoisson.weak_deriv_resolvent line 109
  13. lemma OAI.FrozenPoisson.schwartz_deriv_resolvent line 119
  14. lemma OAI.SobolevChart.schwartz_product_distribution line 133
  15. def OAI.SobolevChart.schwartzWord line 145
  16. def OAI.SobolevChart.weakWord line 149
  17. lemma OAI.SobolevChart.word_distribution line 153
  18. abbrev OAI.SobolevChart.SmoothCoefficients line 163
  19. def OAI.SobolevChart.coefficientBCF line 166
  20. def OAI.SobolevChart.coefficientDeriv line 169
  21. def OAI.SobolevChart.smoothPerturbation line 172
  22. lemma OAI.SobolevChart.smoothPerturbation_apply line 178
  23. lemma OAI.SobolevChart.smoothPerturbation_distribution line 184
  24. lemma OAI.SobolevChart.schwartzCoord_perturbation line 200
  25. lemma OAI.SobolevChart.smoothPerturbation_bound line 208
  26. lemma OAI.SobolevChart.schwartz_deriv_perturbation line 215
  27. def OAI.SobolevChart.commutatorTerms line 239
  28. lemma OAI.SobolevChart.commutatorTerms_order line 247
  29. lemma OAI.SobolevChart.list_sum_add line 259
  30. lemma OAI.SobolevChart.schwartz_word_perturbation line 265
  31. lemma OAI.FrozenPoisson.schwartz_word_resolvent line 293
  32. def OAI.FrozenPoisson.schwartzNeumann line 304
  33. lemma OAI.FrozenPoisson.schwartzResolvent_bound line 308
  34. lemma OAI.FrozenPoisson.schwartzNeumann_bound line 317
  35. lemma OAI.FrozenPoisson.schwartz_word_neumann line 330
  36. lemma OAI.SobolevChart.schwartzCoord_zero line 347
  37. lemma OAI.SobolevChart.schwartzCoord_list_sum line 351
  38. lemma OAI.SobolevChart.summable_norm_schwartzCoord_list line 357
  39. def OAI.FrozenPoisson.schwartzIterate line 378
  40. lemma OAI.FrozenPoisson.schwartzIterate_succ line 382
  41. lemma OAI.FrozenPoisson.summable_norm_neumann_of line 387
  42. theorem OAI.FrozenPoisson.neumann_summable_word line 397
  43. lemma OAI.SobolevChart.memSobolev_word_of_summable line 425
  44. lemma OAI.SobolevChart.memSobolev_even_of_words line 435
  45. def OAI.FrozenPoisson.neumannSum line 457
  46. lemma OAI.FrozenPoisson.schwartzCoord_neumann line 461
  47. lemma OAI.FrozenPoisson.neumannSum_fixed line 470
  48. lemma OAI.FrozenPoisson.equation_of_fixed line 487
  49. lemma OAI.FrozenPoisson.neumannSum_eq_localResolvent line 503
  50. theorem OAI.FrozenPoisson.localResolvent_schwartz_memSobolev line 521