Caccioppoli estimate for a weak solution in H¹

caccioppoli bounds the cutoff-weighted gradient energy of a weak solution in H₀¹(Ω) by ‖f‖² + ‖u‖². Its proof tests the equation with ζ² u, and that test function is admissible for a local weak solution U ∈ W12 Ω as well (cutoffMul_mem_H01_of_mem_W12), with the identity against it supplied by IsLocalWeakSolution.weakForm. Nothing else in the proof uses the boundary condition, so the statement holds for W12 solutions with the same constant.

This is the step Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 1 takes in the proof before (8) to replace ‖u‖_{H¹(U)} by ‖u‖_{L²(U)} on the right of the estimate.

Main declarations

• caccioppoli_W12: the energy estimate.
• exists_norm_mulTest_grad_le: its consequence for each gradient coordinate, with the norms unsquared.

theorem EllipticPdes.Regularity.caccioppoli_W12 {d : ℕ} (Op : Sobolev.FullEllipticOp d) {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩo : IsOpen Ω) {ζ : EuclideanSpace ℝ (Fin d) → ℝ} (hζ : Sobolev.IsTestFn Ω ζ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (U : Sobolev.H1amb Ω) (f : Sobolev.L2D Ω), IsLocalWeakSolution Op Ω U f → Op.lam / 2 * ∑ i : Fin d, ‖(mulTest hζ) (U.ofLp i.succ)‖ ^ 2 ≤ C * (‖f‖ ^ 2 + ‖U.ofLp 0‖ ^ 2)

Caccioppoli estimate for a weak solution in H¹. For a local weak solution U ∈ W12 Ω of L U = f on an open Ω, with no boundary condition, and a test function ζ of Ω, the cutoff-weighted gradient energy (λ/2) Σ ‖ζ ∂_i U‖² is bounded by C (‖f‖² + ‖U₀‖²), with C quantified before the solution and the datum. The proof is that of caccioppoli, with IsLocalWeakSolution.weakForm against ζ² U in place of the H₀¹ weak formulation.

theorem EllipticPdes.Regularity.le_sqrt_mul_of_sum_sq_le {ι : Type u_1} [Fintype ι] (g : ι → ℝ) (hg : ∀ (j : ι), 0 ≤ g j) {lam C0 a b : ℝ} (hlam : 0 < lam) (hC0 : 0 ≤ C0) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : lam / 2 * ∑ j : ι, g j ^ 2 ≤ C0 * (a ^ 2 + b ^ 2)) (i : ι) : g i ≤ √(2 * C0 / lam) * (a + b)

A term of a sum of squares, from a bound on the weighted sum, with the square root taken.

theorem EllipticPdes.Regularity.exists_norm_mulTest_grad_le {d : ℕ} (Op : Sobolev.FullEllipticOp d) {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩo : IsOpen Ω) {ζ : EuclideanSpace ℝ (Fin d) → ℝ} (hζ : Sobolev.IsTestFn Ω ζ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (U : Sobolev.H1amb Ω) (f : Sobolev.L2D Ω), IsLocalWeakSolution Op Ω U f → ∀ (i : Fin d), ‖(mulTest hζ) (U.ofLp i.succ)‖ ≤ C * (‖f‖ + ‖U.ofLp 0‖)

Cutoff gradient bounded by the function and the datum. Each gradient coordinate of a local weak solution, cut off by a test function ζ, is bounded in L²(Ω) by C (‖f‖ + ‖U₀‖): the square root of caccioppoli_W12.