Interior H² estimate for a weak solution in H¹

Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 1 (p. 327): for a^{ij} ∈ C¹(U), b^i, c ∈ L^∞(U), f ∈ L²(U) and a weak solution u ∈ H¹(U) of L u = f, u ∈ H²_loc(U) with ‖u‖_{H²(V)} ≤ C (‖f‖_{L²(U)} + ‖u‖_{L²(U)}) for V ⋐ U.

The statement here asks nothing of u at the boundary. It is read off the H₀¹ estimate interior_H2_estimate through the cutoff reduction: for η equal to 1 near V and supported in Ω, the element η U ∈ H₀¹(Ω) solves an equation whose datum redDatum pairs f, U₀ and the gradient of U against weights supported in tsupport η, and the cutoff is invisible on V. The gradient enters the datum only through ζ ∇U for a cutoff ζ equal to 1 on tsupport η (exists_norm_redDatum_le), and exists_norm_mulTest_grad_le, the Caccioppoli estimate, bounds that by ‖f‖ + ‖U₀‖. The right-hand side is then Evans's.

Main declarations

• exists_norm_redDatum_le: the bound on the reduction datum.
• interior_H2_estimate_W12: Theorem 1.

theorem EllipticPdes.Regularity.norm_double_sum_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {m : ℕ} (T : Fin m → Fin m → Sobolev.L2D Ω) (K : Fin m → Fin m → ℝ) (N : ℝ) (h : ∀ (i j : Fin m), ‖T i j‖ ≤ K i j * N) : ‖∑ i : Fin m, ∑ j : Fin m, T i j‖ ≤ (∑ i : Fin m, ∑ j : Fin m, K i j) * N

theorem EllipticPdes.Regularity.norm_single_sum_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {m : ℕ} (T : Fin m → Sobolev.L2D Ω) (K : Fin m → ℝ) (N : ℝ) (h : ∀ (i : Fin m), ‖T i‖ ≤ K i * N) : ‖∑ i : Fin m, T i‖ ≤ (∑ i : Fin m, K i) * N

theorem EllipticPdes.Regularity.norm_six_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (a b c e g h : Sobolev.L2D Ω) : ‖a - b - c - e - g + h‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖e‖ + ‖g‖ + ‖h‖

theorem EllipticPdes.Regularity.weightL_coeFn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {c ψ : EuclideanSpace ℝ (Fin d) → ℝ} (hcm : Measurable c) {M : ℝ} (hc : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |c x| ≤ M) (hψ : Continuous ψ) (hψcs : HasCompactSupport ψ) (g : Sobolev.L2D Ω) : ↑↑((weightL Ω hcm hc hψ hψcs) g) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => c x * ψ x * ↑↑g x

The weight of weightL, read almost everywhere.

theorem EllipticPdes.Regularity.weightL_mulTest_eq {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {c ψ ζ : EuclideanSpace ℝ (Fin d) → ℝ} (hcm : Measurable c) {M : ℝ} (hc : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |c x| ≤ M) (hψ : Continuous ψ) (hψcs : HasCompactSupport ψ) (hζ : Sobolev.IsTestFn Ω ζ) (hζψ : Set.EqOn ζ 1 (tsupport ψ)) (g : Sobolev.L2D Ω) : (weightL Ω hcm hc hψ hψcs) ((mulTest hζ) g) = (weightL Ω hcm hc hψ hψcs) g

Invisibility of a cutoff under a weight it is one on. For ζ = 1 on tsupport ψ, multiplying by ζ before weightL changes nothing.

theorem EllipticPdes.Regularity.exists_norm_redDatum_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (Op : Sobolev.FullEllipticOp d) (D : CoeffWeakGrad Op.toEllipticCoeff) {η : EuclideanSpace ℝ (Fin d) → ℝ} (hη : Sobolev.IsTestFn Ω η) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ {ζ : EuclideanSpace ℝ (Fin d) → ℝ} (hζ : Sobolev.IsTestFn Ω ζ), Set.EqOn ζ 1 (tsupport η) → ∀ (U : Sobolev.H1amb Ω) (f : Sobolev.L2D Ω), ‖redDatum Op D hη U f‖ ≤ K * (‖f‖ + (‖U.ofLp 0‖ + ∑ i : Fin d, ‖(mulTest hζ) (U.ofLp i.succ)‖))

Bound on the reduction datum. For a cutoff ζ equal to 1 on tsupport η, ‖F‖ ≤ K (‖f‖ + ‖U₀‖ + Σ ‖ζ ∂_i U‖), with K depending on the coefficients and η alone. The gradient of U enters only where η lives, which is what lets the Caccioppoli estimate remove it.

theorem EllipticPdes.Regularity.cutoffMul_zero_ae {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {η : EuclideanSpace ℝ (Fin d) → ℝ} (hη : Sobolev.IsTestFn Ω η) (U : Sobolev.H1amb Ω) : ↑↑(((cutoffMul hη) U).ofLp 0) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => η x * ↑↑(U.ofLp 0) x

The function coordinate of η U is η U₀.

theorem EllipticPdes.Regularity.cutoffMul_succ_ae {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {η : EuclideanSpace ℝ (Fin d) → ℝ} (hη : Sobolev.IsTestFn Ω η) (U : Sobolev.H1amb Ω) (i : Fin d) : ↑↑(((cutoffMul hη) U).ofLp i.succ) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => η x * ↑↑(U.ofLp i.succ) x + Sobolev.partialD i η x * ↑↑(U.ofLp 0) x

The gradient coordinates of η U are η U_{i+1} + ∂_i η U₀.

theorem EllipticPdes.Regularity.restrictL2_extendL2_cutoffMul {d : ℕ} {Ω V : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (hVm : MeasurableSet V) (hVΩ : V ⊆ Ω) {η : EuclideanSpace ℝ (Fin d) → ℝ} (hη : Sobolev.IsTestFn Ω η) (hη1 : ∀ᶠ (x : EuclideanSpace ℝ (Fin d)) in nhdsSet V, η x = 1) (U : Sobolev.H1amb Ω) (j : Fin (d + 1)) : restrictL2 ((extendL2 hΩm) (((cutoffMul hη) U).ofLp j)) = restrictL2 ((extendL2 hΩm) (U.ofLp j))

Invisibility of the cutoff where it is one. If η = 1 near V ⊆ Ω, every coordinate of η U, cut down to V, is the same coordinate of U.

theorem EllipticPdes.Regularity.interior_H2_estimate_W12 {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩo : IsOpen Ω) (hA : IsC1Coeff Op.toEllipticCoeff) {V : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hVc : IsCompact V) (hVΩ : V ⊆ Ω) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (U : Sobolev.H1amb Ω) (f : Sobolev.L2D Ω), IsLocalWeakSolution Op Ω U f → ∀ (k i : Fin (n + 1)), ∃ (wki : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict V))), HasWeakDerivOn V k (restrictL2 ((extendL2 ⋯) (U.ofLp i.succ))) wki ∧ ‖wki‖ ≤ C * (‖f‖ + ‖U.ofLp 0‖)

Interior H² estimate for a weak solution in H¹(Ω) (Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 1, p. 327). For C¹ principal coefficients with a bounded derivative and a local weak solution U ∈ W12 Ω of L U = f on an open Ω, with no boundary condition, each gradient coordinate of U has every weak first derivative on a compact V ⊆ Ω, bounded by C (‖f‖ + ‖U₀‖) with C quantified before U and f.