Interior H² estimate

The capstone of the interior regularity chain. This file passes to the limit in the uniform difference-quotient bound of EllipticPdes.Regularity.Interior.NormBound to produce the second weak derivative, then assembles the coordinates into the interior H² estimate.

This module keeps the import path EllipticPdes.Regularity.Interior and re-exports the whole chain, so dependents see the same API as before the file was split.

Main declarations

• interior_secondWeakDeriv: existence of the interior second weak derivative.
• HasWeakDerivOn: the region-restricted weak derivative.
• interior_H2_estimate: the interior H² estimate.

Existence of the second weak derivative

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

Existence of the interior second weak derivative (Evans §6.3.1, VIII.2.1). For each (k, i) there is a constant Cd, fixed before the solution and the datum, such that for every weak solution u of L u = f the whole-space extension of ζ · ∂ᵢu has an L² weak k-derivative w with ‖w‖ ≤ Cd (‖f‖ + ‖u₀‖): this is the weak-limit converse weakDeriv_of_diffQuot_bounded fed with the uniform difference-quotient bound interior_diffQuot_norm_bound. Because ζ ≡ 1 on V, the restriction of w to V is ∂ₖ∂ᵢu there.

Assembly of the interior H² estimate

def EllipticPdes.Regularity.HasWeakDerivOn {d : ℕ} (V : Set (EuclideanSpace ℝ (Fin d))) (k : Fin d) (g g' : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict V))) : Prop

Weak derivative on an open region. g' is the weak k-derivative of g on V if the integration by parts identity is satisfied against every test function in V. This is the V-restricted analogue of HasWeakDeriv, and is the L²-level statement of ∂ₖ g = g' on V.

Equations

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

theorem EllipticPdes.Regularity.hasWeakDerivOn_of_hasWeakDeriv {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} (k : Fin d) {g w : ↥(MeasureTheory.EucL2 d)} (h : HasWeakDeriv k g w) : HasWeakDerivOn V k (restrictL2 g) (restrictL2 w)

A whole-space weak derivative restricts to a weak derivative on any measurable V: test functions supported in V see only the restricted classes, and the whole-space integration-by-parts identity localises because both integrands vanish off V.

theorem EllipticPdes.Regularity.interior_H2_estimate {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)))} (hVc : IsCompact V) (hVΩ : 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 V))), HasWeakDerivOn V 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 (Evans, Partial Differential Equations (2nd ed.), §6.3.1; Gilbarg-Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 8.8). For a weak solution u ∈ H₀¹(Ω) of L u = f with W^{1,∞} principal coefficients, in the pointwise form of IsLipCoeff, and bounded transport and zeroth-order coefficients, and for any compact V ⋐ Ω, the second weak derivatives exist in L²(V) and are bounded by the data: for every direction pair (k, i) there is a weak k-derivative wki of ∂ᵢu on V (that is, ∂ₖ∂ᵢu ∈ L²(V)) with ‖∂ₖ∂ᵢu‖_{L²(V)} + ‖∂ᵢu‖_{L²(V)} + ‖u‖_{L²(V)} ≤ C (‖f‖ + ‖u‖). The constant is quantified before the solution and the datum, so it depends only on the data (λ, Λ, A₁, d, ‖b‖∞, ‖c‖∞, the cutoff tower for V ⋐ Ω) and on neither u nor f. This is the L²-level statement that u ∈ H²_loc(Ω) with the interior estimate.