A priori bound from the maximum principle

For a subsolution of L u = f on a bounded open set lying in a slab of width D in a coordinate direction, with c ≥ 0, the supremum of u is bounded by the supremum of its positive part over the boundary plus (e^{(B/θ + 1) D} - 1) times the bound on f over θ. The comparison function is sup u⁺ + (F/θ)(e^{αD} - e^{α (x_{i₀} - m)}) at α = B/θ + 1, whose image under L is at least F, so the comparison principle applies. A solution is bounded in absolute value by the same expression with the boundary supremum of |u|.

Main declarations

• EllipticPdes.Classical.apriori_bound_sub: the bound for a subsolution.
• EllipticPdes.Classical.apriori_bound_abs: the bound for a solution.

Operator convention

The non-divergence operator here is L u = -∑ aᵢⱼ ∂ᵢⱼu + ∑ bᵢ ∂ᵢu + c u. All Guo results cited in this file are translated by negating the source operator: Guo's operator is -L, with coefficients a, -b, -c. Thus his subsolution inequality (-L) u ≥ 0 becomes L u ≤ 0, and his potential condition -c ≤ 0 becomes c ≥ 0.

References

James Guo, Partial Differential Equations (Course Lecture Notes), Theorem XI.5.1 (p. 103); D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 3.7 (p. 36).

theorem EllipticPdes.Classical.le_diag_of_ell {d : ℕ} {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {θ : ℝ} {z : EuclideanSpace ℝ (Fin d)} (hell : ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a z i j * ξ i * ξ j) (i₀ : Fin d) : θ ≤ a z i₀ i₀

The diagonal coefficient is at least the ellipticity constant.

theorem EllipticPdes.Classical.continuous_coord {d : ℕ} (i₀ : Fin d) : Continuous fun (x : EuclideanSpace ℝ (Fin d)) => x.ofLp i₀

The coordinate map is continuous.

theorem EllipticPdes.Classical.slab_closure {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} {i₀ : Fin d} {m D : ℝ} (hslab : ∀ x ∈ U, m ≤ x.ofLp i₀ ∧ x.ofLp i₀ ≤ m + D) (x : EuclideanSpace ℝ (Fin d)) : x ∈ closure U → m ≤ x.ofLp i₀ ∧ x.ofLp i₀ ≤ m + D

A slab bound on an open set extends to its closure.

theorem EllipticPdes.Classical.apriori_bound_sub {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hUne : U.Nonempty) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {c : EuclideanSpace ℝ (Fin d) → ℝ} {θ B : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) (hc : ∀ x ∈ U, 0 ≤ c x) {i₀ : Fin d} {m D : ℝ} (hslab : ∀ x ∈ U, m ≤ x.ofLp i₀ ∧ x.ofLp i₀ ≤ m + D) {u f : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (huc : ContinuousOn u (closure U)) (hsub : ∀ x ∈ U, nondivOp a b c u x ≤ f x) {F : ℝ} (hF0 : 0 ≤ F) (hF : ∀ x ∈ U, f x ≤ F) : ∃ y ∈ frontier U, ∀ x ∈ closure U, u x ≤ max (u y) 0 + (Real.exp ((B / θ + 1) * D) - 1) * (F / θ)

Maximum-principle bound for a subsolution (Guo Theorem XI.5.1(i), Gilbarg and Trudinger Theorem 3.7). On a bounded open set inside the slab m ≤ x_{i₀} ≤ m + D, with c ≥ 0, a function with L u ≤ f and f ≤ F is bounded by the maximum of its positive part over the boundary plus (e^{(B/θ + 1) D} - 1) F/θ.

theorem EllipticPdes.Classical.apriori_bound_abs {d : ℕ} (hd : 0 < d) {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hUne : U.Nonempty) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {c : EuclideanSpace ℝ (Fin d) → ℝ} {θ B : ℝ} (hθ : 0 < θ) (hsymm : ∀ x ∈ U, ∀ (i j : Fin d), a x i j = a x j i) (hell : ∀ x ∈ U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (hb : ∀ x ∈ U, ∀ (i : Fin d), |b x i| ≤ B) (hc : ∀ x ∈ U, 0 ≤ c x) {i₀ : Fin d} {m D : ℝ} (hslab : ∀ x ∈ U, m ≤ x.ofLp i₀ ∧ x.ofLp i₀ ≤ m + D) {u f : EuclideanSpace ℝ (Fin d) → ℝ} (hu : ContDiffOn ℝ 2 u U) (huc : ContinuousOn u (closure U)) (hsol : ∀ x ∈ U, nondivOp a b c u x = f x) {F : ℝ} (hF : ∀ x ∈ U, |f x| ≤ F) : ∃ y ∈ frontier U, ∀ x ∈ closure U, |u x| ≤ |u y| + (Real.exp ((B / θ + 1) * D) - 1) * (F / θ)

Maximum-principle bound for a solution (Guo Theorem XI.5.1(ii), Gilbarg and Trudinger Theorem 3.7). On a bounded open set inside the slab m ≤ x_{i₀} ≤ m + D, with c ≥ 0, a function with L u = f and |f| ≤ F is bounded in absolute value by the maximum of |u| over the boundary plus (e^{(B/θ + 1) D} - 1) F/θ.