The method of continuity

Let E be a Banach space, F a normed space, and t ↦ L t a family of continuous linear maps E →L[𝕜] F, continuous in operator norm on a preconnected parameter set S. Suppose the family satisfies an a priori estimate that is uniform in the parameter:

‖x‖ ≤ C * ‖L t x‖ for every t ∈ S and every x ∈ E.

Then either every L t, t ∈ S, is surjective, or none is. So solvability of a single, simpler problem (for instance one with constant coefficients) gives solvability along the whole family, and the uniform estimate then makes every L t invertible with ‖(L t)⁻¹ y‖ ≤ C * ‖y‖, the inverse depending continuously on t in operator norm.

The proof is the classical one. If L s is surjective, the estimate makes it invertible with inverse of norm at most C, and a Neumann series shows that every M with C * ‖M - L s‖ < 1 is invertible too (ContinuousLinearMap.isInvertible_of_mul_norm_sub_lt). The radius 1 / C does not depend on s, so the set of parameters where L t is surjective is both open and closed in S; preconnectedness concludes.

This is the abstract step behind existence theorems for linear elliptic and parabolic equations with variable coefficients: the a priori Schauder estimate along the path from the Laplacian or the heat operator to the given operator, together with solvability at the starting point, gives solvability at the end point.

Main declarations

• IsPreconnected.surjective_iff_of_forall_norm_le: the method of continuity for a family on a preconnected parameter set.
• IsPreconnected.isInvertible_of_forall_norm_le and IsPreconnected.continuousOn_inverse_of_forall_norm_le: once one member is surjective, every member is invertible and the inverses depend continuously on the parameter.
• ContinuousLinearMap.surjective_iff_of_forall_norm_le_lineMap: the classical statement for the segment t ↦ (1 - t) L₀ + t L₁, t ∈ [0, 1].

References

• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 5.2 (the method of continuity) and its use in Theorem 6.8.

theorem IsPreconnected.surjective_iff_of_forall_norm_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {X : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace X] {S : Set X} {L : X → E →L[𝕜] F} {C : ℝ} {s t : X} (hS : IsPreconnected S) (hL : ContinuousOn L S) (hC : ∀ t ∈ S, ∀ (x : E), ‖x‖ ≤ C * ‖(L t) x‖) (hs : s ∈ S) (ht : t ∈ S) : Function.Surjective ⇑(L s) ↔ Function.Surjective ⇑(L t)

The method of continuity. Let E be a Banach space and L a family of continuous linear maps E →L[𝕜] F, continuous in operator norm on a preconnected set S, satisfying the uniform a priori estimate ‖x‖ ≤ C * ‖L t x‖ for t ∈ S. Then for s, t ∈ S, L s is surjective if and only if L t is.

theorem IsPreconnected.isInvertible_of_forall_norm_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {X : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace X] {S : Set X} {L : X → E →L[𝕜] F} {C : ℝ} {s t : X} (hS : IsPreconnected S) (hL : ContinuousOn L S) (hC : ∀ t ∈ S, ∀ (x : E), ‖x‖ ≤ C * ‖(L t) x‖) (hs : s ∈ S) (ht : t ∈ S) (h : Function.Surjective ⇑(L s)) : (L t).IsInvertible

The method of continuity, invertible form. Under the hypotheses of IsPreconnected.surjective_iff_of_forall_norm_le, if one L s, s ∈ S, is surjective, then every L t, t ∈ S, is invertible. Its inverse satisfies ‖(L t)⁻¹ y‖ ≤ C * ‖y‖ by ContinuousLinearMap.norm_inverse_apply_le_of_forall_norm_le.

theorem IsPreconnected.continuousOn_inverse_of_forall_norm_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {X : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace X] {S : Set X} {L : X → E →L[𝕜] F} {C : ℝ} {s : X} (hS : IsPreconnected S) (hL : ContinuousOn L S) (hC : ∀ t ∈ S, ∀ (x : E), ‖x‖ ≤ C * ‖(L t) x‖) (hs : s ∈ S) (h : Function.Surjective ⇑(L s)) : ContinuousOn (fun (t : X) => (L t).inverse) S

Under the hypotheses of IsPreconnected.surjective_iff_of_forall_norm_le, if one L s, s ∈ S, is surjective, then the inverses (L t)⁻¹ depend continuously on t ∈ S in operator norm.

theorem ContinuousLinearMap.surjective_iff_of_forall_norm_le_lineMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {C : ℝ} [NormedSpace ℝ F] [SMulCommClass 𝕜 ℝ F] {L₀ L₁ : E →L[𝕜] F} (hC : ∀ t ∈ Set.Icc 0 1, ∀ (x : E), ‖x‖ ≤ C * ‖((AffineMap.lineMap L₀ L₁) t) x‖) : Function.Surjective ⇑L₀ ↔ Function.Surjective ⇑L₁

The method of continuity (Gilbarg–Trudinger, Theorem 5.2). Let E be a Banach space and L₀, L₁ : E →L[𝕜] F. If the operators L t = (1 - t) L₀ + t L₁ satisfy the a priori estimate ‖x‖ ≤ C * ‖L t x‖ for every t ∈ [0, 1], then L₀ is surjective if and only if L₁ is.