Quantitative cutoff energy estimates used in the three-dimensional interior bound.

theorem EulerMeanHarmonic.integrable_weighted_square (η h : EulerSmoothLimit.Space → ℝ) (hcη : HasCompactSupport η) (hη : Continuous η) (hh : Continuous h) : MeasureTheory.Integrable (fun (x : EulerSmoothLimit.Space) => η x ^ 2 * h x ^ 2) MeasureTheory.volume

theorem EulerMeanHarmonic.integrable_weighted_gradient_square (η h : EulerSmoothLimit.Space → ℝ) (hcη : HasCompactSupport η) (hη : Continuous η) (hh : ContDiff ℝ (↑⊤) h) : MeasureTheory.Integrable (fun (x : EulerSmoothLimit.Space) => η x ^ 2 * ‖gradient h x‖ ^ 2) MeasureTheory.volume

theorem EulerMeanHarmonic.integrable_square_gradient_cutoff (η h : EulerSmoothLimit.Space → ℝ) (hcη : HasCompactSupport η) (hη : ContDiff ℝ (↑⊤) η) (hh : Continuous h) : MeasureTheory.Integrable (fun (x : EulerSmoothLimit.Space) => h x ^ 2 * ‖gradient η x‖ ^ 2) MeasureTheory.volume

theorem EulerMeanHarmonic.gradient_eq_zero_off_support (η : EulerSmoothLimit.Space → ℝ) {x : EulerSmoothLimit.Space} (hx : x ∉ tsupport η) : gradient η x = 0

theorem EulerMeanHarmonic.cutoff_gradient_majorant (η ρ : EulerSmoothLimit.Space → ℝ) (C : ℝ) (hC : ∀ (x : EulerSmoothLimit.Space), ‖gradient η x‖ ≤ C) (hρ : ∀ x ∈ tsupport η, ρ x = 1) (x : EulerSmoothLimit.Space) : ‖gradient η x‖ ^ 2 ≤ C ^ 2 * ρ x ^ 2

theorem EulerMeanHarmonic.cutoff_square_majorant (η ρ : EulerSmoothLimit.Space → ℝ) (hη : ∀ (x : EulerSmoothLimit.Space), |η x| ≤ 1) (hρ : ∀ x ∈ tsupport η, ρ x = 1) (x : EulerSmoothLimit.Space) : η x ^ 2 ≤ ρ x ^ 2

theorem EulerMeanHarmonic.partialDerivative_sq_le_gradient_sq (h : EulerSmoothLimit.Space → ℝ) (i : Fin 3) (x : EulerSmoothLimit.Space) : EulerVectorCalculus.partialDerivative h i x ^ 2 ≤ ‖gradient h x‖ ^ 2

theorem EulerMeanHarmonic.caccioppoli_weighted_bound (η ρ h : EulerSmoothLimit.Space → ℝ) (C : ℝ) (hcη : HasCompactSupport η) (hη : ContDiff ℝ (↑⊤) η) (hh : ContDiff ℝ (↑⊤) h) (hharmonic : ∀ x ∈ tsupport η, Laplacian.laplacian h x = 0) (hi : MeasureTheory.Integrable (fun (x : EulerSmoothLimit.Space) => ρ x ^ 2 * h x ^ 2) MeasureTheory.volume) (hbound : ∀ (x : EulerSmoothLimit.Space), ‖gradient η x‖ ^ 2 ≤ C ^ 2 * ρ x ^ 2) : ∫ (x : EulerSmoothLimit.Space), η x ^ 2 * ‖gradient h x‖ ^ 2 ≤ 4 * C ^ 2 * ∫ (x : EulerSmoothLimit.Space), ρ x ^ 2 * h x ^ 2

A cutoff derivative estimate transports Caccioppoli to a larger weight.