MeasureProductEnergy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Energy product identity for compact measure-source constructions

The actual bounded Sobolev product satisfies the integration-by-parts identity needed to multiply a local measure Laplacian by a cutoff.

theorem OAI.RegularPointCoordinates.bounded_gamma_integrable line 23

theorem OAI.RegularPointCoordinates.energy_bounded_product line 31

Source documentation

Integrating the genuine carré-du-champ product rule.

theorem energy_bounded_product (f g h : SobolevSpace μ hQ) (C D : ℝ≥0)
    (hf : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ f x| ≤ C)
    (hg : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ g x| ≤ D) :
    energyForm μ hQ (SobolevSpace.product μ hQ f g C D) h =
      (∫ x, SobolevSpace.toLp μ hQ f x * localGamma μ hQ g h x ∂μ) +
      (∫ x, SobolevSpace.toLp μ hQ g x * localGamma μ hQ f h x ∂μ) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.SobolevSpace.product, OAI.RegularPointCoordinates.localGamma

theorem OAI.RegularPointCoordinates.gamma_weight_comm line 43

theorem OAI.RegularPointCoordinates.energy_product_integration_by_parts line 49

Source documentation

The two cross terms needed for the full signed cutoff source.

theorem energy_product_integration_by_parts (f g h : SobolevSpace μ hQ) (C D H : ℝ≥0)
    (hf : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ f x| ≤ C)
    (hg : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ g x| ≤ D)
    (hh : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ h x| ≤ H) :
    energyForm μ hQ (SobolevSpace.product μ hQ f g C D) h =
      energyForm μ hQ f (SobolevSpace.product μ hQ g h D H) +
      energyForm μ hQ g (SobolevSpace.product μ hQ f h C H) -
      2 * ∫ x, SobolevSpace.toLp μ hQ h x * localGamma μ hQ f g x ∂μ := by
…