Local energy identities for the harmonic part of the mean inverse

The mean inverse requires an interior L² estimate for a genuinely harmonic field. This file starts that argument with the classical localized energy identity, proved by ordinary-space integration by parts. No interior estimate or mean-value formula is assumed.

theorem EulerMeanHarmonic.gradient_mul {f g : EulerSmoothLimit.Space → ℝ} {x : EulerSmoothLimit.Space} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : gradient (f * g) x = g x • gradient f x + f x • gradient g x

theorem EulerMeanHarmonic.localized_gradient_identity (η h : EulerSmoothLimit.Space → ℝ) (hη : ContDiff ℝ (↑⊤) η) (hh : ContDiff ℝ (↑⊤) h) (x : EulerSmoothLimit.Space) : ‖gradient (η * h) x‖ ^ 2 = inner ℝ (gradient (η * (η * h)) x) (gradient h x) + h x ^ 2 * ‖gradient η x‖ ^ 2

theorem EulerMeanHarmonic.caccioppoli_identity (η h : EulerSmoothLimit.Space → ℝ) (hcη : HasCompactSupport η) (hη : ContDiff ℝ (↑⊤) η) (hh : ContDiff ℝ (↑⊤) h) (hharmonic : ∀ x ∈ tsupport η, EulerSmoothLimit.divergence (gradient h) x = 0) : ∫ (x : EulerSmoothLimit.Space), ‖gradient (η * h) x‖ ^ 2 = ∫ (x : EulerSmoothLimit.Space), h x ^ 2 * ‖gradient η x‖ ^ 2

Exact localized Dirichlet-energy identity for a classical harmonic scalar.