OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarSobolev.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Closure of the actual manufactured-well inequality on the planar Sobolev graph. The bounded potential acts on actual L² classes, and the form is continuous in the function-and-gradient norm.

  1. def OAI.ContinuumCoulomb.PlanarSobolev.originalIntegral line 17
  2. abbrev OAI.ContinuumCoulomb.PlanarSobolev.originalMeasurable line 19
  3. abbrev OAI.ContinuumCoulomb.PlanarSobolev.originalBorel line 21
  4. def OAI.ContinuumCoulomb.PlanarSobolev.originalIntegrable line 23
  5. theorem OAI.ContinuumCoulomb.PlanarSobolev.planar_integrable_change_borel line 25
  6. theorem OAI.ContinuumCoulomb.PlanarSobolev.planar_integral_change_borel line 37
  7. abbrev OAI.ContinuumCoulomb.PlanarSobolev.Sobolev line 53
  8. abbrev OAI.ContinuumCoulomb.PlanarSobolev.Target line 56
  9. abbrev OAI.ContinuumCoulomb.PlanarSobolev.Test line 59
  10. theorem OAI.ContinuumCoulomb.PlanarSobolev.well_bounded line 62
  11. def OAI.ContinuumCoulomb.PlanarSobolev.wellBound line 66
  12. theorem OAI.ContinuumCoulomb.PlanarSobolev.wellBound_spec line 68
  13. theorem OAI.ContinuumCoulomb.PlanarSobolev.wellBound_nonnegative line 71
  14. theorem OAI.ContinuumCoulomb.PlanarSobolev.well_mul_memLp line 74
  15. def OAI.ContinuumCoulomb.PlanarSobolev.wellMultiply line 83
  16. theorem OAI.ContinuumCoulomb.PlanarSobolev.wellMultiply_ae line 87
  17. def OAI.ContinuumCoulomb.PlanarSobolev.wellMultiplyLinear line 91
  18. def OAI.ContinuumCoulomb.PlanarSobolev.wellMultiplier line 109
  19. def OAI.ContinuumCoulomb.PlanarSobolev.form line 118
  20. theorem OAI.ContinuumCoulomb.PlanarSobolev.form_continuous line 121
  21. theorem OAI.ContinuumCoulomb.PlanarSobolev.l2_norm_sq line 125
  22. theorem OAI.ContinuumCoulomb.PlanarSobolev.l2_real_norm_sq line 130
  23. theorem OAI.ContinuumCoulomb.PlanarSobolev.grad_coordinate line 136
  24. theorem OAI.ContinuumCoulomb.PlanarSobolev.graph_mass line 144
  25. theorem OAI.ContinuumCoulomb.PlanarSobolev.graph_kinetic line 152
  26. theorem OAI.ContinuumCoulomb.PlanarSobolev.graph_form line 171
  27. theorem OAI.ContinuumCoulomb.PlanarSobolev.form_lower line 194

    Source documentation

    The proved inequality survives closure in the actual Sobolev norm.

    theorem form_lower (u : Sobolev) :
    -(1 / 2 : ℝ) * ‖u.val.1‖ ^ 2 ≤ form u.val := by
…

    Mentions: OAI.ContinuumCoulomb.PlanarSobolev.Sobolev, OAI.ContinuumCoulomb.PlanarSobolev.form