OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/H1BoundedForm.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContinuumCoulomb.H1Coordinates line 12
2. def OAI.ContinuumCoulomb.graphMass line 14
3. def OAI.ContinuumCoulomb.graphKinetic line 17
4. theorem OAI.ContinuumCoulomb.h1Coordinates_norm_sq line 20
5. theorem OAI.ContinuumCoulomb.mass_eq_graphMass line 27
6. theorem OAI.ContinuumCoulomb.kinetic_eq_graphKinetic line 31
7. theorem OAI.ContinuumCoulomb.graphMass_continuous line 35
8. theorem OAI.ContinuumCoulomb.graphKinetic_continuous line 38
9. def OAI.ContinuumCoulomb.graphBoundedForm line 42
10. theorem OAI.ContinuumCoulomb.graphBoundedForm_continuous line 47
11. theorem OAI.ContinuumCoulomb.boundedForm_lower_of_compact line 55

    Source documentation

    A compact-test lower bound for an actual bounded L2 operator extends with the kinetic energy to the entire declared weak-H1 domain.

    theorem boundedForm_lower_of_compact (hpublished : PublishedSobolevSmoothDensity)
        {n : ℕ} (A : Lp ℂ 2 (volume : Measure (Configuration n)) →L[ℝ]
          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 ≤ graphBoundedForm A (h1Coordinates v))
        (u : Coulomb.H1Vector n) : E*Coulomb.mass u ≤ graphBoundedForm A (h1Coordinates u) := by
    …

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