OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedHigherMoments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The spatial moments needed to control the finite-slab operator residual. All moments refer to the actual normalized orbital density.

  1. theorem OAI.ContinuumCoulomb.polynomial_exponential_bound line 12
  2. theorem OAI.ContinuumCoulomb.normalizedPlanarMode_norm_moment_integrable line 29
  3. theorem OAI.ContinuumCoulomb.localizedDensity_even_moment_integrable line 63
  4. theorem OAI.ContinuumCoulomb.localizedDensity_fourth_moment_integrable line 86
  5. theorem OAI.ContinuumCoulomb.localizedDensity_eighth_moment_integrable line 90
  6. theorem OAI.ContinuumCoulomb.localizedDensity_twentyFourth_moment_integrable line 96

    Source documentation

    This moment absorbs the polynomial growth of the finite slab's global potential bound when the horizontal radius is the fourth power of its thickness.

    theorem localizedDensity_twentyFourth_moment_integrable {freq : ℝ} (hfreq : 0 < freq) :
    Integrable (fun x : Position => ‖x‖^24*localizedDensity freq 0 x) :=
…

    Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.localizedDensity

  7. theorem OAI.ContinuumCoulomb.localizedDensity_seventySecond_moment_integrable line 102

    Source documentation

    A wider horizontal slab is needed for simultaneous nuclear cubature and compressed-energy accuracy. This moment absorbs its polynomial growth.

    theorem localizedDensity_seventySecond_moment_integrable {freq : ℝ} (hfreq : 0 < freq) :
    Integrable (fun x : Position => ‖x‖^72*localizedDensity freq 0 x) :=
…

    Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.localizedDensity