OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ClassicalResidualPairing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

An actual differential residual controls the mixed bounded-potential form against every weak-H1 state, without restricting its smoothness.

  1. theorem OAI.ContinuumCoulomb.h1Coordinates_complex_inner line 15
  2. theorem OAI.ContinuumCoulomb.h1Coordinates_complex_mass_inner line 20
  3. theorem OAI.ContinuumCoulomb.boundedPotential_complex_pairing line 26
  4. theorem OAI.ContinuumCoulomb.classical_residual_pairing line 42
  5. theorem OAI.ContinuumCoulomb.residual_integral_square_bound line 113