OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarModeH1.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Membership of the manufactured mode in the closed planar Sobolev graph, obtained by expanding compact cutoffs.

  1. def OAI.ContinuumCoulomb.PlanarSobolev.cutoffBump line 19
  2. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoffBump_smooth line 21
  3. def OAI.ContinuumCoulomb.PlanarSobolev.cutoffScale line 23
  4. def OAI.ContinuumCoulomb.PlanarSobolev.cutoff line 25
  5. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoffScale_positive line 27
  6. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoffScale_le_one line 29
  7. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoffScale_tendsto line 34
  8. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoff_smooth line 38
  9. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoff_nonnegative line 41
  10. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoff_le_one line 43
  11. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoff_hasCompactSupport line 45
  12. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoff_tendsto line 57
  13. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoff_fderiv line 65
  14. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoff_grad line 74
  15. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoff_grad_tendsto line 78
  16. theorem OAI.ContinuumCoulomb.PlanarSobolev.bump_grad_bounded line 85
  17. def OAI.ContinuumCoulomb.PlanarSobolev.cutoffGradBound line 89
  18. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoffGradBound_spec line 91
  19. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoffGradBound_nonnegative line 94
  20. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoff_grad_bound line 97
  21. theorem OAI.ContinuumCoulomb.PlanarSobolev.mode_square_integrable line 104
  22. theorem OAI.ContinuumCoulomb.PlanarSobolev.mode_memLp line 108
  23. theorem OAI.ContinuumCoulomb.PlanarSobolev.grad_norm_sq line 112
  24. theorem OAI.ContinuumCoulomb.PlanarSobolev.mode_grad_square_integrable line 117
  25. theorem OAI.ContinuumCoulomb.PlanarSobolev.mode_grad_memLp line 124
  26. def OAI.ContinuumCoulomb.PlanarSobolev.cutoffMode line 129
  27. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoffMode_grad line 133
  28. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoffMode_grad_tendsto line 143
  29. theorem OAI.ContinuumCoulomb.PlanarSobolev.toLp_sub_norm_sq line 150
  30. theorem OAI.ContinuumCoulomb.PlanarSobolev.toLp_tendsto_of_integral_sub_sq line 161
  31. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoffMode_value_integral_tendsto line 174
  32. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoffMode_grad_integral_tendsto line 202
  33. def OAI.ContinuumCoulomb.PlanarSobolev.modeTarget line 243
  34. theorem OAI.ContinuumCoulomb.PlanarSobolev.cutoffMode_graph_tendsto line 246
  35. theorem OAI.ContinuumCoulomb.PlanarSobolev.modeTarget_mem line 256
  36. def OAI.ContinuumCoulomb.PlanarSobolev.mode line 264

    Source documentation

    The positive resolvent mode belongs to the closed H¹ graph.

    def mode : Sobolev := ⟨modeTarget, modeTarget_mem⟩
…

    Mentions: OAI.ContinuumCoulomb.PlanarSobolev.Sobolev, OAI.ContinuumCoulomb.PlanarSobolev.modeTarget, OAI.ContinuumCoulomb.PlanarSobolev.modeTarget_mem