HarmonicQuadraticPotential.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The local equation for the square of a harmonic coordinate

theorem OAI.RegularPointCoordinates.bounded_cutoff_product_mem_dirichlet line 21

Source documentation

A bounded Sobolev function multiplied by an actual compact Lipschitz cutoff belongs to the canonical zero-boundary space.

theorem bounded_cutoff_product_mem_dirichlet (Ω : Set X)
    (c u : SobolevSpace μ hQ) (C D L : ℝ≥0)
    (χ : X → ℝ) (hχ : LipschitzWith L χ) (hcpt : HasCompactSupport χ)
    (hbound : ∀ x, |χ x| ≤ C) (hnonneg : ∀ x, 0 ≤ χ x)
    (hsupp : tsupport χ ⊆ Ω) (hcrep : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    (hu : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ u x| ≤ D) :
    SobolevSpace.product μ hQ c u C D ∈ SobolevSpace.dirichlet μ hQ Ω := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.product, OAI.RegularPointCoordinates.SobolevSpace.dirichlet

theorem OAI.RegularPointCoordinates.harmonic_half_square_energy line 44
Source documentation
The local distributional Laplacian of half the square of a harmonic coordinate is its actual energy density. No second-order input is used.
```
theorem harmonic_half_square_energy {Ω : Set X} (u φ : SobolevSpace μ hQ)
    (C D : ℝ≥0) (hu : IsSobolevHarmonicOn μ hQ Ω u)
    (hub : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ u x| ≤ C)
    (hφb : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ φ x| ≤ D)
    (hprod : SobolevSpace.product μ hQ u φ C D ∈ SobolevSpace.dirichlet μ hQ Ω) :
    energyForm μ hQ ((1 / 2 : ℝ) • SobolevSpace.square μ hQ u C) φ =
      -(∫ x, SobolevSpace.toLp μ hQ φ x * localGamma μ hQ u u x ∂μ) := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.product, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.SobolevSpace.square, OAI.RegularPointCoordinates.localGamma
def OAI.RegularPointCoordinates.coordinateQuadratic line 67
Source documentation
The actual Euclidean quadratic model associated to bounded harmonic coordinates. Its gradient is used to compare distance gradients.
```
def coordinateQuadratic {n : ℕ} (u : Fin n → SobolevSpace μ hQ) (C : ℝ≥0) :
    SobolevSpace μ hQ := ∑ j, (1 / 2 : ℝ) • SobolevSpace.square μ hQ (u j) C
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.square
theorem OAI.RegularPointCoordinates.coordinateQuadratic_energy line 70
theorem OAI.RegularPointCoordinates.coordinateQuadratic_representative line 97