LaplacianCoordinateForm.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Pointwise linear representatives of the actual finite Laplacian map

def OAI.RegularPointCoordinates.laplacianCoordinateForm line 18
Source documentation
Evaluation of the finitely many L² source coordinates defines a pointwise linear form without choosing representatives for each direction.
```
def laplacianCoordinateForm (D : Euclidean m →L[ℝ] Lp ℝ 2 μ) (x : X) :
    Euclidean m →ₗ[ℝ] ℝ :=
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.laplacianCoordinateForm_apply line 23
theorem OAI.RegularPointCoordinates.laplacianCoordinateForm_rep line 29

theorem OAI.RegularPointCoordinates.laplacianCoordinateForm_square line 53

Source documentation

The source of an actual squared direction is the exact linear source correction used by the shifted quadratic-perturbation argument.

theorem laplacianCoordinateForm_square
    (U : Euclidean m →L[ℝ] SobolevSpace μ hQ) (D : Euclidean m →L[ℝ] Lp ℝ 2 μ)
    (hD : ∀ a, IsWeakLaplacian μ hQ (U a) (D a))
    (w z : Euclidean m) (A L : ℝ≥0)
    (hA : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (U w) x|≤A)
    (hL : ∀ᵐ x ∂μ, localGamma μ hQ (U w) (U w) x≤(L:ℝ)^2)
    (hz : U z=SobolevSpace.product μ hQ (U w) (U w) A A) :
    ∀ᵐ x ∂μ, laplacianCoordinateForm μ D x z =
      2*SobolevSpace.toLp μ hQ (U w) x*laplacianCoordinateForm μ D x w+
        2*localGamma μ hQ (U w) (U w) x := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.product, OAI.RegularPointCoordinates.laplacianCoordinateForm