Caccioppoli (interior energy) estimate

The first-derivative interior estimate: for a weak solution of L u = f, the energy ∫_V |∇u|² is bounded by the data on a slightly larger set W. Obtained by testing the weak formulation with ζ² u, using uniform ellipticity from below and Young's inequality to absorb the gradient term. See Gilbarg-Trudinger, Elliptic PDE of Second Order, Theorem 8.8, and Evans, Partial Differential Equations (2nd ed.), §6.3.1.

Cutoff-multiplication keystone

The test function ζ² u for u ∈ H₀¹(Ω) is not directly available from the graph encoding of Sobolev/Basic.lean. We build it here. For a smooth compactly supported cutoff η (an [IsTestFn]) we assemble the cutoff-multiplication operator on the ambient graph space,

(cutoffMul η U)₀ = η · U₀, (cutoffMul η U)_{i+1} = η · U_{i+1} + (∂ᵢη) · U₀,

which is exactly the Leibniz rule ∇(η u) = η ∇u + (∇η) u. It is a bounded operator, it sends the graph of a test function φ to the graph of the product η φ, hence by closure it maps H₀¹(Ω) into itself: [cutoffMul_mem_H01].

Global sup bounds for a test function and its partials

theorem EllipticPdes.Regularity.exists_abs_bound {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω φ) : ∃ (M : ℝ), ∀ (x : EuclideanSpace ℝ (Fin d)), |φ x| ≤ M

A smooth compactly supported function is globally bounded in absolute value.

theorem EllipticPdes.Regularity.exists_abs_bound_partialD {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω φ) (i : Fin d) : ∃ (M : ℝ), ∀ (x : EuclideanSpace ℝ (Fin d)), |Sobolev.partialD i φ x| ≤ M

Each partial derivative of a test function is globally bounded in absolute value.

Multiplier actions of a cutoff on L²(Ω)

noncomputable def EllipticPdes.Regularity.mulTest {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {η : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω η) : Sobolev.L2D Ω →L[ℝ] Sobolev.L2D Ω

Multiplication by the cutoff η on L²(Ω), as a continuous linear map.

Equations

• EllipticPdes.Regularity.mulTest h = EllipticPdes.Sobolev.mulCoeffL ⋯ ⋯

noncomputable def EllipticPdes.Regularity.mulTestPartial {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {η : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω η) (i : Fin d) : Sobolev.L2D Ω →L[ℝ] Sobolev.L2D Ω

Multiplication by the partial ∂ᵢη of the cutoff on L²(Ω), continuous linear map.

Equations

• EllipticPdes.Regularity.mulTestPartial h i = EllipticPdes.Sobolev.mulCoeffL ⋯ ⋯

theorem EllipticPdes.Regularity.mulTest_coeFn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {η : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω η) (g : Sobolev.L2D Ω) : ↑↑((mulTest h) g) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => η x * ↑↑g x

The a.e. representative of mulTest: mulTest h g =ᵐ x ↦ η x · g x.

theorem EllipticPdes.Regularity.mulTestPartial_coeFn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {η : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω η) (i : Fin d) (g : Sobolev.L2D Ω) : ↑↑((mulTestPartial h i) g) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => Sobolev.partialD i η x * ↑↑g x

The a.e. representative of mulTestPartial: mulTestPartial h i g =ᵐ x ↦ ∂ᵢη x · g x.

Cutoff-multiplication operator on the graph space

noncomputable def EllipticPdes.Regularity.cutoffMul {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {η : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω η) : Sobolev.H1amb Ω →L[ℝ] Sobolev.H1amb Ω

The cutoff-multiplication operator cutoffMul η : H1amb Ω →L H1amb Ω, encoding the Leibniz rule ∇(η u) = η ∇u + (∇η) u: coordinate 0 multiplies by η, coordinate i+1 sends U to η · U_{i+1} + (∂ᵢη) · U₀.

Equations

• One or more equations did not get rendered due to their size.

theorem EllipticPdes.Regularity.cutoffMul_apply_zero {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {η : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω η) (U : Sobolev.H1amb Ω) : ((cutoffMul h) U).ofLp 0 = (mulTest h) (U.ofLp 0)

Coordinate 0 of cutoffMul: (cutoffMul η U)₀ = η · U₀.

theorem EllipticPdes.Regularity.cutoffMul_apply_succ {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {η : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω η) (U : Sobolev.H1amb Ω) (i : Fin d) : ((cutoffMul h) U).ofLp i.succ = (mulTest h) (U.ofLp i.succ) + (mulTestPartial h i) (U.ofLp 0)

Coordinate i+1 of cutoffMul: (cutoffMul η U)_{i+1} = η · U_{i+1} + (∂ᵢη) · U₀.

Leibniz product rule and stability of test functions under products

theorem EllipticPdes.Regularity.partialD_mul {d : ℕ} {η φ : EuclideanSpace ℝ (Fin d) → ℝ} (hη : Differentiable ℝ η) (hφ : Differentiable ℝ φ) (i : Fin d) : (Sobolev.partialD i fun (x : EuclideanSpace ℝ (Fin d)) => η x * φ x) = fun (x : EuclideanSpace ℝ (Fin d)) => η x * Sobolev.partialD i φ x + Sobolev.partialD i η x * φ x

The classical Leibniz rule for the i-th partial of a product: ∂ᵢ(η φ) = η ∂ᵢφ + (∂ᵢη) φ.

theorem EllipticPdes.Regularity.isTestFn_mul {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {η φ : EuclideanSpace ℝ (Fin d) → ℝ} (hη : Sobolev.IsTestFn Ω η) (hφ : Sobolev.IsTestFn Ω φ) : Sobolev.IsTestFn Ω fun (x : EuclideanSpace ℝ (Fin d)) => η x * φ x

The pointwise product of two test functions is a test function: smoothness is ContDiff.mul, the support of the product sits inside tsupport φ ⊆ Ω, and compact support is inherited from φ.

Cutoff multiplication sending a graph to the product graph

theorem EllipticPdes.Regularity.cutoffMul_testGraph {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {η φ : EuclideanSpace ℝ (Fin d) → ℝ} (hη : Sobolev.IsTestFn Ω η) (hφ : Sobolev.IsTestFn Ω φ) : (cutoffMul hη) hφ.testGraph = ⋯.testGraph

Keystone (graphs). The cutoff-multiplication operator sends the graph of a test function φ to the graph of the product η φ: cutoffMul η (graph φ) = graph (η φ). This is the Leibniz rule realised at the level of L² classes, and it is what lets cutoffMul extend from test functions to H₀¹(Ω) by closure.

Preservation of H₀¹(Ω) under cutoff multiplication

theorem EllipticPdes.Regularity.cutoffMul_mem_H01 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {η : EuclideanSpace ℝ (Fin d) → ℝ} (hη : Sobolev.IsTestFn Ω η) {U : Sobolev.H1amb Ω} (hU : U ∈ Sobolev.H01 Ω) : (cutoffMul hη) U ∈ Sobolev.H01 Ω

Keystone (membership). The cutoff-multiplication operator maps H₀¹(Ω) into itself. Since cutoffMul η is continuous and sends every test-function graph into H₀¹(Ω) (by [cutoffMul_testGraph]), it maps the closure H₀¹(Ω) into the closed set H₀¹(Ω).

Weighted energy lower bound from ellipticity

theorem EllipticPdes.Regularity.energy_ge {d : ℕ} (A : Sobolev.EllipticCoeff d) {Ω : Set (EuclideanSpace ℝ (Fin d))} (g : Fin d → Sobolev.L2D Ω) : A.lam * ∑ i : Fin d, ‖g i‖ ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, inner ℝ ((A.actL i j) (g i)) (g j)

Ellipticity energy bound for an arbitrary L² gradient family. The lower bound of [EllipticCoeff.bilin_self_ge] uses only the L² classes, not the weak-gradient relation, so it holds for any family g : Fin d → L²(Ω): λ ∑ᵢ ‖gᵢ‖² ≤ ∑ᵢⱼ ⟪aᵢⱼ gᵢ, gⱼ⟫. Applied to gᵢ = ζ · ∂ᵢu this is the cutoff-weighted energy lower bound λ ∫_Ω ζ² |∇u|² ≤ ∫_Ω ζ² ∑ᵢⱼ aᵢⱼ ∂ᵢu ∂ⱼu driving the Caccioppoli estimate (Evans, PDE 2nd ed., §6.3.1).

Operator-norm bounds and regrouping identities for the cutoff

theorem EllipticPdes.Regularity.norm_mulTest_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {η : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω η) (g : Sobolev.L2D Ω) : ‖(mulTest h) g‖ ≤ ⋯.choose * ‖g‖

Operator-norm bound for the cutoff multiplier: ‖η · g‖ ≤ ‖η‖∞ · ‖g‖.

theorem EllipticPdes.Regularity.norm_mulTestPartial_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {η : EuclideanSpace ℝ (Fin d) → ℝ} (h : Sobolev.IsTestFn Ω η) (i : Fin d) (g : Sobolev.L2D Ω) : ‖(mulTestPartial h i) g‖ ≤ ⋯.choose * ‖g‖

Operator-norm bound for the partial-cutoff multiplier: ‖∂ᵢη · g‖ ≤ ‖∂ᵢη‖∞ · ‖g‖.

theorem EllipticPdes.Regularity.actL_mulTest_regroup {d : ℕ} (A : Sobolev.EllipticCoeff d) {Ω : Set (EuclideanSpace ℝ (Fin d))} {ζ : EuclideanSpace ℝ (Fin d) → ℝ} (hζ : Sobolev.IsTestFn Ω ζ) (i j : Fin d) (p q : Sobolev.L2D Ω) : inner ℝ ((A.actL i j) ((mulTest hζ) p)) ((mulTest hζ) q) = inner ℝ ((A.actL i j) p) ((mulTest ⋯) q)

Regrouping one ζ factor across the coefficient action, principal part: ⟪aᵢⱼ (ζ p), ζ q⟫ = ⟪aᵢⱼ p, ζ² q⟫.

theorem EllipticPdes.Regularity.actL_cross_regroup {d : ℕ} (A : Sobolev.EllipticCoeff d) {Ω : Set (EuclideanSpace ℝ (Fin d))} {ζ : EuclideanSpace ℝ (Fin d) → ℝ} (hζ : Sobolev.IsTestFn Ω ζ) (i j : Fin d) (p q : Sobolev.L2D Ω) : inner ℝ ((A.actL i j) p) ((mulTestPartial ⋯ j) q) = 2 * inner ℝ ((A.actL i j) ((mulTest hζ) p)) ((mulTestPartial hζ j) q)

Regrouping the cross term: moving one ζ off ∂ⱼ(ζ²) = 2 ζ ∂ⱼζ onto p, ⟪aᵢⱼ p, ∂ⱼ(ζ²) q⟫ = 2 ⟪aᵢⱼ (ζ p), ∂ⱼζ q⟫.

Interior energy (Caccioppoli) estimate

theorem EllipticPdes.Regularity.caccioppoli_cross_transport_bound {d : ℕ} (Op : Sobolev.FullEllipticOp d) {Ω : Set (EuclideanSpace ℝ (Fin d))} {ζ : EuclideanSpace ℝ (Fin d) → ℝ} (hζ : Sobolev.IsTestFn Ω ζ) : have A := Op.toEllipticCoeff; have Z := ⋯.choose; have SW := ∑ j : Fin d, ⋯.choose; SW = ∑ j : Fin d, ⋯.choose → have β := 2 * A.Λ * SW + Op.Bsup * Z; β = 2 * A.Λ * SW + Op.Bsup * Z → ∀ (U : Sobolev.H1amb Ω) (i : Fin d), 0 ≤ A.lam / 2 * ‖(mulTest hζ) (U.ofLp i.succ)‖ ^ 2 + β ^ 2 / (2 * A.lam) * ‖U.ofLp 0‖ ^ 2 + (∑ j : Fin d, inner ℝ ((A.actL i j) (U.ofLp i.succ)) ((mulTestPartial ⋯ j) (U.ofLp 0)) + inner ℝ ((Op.bAct i) (U.ofLp i.succ)) ((mulTest ⋯) (U.ofLp 0)))

Per-coordinate absorption of the principal cross term and transport term.

theorem EllipticPdes.Regularity.caccioppoli {d : ℕ} (Op : Sobolev.FullEllipticOp d) {Ω : Set (EuclideanSpace ℝ (Fin d))} {ζ : EuclideanSpace ℝ (Fin d) → ℝ} (hζ : Sobolev.IsTestFn Ω ζ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : ↥(Sobolev.H01 Ω)) (f : Sobolev.L2D Ω), (∀ (v : ↥(Sobolev.H01 Ω)), ((Op.fullBilin Ω) u) v = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑f x * ↑↑((↑v).ofLp 0) x) → Op.lam / 2 * ∑ i : Fin d, ‖(mulTest hζ) ((↑u).ofLp i.succ)‖ ^ 2 ≤ C * (‖f‖ ^ 2 + ‖(↑u).ofLp 0‖ ^ 2)

Interior energy (Caccioppoli) estimate. For a weak solution u ∈ H₀¹(Ω) of L u = f and a cutoff ζ (a test function), the cutoff-weighted gradient energy (λ/2) ∫_Ω ζ² |∇u|² is bounded by C · (‖f‖²_{L²} + ‖u₀‖²_{L²}). The constant is quantified before the solution and the datum, so it depends only on λ, Λ, ‖b‖∞, ‖c‖∞, ‖ζ‖∞, and ‖∇ζ‖∞. Testing the weak formulation with ζ² u (admissible by [cutoffMul_mem_H01]), the ellipticity lower bound [energy_ge] controls the principal part from below, and Cauchy-Schwarz together with the Peter-Paul (Young) inequality absorbs the cross, transport, zeroth-order, and right-hand terms into a (λ/2) ∫_Ω ζ² |∇u|² share. Since ζ ≡ 1 on an interior set V, this gives ‖∇u‖_{L²(V)} ≤ C' (‖f‖ + ‖u₀‖). See Gilbarg-Trudinger, Elliptic PDE of Second Order, Theorem 8.8, and Evans, Partial Differential Equations (2nd ed.), §6.3.1.

Guo, Partial Differential Equations (JHU AS.110.631-632), Lemma X.3.5 also has the name Caccioppoli, and is a different statement: it takes a non-negative subsolution Lv ≥ 0 of the principal part alone and bounds ∫ |∇(φv)|² by ‖∇φ‖²_∞ ∫ v², with no datum on the right. This statement takes a solution of Lu = f for the full operator, has f on the right, and imposes no sign condition, so neither implies the other. Gilbarg and Trudinger Theorem 8.8 remains the match, cited here rather than transcribed.