OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarModeJets.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform derivatives through order four of the manufactured planar orbital. Derivatives are transferred to its fixed compact forcing.

  1. theorem OAI.ContinuumCoulomb.forcing_jet_compact line 12
  2. theorem OAI.ContinuumCoulomb.planar_mode_jet_transfer line 18
  3. theorem OAI.ContinuumCoulomb.planar_mode_jets_bounded line 46
  4. theorem OAI.ContinuumCoulomb.normalized_planar_mode_jets_bounded line 71