feat(analysis/calculus/cont_diff): Prove that fderiv_within is `C^n…

…` for functions with parameters (#16946)

* Prove that `fderiv_within` is `C^n` (at a point within a set) for a function with parameters
* There are some inconvenient side-conditions needed for the lemmas, feel free to recommend improvements
* `set.diag_image` is not used, but a (useful) left-over used before a refactor.
* This is useful for lemmas about `mfderiv` and the smooth vector bundle refactor
* From the sphere eversion project

src/analysis/calculus/cont_diff.lean

@@ -169,15 +169,15 @@ universes u v w
 local attribute [instance, priority 1001]
 normed_add_comm_group.to_add_comm_group normed_space.to_module' add_comm_group.to_add_comm_monoid
 
-open set fin filter
+open set fin filter function
 open_locale topological_space
 
 variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
 {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
 {F : Type*} [normed_add_comm_group F] [normed_space 𝕜 F]
 {G : Type*} [normed_add_comm_group G] [normed_space 𝕜 G]
 {X : Type*} [normed_add_comm_group X] [normed_space 𝕜 X]
-{s s₁ t u : set E} {f f₁ : E → F} {g : F → G} {x : E} {c : F}
+{s s₁ t u : set E} {f f₁ : E → F} {g : F → G} {x x₀ : E} {c : F}
 {b : E × F → G} {m n : ℕ∞}
 
 /-! ### Functions with a Taylor series on a domain -/
@@ -2289,6 +2289,22 @@ lemma cont_diff_on.clm_comp {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F
   cont_diff_on 𝕜 n (λ x, (g x).comp (f x)) s :=
 is_bounded_bilinear_map_comp.cont_diff.comp_cont_diff_on₂ hg hf
 
+lemma cont_diff.clm_apply {f : E → F →L[𝕜] G} {g : E → F} {n : ℕ∞}
+  (hf : cont_diff 𝕜 n f) (hg : cont_diff 𝕜 n g) :
+  cont_diff 𝕜 n (λ x, (f x) (g x)) :=
+is_bounded_bilinear_map_apply.cont_diff.comp₂ hf hg
+
+lemma cont_diff_on.clm_apply {f : E → F →L[𝕜] G} {g : E → F} {n : ℕ∞}
+  (hf : cont_diff_on 𝕜 n f s) (hg : cont_diff_on 𝕜 n g s) :
+  cont_diff_on 𝕜 n (λ x, (f x) (g x)) s :=
+is_bounded_bilinear_map_apply.cont_diff.comp_cont_diff_on₂ hf hg
+
+lemma cont_diff.smul_right {f : E → F →L[𝕜] 𝕜} {g : E → G} {n : ℕ∞}
+  (hf : cont_diff 𝕜 n f) (hg : cont_diff 𝕜 n g) :
+  cont_diff 𝕜 n (λ x, (f x).smul_right (g x)) :=
+-- giving the following implicit type arguments speeds up elaboration significantly
+(@is_bounded_bilinear_map_smul_right 𝕜 _ F _ _ G _ _).cont_diff.comp₂ hf hg
+
 end specific_bilinear_maps
 
 /--
@@ -2309,44 +2325,171 @@ Warning: see remarks attached to `cont_diff_prod_assoc`
 lemma cont_diff_prod_assoc_symm : cont_diff 𝕜 ⊤ $ (equiv.prod_assoc E F G).symm :=
 (linear_isometry_equiv.prod_assoc 𝕜 E F G).symm.cont_diff
 
-/-! ### Bundled derivatives -/
-
-lemma cont_diff_within_at.fderiv_within'
-  (hf : cont_diff_within_at 𝕜 n f s x) (hs : ∀ᶠ y in 𝓝[insert x s] x, unique_diff_within_at 𝕜 s y)
-  (hmn : m + 1 ≤ n) :
-  cont_diff_within_at 𝕜 m (fderiv_within 𝕜 f s) s x :=
-begin
-  have : ∀ k : ℕ, (k + 1 : ℕ∞) ≤ n → cont_diff_within_at 𝕜 k (fderiv_within 𝕜 f s) s x,
-  { intros k hkn,
+/-! ### Bundled derivatives are smooth -/
+
+/-- One direction of `cont_diff_within_at_succ_iff_has_fderiv_within_at`, but where all derivatives
+	are taken within the same set. Version for partial derivatives / functions with parameters.
+	If `f x` is a `C^n+1` family of functions and `g x` is a `C^n` family of points, then the
+  derivative of `f x` at `g x` depends in a `C^n` way on `x`. We give a general version of this fact
+  relative to sets which may not have unique derivatives, in the following form.
+	If `f : E × F → G` is `C^n+1` at `(x₀, g(x₀))` in `(s ∪ {x₀}) × t ⊆ E × F` and `g : E → F` is
+	`C^n` at `x₀` within some set `s ⊆ E`, then there is a function `f' : E → F →L[𝕜] G`
+	that is `C^n` at `x₀` within `s` such that for all `x` sufficiently close to `x₀` within
+	`s ∪ {x₀}` the function `y ↦ f x y` has derivative `f' x` at `g x` within `t ⊆ F`.
+	For convenience, we return an explicit set of `x`'s where this holds that is a subset of
+	`s ∪ {x₀}`.
+	We need one additional condition, namely that `t` is a neighborhood of `g(x₀)` within `g '' s`.
+	-/
+lemma cont_diff_within_at.has_fderiv_within_at_nhds {f : E → F → G} {g : E → F}
+  {t : set F} {n : ℕ} {x₀ : E}
+  (hf : cont_diff_within_at 𝕜 (n+1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀))
+  (hg : cont_diff_within_at 𝕜 n g s x₀)
+  (hgt : t ∈ 𝓝[g '' s] g x₀) :
+  ∃ v ∈ 𝓝[insert x₀ s] x₀, v ⊆ insert x₀ s ∧ ∃ f' : E → F →L[𝕜] G,
+    (∀ x ∈ v, has_fderiv_within_at (f x) (f' x) t (g x)) ∧
+    cont_diff_within_at 𝕜 n (λ x, f' x) s x₀ :=
+begin
+  have hst : insert x₀ s ×ˢ t ∈ 𝓝[(λ x, (x, g x)) '' s] (x₀, g x₀),
+  { refine nhds_within_mono _ _ (nhds_within_prod self_mem_nhds_within hgt),
+    simp_rw [image_subset_iff, mk_preimage_prod, preimage_id', subset_inter_iff, subset_insert,
+      true_and, subset_preimage_image] },
+  obtain ⟨v, hv, hvs, f', hvf', hf'⟩ := cont_diff_within_at_succ_iff_has_fderiv_within_at'.mp hf,
+  refine ⟨(λ z, (z, g z)) ⁻¹' v ∩ insert x₀ s, _, inter_subset_right _ _,
+    λ z, (f' (z, g z)).comp (continuous_linear_map.inr 𝕜 E F), _, _⟩,
+  { refine inter_mem _ self_mem_nhds_within,
+    have := mem_of_mem_nhds_within (mem_insert _ _) hv,
+    refine mem_nhds_within_insert.mpr ⟨this, _⟩,
+    refine (continuous_within_at_id.prod hg.continuous_within_at).preimage_mem_nhds_within' _,
+    rw [← nhds_within_le_iff] at hst hv ⊢,
+    refine (hst.trans $ nhds_within_mono _ $ subset_insert _ _).trans hv },
+  { intros z hz,
+    have := hvf' (z, g z) hz.1,
+    refine this.comp _ (has_fderiv_at_prod_mk_right _ _).has_fderiv_within_at _,
+    exact maps_to'.mpr (image_prod_mk_subset_prod_right hz.2) },
+  { exact (hf'.continuous_linear_map_comp $ (continuous_linear_map.compL 𝕜 F (E × F) G).flip
+      (continuous_linear_map.inr 𝕜 E F)).comp_of_mem x₀
+      (cont_diff_within_at_id.prod hg) hst },
+end
+
+/-- The most general lemma stating that `x ↦ fderiv_within 𝕜 (f x) t (g x)` is `C^n`
+at a point within a set.
+To show that `x ↦ D_yf(x,y)g(x)` (taken within `t`) is `C^m` at `x₀` within `s`, we require that
+* `f` is `C^n` at `(x₀, g(x₀))` within `(s ∪ {x₀}) × t` for `n ≥ m+1`.
+* `g` is `C^m` at `x₀` within `s`;
+* Derivatives are unique at `g(x)` within `t` for `x` sufficiently close to `x₀` within `s ∪ {x₀}`;
+* `t` is a neighborhood of `g(x₀)` within `g '' s`; -/
+lemma cont_diff_within_at.fderiv_within'' {f : E → F → G} {g : E → F}
+  {t : set F} {n : ℕ∞}
+  (hf : cont_diff_within_at 𝕜 n (function.uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀))
+  (hg : cont_diff_within_at 𝕜 m g s x₀)
+  (ht : ∀ᶠ x in 𝓝[insert x₀ s] x₀, unique_diff_within_at 𝕜 t (g x))
+  (hmn : m + 1 ≤ n)
+  (hgt : t ∈ 𝓝[g '' s] g x₀) :
+  cont_diff_within_at 𝕜 m (λ x, fderiv_within 𝕜 (f x) t (g x)) s x₀ :=
+begin
+  have : ∀ k : ℕ, (k : ℕ∞) ≤ m →
+    cont_diff_within_at 𝕜 k (λ x, fderiv_within 𝕜 (f x) t (g x)) s x₀,
+  { intros k hkm,
     obtain ⟨v, hv, -, f', hvf', hf'⟩ :=
-      cont_diff_within_at_succ_iff_has_fderiv_within_at'.mp (hf.of_le hkn),
-    apply hf'.congr_of_eventually_eq_insert,
-    filter_upwards [hv, hs],
+      (hf.of_le $ (add_le_add_right hkm 1).trans hmn).has_fderiv_within_at_nhds (hg.of_le hkm) hgt,
+    refine hf'.congr_of_eventually_eq_insert _,
+    filter_upwards [hv, ht],
     exact λ y hy h2y, (hvf' y hy).fderiv_within h2y },
   induction m using with_top.rec_top_coe,
   { obtain rfl := eq_top_iff.mpr hmn,
     rw [cont_diff_within_at_top],
     exact λ m, this m le_top },
-  exact this m hmn
+  exact this m le_rfl
+end
+
+/-- A special case of `cont_diff_within_at.fderiv_within''` where we require that `s ⊆ g⁻¹(t)`. -/
+lemma cont_diff_within_at.fderiv_within' {f : E → F → G} {g : E → F}
+  {t : set F} {n : ℕ∞}
+  (hf : cont_diff_within_at 𝕜 n (function.uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀))
+  (hg : cont_diff_within_at 𝕜 m g s x₀)
+  (ht : ∀ᶠ x in 𝓝[insert x₀ s] x₀, unique_diff_within_at 𝕜 t (g x))
+  (hmn : m + 1 ≤ n)
+  (hst : s ⊆ g ⁻¹' t) :
+  cont_diff_within_at 𝕜 m (λ x, fderiv_within 𝕜 (f x) t (g x)) s x₀ :=
+hf.fderiv_within'' hg ht hmn $ mem_of_superset self_mem_nhds_within $ image_subset_iff.mpr hst
+
+/-- A special case of `cont_diff_within_at.fderiv_within'` where we require that `x₀ ∈ s` and there
+  are unique derivatives everywhere within `t`. -/
+lemma cont_diff_within_at.fderiv_within {f : E → F → G} {g : E → F}
+  {t : set F} {n : ℕ∞}
+  (hf : cont_diff_within_at 𝕜 n (function.uncurry f) (s ×ˢ t) (x₀, g x₀))
+  (hg : cont_diff_within_at 𝕜 m g s x₀)
+  (ht : unique_diff_on 𝕜 t)
+  (hmn : m + 1 ≤ n) (hx₀ : x₀ ∈ s)
+  (hst : s ⊆ g ⁻¹' t) :
+  cont_diff_within_at 𝕜 m (λ x, fderiv_within 𝕜 (f x) t (g x)) s x₀ :=
+begin
+  rw [← insert_eq_self.mpr hx₀] at hf,
+  refine hf.fderiv_within' hg _ hmn hst,
+  rw [insert_eq_self.mpr hx₀],
+  exact eventually_of_mem self_mem_nhds_within (λ x hx, ht _ (hst hx))
+end
+
+/-- `x ↦ fderiv_within 𝕜 (f x) t (g x) (k x)` is smooth at a point within a set. -/
+lemma cont_diff_within_at.fderiv_within_apply {f : E → F → G} {g k : E → F}
+  {t : set F} {n : ℕ∞}
+  (hf : cont_diff_within_at 𝕜 n (function.uncurry f) (s ×ˢ t) (x₀, g x₀))
+  (hg : cont_diff_within_at 𝕜 m g s x₀)
+  (hk : cont_diff_within_at 𝕜 m k s x₀)
+  (ht : unique_diff_on 𝕜 t)
+  (hmn : m + 1 ≤ n) (hx₀ : x₀ ∈ s)
+  (hst : s ⊆ g ⁻¹' t) :
+  cont_diff_within_at 𝕜 m (λ x, fderiv_within 𝕜 (f x) t (g x) (k x)) s x₀ :=
+(cont_diff_fst.clm_apply cont_diff_snd).cont_diff_at.comp_cont_diff_within_at x₀
+  ((hf.fderiv_within hg ht hmn hx₀ hst).prod hk)
+
+/-- `fderiv_within 𝕜 f s` is smooth at `x₀` within `s`. -/
+lemma cont_diff_within_at.fderiv_within_right
+  (hf : cont_diff_within_at 𝕜 n f s x₀) (hs : unique_diff_on 𝕜 s)
+  (hmn : (m + 1 : ℕ∞) ≤ n) (hx₀s : x₀ ∈ s) :
+  cont_diff_within_at 𝕜 m (fderiv_within 𝕜 f s) s x₀ :=
+cont_diff_within_at.fderiv_within
+  (cont_diff_within_at.comp (x₀, x₀) hf cont_diff_within_at_snd $ prod_subset_preimage_snd s s)
+  cont_diff_within_at_id hs hmn hx₀s (by rw [preimage_id'])
+
+/-- `x ↦ fderiv 𝕜 (f x) (g x)` is smooth at `x₀`. -/
+lemma cont_diff_at.cont_diff_at_fderiv {f : E → F → G} {g : E → F} {n : ℕ∞}
+  (hf : cont_diff_at 𝕜 n (function.uncurry f) (x₀, g x₀))
+  (hg : cont_diff_at 𝕜 m g x₀)
+  (hmn : m + 1 ≤ n) :
+  cont_diff_at 𝕜 m (λ x, fderiv 𝕜 (f x) (g x)) x₀ :=
+begin
+  simp_rw [← fderiv_within_univ],
+  refine (cont_diff_within_at.fderiv_within hf.cont_diff_within_at hg.cont_diff_within_at
+    unique_diff_on_univ hmn (mem_univ x₀) _).cont_diff_at univ_mem,
+  rw [preimage_univ]
 end
 
-lemma cont_diff_within_at.fderiv_within
-  (hf : cont_diff_within_at 𝕜 n f s x) (hs : unique_diff_on 𝕜 s)
-  (hmn : (m + 1 : ℕ∞) ≤ n) (hxs : x ∈ s) :
-  cont_diff_within_at 𝕜 m (fderiv_within 𝕜 f s) s x :=
-hf.fderiv_within' (by { rw [insert_eq_of_mem hxs], exact eventually_of_mem self_mem_nhds_within hs})
-  hmn
+/-- `x ↦ fderiv 𝕜 (f x) (g x)` is smooth. -/
+lemma cont_diff.fderiv {f : E → F → G} {g : E → F} {n m : ℕ∞}
+  (hf : cont_diff 𝕜 m $ function.uncurry f) (hg : cont_diff 𝕜 n g) (hnm : n + 1 ≤ m) :
+    cont_diff 𝕜 n (λ x, fderiv 𝕜 (f x) (g x)) :=
+cont_diff_iff_cont_diff_at.mpr $ λ x, hf.cont_diff_at.cont_diff_at_fderiv hg.cont_diff_at hnm
+
+/-- `x ↦ fderiv 𝕜 (f x) (g x)` is continuous. -/
+lemma continuous.fderiv {f : E → F → G} {g : E → F} {n : ℕ∞}
+  (hf : cont_diff 𝕜 n $ function.uncurry f) (hg : continuous g) (hn : 1 ≤ n) :
+    continuous (λ x, fderiv 𝕜 (f x) (g x)) :=
+(hf.fderiv (cont_diff_zero.mpr hg) hn).continuous
+
+/-- `x ↦ fderiv 𝕜 (f x) (g x) (k x)` is smooth. -/
+lemma cont_diff.fderiv_apply {f : E → F → G} {g k : E → F} {n m : ℕ∞}
+  (hf : cont_diff 𝕜 m $ function.uncurry f) (hg : cont_diff 𝕜 n g) (hk : cont_diff 𝕜 n k)
+  (hnm : n + 1 ≤ m) :
+  cont_diff 𝕜 n (λ x, fderiv 𝕜 (f x) (g x) (k x)) :=
+(hf.fderiv hg hnm).clm_apply hk
 
 /-- The bundled derivative of a `C^{n+1}` function is `C^n`. -/
-lemma cont_diff_on_fderiv_within_apply {m n : with_top  ℕ} {s : set E}
+lemma cont_diff_on_fderiv_within_apply {m n : ℕ∞} {s : set E}
   {f : E → F} (hf : cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) (hmn : m + 1 ≤ n) :
   cont_diff_on 𝕜 m (λp : E × E, (fderiv_within 𝕜 f s p.1 : E →L[𝕜] F) p.2) (s ×ˢ univ) :=
-have I : cont_diff_on 𝕜 m (λ (x : E), fderiv_within 𝕜 f s x) s := hf.fderiv_within hs hmn,
-have J : cont_diff_on 𝕜 m (λ (x : E × E), x.1) (s ×ˢ univ) := cont_diff_fst.cont_diff_on,
-have A : cont_diff 𝕜 m (λp : (E →L[𝕜] F) × E, p.1 p.2) := is_bounded_bilinear_map_apply.cont_diff,
-have B : cont_diff_on 𝕜 m (λ (p : E × E), ((fderiv_within 𝕜 f s p.fst), p.snd)) (s ×ˢ univ) :=
-(I.comp J (prod_subset_preimage_fst _ _)).prod is_bounded_linear_map.snd.cont_diff.cont_diff_on,
-A.comp_cont_diff_on B
+((hf.fderiv_within hs hmn).comp cont_diff_on_fst (prod_subset_preimage_fst _ _)).clm_apply
+  cont_diff_on_snd
 
 /-- If a function is at least `C^1`, its bundled derivative (mapping `(x, v)` to `Df(x) v`) is
 continuous. -/
@@ -3141,7 +3284,7 @@ lemma cont_diff_on_clm_apply {n : ℕ∞} {f : E → F →L[𝕜] G}
   {s : set E} [finite_dimensional 𝕜 F] :
   cont_diff_on 𝕜 n f s ↔ ∀ y, cont_diff_on 𝕜 n (λ x, f x y) s :=
 begin
-  refine ⟨λ h y, (continuous_linear_map.apply 𝕜 G y).cont_diff.comp_cont_diff_on h, λ h, _⟩,
+  refine ⟨λ h y, h.clm_apply cont_diff_on_const, λ h, _⟩,
   let d := finrank 𝕜 F,
   have hd : d = finrank 𝕜 (fin d → 𝕜) := (finrank_fin_fun 𝕜).symm,
   let e₁ := continuous_linear_equiv.of_finrank_eq hd,

src/data/set/prod.lean

@@ -353,6 +353,15 @@ prod_subset_iff.trans disjoint_iff_forall_ne.symm
 
 lemma diag_preimage_prod_self (s : set α) : (λ x, (x, x)) ⁻¹' (s ×ˢ s) = s := inter_self s
 
+lemma diag_image (s : set α) : (λ x, (x, x)) '' s = diagonal α ∩ (s ×ˢ s) :=
+begin
+  ext x, split,
+  { rintro ⟨x, hx, rfl⟩, exact ⟨rfl, hx, hx⟩ },
+  { obtain ⟨x, y⟩ := x,
+    rintro ⟨rfl : x = y, h2x⟩,
+    exact mem_image_of_mem _ h2x.1 }
+end
+
 end diagonal
 
 section off_diag