Maps with bounded below derivative reflect smoothness

Let j : E → F be a smooth map from a Banach space E (complete) to a normed space F (complete or not) whose derivative is bounded below on an open set U: m ‖v‖ ≤ ‖dj(x) v‖ for x ∈ U. No complement of the range of dj(x) is assumed. Then j reflects smoothness of continuous maps: if γ : W → U is continuous on an open subset W of a locally convex space and j ∘ γ is C^k in the sense of Michal–Bastiani, then so is γ (ContDiffMBOn.of_comp_of_boundedBelow).

The proof bootstraps a linear version (ContDiffMBOn.of_fderiv_eq_of_boundedBelow): if dj(γ q)(z q) = w q with γ, w of class C^k and z continuous, then z is C^k. The derivative of z is obtained as a limit of difference quotients, which are Cauchy because dj(γ q) is bounded below and E is complete.

Subtleties.

• The Michal–Bastiani definition gives joint continuity of (x, v) ↦ dj(x) v, not continuity of x ↦ dj(x) in the operator norm. The proof needs the latter, to keep the lower bound near a point. For normed spaces it follows from Michal–Bastiani C^{k+1} ⇒ Fréchet C^k (ContDiffMBOn.contDiffOn). For Fréchet or more general locally convex models the result is open.
• The test domain W may be any open subset of a locally convex space: only lines through its points are used to differentiate, and joint continuity comes from the lower bound.

Normed preliminaries

theorem LCAnalysis.exists_tendsto_of_boundedBelow {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace E] {A : E →L[ℝ] F} {m : ℝ} (hm : 0 < m) (hA : ∀ (v : E), m * ‖v‖ ≤ ‖A v‖) {ι : Type u_1} {l : Filter ι} [l.NeBot] {z : ι → E} {R : F} (h : Filter.Tendsto (fun (i : ι) => A (z i)) l (nhds R)) : ∃ (D : E), Filter.Tendsto z l (nhds D) ∧ A D = R

If A is bounded below and A z_t → R, then z_t converges to a solution of A D = R.

theorem LCAnalysis.continuousOn_of_boundedBelow {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace ℝ F] {X : Type u_1} [TopologicalSpace X] {W : Set X} {A : X → E →L[ℝ] F} (hA : ContinuousOn A W) {m : ℝ} (hm : 0 < m) (hbd : ∀ q ∈ W, ∀ (v : E), m * ‖v‖ ≤ ‖(A q) v‖) {z : X → E} {r : X → F} (hr : ContinuousOn r W) (heq : ∀ q ∈ W, (A q) (z q) = r q) : ContinuousOn z W

Solutions of A(q) z(q) = r(q) are continuous when A is continuous in the operator norm and uniformly bounded below, and r is continuous.

theorem LCAnalysis.exists_boundedBelow_of_isEmbedding {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace ℝ F] {L : E →L[ℝ] F} (hL : Topology.IsEmbedding ⇑L) : ∃ m > 0, ∀ (v : E), m * ‖v‖ ≤ ‖L v‖

A continuous linear map between normed spaces which is a topological embedding is bounded below.

theorem LCAnalysis.exists_nhds_boundedBelow {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace ℝ F] {j : E → F} {U : Set E} (hU : IsOpen U) (hj : ContinuousOn (fderiv ℝ j) U) {x₀ : E} (hx₀ : x₀ ∈ U) {m : ℝ} (hm : 0 < m) (hbd : ∀ (v : E), m * ‖v‖ ≤ ‖(fderiv ℝ j x₀) v‖) : ∃ V ⊆ U, IsOpen V ∧ Convex ℝ V ∧ x₀ ∈ V ∧ ∀ x ∈ V, ∀ (v : E), m / 2 * ‖v‖ ≤ ‖(fderiv ℝ j x) v‖

The lower bound of the derivative propagates to a neighborhood.

Bootstrapping

theorem LCAnalysis.hasDerivAt_line_of_hasDirDerivAt {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u} [AddCommGroup H] [Module ℝ H] {γ : H → E} {q h : H} {y : E} (hγ : HasDirDerivAt γ q h y) : HasDerivAt (fun (t : ℝ) => γ (q + t • h)) y 0

A directional derivative into a normed space is the derivative of the line.

theorem LCAnalysis.SmoothMBOn.fderiv_facts {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace ℝ F] {j : E → F} {U : Set E} (hU : IsOpen U) (hj : SmoothMBOn j U) : ContDiffOn ℝ (↑⊤) j U ∧ ContDiffOn ℝ (↑⊤) (fderiv ℝ j) U ∧ SmoothMBOn (fun (p : E × E × E) => ((fderiv ℝ (fderiv ℝ j) p.1) p.2.1) p.2.2) (U ×ˢ Set.univ)

The Fréchet derivatives of a Michal–Bastiani smooth map.

theorem LCAnalysis.ContDiffMBOn.of_fderiv_eq_of_boundedBelow {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : Type w} [NormedAddCommGroup F] [NormedSpace ℝ F] {j : E → F} {U : Set E} (hU : IsOpen U) (hj : SmoothMBOn j U) {m : ℝ} (hm : 0 < m) (hbd : ∀ x ∈ U, ∀ (v : E), m * ‖v‖ ≤ ‖(fderiv ℝ j x) v‖) (k : ℕ) {H : Type u} [AddCommGroup H] [Module ℝ H] [TopologicalSpace H] [IsTopologicalAddGroup H] [ContinuousSMul ℝ H] [LocallyConvexSpace ℝ H] [T2Space H] {W : Set H} {γ z : H → E} {w : H → F} : IsOpen W → ContDiffMBOn k γ W → Set.MapsTo γ W U → ContinuousOn z W → ContDiffMBOn k w W → (∀ q ∈ W, (fderiv ℝ j (γ q)) (z q) = w q) → ContDiffMBOn k z W

Linear bootstrap. If dj is bounded below on U and dj(γ q)(z q) = w q on W, with γ and w of class C^k and z continuous, then z is of class C^k.

theorem LCAnalysis.ContDiffMBOn.of_comp_of_boundedBelow {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {F : Type w} [NormedAddCommGroup F] [NormedSpace ℝ F] {j : E → F} {U : Set E} (hU : IsOpen U) (hj : SmoothMBOn j U) {m : ℝ} (hm : 0 < m) (hbd : ∀ x ∈ U, ∀ (v : E), m * ‖v‖ ≤ ‖(fderiv ℝ j x) v‖) (k : ℕ) {H : Type u} [AddCommGroup H] [Module ℝ H] [TopologicalSpace H] [IsTopologicalAddGroup H] [ContinuousSMul ℝ H] [LocallyConvexSpace ℝ H] [T2Space H] {W : Set H} {γ : H → E} : IsOpen W → ContinuousOn γ W → Set.MapsTo γ W U → ContDiffMBOn k (j ∘ γ) W → ContDiffMBOn k γ W

Maps with bounded below derivative reflect smoothness. If dj is bounded below on the open set U and γ : W → U is continuous with j ∘ γ of class C^k, then γ is of class C^k.