Outer cutoff tower and second derivatives near tsupport ξ

Higher interior regularity (Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2) runs the interior H² estimate a second time, on the cutoff derivative ξ · ∂_ℓu rather than on u. The commutator terms it produces are supported inside tsupport ξ of the first tower, so the second run needs its own tower, based at that compact set rather than at the original V, together with the second derivatives of u there.

Both follow from what the interior H² chain already provides. tsupport ξ is compact and sits inside Ω, so cutoffTowerOfIsCompactSubsetIsOpen builds the outer tower, and interior_secondWeakDeriv and interior_H2_estimate apply at that compact set verbatim.

Main declarations

• outerCutoffTower: a cutoff tower based at tsupport T.ξ.
• outer_secondWeakDeriv: the interior second derivatives at the outer tower, as whole-space EucL2 d classes with one constant covering every direction pair.
• interior_H2_estimate_near_tsupport_xi: the interior H² estimate on tsupport T.ξ.

Outer tower

noncomputable def EllipticPdes.Regularity.outerCutoffTower {d : ℕ} {Ω V : Set (EuclideanSpace ℝ (Fin d))} (hΩo : IsOpen Ω) (T : CutoffTower Ω V) : CutoffTower Ω (tsupport T.ξ)

Outer cutoff tower. A tower based at the compact set tsupport T.ξ of a given tower T. Its innermost cutoff is identically 1 on tsupport T.ξ (CutoffTower.zeta_eqOn_one), which is what makes it invisible to every term of the differentiated equation.

Equations

• EllipticPdes.Regularity.outerCutoffTower hΩo T = EllipticPdes.Regularity.cutoffTowerOfIsCompactSubsetIsOpen ⋯ hΩo ⋯

Second derivatives at the outer tower

theorem EllipticPdes.Regularity.outer_secondWeakDeriv {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (Op : Sobolev.FullEllipticOp d) (hΩm : MeasurableSet Ω) (hΩo : IsOpen Ω) (hA : IsLipCoeff Op.toEllipticCoeff) {V : Set (EuclideanSpace ℝ (Fin d))} (T : CutoffTower Ω V) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : ↥(Sobolev.H01 Ω)) (f : Sobolev.L2D Ω), (∀ (w : ↥(Sobolev.H01 Ω)), ((Op.fullBilin Ω) u) w = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑f x * ↑↑((↑w).ofLp 0) x) → ∀ (k i : Fin d), ∃ (w : ↥(MeasureTheory.EucL2 d)), HasWeakDeriv k ((extendL2 hΩm) ((mulTest ⋯) ((↑u).ofLp i.succ))) w ∧ ‖w‖ ≤ C * (‖f‖ + ‖(↑u).ofLp 0‖)

Interior second derivatives at the outer tower. For every direction pair (k, i) the whole-space extension of ζ' · ∂ᵢu, with ζ' the innermost cutoff of the outer tower, has an L² weak k-derivative bounded by the data, with a single constant covering the whole index square. The constant is quantified before the solution and the datum, so it depends only on the operator and the tower. This is interior_secondWeakDeriv at outerCutoffTower, with the per-pair constants collected into one.

theorem EllipticPdes.Regularity.interior_H2_estimate_near_tsupport_xi {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩm : MeasurableSet Ω) (hΩo : IsOpen Ω) (hA : IsLipCoeff Op.toEllipticCoeff) {V : Set (EuclideanSpace ℝ (Fin (n + 1)))} (T : CutoffTower Ω V) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : ↥(Sobolev.H01 Ω)) (f : Sobolev.L2D Ω), (∀ (w : ↥(Sobolev.H01 Ω)), ((Op.fullBilin Ω) u) w = ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, ↑↑f x * ↑↑((↑w).ofLp 0) x) → ∀ (k i : Fin (n + 1)), ∃ (wki : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict (tsupport T.ξ)))), HasWeakDerivOn (tsupport T.ξ) k (restrictL2 ((extendL2 hΩm) ((↑u).ofLp i.succ))) wki ∧ ‖wki‖ + ‖restrictL2 ((extendL2 hΩm) ((↑u).ofLp i.succ))‖ + ‖restrictL2 ((extendL2 hΩm) ((↑u).ofLp 0))‖ ≤ C * (‖f‖ + ‖(↑u).ofLp 0‖)

Interior H² estimate on tsupport T.ξ. The middle cutoff of a tower has compact support inside Ω, so the interior H² estimate applies at that set: the second weak derivatives of u exist in L²(tsupport T.ξ) and are bounded by the data. This is the regularity of u the differentiated equation consumes on the region where the cutoff commutators live.