H1FiniteProjection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Finite orbital penalties pass from compact tests to the complete weak-H1 domain without asking approximants to preserve exact orthogonality.

def OAI.ContinuumCoulomb.graphOrbitalMass line 13
theorem OAI.ContinuumCoulomb.graphOrbitalMass_continuous line 17
theorem OAI.ContinuumCoulomb.graphOrbitalMass_eq_zero line 23

theorem OAI.ContinuumCoulomb.boundedPotential_projection_lower_of_compact line 32

Source documentation

The finite projection term is continuous on the same graph as the kinetic and bounded potential terms.

theorem boundedPotential_projection_lower_of_compact
    (hpublished : PublishedSobolevSmoothDensity) {n : ℕ} {ι : Type*} [Fintype ι]
    (V : Configuration n → ℝ) (hV : Continuous V) (B : ℝ)
    (hB : ∀ x, |V x| ≤ B)
    (ψ : ι → Lp ℂ 2 (volume : Measure (Configuration n))) (E κ : ℝ)
    (hcompact : ∀ v : Coulomb.H1Vector n,
      (∀ s, ContDiff ℝ 1 (v.value s) ∧ HasCompactSupport (v.value s)) →
      (∀ s a x, v.gradient s a x =
        fderiv ℝ (v.value s) x (EuclideanSpace.single a 1)) →
      E*Coulomb.mass v - κ*graphOrbitalMass ψ (h1Coordinates v) ≤ boundedPotentialForm V v)
    (u : Coulomb.H1Vector n) :
    E*Coulomb.mass u - κ*graphOrbitalMass ψ (h1Coordinates u) ≤ boundedPotentialForm V u := by
…

Mentions: OAI.ContinuumCoulomb.PublishedSobolevSmoothDensity, OAI.ContinuumCoulomb.Configuration, OAI.Coulomb.H1Vector, OAI.Coulomb.mass, OAI.ContinuumCoulomb.graphOrbitalMass, OAI.ContinuumCoulomb.h1Coordinates, OAI.ContinuumCoulomb.boundedPotentialForm

theorem OAI.ContinuumCoulomb.boundedPotential_complement_lower_of_compact line 60