OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarLocalization.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Actual compact localization on the planar Sobolev graph. Multiplication by a compactly supported C¹ function is constructed on L² classes and their gradients, then factored through the proved supported Rellich inclusion.

  1. structure OAI.ContinuumCoulomb.PlanarSobolev.BoundedLinearField line 25
  2. theorem OAI.ContinuumCoulomb.PlanarSobolev.BoundedLinearField.memLp line 32
  3. def OAI.ContinuumCoulomb.PlanarSobolev.BoundedLinearField.applyLp line 41
  4. theorem OAI.ContinuumCoulomb.PlanarSobolev.BoundedLinearField.applyLp_ae line 45
  5. def OAI.ContinuumCoulomb.PlanarSobolev.BoundedLinearField.linear line 49
  6. def OAI.ContinuumCoulomb.PlanarSobolev.BoundedLinearField.operator line 65
  7. theorem OAI.ContinuumCoulomb.PlanarSobolev.test_norm_bounded line 76
  8. theorem OAI.ContinuumCoulomb.PlanarSobolev.test_grad_bounded line 79
  9. def OAI.ContinuumCoulomb.PlanarSobolev.testNormBound line 82
  10. theorem OAI.ContinuumCoulomb.PlanarSobolev.testNormBound_spec line 84
  11. def OAI.ContinuumCoulomb.PlanarSobolev.testGradBound line 87
  12. theorem OAI.ContinuumCoulomb.PlanarSobolev.testGradBound_spec line 89
  13. def OAI.ContinuumCoulomb.PlanarSobolev.testScalarField line 92
  14. def OAI.ContinuumCoulomb.PlanarSobolev.testGradientField line 102
  15. def OAI.ContinuumCoulomb.PlanarSobolev.testTargetMultiplier line 111
  16. def OAI.ContinuumCoulomb.PlanarSobolev.testProduct line 116
  17. theorem OAI.ContinuumCoulomb.PlanarSobolev.testProduct_grad line 119
  18. theorem OAI.ContinuumCoulomb.PlanarSobolev.testTargetMultiplier_graph line 127
  19. theorem OAI.ContinuumCoulomb.PlanarSobolev.testTargetMultiplier_mem line 160
  20. def OAI.ContinuumCoulomb.PlanarSobolev.testSobolevMultiplier line 170
  21. def OAI.ContinuumCoulomb.PlanarSobolev.testLocalizedL2 line 173
  22. theorem OAI.ContinuumCoulomb.PlanarSobolev.testLocalizedL2_ae line 176
  23. theorem OAI.ContinuumCoulomb.PlanarSobolev.mem_extendByZero_range line 180
  24. theorem OAI.ContinuumCoulomb.PlanarSobolev.testSobolevMultiplier_supported line 197
  25. def OAI.ContinuumCoulomb.PlanarSobolev.testSupportedMultiplier line 205
  26. theorem OAI.ContinuumCoulomb.PlanarSobolev.testLocalizedL2_compact line 209
  27. def OAI.ContinuumCoulomb.PlanarSobolev.wellTest line 213
  28. theorem OAI.ContinuumCoulomb.PlanarSobolev.wellTest_operator line 216
  29. theorem OAI.ContinuumCoulomb.PlanarSobolev.wellMultiplier_compact line 225