RegularBochnerMeasureLaplacian.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The local measure Laplacian of a regular Gram entry

theorem OAI.RegularPointCoordinates.regularBochner_measure_laplacian line 21

Source documentation

Local Sobolev representatives of the Laplacians turn the common Bochner identity into the full distributional equation for each Gram entry. Global derivatives of the chosen extensions are not required.

theorem regularBochner_measure_laplacian (K : ℝ)
    (U : Euclidean m →L[ℝ] SobolevSpace μ hQ) (D : Euclidean m →L[ℝ] Lp ℝ 2 μ)
    (H : Euclidean m →ₗ[ℝ] Euclidean m →ₗ[ℝ] SobolevSpace μ hQ)
    (L : Euclidean m → ℝ≥0)
    (hU : ∀ a, ∀ᵐ x ∂μ, SobolevSpace.minimalSlope μ hQ (U a) x≤L a)
    (hsym : ∀ a b, H a b=H b a)
    {Ω : Set X} (hΩ : MeasurableSet Ω) (M : PositiveBilinearMeasure X (Euclidean m))
    (hM : ∀ (a : Euclidean m) (ψ : SobolevSpace μ hQ) (q : X →ᵇ ℝ),
      HasCompactSupport (q : X → ℝ) → tsupport q ⊆ Ω →
      SobolevSpace.toLp μ hQ ψ =ᵐ[μ] q →
      (∫ x, q x ∂M.measure a)=regularBochnerForm μ hQ K U D H q ψ L hU a a)
    (a b : Euclidean m) (da db : SobolevSpace μ hQ)
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.regularBochnerForm