Ehrling's inequality

Let i : X → Y be a compact linear operator and j : Y → Z an injective continuous linear map. Ehrling's inequality says that the Y-norm of i x is bounded by an arbitrarily small multiple of the X-norm of x plus a multiple of the weaker Z-norm of j (i x): for every ε > 0 there is C with

‖i x‖ ≤ ε * ‖x‖ + C * ‖j (i x)‖ for all x.

The typical instance is a chain of Sobolev spaces W^{k,p} ⊆ W^{l,p} ⊆ Lᵖ on a compact base with k > l, where the first inclusion is compact by Rellich's theorem. The inequality is then the interpolation bound ‖u‖_{W^{l,p}} ≤ ε ‖u‖_{W^{k,p}} + C_ε ‖u‖_{Lᵖ}.

Its main use is in a priori estimates. An estimate ‖x‖ ≤ C * ‖T x‖ + ‖i x‖ whose error term is measured in an intermediate norm can be rewritten with the error term in any weaker norm (IsCompactOperator.exists_norm_le_of_compact_estimate). For elliptic estimates on a compact base this replaces the lower-order Sobolev norm by any weaker norm of the Sobolev scale.

No completeness is assumed, the domain and the intermediate space may be seminormed, and the scalar field is any nontrivially normed field.

The proof adapts the shell normalization of ContinuousLinearMap.exists_pos_mul_norm_le_of_compact_estimate in TauCeti.Analysis.Normed.Operator.Compact.Estimate: a failing sequence is rescaled so that its images under the compact operator lie in a fixed shell.

Main declarations

• IsCompactOperator.exists_norm_le_mul_norm_add_mul_norm: Ehrling's inequality.
• IsCompactOperator.exists_norm_le_of_compact_estimate: weakening the norm of the error term in an a priori estimate.

References

• G. Ehrling, On a type of eigenvalue problem for certain elliptic differential operators, Math. Scand. 2 (1954), 267–285.
• J.-L. Lions, Quelques méthodes de résolution des problèmes aux limites non linéaires, Dunod, 1969, Chapitre 1, Lemme 5.1.

theorem IsCompactOperator.exists_norm_le_mul_norm_add_mul_norm {𝕜 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup X] [NormedSpace 𝕜 X] [SeminormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] {i : X →ₗ[𝕜] Y} {j : Y →L[𝕜] Z} (hi : IsCompactOperator ⇑i) (hj : Function.Injective ⇑j) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : X), ‖i x‖ ≤ ε * ‖x‖ + C * ‖j (i x)‖

Ehrling's inequality. If i : X → Y is a compact operator and j : Y → Z is an injective continuous linear map, then for every ε > 0 there is C ≥ 0 with ‖i x‖ ≤ ε * ‖x‖ + C * ‖j (i x)‖ for all x.

theorem IsCompactOperator.exists_norm_le_of_compact_estimate {𝕜 : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup X] [NormedSpace 𝕜 X] [SeminormedAddCommGroup Y] [NormedSpace 𝕜 Y] [NormedAddCommGroup Z] [NormedSpace 𝕜 Z] {i : X →ₗ[𝕜] Y} {j : Y →L[𝕜] Z} {F : Type u_5} [SeminormedAddCommGroup F] (hi : IsCompactOperator ⇑i) (hj : Function.Injective ⇑j) {T : X → F} {C : ℝ} (hbound : ∀ (x : X), ‖x‖ ≤ C * ‖T x‖ + ‖i x‖) : ∃ (D : ℝ), 0 ≤ D ∧ ∀ (x : X), ‖x‖ ≤ 2 * C * ‖T x‖ + D * ‖j (i x)‖

Weakening the error term of an a priori estimate. If i : X → Y is compact, j : Y → Z is injective and ‖x‖ ≤ C * ‖T x‖ + ‖i x‖ for all x, then the error term may be measured in the weaker norm of Z: there is D ≥ 0 with ‖x‖ ≤ 2 * C * ‖T x‖ + D * ‖j (i x)‖ for all x.