OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ManufacturedOrbitalResidual.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The residual for the actual manufactured one-body operator is the sum of the checked off-site, finite-slab, and cutoff/counterterm residuals.

  1. def OAI.ContinuumCoulomb.manufacturedOrbitalResidual line 14
  2. theorem OAI.ContinuumCoulomb.manufacturedOrbitalResidual_eq line 19
  3. theorem OAI.ContinuumCoulomb.slab_residual_continuous line 32
  4. theorem OAI.ContinuumCoulomb.well_residual_continuous line 39
  5. theorem OAI.ContinuumCoulomb.manufacturedOrbitalResidual_memLp line 46
  6. theorem OAI.ContinuumCoulomb.manufacturedOrbitalResidual_square_integrable line 60
  7. def OAI.ContinuumCoulomb.manufacturedOrbitalSquaredError line 70

    Source documentation

    The seventy-second-moment tail keeps the residual compatible with the physical mesh scale even for high-aspect slabs.

    def manufacturedOrbitalSquaredError (rho H S freq δ D R : ℝ) {m : ℕ}
    (u : Fin m → PlanarPosition) (j : Fin m) : ℝ :=
…

    Mentions: OAI.ContinuumCoulomb.PlanarPosition

  8. theorem OAI.ContinuumCoulomb.manufacturedOrbitalResidual_square_bound line 80