LocalBochnerDensityProduct.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The pointwise density consequence of the full Bochner product identity

theorem OAI.RegularPointCoordinates.signed_rnDeriv_local_product line 19

Source documentation

Taking the density of the full local identity retains its exact Hessian term. Singular mass remains present in the original identity.

theorem signed_rnDeriv_local_product (Sg Sh Sz : SignedMeasure X)
    (G H : X →ᵇ ℝ) {h : X → ℝ} (hh : Integrable h μ)
    {S : Set X} (hS : MeasurableSet S)
    (he : Sz.restrict S=(signedSourceWeight Sh G+signedSourceWeight Sg H+
      (2 : ℝ) • μ.withDensityᵥ h).restrict S) :
    Sz.rnDeriv μ =ᵐ[μ.restrict S] fun x =>
      G x*Sh.rnDeriv μ x+H x*Sg.rnDeriv μ x+2*h x := by
…

Mentions: OAI.RegularPointCoordinates.signedSourceWeight