Interior Hölder continuity of a weak solution

The interior H² estimate and the Morrey embedding are joined here, so that a weak solution of L u = f is shown to have a Hölder continuous representative on a ball compactly contained in the domain, with the Hölder constant controlled by ‖f‖ + ‖u‖.

Three dimensions are covered, each with Hölder exponent 1/2.

• d = 1. Morrey applies at p = 2 > 1 = d to the first-order weak gradient, so the first-order energy estimate alone suffices and the exponent is 1 - 1/2 = 1/2.
• d = 2. The Sobolev conjugate of 2 degenerates at d = 2, so the bootstrap of EllipticPdes.Embedding.GagliardoNirenberg takes its step at p = 4/3, whose conjugate is 4. The ball has finite measure, so the L² second derivatives of the interior H² estimate are L^{4/3} data, and Morrey applies at p = 4 > 2 = d with exponent 1 - 2/4 = 1/2.
• d = 3. Morrey needs p > 3, and the interior H² estimate supplies second derivatives in L². The bootstrap raises the gradient from L² to L⁶, and Morrey then applies at p = 6 > 3 = d with exponent 1 - 3/6 = 1/2.

d ≥ 4 stays open. Reaching Morrey from L² second derivatives asks for an exponent p with d/2 < p ≤ 2, since 1/p' = 1/p - 1/d gives p' > d exactly when p > d/2, and the ball turns L² data into Lᵖ data only for p ≤ 2. That range is empty once d ≥ 4, so one Sobolev step never reaches Morrey there. Those dimensions require iteration through the H^k ladder, which this library does not yet have.

Main declarations

• interior_holder_estimate_one: the one-dimensional statement.
• interior_holder_estimate_two: the two-dimensional statement.
• interior_holder_estimate: the three-dimensional statement.

Morrey exponent at the two exponent pairs used here

theorem EllipticPdes.Embedding.morreyExponent_one_two : morreyExponent 1 2 = 1 / 2

At d = 1 and p = 2 the Morrey exponent is 1/2.

theorem EllipticPdes.Embedding.morreyExponent_two_four : morreyExponent 2 4 = 1 / 2

At d = 2 and p = 4 the Morrey exponent is 1/2.

theorem EllipticPdes.Embedding.morreyExponent_three_six : morreyExponent 3 6 = 1 / 2

At d = 3 and p = 6 the Morrey exponent is 1/2.

Restriction of a whole-space L² class to a ball

theorem EllipticPdes.Embedding.eLpNorm_restrictL2 {d : ℕ} (B : Set (EuclideanSpace ℝ (Fin d))) (X : ↥(MeasureTheory.EucL2 d)) : MeasureTheory.eLpNorm (↑↑(Regularity.restrictL2 X)) 2 (MeasureTheory.volume.restrict B) = MeasureTheory.eLpNorm (↑↑X) 2 (MeasureTheory.volume.restrict B)

The restricted class has the same L² seminorm as the class it restricts, measured against the restricted measure.

theorem EllipticPdes.Embedding.nnnorm_restrictL2_le {d : ℕ} (B : Set (EuclideanSpace ℝ (Fin d))) (X : ↥(MeasureTheory.EucL2 d)) : ‖Regularity.restrictL2 X‖₊ ≤ ‖X‖₊

Restricting a whole-space L² class to a set does not increase its norm.

theorem EllipticPdes.Embedding.eLpNorm_restrict_toNNReal_le {d : ℕ} (B : Set (EuclideanSpace ℝ (Fin d))) (X : ↥(MeasureTheory.EucL2 d)) : (MeasureTheory.eLpNorm (↑↑X) 2 (MeasureTheory.volume.restrict B)).toNNReal ≤ ‖X‖₊

The L² seminorm of a whole-space class over a set is bounded by the class norm.

theorem EllipticPdes.Embedding.eLpNorm_restrict_mono_toNNReal_le {d : ℕ} {S T : Set (EuclideanSpace ℝ (Fin d))} (hST : S ⊆ T) (X : ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict T))) : (MeasureTheory.eLpNorm (↑↑X) 2 (MeasureTheory.volume.restrict S)).toNNReal ≤ ‖X‖₊

The L² seminorm of a class on a set, measured over a smaller set, is bounded by the class norm.

One-dimensional estimate

theorem EllipticPdes.Embedding.interior_holder_estimate_one (Op : Sobolev.FullEllipticOp 1) {Ω : Set (EuclideanSpace ℝ (Fin 1))} (hΩm : MeasurableSet Ω) (c : EuclideanSpace ℝ (Fin 1)) {r : ℝ} (hr : 0 < r) : ∃ (C : NNReal), ∀ (u : ↥(Sobolev.H01 Ω)) (f : Sobolev.L2D Ω), (∀ (w : ↥(Sobolev.H01 Ω)), ((Op.fullBilin Ω) u) w = ∫ (x : EuclideanSpace ℝ (Fin 1)) in Ω, ↑↑f x * ↑↑((↑w).ofLp 0) x) → ∃ (u' : EuclideanSpace ℝ (Fin 1) → ℝ), u' =ᵐ[MeasureTheory.volume.restrict (Metric.ball c r)] ↑↑((Regularity.extendL2 hΩm) ((↑u).ofLp 0)) ∧ HolderOnWith (C * (‖f‖ + ‖(↑u).ofLp 0‖).toNNReal) (1 / 2) u' (Metric.ball c r)

Interior Hölder estimate in one dimension (Evans, Partial Differential Equations (2nd ed.), §5.6.2 Thm 5). A weak solution u ∈ H₀¹(Ω) of L u = f has, on every ball, a representative that is Hölder continuous with exponent 1/2 and constant a multiple of ‖f‖ + ‖u‖, the multiplier being quantified before the solution and the datum, so it depends only on the operator and the ball. In one dimension the first-order weak gradient already lies in L² and 2 > 1, so Morrey applies to it directly and only the first-order energy estimate is used: neither the interior H² estimate nor any hypothesis on the geometry of Ω is needed.

Two-dimensional estimate

theorem EllipticPdes.Embedding.interior_holder_estimate_two (Op : Sobolev.FullEllipticOp 2) {Ω : Set (EuclideanSpace ℝ (Fin 2))} (hΩm : MeasurableSet Ω) (hΩo : IsOpen Ω) (hA : Regularity.IsLipCoeff Op.toEllipticCoeff) (c : EuclideanSpace ℝ (Fin 2)) {r R : ℝ} (hr : 0 < r) (hrR : r < R) (hRΩ : Metric.closedBall c R ⊆ Ω) : ∃ (C : NNReal), ∀ (u : ↥(Sobolev.H01 Ω)) (f : Sobolev.L2D Ω), (∀ (w : ↥(Sobolev.H01 Ω)), ((Op.fullBilin Ω) u) w = ∫ (x : EuclideanSpace ℝ (Fin 2)) in Ω, ↑↑f x * ↑↑((↑w).ofLp 0) x) → ∃ (u' : EuclideanSpace ℝ (Fin 2) → ℝ), u' =ᵐ[MeasureTheory.volume.restrict (Metric.ball c r)] ↑↑((Regularity.extendL2 hΩm) ((↑u).ofLp 0)) ∧ HolderOnWith (C * (‖f‖ + ‖(↑u).ofLp 0‖).toNNReal) (1 / 2) u' (Metric.ball c r)

Interior Hölder estimate in two dimensions (Evans, Partial Differential Equations (2nd ed.), §5.6.2 Thm 5, applied to the interior H² estimate of §6.3.1 Thm 1). A weak solution u ∈ H₀¹(Ω) of L u = f with W^{1,∞} principal coefficients has, on every ball B(c, r) with r < R and closedBall c R ⊆ Ω, a representative that is Hölder continuous with exponent 1/2 and constant a multiple of ‖f‖ + ‖u‖, the multiplier being quantified before the solution and the datum, so it depends only on the operator and the two radii. The interior H² estimate puts the second derivatives in L²; at d = 2 the Sobolev conjugate of 2 degenerates, so the bootstrap exists_eLpNorm_four_le takes its step at p = 4/3, paying the finite measure of the ball, and raises the gradient from L² to L⁴. morrey_ball then applies at p = 4 > 2 = d.

Three-dimensional estimate

theorem EllipticPdes.Embedding.interior_holder_estimate (Op : Sobolev.FullEllipticOp 3) {Ω : Set (EuclideanSpace ℝ (Fin 3))} (hΩm : MeasurableSet Ω) (hΩo : IsOpen Ω) (hA : Regularity.IsLipCoeff Op.toEllipticCoeff) (c : EuclideanSpace ℝ (Fin 3)) {r R : ℝ} (hr : 0 < r) (hrR : r < R) (hRΩ : Metric.closedBall c R ⊆ Ω) : ∃ (C : NNReal), ∀ (u : ↥(Sobolev.H01 Ω)) (f : Sobolev.L2D Ω), (∀ (w : ↥(Sobolev.H01 Ω)), ((Op.fullBilin Ω) u) w = ∫ (x : EuclideanSpace ℝ (Fin 3)) in Ω, ↑↑f x * ↑↑((↑w).ofLp 0) x) → ∃ (u' : EuclideanSpace ℝ (Fin 3) → ℝ), u' =ᵐ[MeasureTheory.volume.restrict (Metric.ball c r)] ↑↑((Regularity.extendL2 hΩm) ((↑u).ofLp 0)) ∧ HolderOnWith (C * (‖f‖ + ‖(↑u).ofLp 0‖).toNNReal) (1 / 2) u' (Metric.ball c r)

Interior Hölder estimate in three dimensions (Evans, Partial Differential Equations (2nd ed.), §5.6.2 Thm 5, applied to the interior H² estimate of §6.3.1 Thm 1). A weak solution u ∈ H₀¹(Ω) of L u = f with W^{1,∞} principal coefficients has, on every ball B(c, r) with r < R and closedBall c R ⊆ Ω, a representative that is Hölder continuous with exponent 1/2 and constant a multiple of ‖f‖ + ‖u‖, the multiplier being quantified before the solution and the datum, so it depends only on the operator and the two radii. The interior H² estimate puts the second derivatives in L², the Gagliardo-Nirenberg-Sobolev bootstrap exists_eLpNorm_six_le raises the gradient from L² to L⁶, and morrey_ball applies at p = 6 > 3 = d, so the weak solution is classically differentiable in the Hölder sense.