OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/BoundedPotentialOperator.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual bounded real multiplication potentials on the weak-H1 graph.

  1. theorem OAI.ContinuumCoulomb.BoundedPotential.product_memLp line 17
  2. def OAI.ContinuumCoulomb.BoundedPotential.value line 26
  3. theorem OAI.ContinuumCoulomb.BoundedPotential.value_ae line 30
  4. def OAI.ContinuumCoulomb.BoundedPotential.linear line 34
  5. def OAI.ContinuumCoulomb.BoundedPotential.operator line 52
  6. theorem OAI.ContinuumCoulomb.BoundedPotential.operator_ae line 61
  7. theorem OAI.ContinuumCoulomb.BoundedPotential.operator_pairing line 64
  8. def OAI.ContinuumCoulomb.boundedPotentialForm line 72
  9. theorem OAI.ContinuumCoulomb.boundedPotentialForm_eq_graph line 75
  10. theorem OAI.ContinuumCoulomb.boundedPotential_lower_of_compact line 90