feat(calculus/fderiv): invariance of fderiv under linear equivs (#1977)

* feat(calculus/fderiv): invariance of fderiv under linear equivs

* missing material

* coherent naming conventions

* fix build

* coherent naming conventions

* yury's comments

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: sgouezel

src/analysis/calculus/fderiv.lean

@@ -395,6 +395,10 @@ lemma differentiable_at.differentiable_within_at
   (h : differentiable_at 𝕜 f x) : differentiable_within_at 𝕜 f s x :=
 (differentiable_within_at_univ.2 h).mono (subset_univ _)
 
+lemma differentiable.differentiable_at (h : differentiable 𝕜 f) :
+  differentiable_at 𝕜 f x :=
+h x
+
 lemma differentiable_within_at.differentiable_at
   (h : differentiable_within_at 𝕜 f s x) (hs : s ∈ 𝓝 x) : differentiable_at 𝕜 f x :=
 h.imp (λ f' hf', hf'.has_fderiv_at hs)
@@ -435,7 +439,7 @@ lemma fderiv_within_subset (st : s ⊆ t) (ht : unique_diff_within_at 𝕜 s x)
 begin
   ext x : 1,
   by_cases h : differentiable_at 𝕜 f x,
-  { apply has_fderiv_within_at.fderiv_within _ (is_open_univ.unique_diff_within_at (mem_univ _)),
+  { apply has_fderiv_within_at.fderiv_within _ unique_diff_within_at_univ,
     rw has_fderiv_within_at_univ,
     apply h.has_fderiv_at },
   { have : ¬ differentiable_within_at 𝕜 f univ x,
@@ -512,6 +516,11 @@ lemma differentiable_on.congr (h : differentiable_on 𝕜 f s) (h' : ∀x ∈ s,
   differentiable_on 𝕜 f₁ s :=
 λ x hx, (h x hx).congr h' (h' x hx)
 
+lemma differentiable_on_congr (h' : ∀x ∈ s, f₁ x = f x) :
+  differentiable_on 𝕜 f₁ s ↔ differentiable_on 𝕜 f s :=
+⟨λ h, differentiable_on.congr h (λy hy, (h' y hy).symm),
+λ h, differentiable_on.congr h h'⟩
+
 lemma differentiable_at.congr_of_mem_nhds (h : differentiable_at 𝕜 f x)
   (hL : ∀ᶠ y in 𝓝 x, f₁ y = f y) : differentiable_at 𝕜 f₁ x :=
 has_fderiv_at.differentiable_at (has_fderiv_at_filter.congr_of_mem_sets h.has_fderiv_at hL (mem_of_nhds hL : _))
@@ -622,14 +631,17 @@ lemma differentiable_at_const (c : F) : differentiable_at 𝕜 (λx, c) x :=
 lemma differentiable_within_at_const (c : F) : differentiable_within_at 𝕜 (λx, c) s x :=
 differentiable_at.differentiable_within_at (differentiable_at_const _)
 
-lemma fderiv_const (c : F) : fderiv 𝕜 (λy, c) x = 0 :=
+lemma fderiv_const_apply (c : F) : fderiv 𝕜 (λy, c) x = 0 :=
 has_fderiv_at.fderiv (has_fderiv_at_const c x)
 
-lemma fderiv_within_const (c : F) (hxs : unique_diff_within_at 𝕜 s x) :
+lemma fderiv_const (c : F) : fderiv 𝕜 (λ (y : E), c) = 0 :=
+by { ext m, rw fderiv_const_apply, refl }
+
+lemma fderiv_within_const_apply (c : F) (hxs : unique_diff_within_at 𝕜 s x) :
   fderiv_within 𝕜 (λy, c) s x = 0 :=
 begin
   rw differentiable_at.fderiv_within (differentiable_at_const _) hxs,
-  exact fderiv_const _
+  exact fderiv_const_apply _
 end
 
 lemma differentiable_const (c : F) : differentiable 𝕜 (λx : E, c) :=
@@ -705,7 +717,7 @@ end
 protected lemma continuous_linear_map.has_fderiv_within_at : has_fderiv_within_at e e s x :=
 e.has_fderiv_at_filter
 
-protected lemma continuous_linear_map.has_fderiv_at : has_fderiv_at e e x  :=
+protected lemma continuous_linear_map.has_fderiv_at : has_fderiv_at e e x :=
 e.has_fderiv_at_filter
 
 protected lemma continuous_linear_map.differentiable_at : differentiable_at 𝕜 e x :=
@@ -1363,24 +1375,37 @@ lemma differentiable_at.comp {g : F → G}
   differentiable_at 𝕜 (g ∘ f) x :=
 (hg.has_fderiv_at.comp x hf.has_fderiv_at).differentiable_at
 
+lemma differentiable_at.comp_differentiable_within_at {g : F → G}
+  (hg : differentiable_at 𝕜 g (f x)) (hf : differentiable_within_at 𝕜 f s x) :
+  differentiable_within_at 𝕜 (g ∘ f) s x :=
+(differentiable_within_at_univ.2 hg).comp x hf (by simp)
+
 lemma fderiv_within.comp {g : F → G} {t : set F}
   (hg : differentiable_within_at 𝕜 g t (f x)) (hf : differentiable_within_at 𝕜 f s x)
   (h : s ⊆ f ⁻¹' t) (hxs : unique_diff_within_at 𝕜 s x) :
-  fderiv_within 𝕜 (g ∘ f) s x =
-    continuous_linear_map.comp (fderiv_within 𝕜 g t (f x)) (fderiv_within 𝕜 f s x) :=
+  fderiv_within 𝕜 (g ∘ f) s x = (fderiv_within 𝕜 g t (f x)).comp (fderiv_within 𝕜 f s x) :=
 begin
   apply has_fderiv_within_at.fderiv_within _ hxs,
   exact has_fderiv_within_at.comp x (hg.has_fderiv_within_at) (hf.has_fderiv_within_at) h
 end
 
 lemma fderiv.comp {g : F → G}
   (hg : differentiable_at 𝕜 g (f x)) (hf : differentiable_at 𝕜 f x) :
-  fderiv 𝕜 (g ∘ f) x = continuous_linear_map.comp (fderiv 𝕜 g (f x)) (fderiv 𝕜 f x) :=
+  fderiv 𝕜 (g ∘ f) x = (fderiv 𝕜 g (f x)).comp (fderiv 𝕜 f x) :=
 begin
   apply has_fderiv_at.fderiv,
   exact has_fderiv_at.comp x hg.has_fderiv_at hf.has_fderiv_at
 end
 
+lemma fderiv.comp_fderiv_within {g : F → G}
+  (hg : differentiable_at 𝕜 g (f x)) (hf : differentiable_within_at 𝕜 f s x)
+  (hxs : unique_diff_within_at 𝕜 s x) :
+  fderiv_within 𝕜 (g ∘ f) s x = (fderiv 𝕜 g (f x)).comp (fderiv_within 𝕜 f s x) :=
+begin
+  apply has_fderiv_within_at.fderiv_within _ hxs,
+  exact has_fderiv_at.comp_has_fderiv_within_at x (hg.has_fderiv_at) (hf.has_fderiv_within_at)
+end
+
 lemma differentiable_on.comp {g : F → G} {t : set F}
   (hg : differentiable_on 𝕜 g t) (hf : differentiable_on 𝕜 f s) (st : s ⊆ f ⁻¹' t) :
   differentiable_on 𝕜 (g ∘ f) s :=
@@ -1390,6 +1415,11 @@ lemma differentiable.comp {g : F → G} (hg : differentiable 𝕜 g) (hf : diffe
   differentiable 𝕜 (g ∘ f) :=
 λx, differentiable_at.comp x (hg (f x)) (hf x)
 
+lemma differentiable.comp_differentiable_on {g : F → G} (hg : differentiable 𝕜 g)
+  (hf : differentiable_on 𝕜 f s) :
+  differentiable_on 𝕜 (g ∘ f) s :=
+(differentiable_on_univ.2 hg).comp hf (by simp)
+
 end composition
 
 section smul
@@ -1626,6 +1656,122 @@ lemma fderiv_const_mul (hc : differentiable_at 𝕜 c x) (d : 𝕜) :
 
 end mul
 
+section continuous_linear_equiv
+/-! ### Differentiability of linear equivs, and invariance of differentiability -/
+
+variable (iso : E ≃L[𝕜] F)
+
+protected lemma continuous_linear_equiv.has_fderiv_within_at :
+  has_fderiv_within_at iso (iso : E →L[𝕜] F) s x :=
+iso.to_continuous_linear_map.has_fderiv_within_at
+
+protected lemma continuous_linear_equiv.has_fderiv_at : has_fderiv_at iso (iso : E →L[𝕜] F) x :=
+iso.to_continuous_linear_map.has_fderiv_at_filter
+
+protected lemma continuous_linear_equiv.differentiable_at : differentiable_at 𝕜 iso x :=
+iso.has_fderiv_at.differentiable_at
+
+protected lemma continuous_linear_equiv.differentiable_within_at :
+  differentiable_within_at 𝕜 iso s x :=
+iso.differentiable_at.differentiable_within_at
+
+protected lemma continuous_linear_equiv.fderiv : fderiv 𝕜 iso x = iso :=
+iso.has_fderiv_at.fderiv
+
+protected lemma continuous_linear_equiv.fderiv_within (hxs : unique_diff_within_at 𝕜 s x) :
+  fderiv_within 𝕜 iso s x = iso :=
+iso.to_continuous_linear_map.fderiv_within hxs
+
+protected lemma continuous_linear_equiv.differentiable : differentiable 𝕜 iso :=
+λx, iso.differentiable_at
+
+protected lemma continuous_linear_equiv.differentiable_on : differentiable_on 𝕜 iso s :=
+iso.differentiable.differentiable_on
+
+lemma continuous_linear_equiv.comp_differentiable_within_at_iff {f : G → E} {s : set G} {x : G} :
+  differentiable_within_at 𝕜 (iso ∘ f) s x ↔ differentiable_within_at 𝕜 f s x :=
+begin
+  refine ⟨λ H, _, λ H, iso.differentiable.differentiable_at.comp_differentiable_within_at x H⟩,
+  have : differentiable_within_at 𝕜 (iso.symm ∘ (iso ∘ f)) s x :=
+    iso.symm.differentiable.differentiable_at.comp_differentiable_within_at x H,
+  rwa [← function.comp.assoc iso.symm iso f, iso.symm_comp_self] at this,
+end
+
+lemma continuous_linear_equiv.comp_differentiable_at_iff {f : G → E} {x : G} :
+  differentiable_at 𝕜 (iso ∘ f) x ↔ differentiable_at 𝕜 f x :=
+by rw [← differentiable_within_at_univ, ← differentiable_within_at_univ,
+       iso.comp_differentiable_within_at_iff]
+
+lemma continuous_linear_equiv.comp_differentiable_on_iff {f : G → E} {s : set G} :
+  differentiable_on 𝕜 (iso ∘ f) s ↔ differentiable_on 𝕜 f s :=
+begin
+  rw [differentiable_on, differentiable_on],
+  simp only [iso.comp_differentiable_within_at_iff],
+end
+
+lemma continuous_linear_equiv.comp_differentiable_iff {f : G → E} :
+  differentiable 𝕜 (iso ∘ f) ↔ differentiable 𝕜 f :=
+begin
+  rw [← differentiable_on_univ, ← differentiable_on_univ],
+  exact iso.comp_differentiable_on_iff
+end
+
+lemma continuous_linear_equiv.comp_has_fderiv_within_at_iff
+  {f : G → E} {s : set G} {x : G} {f' : G →L[𝕜] E} :
+  has_fderiv_within_at (iso ∘ f) ((iso : E →L[𝕜] F).comp f') s x ↔ has_fderiv_within_at f f' s x :=
+begin
+  refine ⟨λ H, _, λ H, iso.has_fderiv_at.comp_has_fderiv_within_at x H⟩,
+  have A : f = iso.symm ∘ (iso ∘ f), by { rw [← function.comp.assoc, iso.symm_comp_self], refl },
+  have B : f' = (iso.symm : F →L[𝕜] E).comp ((iso : E →L[𝕜] F).comp f'),
+    by rw [← continuous_linear_map.comp_assoc, iso.coe_symm_comp_coe, continuous_linear_map.id_comp],
+  rw [A, B],
+  exact iso.symm.has_fderiv_at.comp_has_fderiv_within_at x H
+end
+
+lemma continuous_linear_equiv.comp_has_fderiv_at_iff {f : G → E} {x : G} {f' : G →L[𝕜] E} :
+  has_fderiv_at (iso ∘ f) ((iso : E →L[𝕜] F).comp f') x ↔ has_fderiv_at f f' x :=
+by rw [← has_fderiv_within_at_univ, ← has_fderiv_within_at_univ, iso.comp_has_fderiv_within_at_iff]
+
+lemma continuous_linear_equiv.comp_has_fderiv_within_at_iff'
+  {f : G → E} {s : set G} {x : G} {f' : G →L[𝕜] F} :
+  has_fderiv_within_at (iso ∘ f) f' s x ↔
+  has_fderiv_within_at f ((iso.symm : F →L[𝕜] E).comp f') s x :=
+begin
+  set g := (iso.symm : F →L[𝕜] E).comp f' with h,
+  have : f' = (iso : E →L[𝕜] F).comp g,
+    by rw [h, ← continuous_linear_map.comp_assoc, iso.coe_comp_coe_symm,
+           continuous_linear_map.id_comp],
+  rw this,
+  exact iso.comp_has_fderiv_within_at_iff
+end
+
+lemma continuous_linear_equiv.comp_has_fderiv_at_iff' {f : G → E} {x : G} {f' : G →L[𝕜] F} :
+  has_fderiv_at (iso ∘ f) f' x ↔ has_fderiv_at f ((iso.symm : F →L[𝕜] E).comp f') x :=
+by rw [← has_fderiv_within_at_univ, ← has_fderiv_within_at_univ, iso.comp_has_fderiv_within_at_iff']
+
+lemma continuous_linear_equiv.comp_fderiv_within {f : G → E} {s : set G} {x : G}
+  (hxs : unique_diff_within_at 𝕜 s x) :
+  fderiv_within 𝕜 (iso ∘ f) s x = (iso : E →L[𝕜] F).comp (fderiv_within 𝕜 f s x) :=
+begin
+  by_cases h : differentiable_within_at 𝕜 f s x,
+  { rw [fderiv.comp_fderiv_within x iso.differentiable_at h hxs, iso.fderiv] },
+  { have : ¬differentiable_within_at 𝕜 (iso ∘ f) s x,
+      by simp [-coe_fn_coe_base, iso.comp_differentiable_within_at_iff, h],
+    rw [fderiv_within_zero_of_not_differentiable_within_at h,
+        fderiv_within_zero_of_not_differentiable_within_at this],
+    ext y,
+    simp [-coe_fn_coe_base] }
+end
+
+lemma continuous_linear_equiv.comp_fderiv {f : G → E} {x : G} :
+  fderiv 𝕜 (iso ∘ f) x = (iso : E →L[𝕜] F).comp (fderiv 𝕜 f x) :=
+begin
+  rw [← fderiv_within_univ, ← fderiv_within_univ],
+  exact iso.comp_fderiv_within unique_diff_within_at_univ,
+end
+
+end continuous_linear_equiv
+
 end
 
 section
@@ -1726,6 +1872,27 @@ begin
   rw [this, closure_univ]
 end
 
+lemma continuous_linear_equiv.unique_diff_on_preimage_iff (e : F ≃L[𝕜] E) :
+  unique_diff_on 𝕜 (e ⁻¹' s) ↔ unique_diff_on 𝕜 s :=
+begin
+  split,
+  { assume hs x hx,
+    have A : s = e '' (e.symm '' s) :=
+      (equiv.symm_image_image (e.symm.to_linear_equiv.to_equiv) s).symm,
+    have B : e.symm '' s = e⁻¹' s :=
+      equiv.image_eq_preimage e.symm.to_linear_equiv.to_equiv s,
+    rw [A, B, (e.apply_symm_apply x).symm],
+    refine has_fderiv_within_at.unique_diff_within_at_of_continuous_linear_equiv e
+      e.has_fderiv_within_at (hs _ _),
+    rwa [mem_preimage, e.apply_symm_apply x] },
+  { assume hs x hx,
+    have : e ⁻¹' s = e.symm '' s :=
+      (equiv.image_eq_preimage e.symm.to_linear_equiv.to_equiv s).symm,
+    rw [this, (e.symm_apply_apply x).symm],
+    exact has_fderiv_within_at.unique_diff_within_at_of_continuous_linear_equiv e.symm
+      e.symm.has_fderiv_within_at (hs _ hx) },
+end
+
 end tangent_cone
 
 section restrict_scalars

src/analysis/normed_space/basic.lean

@@ -245,6 +245,10 @@ by simp [norm, le_max_left]
 lemma norm_snd_le (x : α × β) : ∥x.2∥ ≤ ∥x∥ :=
 by simp [norm, le_max_right]
 
+lemma norm_prod_le_iff {x : α × β} {r : ℝ} :
+  ∥x∥ ≤ r ↔ ∥x.1∥ ≤ r ∧ ∥x.2∥ ≤ r :=
+max_le_iff
+
 /-- normed group instance on the product of finitely many normed groups, using the sup norm. -/
 instance pi.normed_group {π : ι → Type*} [fintype ι] [∀i, normed_group (π i)] :
   normed_group (Πi, π i) :=

src/linear_algebra/basic.lean

@@ -1343,6 +1343,10 @@ e.to_add_equiv.map_eq_zero_iff
 @[simp] theorem map_ne_zero_iff (e : M ≃ₗ[R] M₂) {x : M} : e x ≠ 0 ↔ x ≠ 0 :=
 e.to_add_equiv.map_ne_zero_iff
 
+@[simp] theorem symm_symm (e : M ≃ₗ[R] M₂) : e.symm.symm = e := by { cases e, refl }
+
+@[simp] theorem symm_symm_apply (e : M ≃ₗ[R] M₂) (x : M) : e.symm.symm x = e x := by { cases e, refl }
+
 /-- A bijective linear map is a linear equivalence. Here, bijectivity is described by saying that
 the kernel of `f` is `{0}` and the range is the universal set. -/
 noncomputable def of_bijective

src/topology/algebra/module.lean

@@ -165,7 +165,8 @@ variables
 {M : Type*} [topological_space M] [add_comm_group M]
 {M₂ : Type*} [topological_space M₂] [add_comm_group M₂]
 {M₃ : Type*} [topological_space M₃] [add_comm_group M₃]
-[module R M] [module R M₂] [module R M₃]
+{M₄ : Type*} [topological_space M₄] [add_comm_group M₄]
+[module R M] [module R M₂] [module R M₃] [module R M₄]
 
 /-- Coerce continuous linear maps to linear maps. -/
 instance : has_coe (M →L[R] M₂) (M →ₗ[R] M₂) := ⟨to_linear_map⟩
@@ -274,6 +275,10 @@ by { ext, simp }
   (g₁ + g₂).comp f = g₁.comp f + g₂.comp f :=
 by { ext, simp }
 
+theorem comp_assoc (h : M₃ →L[R] M₄) (g : M₂ →L[R] M₃) (f : M →L[R] M₂) :
+  (h.comp g).comp f = h.comp (g.comp f) :=
+rfl
+
 instance : has_mul (M →L[R] M) := ⟨comp⟩
 
 instance [topological_add_group M] : ring (M →L[R] M) :=
@@ -413,6 +418,29 @@ def to_homeomorph (e : M ≃L[R] M₂) : M ≃ₜ M₂ := { ..e }
 @[simp] lemma map_eq_zero_iff (e : M ≃L[R] M₂) {x : M} : e x = 0 ↔ x = 0 :=
 e.to_linear_equiv.map_eq_zero_iff
 
+protected lemma continuous (e : M ≃L[R] M₂) : continuous (e : M → M₂) :=
+e.continuous_to_fun
+
+protected lemma continuous_on (e : M ≃L[R] M₂) {s : set M} : continuous_on (e : M → M₂) s :=
+e.continuous.continuous_on
+
+protected lemma continuous_at (e : M ≃L[R] M₂) {x : M} : continuous_at (e : M → M₂) x :=
+e.continuous.continuous_at
+
+protected lemma continuous_within_at (e : M ≃L[R] M₂) {s : set M} {x : M} :
+  continuous_within_at (e : M → M₂) s x :=
+e.continuous.continuous_within_at
+
+lemma comp_continuous_on_iff
+  {α : Type*} [topological_space α] (e : M ≃L[R] M₂) (f : α → M) (s : set α) :
+  continuous_on (e ∘ f) s ↔ continuous_on f s :=
+e.to_homeomorph.comp_continuous_on_iff _ _
+
+lemma comp_continuous_iff
+  {α : Type*} [topological_space α] (e : M ≃L[R] M₂) (f : α → M) :
+  continuous (e ∘ f) ↔ continuous f :=
+e.to_homeomorph.comp_continuous_iff _
+
 section
 variable (M)
 
@@ -454,4 +482,18 @@ continuous_linear_map.ext e.apply_symm_apply
   (e.symm : M₂ →L[R] M).comp (e : M →L[R] M₂) = continuous_linear_map.id :=
 continuous_linear_map.ext e.symm_apply_apply
 
+@[simp] lemma symm_comp_self (e : M ≃L[R] M₂) :
+  (e.symm : M₂ → M) ∘ (e : M → M₂) = id :=
+by{ ext x, exact symm_apply_apply e x }
+
+@[simp] lemma self_comp_symm (e : M ≃L[R] M₂) :
+  (e : M → M₂) ∘ (e.symm : M₂ → M) = id :=
+by{ ext x, exact apply_symm_apply e x }
+
+@[simp] theorem symm_symm (e : M ≃L[R] M₂) : e.symm.symm = e :=
+by { ext x, refl }
+
+@[simp] theorem symm_symm_apply (e : M ≃L[R] M₂) (x : M) : e.symm.symm x = e x :=
+rfl
+
 end continuous_linear_equiv

src/topology/continuous_on.lean

@@ -355,6 +355,10 @@ lemma continuous_on.congr {f g : α → β} {s : set α} (h : continuous_on f s)
   (h' : ∀x ∈ s, g x = f x) : continuous_on g s :=
 h.congr_mono h' (subset.refl _)
 
+lemma continuous_on_congr {f g : α → β} {s : set α} (h' : ∀x ∈ s, g x = f x) :
+  continuous_on g s ↔ continuous_on f s :=
+⟨λ h, continuous_on.congr h (λx hx, (h' x hx).symm), λ h, continuous_on.congr h h'⟩
+
 lemma continuous_at.continuous_within_at {f : α → β} {s : set α} {x : α} (h : continuous_at f x) :
   continuous_within_at f s x :=
 continuous_within_at.mono ((continuous_within_at_univ f x).2 h) (subset_univ _)

src/topology/homeomorph.lean

@@ -110,6 +110,21 @@ def homeomorph_of_continuous_open (e : α ≃ β) (h₁ : continuous e) (h₂ :
   end,
   .. e }
 
+lemma comp_continuous_on_iff (h : α ≃ₜ β) (f : γ → α) (s : set γ) :
+  continuous_on (h ∘ f) s ↔ continuous_on f s :=
+begin
+  split,
+  { assume H,
+    have : continuous_on (h.symm ∘ (h ∘ f)) s :=
+      h.symm.continuous.comp_continuous_on H,
+    rwa [← function.comp.assoc h.symm h f, symm_comp_self h] at this },
+  { exact λ H, h.continuous.comp_continuous_on H }
+end
+
+lemma comp_continuous_iff (h : α ≃ₜ β) (f : γ → α) :
+  continuous (h ∘ f) ↔ continuous f :=
+by simp [continuous_iff_continuous_on_univ, comp_continuous_on_iff]
+
 protected lemma quotient_map (h : α ≃ₜ β) : quotient_map h :=
 ⟨h.to_equiv.surjective, h.coinduced_eq.symm⟩