HeatSquarePairing.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The heat-square pairing identity

The weak square rule identifies the derivative contributed by the moving heat weight. All squares and Laplacians below are actual L² elements.

theorem OAI.RegularPointCoordinates.heat_square_inner_laplacian line 22

Source documentation

Move the heat generator from a weight to a bounded Sobolev square.

theorem heat_square_inner_laplacian (u : SobolevSpace μ hQ) (d : Lp ℝ 2 μ)
    (C L : ℝ≥0) (hu : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ u x| ≤ C)
    (hg : ∀ᵐ x ∂μ, SobolevSpace.minimalSlope μ hQ u x ≤ L)
    (hd : IsWeakLaplacian μ hQ u d) (w : Lp ℝ 2 μ) (s : ℝ) (hs : 0 < s) :
    inner ℝ (-heatGeneratorAt μ hQ s w)
        (boundedLpSquare μ (SobolevSpace.toLp μ hQ u) C C.coe_nonneg hu) =
      2*∫ x, heatAt μ hQ s w x*(SobolevSpace.toLp μ hQ u x*d x+
        (SobolevSpace.minimalSlope μ hQ u x)^2) ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.heatGeneratorAt, OAI.RegularPointCoordinates.boundedLpSquare, OAI.RegularPointCoordinates.heatAt