OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/BoundedFormCross.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Polarization of the actual bounded-potential quadratic form on the full weak-H1 graph.

  1. theorem OAI.ContinuumCoulomb.h1Coordinates_add line 13
  2. def OAI.ContinuumCoulomb.graphBoundedCross line 29
  3. theorem OAI.ContinuumCoulomb.graphBoundedForm_add line 35
  4. theorem OAI.ContinuumCoulomb.boundedPotential_operator_symmetric line 48
  5. theorem OAI.ContinuumCoulomb.boundedPotentialForm_add line 60
  6. theorem OAI.ContinuumCoulomb.Lp_real_inner_eq_re line 68
  7. def OAI.ContinuumCoulomb.graphComplexCross line 79
  8. theorem OAI.ContinuumCoulomb.re_finite_sum line 85
  9. theorem OAI.ContinuumCoulomb.graphBoundedCross_eq_re line 89