SobolevDensityInput.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The Sobolev density input for conditional estimates

N. G. Meyers and J. Serrin, H = W, Proc. Natl. Acad. Sci. USA 51 (1964), 1055–1056, DOI 10.1073/pnas.51.6.1055, Theorem and the Lemma on p.1056. We use only m=1, p=2 on the full Euclidean configuration space. The finite spin index is handled componentwise. This is smooth approximation in the value-and-weak-gradient norm; no compact support or Coulomb-form comparison is included in the assumption.

def OAI.ContinuumCoulomb.h1GraphError line 22
Source documentation
Squared error in the actual value-and-gradient graph.
```
def h1GraphError {n : ℕ} (u v : Coulomb.H1Vector n) : ℝ :=
…
```
Mentions: OAI.Coulomb.H1Vector
theorem OAI.ContinuumCoulomb.h1GraphError_nonnegative line 26
def OAI.ContinuumCoulomb.PublishedSobolevSmoothDensity line 35
Source documentation
The precise specialization of the published H=W theorem.
```
def PublishedSobolevSmoothDensity : Prop :=
…
```

theorem OAI.ContinuumCoulomb.exists_smooth_h1_approximation line 45

Source documentation

A convenient actual-H1 version, preserving the published input explicitly.

theorem exists_smooth_h1_approximation (hpublished : PublishedSobolevSmoothDensity)
    {n : ℕ} (u : Coulomb.H1Vector n) {ε : ℝ} (hε : 0 < ε) :
    ∃ v : Coulomb.H1Vector n,
      (∀ s, ContDiff ℝ (⊤ : ℕ∞) (v.value s)) ∧
      (∀ s a x, v.gradient s a x =
        fderiv ℝ (v.value s) x (EuclideanSpace.single a 1)) ∧
      h1GraphError u v < ε := by
…

Mentions: OAI.ContinuumCoulomb.PublishedSobolevSmoothDensity, OAI.Coulomb.H1Vector, OAI.ContinuumCoulomb.h1GraphError