QuadraticLocalEnergy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Local form of the distance-model energy identity

theorem OAI.RegularPointCoordinates.cutoff_integral_local line 17
theorem OAI.RegularPointCoordinates.cutoff_gradient_integral_local line 29

theorem OAI.RegularPointCoordinates.coordinateQuadratic_local_difference_energy line 43

Source documentation

All terms in the cutoff identity are supported in the same working region. In particular the value error only needs to be small there.

theorem coordinateQuadratic_local_difference_energy {n : ℕ} {Ω : Set X}
    (u : Fin n → SobolevSpace μ hQ) (C D E L : ℝ≥0)
    (hu : ∀ j, IsSobolevHarmonicOn μ hQ Ω (u j))
    (hub : ∀ j, ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (u j) x| ≤ C)
    (c q : SobolevSpace μ hQ) (χ : X → ℝ)
    (hχ : LipschitzWith L χ) (hcpt : HasCompactSupport χ)
    (hbound : ∀ x, |χ x| ≤ E) (hnonneg : ∀ x, 0 ≤ χ x)
    (hsupp : tsupport χ ⊆ Ω) (hcrep : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    (hw : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (q - coordinateQuadratic μ hQ u C) x| ≤ D) :
    let H := coordinateQuadratic μ hQ u C
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.coordinateQuadratic