feat(analysis/complex/basic): add several trivial lemmas for differen…

…tiable functions. (#8418)

This file relates the differentiability of a function to the linearity of its `fderiv`.



Co-authored-by: justadzr <66561890+justadzr@users.noreply.github.com>

src/analysis/calculus/fderiv.lean

@@ -2867,4 +2867,37 @@ lemma differentiable.restrict_scalars (h : differentiable 𝕜' f) :
   differentiable 𝕜 f :=
 λx, (h x).restrict_scalars 𝕜
 
+lemma has_fderiv_within_at_of_restrict_scalars
+  {g' : E →L[𝕜] F} (h : has_fderiv_within_at f g' s x)
+  (H : f'.restrict_scalars 𝕜 = g') : has_fderiv_within_at f f' s x :=
+by { rw ← H at h, exact h }
+
+lemma has_fderiv_at_of_restrict_scalars {g' : E →L[𝕜] F} (h : has_fderiv_at f g' x)
+  (H : f'.restrict_scalars 𝕜 = g') : has_fderiv_at f f' x :=
+by { rw ← H at h, exact h }
+
+lemma differentiable_at.fderiv_restrict_scalars (h : differentiable_at 𝕜' f x) :
+  fderiv 𝕜 f x = (fderiv 𝕜' f x).restrict_scalars 𝕜 :=
+(h.has_fderiv_at.restrict_scalars 𝕜).fderiv
+
+lemma differentiable_within_at_iff_restrict_scalars
+  (hf : differentiable_within_at 𝕜 f s x) (hs : unique_diff_within_at 𝕜 s x) :
+  differentiable_within_at 𝕜' f s x ↔
+  ∃ (g' : E →L[𝕜'] F), g'.restrict_scalars 𝕜 = fderiv_within 𝕜 f s x :=
+begin
+  split,
+  { rintros ⟨g', hg'⟩,
+    exact ⟨g', hs.eq (hg'.restrict_scalars 𝕜) hf.has_fderiv_within_at⟩, },
+  { rintros ⟨f', hf'⟩,
+    exact ⟨f', has_fderiv_within_at_of_restrict_scalars 𝕜 hf.has_fderiv_within_at hf'⟩, },
+end
+
+lemma differentiable_at_iff_restrict_scalars (hf : differentiable_at 𝕜 f x) :
+  differentiable_at 𝕜' f x ↔ ∃ (g' : E →L[𝕜'] F), g'.restrict_scalars 𝕜 = fderiv 𝕜 f x :=
+begin
+  rw [← differentiable_within_at_univ, ← fderiv_within_univ],
+  exact differentiable_within_at_iff_restrict_scalars 𝕜
+    hf.differentiable_within_at unique_diff_within_at_univ,
+end
+
 end restrict_scalars