Canonical Laplacian and the quantitative local harmonic energy bound.

theorem EulerMeanHarmonic.gradient_coordinate (f : EulerSmoothLimit.Space → ℝ) (x : EulerSmoothLimit.Space) (i : Fin 3) : (gradient f x).ofLp i = EulerVectorCalculus.partialDerivative f i x

theorem EulerMeanHarmonic.laplacian_eq_coordinate_sum (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (x : EulerSmoothLimit.Space) : Laplacian.laplacian f x = ∑ i : Fin 3, EulerVectorCalculus.partialDerivative (EulerVectorCalculus.partialDerivative f i) i x

theorem EulerMeanHarmonic.divergence_gradient_eq_laplacian (f : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.divergence (gradient f) x = Laplacian.laplacian f x

The Laplacian used in the harmonic argument is the canonical one.

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

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

The usual Caccioppoli inequality, with an explicit universal constant.