Commutator of the bilinear form with a cutoff

Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2 differentiates the equation without cutting off, because his interior H² theorem asks only u ∈ H¹(U). The interior H² estimate here quantifies its solution over H₀¹(Ω), and ∂_ℓu has no boundary condition, so the induction runs on ξ·∂_ℓu and pays a commutator.

This file computes it. Each block of Op.fullBilin is expanded on the cut-off element, one entry at a time, and every term either matches the differentiated equation tested against ξv or becomes an L² pairing against v.

Principal entry

∂ᵢ(ξ·∂_ℓu) is (∂ᵢξ)(∂_ℓu) + ξ(∂ᵢ∂_ℓu), so the entry splits in two.

• The term with ξ keeps its derivative on the solution. Writing ξ∂ⱼv = ∂ⱼ(ξv) - (∂ⱼξ)v turns it into the differentiated equation tested against ξv, plus a pairing.
• The term with ∂ᵢξ keeps its derivative on the test function, and has to be integrated by parts. It is admissible because ∂ᵢξ is supported in W, which is EllipticPdes.Regularity.setIntegral_mul_mulTest_partialD.

Nothing here is specific to the operator: the coefficient enters as a bounded measurable weight and the second derivative of the solution enters as a weak derivative on W. The entries are supplied as classes with their defining almost-everywhere descriptions, so the caller names its own and no product is constructed twice.

Main declarations

• mul_eq_self_of_eqOn_one: a cutoff that is one where a weight lives is invisible.
• setIntegral_principal_entry: one entry of the principal block, expanded.
• setIntegral_principal_entry_coeff: the same at the operator's coefficient, in the shape the datum pairs against.
• setIntegral_lower_entry: one entry of a block with no derivative on the test function.
• setIntegral_blocks_eq: all three blocks, as the shapes the datum names.

Open collar the identifications use

theorem EllipticPdes.Regularity.CutoffTower.exists_isOpen_collar {d : ℕ} {Ω V : Set (EuclideanSpace ℝ (Fin d))} (T : CutoffTower Ω V) : ∃ (N : Set (EuclideanSpace ℝ (Fin d))), IsOpen N ∧ tsupport T.ξ ⊆ N ∧ N ⊆ tsupport T.θ ∧ Set.EqOn T.θ 1 N

Open collar around the middle cutoff. There is an open N with tsupport ξ ⊆ N ⊆ tsupport θ on which θ is identically 1.

Every identification the induction step makes holds only after a cutoff, and N is where the cutoff is invisible. Running the differentiated equation on N rather than on the compact tsupport θ is what lets the inductive hypothesis's own family supply every derivative: the first derivatives it names agree with the ambient element's gradient coordinates almost everywhere on N, which is enough for both to be weak derivatives of one class there.

theorem EllipticPdes.Regularity.mul_eq_self_of_eqOn_one {d : ℕ} {χ : EuclideanSpace ℝ (Fin d) → ℝ} {S : Set (EuclideanSpace ℝ (Fin d))} (hχ : Set.EqOn χ 1 S) {ψ : EuclideanSpace ℝ (Fin d) → ℝ} (hψ : tsupport ψ ⊆ S) (x : EuclideanSpace ℝ (Fin d)) : χ x * ψ x = ψ x

Invisibility of a cutoff that is one where the weight lives. Every identification the induction step makes holds only after a cutoff, and every weight it pairs against is supported where that cutoff is identically one, so the cutoff never reaches the conclusion.

theorem EllipticPdes.Regularity.setIntegral_principal_entry {d : ℕ} {Ω W : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (hWm : MeasurableSet W) {ξ : EuclideanSpace ℝ (Fin d) → ℝ} (hξW : Sobolev.IsTestFn W ξ) (a : EuclideanSpace ℝ (Fin d) → ℝ) {Uamb : Sobolev.H1amb Ω} {p Dgi : Sobolev.L2D W} (i j : Fin d) (hgrad : (extendL2 hΩm) (Uamb.ofLp i.succ) = (extendL2 hWm) ((mulTest ⋯) p + (mulTest hξW) Dgi)) (Aip : Sobolev.L2D W) (hAip : ↑↑Aip =ᵐ[MeasureTheory.volume.restrict W] fun (x : EuclideanSpace ℝ (Fin d)) => a x * ↑↑p x) (dAip : Sobolev.L2D W) (hdAip : HasWeakDerivOn W j Aip dAip) (Aig : Sobolev.L2D W) (hAig : ↑↑Aig =ᵐ[MeasureTheory.volume.restrict W] fun (x : EuclideanSpace ℝ (Fin d)) => a x * ↑↑Dgi x) {v : EuclideanSpace ℝ (Fin d) → ℝ} (hvc : ContDiff ℝ (↑⊤) v) : ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, a x * ↑↑(Uamb.ofLp i.succ) x * Sobolev.partialD j v x = ((∫ (x : EuclideanSpace ℝ (Fin d)) in W, ↑↑Aig x * Sobolev.partialD j (fun (y : EuclideanSpace ℝ (Fin d)) => ξ y * v y) x) - ∫ (x : EuclideanSpace ℝ (Fin d)) in W, ↑↑Aig x * (Sobolev.partialD j ξ x * v x)) - ∫ (x : EuclideanSpace ℝ (Fin d)) in W, (Sobolev.partialD j (Sobolev.partialD i ξ) x * ↑↑Aip x + Sobolev.partialD i ξ x * ↑↑dAip x) * v x

One entry of the principal block of the cut-off element. With Uamb an ambient element whose i-th gradient coordinate is (∂ᵢξ)·p + ξ·(∂ᵢp), the entry ∫_Ω a·(∂ᵢ(ξp))·∂ⱼv splits into the differentiated equation's principal term tested against ξv, a pairing coming from ξ∂ⱼv = ∂ⱼ(ξv) - (∂ⱼξ)v, and the integration by parts of the term in which the derivative landed on the cutoff.

Aip is the class of a·p, dAip its weak j-derivative on W, and Aig the class of a·∂ᵢp. Only dAip needs the coefficient to be differentiable, and it enters as a hypothesis rather than as a construction, so this statement is free of every coefficient bundle.

theorem EllipticPdes.Regularity.setIntegral_principal_entry_coeff {d : ℕ} (Op : Sobolev.FullEllipticOp d) {Ω N : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (hNm : MeasurableSet N) {ξ : EuclideanSpace ℝ (Fin d) → ℝ} (hξN : Sobolev.IsTestFn N ξ) {k : ℕ} (hA : IsWkInftyCoeff Op.toEllipticCoeff (k + 1)) {Uamb : Sobolev.H1amb Ω} {p : Sobolev.L2D N} {D2 : Fin d → Sobolev.L2D N} (i j : Fin d) (hgrad : (extendL2 hΩm) (Uamb.ofLp i.succ) = (extendL2 hNm) ((mulTest ⋯) p + (mulTest hξN) (D2 i))) (hpD : ∀ (m : Fin d), HasWeakDerivOn N m p (D2 m)) {v : EuclideanSpace ℝ (Fin d) → ℝ} (hvc : ContDiff ℝ (↑⊤) v) : ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, Op.a x i j * ↑↑(Uamb.ofLp i.succ) x * Sobolev.partialD j v x = ((((∫ (x : EuclideanSpace ℝ (Fin d)) in N, Op.a x i j * ↑↑(D2 i) x * Sobolev.partialD j (fun (y : EuclideanSpace ℝ (Fin d)) => ξ y * v y) x) - ∫ (x : EuclideanSpace ℝ (Fin d)) in N, Sobolev.partialD j ξ x * (Op.a x i j * ↑↑(D2 i) x) * v x) - ∫ (x : EuclideanSpace ℝ (Fin d)) in N, Sobolev.partialD j (Sobolev.partialD i ξ) x * (Op.a x i j * ↑↑p x) * v x) - ∫ (x : EuclideanSpace ℝ (Fin d)) in N, Sobolev.partialD i ξ x * (hA.D [j] i j x * ↑↑p x) * v x) - ∫ (x : EuclideanSpace ℝ (Fin d)) in N, Sobolev.partialD i ξ x * (Op.a x i j * ↑↑(D2 j) x) * v x

One entry of the principal block in the shape the datum pairs against. The general entry is instantiated at the operator's coefficient, its weak derivative is supplied by the W^{k,∞} bundle through the Leibniz rule, and the three integrals it returns are split into the five the datum names.

The first is the differentiated equation's principal term tested against ξv, with the second derivative in the order the gradient of the cut-off derivative produces it. The other four are pairings, and each is one of the datum's shapes.

theorem EllipticPdes.Regularity.setIntegral_lower_entry {d : ℕ} {Ω W : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (hWm : MeasurableSet W) (F : Sobolev.L2D Ω) (G : Sobolev.L2D W) (hFG : (extendL2 hΩm) F = (extendL2 hWm) G) (a v : EuclideanSpace ℝ (Fin d) → ℝ) : ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, a x * ↑↑F x * v x = ∫ (x : EuclideanSpace ℝ (Fin d)) in W, a x * ↑↑G x * v x

One entry of a block with no derivative on the test function. The transport and zeroth-order blocks need no integration by parts: the entry is already an L² pairing, and only the gradient formula and the move down to W are used.

theorem EllipticPdes.Regularity.setIntegral_blocks_eq {d : ℕ} (Op : Sobolev.FullEllipticOp d) {Ω N : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (hNm : MeasurableSet N) {ξ : EuclideanSpace ℝ (Fin d) → ℝ} (hξN : Sobolev.IsTestFn N ξ) {k m : ℕ} (hA : IsWkInftyCoeff Op.toEllipticCoeff (k + 1)) (hbc : IsWkInftyLower Op m) {Uamb : Sobolev.H1amb Ω} {p : Sobolev.L2D N} {D2 : Fin d → Sobolev.L2D N} (hgrad : ∀ (i : Fin d), (extendL2 hΩm) (Uamb.ofLp i.succ) = (extendL2 hNm) ((mulTest ⋯) p + (mulTest hξN) (D2 i))) (hU0N : (extendL2 hΩm) (Uamb.ofLp 0) = (extendL2 hNm) ((mulTest hξN) p)) (hpD : ∀ (i : Fin d), HasWeakDerivOn N i p (D2 i)) {v : EuclideanSpace ℝ (Fin d) → ℝ} (hvc : ContDiff ℝ (↑⊤) v) : ((∑ i : Fin d, ∑ j : Fin d, ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, Op.a x i j * ↑↑(Uamb.ofLp i.succ) x * Sobolev.partialD j v x) + ∑ i : Fin d, ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, Op.b x i * ↑↑(Uamb.ofLp i.succ) x * v x) + ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, Op.c x * ↑↑(Uamb.ofLp 0) x * v x = (((((((∑ i : Fin d, ∑ j : Fin d, ∫ (x : EuclideanSpace ℝ (Fin d)) in N, Op.a x i j * ↑↑(D2 i) x * Sobolev.partialD j (fun (y : EuclideanSpace ℝ (Fin d)) => ξ y * v y) x) - ∑ i : Fin d, ∑ j : Fin d, ∫ (x : EuclideanSpace ℝ (Fin d)) in N, Sobolev.partialD j ξ x * (Op.a x i j * ↑↑(D2 i) x) * v x) - ∑ i : Fin d, ∑ j : Fin d, ∫ (x : EuclideanSpace ℝ (Fin d)) in N, Sobolev.partialD j (Sobolev.partialD i ξ) x * (Op.a x i j * ↑↑p x) * v x) - ∑ i : Fin d, ∑ j : Fin d, ∫ (x : EuclideanSpace ℝ (Fin d)) in N, Sobolev.partialD i ξ x * (hA.D [j] i j x * ↑↑p x) * v x) - ∑ i : Fin d, ∑ j : Fin d, ∫ (x : EuclideanSpace ℝ (Fin d)) in N, Sobolev.partialD i ξ x * (Op.a x i j * ↑↑(D2 j) x) * v x) + ∑ i : Fin d, ∫ (x : EuclideanSpace ℝ (Fin d)) in N, Sobolev.partialD i ξ x * (Op.b x i * ↑↑p x) * v x) + ∑ i : Fin d, ∫ (x : EuclideanSpace ℝ (Fin d)) in N, ξ x * (Op.b x i * ↑↑(D2 i) x) * v x) + ∫ (x : EuclideanSpace ℝ (Fin d)) in N, ξ x * (Op.c x * ↑↑p x) * v x

Three blocks of the bilinear form on the cut-off element. Summing the principal entry over both directions and adding the transport and zeroth-order blocks, which need no integration by parts, gives the whole pairing as eight sums, each of them a shape the datum of the induction step names.

The first sum is the differentiated equation's principal term tested against ξv, with the second derivative in the order the gradient produces it. Everything else is a pairing against v.