BoundedSquareLaplacian.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Constructing the L² Laplacian of a bounded Lipschitz square

theorem OAI.RegularPointCoordinates.exists_weakLaplacian_square line 18

Source documentation

A bounded function with bounded weak gradient has an actual L² square-Laplacian, with the exact carré-du-champ formula.

theorem exists_weakLaplacian_square (f : SobolevSpace μ hQ) (d : Lp ℝ 2 μ)
    (C L : ℝ≥0) (hf : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ f x| ≤ C)
    (hgrad : ∀ᵐ x ∂μ, SobolevSpace.minimalSlope μ hQ f x ≤ L)
    (hd : IsWeakLaplacian μ hQ f d) :
    ∃ q : Lp ℝ 2 μ, IsWeakLaplacian μ hQ (SobolevSpace.square μ hQ f C) q ∧
      (q =ᵐ[μ] fun x => 2*(SobolevSpace.toLp μ hQ f x*d x+
        (SobolevSpace.minimalSlope μ hQ f x)^2)) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.SobolevSpace.square