Integrability of the weak solution above L²

EllipticPdes.Embedding.eLpNorm_le_of_mem_H01_of_isBounded bounds the L^q(Ω) seminorm of an element of H₀¹(Ω) by its gradient coordinates, for every q up to the Sobolev conjugate of 2. EllipticPdes.Sobolev.FullEllipticOp.weak_solution_L2_of_nonneg_zeroth_of_bounded bounds the H¹ norm of the weak solution by the L² norm of the datum. Composing them takes the solution out of L² and up to the critical exponent, with a bound by the datum alone.

The two hypotheses are those of the existence theorem, no drift and a nonnegative zeroth-order coefficient, together with 2 < d, which is what the critical exponent asks for.

Main declarations

• EllipticPdes.Embedding.eLpNorm_weakSolution_le: the weak solution lies in L^q(Ω) for every q up to the critical exponent, with ‖u‖_{L^q} ≤ K ‖f‖_{L²}.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §5.6.1 Theorem 3 and §6.2.2 Theorem 3.

theorem EllipticPdes.Embedding.eLpNorm_weakSolution_le {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩm : MeasurableSet Ω) (hΩb : Bornology.IsBounded Ω) (hd : 2 < n + 1) (hb : ∀ (i : Fin (n + 1)), ∀ᵐ (x : EuclideanSpace ℝ (Fin (n + 1))) ∂MeasureTheory.volume.restrict Ω, Op.b x i = 0) (hc : ∀ᵐ (x : EuclideanSpace ℝ (Fin (n + 1))) ∂MeasureTheory.volume.restrict Ω, 0 ≤ Op.c x) {q : NNReal} (hq : (↑2)⁻¹ - (↑(n + 1))⁻¹ ≤ (↑q)⁻¹) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : Sobolev.L2D Ω) (u : ↥(Sobolev.H01 Ω)), (∀ (v : ↥(Sobolev.H01 Ω)), ((Op.fullBilin Ω) u) v = ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, ↑↑f x * ↑↑((↑v).ofLp 0) x) → MeasureTheory.MemLp (↑↑((↑u).ofLp 0)) (↑q) (MeasureTheory.volume.restrict Ω) ∧ MeasureTheory.eLpNorm (↑↑((↑u).ofLp 0)) (↑q) (MeasureTheory.volume.restrict Ω) ≤ ENNReal.ofReal (K * ‖f‖)

Weak solution above L². On a bounded measurable domain in dimension greater than two, with no drift and a nonnegative zeroth-order coefficient, the weak solution of L u = f lies in L^q(Ω) for every exponent q up to the Sobolev conjugate of 2, and its L^q seminorm is bounded by the L² norm of the datum.

The constant is the Sobolev constant times the dimension times the constant of the existence theorem, so it depends on the domain, the operator and the exponent, and not on the datum.