feat: behavior of unique differentiablity under field extension (#26429)

If `s` is a domain of unique differentiability for a field `k`, then it is also a domain of unique differentiability for larger fields.

This PR provides material required to implement a reviewer's suggestion in #26353



Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

Author: kebekus

Mathlib/Analysis/Calculus/TangentCone.lean

@@ -436,7 +436,8 @@ theorem UniqueDiffWithinAt.congr_pt (h : UniqueDiffWithinAt 𝕜 s x) (hy : x =
 end TVS
 
 section Normed
-variable [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+variable {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
+variable [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E]
 variable [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 variable {x y : E} {s t : Set E}
 
@@ -545,6 +546,46 @@ theorem UniqueDiffOn.univ_pi (ι : Type*) [Finite ι] (E : ι → Type*)
     (h : ∀ i, UniqueDiffOn 𝕜 (s i)) : UniqueDiffOn 𝕜 (Set.pi univ s) :=
   UniqueDiffOn.pi _ _ _ _ fun i _ => h i
 
+/--
+Given `x ∈ s` and a field extension `𝕜 ⊆ 𝕜'`, the tangent cone of `s` at `x` with
+respect to `𝕜` is contained in the tangent cone of `s` at `x` with respect to `𝕜'`.
+-/
+theorem tangentConeAt_mono_field : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜' s x := by
+  intro α hα
+  simp only [tangentConeAt, eventually_atTop, ge_iff_le, tendsto_norm_atTop_iff_cobounded,
+    mem_setOf_eq] at hα ⊢
+  obtain ⟨c, d, ⟨a, h₁a⟩, h₁, h₂⟩ := hα
+  use ((algebraMap 𝕜 𝕜') ∘ c), d
+  constructor
+  · use a
+  · constructor
+    · intro β hβ
+      rw [mem_map, mem_atTop_sets]
+      obtain ⟨n, hn⟩ := mem_atTop_sets.1
+        (mem_map.1 (h₁ (algebraMap_cobounded_le_cobounded (𝕜 := 𝕜) (𝕜' := 𝕜') hβ)))
+      use n, fun _ _ ↦ by simp_all
+    · simpa
+
+/--
+Assume that `E` is a normed vector space over normed fields `𝕜 ⊆ 𝕜'` and that `x ∈ s` is a point
+of unique differentiability with respect to the set `s` and the smaller field `𝕜`, then `x` is also
+a point of unique differentiability with respect to the set `s` and the larger field `𝕜'`.
+-/
+theorem UniqueDiffWithinAt.mono_field (h₂s : UniqueDiffWithinAt 𝕜 s x) :
+    UniqueDiffWithinAt 𝕜' s x := by
+  simp_all only [uniqueDiffWithinAt_iff, and_true]
+  apply Dense.mono _ h₂s.1
+  trans ↑(Submodule.span 𝕜 (tangentConeAt 𝕜' s x))
+  <;> simp [Submodule.span_mono tangentConeAt_mono_field]
+
+/--
+Assume that `E` is a normed vector space over normed fields `𝕜 ⊆ 𝕜'` and all points of `s` are
+points of unique differentiability with respect to the smaller field `𝕜`, then they are also points
+of unique differentiability with respect to the larger field `𝕜`.
+-/
+theorem UniqueDiffOn.mono_field (h₂s : UniqueDiffOn 𝕜 s) :
+    UniqueDiffOn 𝕜' s := fun x hx ↦ (h₂s x hx).mono_field
+
 end Normed
 
 section RealNormed

Mathlib/Analysis/Normed/Module/Basic.lean

@@ -288,6 +288,19 @@ end NNReal
 
 variable (𝕜)
 
+/--
+Preimages of cobounded sets under the algebra map are cobounded.
+-/
+theorem algebraMap_cobounded_le_cobounded [NormOneClass 𝕜'] :
+    Filter.map (algebraMap 𝕜 𝕜') (Bornology.cobounded 𝕜) ≤ Bornology.cobounded 𝕜' := by
+  intro c hc
+  rw [Filter.mem_map, ← Bornology.isCobounded_def, ← Bornology.isBounded_compl_iff,
+    isBounded_iff_forall_norm_le]
+  obtain ⟨s, hs⟩ := isBounded_iff_forall_norm_le.1
+    (Bornology.isBounded_compl_iff.2 (Bornology.isCobounded_def.1 hc))
+  use s
+  exact fun x hx ↦ by simpa [norm_algebraMap, norm_one] using hs ((algebraMap 𝕜 𝕜') x) hx
+
 /-- In a normed algebra, the inclusion of the base field in the extended field is an isometry. -/
 theorem algebraMap_isometry [NormOneClass 𝕜'] : Isometry (algebraMap 𝕜 𝕜') := by
   refine Isometry.of_dist_eq fun x y => ?_

Mathlib/Analysis/RCLike/TangentCone.lean

@@ -20,20 +20,12 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [h𝕜 : IsRCLikeNormedFi
 theorem tangentConeAt_real_subset_isRCLikeNormedField :
     tangentConeAt ℝ s x ⊆ tangentConeAt 𝕜 s x := by
   letI := h𝕜.rclike
-  rintro y ⟨c, d, d_mem, c_lim, hcd⟩
-  let c' : ℕ → 𝕜 := fun n ↦ c n
-  refine ⟨c', d, d_mem, by simpa [c'] using c_lim, ?_⟩
-  convert hcd using 2 with n
-  simp [c']
+  exact tangentConeAt_mono_field
 
 theorem UniqueDiffWithinAt.of_real (hs : UniqueDiffWithinAt ℝ s x) :
     UniqueDiffWithinAt 𝕜 s x := by
-  refine ⟨?_, hs.mem_closure⟩
-  letI : RCLike 𝕜 := h𝕜.rclike
-  apply hs.dense_tangentConeAt.mono
-  have : (Submodule.span ℝ (tangentConeAt ℝ s x) : Set E)
-      ⊆ (Submodule.span 𝕜 (tangentConeAt ℝ s x)) := Submodule.span_subset_span _ _ _
-  exact this.trans (Submodule.span_mono tangentConeAt_real_subset_isRCLikeNormedField)
+  letI := h𝕜.rclike
+  exact hs.mono_field
 
 theorem UniqueDiffOn.of_real (hs : UniqueDiffOn ℝ s) :
     UniqueDiffOn 𝕜 s :=