feat(analysis/calculus/times_cont_diff): more thorough times_cont_diff interface (#3551)

Add missing lemmas on smooth functions between vector spaces, that were necessary to solve the manifold exercises in Lftcm2020.

Changes the `{x : E}` argument from implicit to explicit in `lemma times_cont_diff_within_at.comp` and `lemma times_cont_diff_within_at.comp'`.

Author: sgouezel

src/analysis/calculus/fderiv.lean

@@ -729,13 +729,20 @@ differentiable_id.differentiable_on
 lemma fderiv_id : fderiv 𝕜 id x = id 𝕜 E :=
 has_fderiv_at.fderiv (has_fderiv_at_id x)
 
+lemma fderiv_id' : fderiv 𝕜 (λ (x : E), x) x = continuous_linear_map.id 𝕜 E :=
+fderiv_id
+
 lemma fderiv_within_id (hxs : unique_diff_within_at 𝕜 s x) :
   fderiv_within 𝕜 id s x = id 𝕜 E :=
 begin
   rw differentiable_at.fderiv_within (differentiable_at_id) hxs,
   exact fderiv_id
 end
 
+lemma fderiv_within_id' (hxs : unique_diff_within_at 𝕜 s x) :
+  fderiv_within 𝕜 (λ (x : E), x) s x = continuous_linear_map.id 𝕜 E :=
+fderiv_within_id hxs
+
 end id
 
 section const

src/analysis/calculus/times_cont_diff.lean

@@ -91,7 +91,7 @@ for each natural `m` is by definition `C^∞` at `0`.
 
 There is another issue with the definition of `times_cont_diff_within_at 𝕜 n f s x`. We can
 require the existence and good behavior of derivatives up to order `n` on a neighborhood of `x`
-within `s`. However, this does not imply continuity or differentiability within `s`of the function
+within `s`. However, this does not imply continuity or differentiability within `s` of the function
 at `x`. Therefore, we require such existence and good behavior on a neighborhood of `x` within
 `s ∪ {x}` (which appears as `insert x s` in this file).
 
@@ -157,7 +157,7 @@ derivative, differentiability, higher derivative, `C^n`, multilinear, Taylor ser
 -/
 
 noncomputable theory
-open_locale classical
+open_locale classical big_operators
 
 local notation `∞` := (⊤ : with_top ℕ)
 
@@ -1238,6 +1238,10 @@ lemma times_cont_diff.times_cont_diff_at {n : with_top ℕ} (h : times_cont_diff
   times_cont_diff_at 𝕜 n f x :=
 times_cont_diff_iff_times_cont_diff_at.1 h x
 
+lemma times_cont_diff.times_cont_diff_within_at {n : with_top ℕ} (h : times_cont_diff 𝕜 n f) :
+  times_cont_diff_within_at 𝕜 n f s x :=
+h.times_cont_diff_at.times_cont_diff_within_at
+
 lemma times_cont_diff_top :
   times_cont_diff 𝕜 ∞ f ↔ ∀ (n : ℕ), times_cont_diff 𝕜 n f :=
 by simp [times_cont_diff_on_univ.symm, times_cont_diff_on_top]
@@ -1876,7 +1880,7 @@ times_cont_diff_on_univ.1 $ times_cont_diff_on.comp (times_cont_diff_on_univ.2 h
 
 /-- The composition of `C^n` functions at points in domains is `C^n`. -/
 lemma times_cont_diff_within_at.comp
-  {n : with_top ℕ} {s : set E} {t : set F} {g : F → G} {f : E → F} {x : E}
+  {n : with_top ℕ} {s : set E} {t : set F} {g : F → G} {f : E → F} (x : E)
   (hg : times_cont_diff_within_at 𝕜 n g t (f x))
   (hf : times_cont_diff_within_at 𝕜 n f s x) (st : s ⊆ f ⁻¹' t) :
   times_cont_diff_within_at 𝕜 n (g ∘ f) s x :=
@@ -1906,10 +1910,20 @@ end
 
 /-- The composition of `C^n` functions at points in domains is `C^n`. -/
 lemma times_cont_diff_within_at.comp' {n : with_top ℕ} {s : set E} {t : set F} {g : F → G}
-  {f : E → F} {x : E}
+  {f : E → F} (x : E)
   (hg : times_cont_diff_within_at 𝕜 n g t (f x)) (hf : times_cont_diff_within_at 𝕜 n f s x) :
   times_cont_diff_within_at 𝕜 n (g ∘ f) (s ∩ f⁻¹' t) x :=
-hg.comp (hf.mono (inter_subset_left _ _)) (inter_subset_right _ _)
+hg.comp x (hf.mono (inter_subset_left _ _)) (inter_subset_right _ _)
+
+lemma times_cont_diff.comp_times_cont_diff_within_at
+  {n : with_top ℕ} {g : F → G} {f : E → F} (h : times_cont_diff 𝕜 n g)
+  (hf : times_cont_diff_within_at 𝕜 n f t x) :
+  times_cont_diff_within_at 𝕜 n (g ∘ f) t x :=
+begin
+  have : times_cont_diff_within_at 𝕜 n g univ (f x) :=
+    h.times_cont_diff_at.times_cont_diff_within_at,
+  exact this.comp x hf (subset_univ _),
+end
 
 /-- The bundled derivative of a `C^{n+1}` function is `C^n`. -/
 lemma times_cont_diff_on_fderiv_within_apply {m n : with_top  ℕ} {s : set E}
@@ -1943,59 +1957,143 @@ begin
   exact times_cont_diff_on_fderiv_within_apply hf unique_diff_on_univ hmn
 end
 
-/-- The sum of two `C^n`functions on a domain is `C^n`. -/
-lemma times_cont_diff_on.add {n : with_top ℕ} {s : set E} {f g : E → F}
-  (hf : times_cont_diff_on 𝕜 n f s) (hg : times_cont_diff_on 𝕜 n g s) :
-  times_cont_diff_on 𝕜 n (λx, f x + g x) s :=
+/-! ### Sum of two functions -/
+
+/-- The sum of two `C^n` functions within a set at a point is `C^n` within this set
+at this point. -/
+lemma times_cont_diff_within_at.add {n : with_top ℕ} {s : set E} {f g : E → F}
+  (hf : times_cont_diff_within_at 𝕜 n f s x) (hg : times_cont_diff_within_at 𝕜 n g s x) :
+  times_cont_diff_within_at 𝕜 n (λx, f x + g x) s x :=
 begin
-  have : times_cont_diff 𝕜 n (λp : F × F, p.1 + p.2),
+  have A : times_cont_diff 𝕜 n (λp : F × F, p.1 + p.2),
   { apply is_bounded_linear_map.times_cont_diff,
     exact is_bounded_linear_map.add is_bounded_linear_map.fst is_bounded_linear_map.snd },
-  exact this.comp_times_cont_diff_on (hf.prod hg)
+  exact A.times_cont_diff_within_at.comp x (hf.prod hg) subset_preimage_univ,
+end
+
+/-- The sum of two `C^n` functions at a point is `C^n` at this point. -/
+lemma times_cont_diff_at.add {n : with_top ℕ} {f g : E → F}
+  (hf : times_cont_diff_at 𝕜 n f x) (hg : times_cont_diff_at 𝕜 n g x) :
+  times_cont_diff_at 𝕜 n (λx, f x + g x) x :=
+begin
+  rw [← times_cont_diff_within_at_univ] at *,
+  exact hf.add hg
 end
 
-/-- The sum of two `C^n`functions is `C^n`. -/
+/-- The sum of two `C^n` functions on a domain is `C^n`. -/
+lemma times_cont_diff_on.add {n : with_top ℕ} {s : set E} {f g : E → F}
+  (hf : times_cont_diff_on 𝕜 n f s) (hg : times_cont_diff_on 𝕜 n g s) :
+  times_cont_diff_on 𝕜 n (λx, f x + g x) s :=
+λ x hx, (hf x hx).add (hg x hx)
+
+/-- The sum of two `C^n` functions is `C^n`. -/
 lemma times_cont_diff.add {n : with_top ℕ} {f g : E → F}
   (hf : times_cont_diff 𝕜 n f) (hg : times_cont_diff 𝕜 n g) : times_cont_diff 𝕜 n (λx, f x + g x) :=
 begin
-  have : times_cont_diff 𝕜 n (λp : F × F, p.1 + p.2),
-  { apply is_bounded_linear_map.times_cont_diff,
-    exact is_bounded_linear_map.add is_bounded_linear_map.fst is_bounded_linear_map.snd },
-  exact this.comp (hf.prod hg)
+  rw ← times_cont_diff_on_univ at *,
+  exact hf.add hg
 end
 
-/-- The negative of a `C^n`function on a domain is `C^n`. -/
-lemma times_cont_diff_on.neg {n : with_top ℕ} {s : set E} {f : E → F}
-  (hf : times_cont_diff_on 𝕜 n f s) : times_cont_diff_on 𝕜 n (λx, -f x) s :=
+/-! ### Negative -/
+
+/-- The negative of a `C^n` function within a domain at a point is `C^n` within this domain at
+this point. -/
+lemma times_cont_diff_within_at.neg {n : with_top ℕ} {s : set E} {f : E → F}
+  (hf : times_cont_diff_within_at 𝕜 n f s x) : times_cont_diff_within_at 𝕜 n (λx, -f x) s x :=
 begin
   have : times_cont_diff 𝕜 n (λp : F, -p),
   { apply is_bounded_linear_map.times_cont_diff,
     exact is_bounded_linear_map.neg is_bounded_linear_map.id },
-  exact this.comp_times_cont_diff_on hf
+  exact this.times_cont_diff_within_at.comp x hf subset_preimage_univ
+end
+
+/-- The negative of a `C^n` function at a point is `C^n` at this point. -/
+lemma times_cont_diff_at.neg {n : with_top ℕ} {f : E → F}
+  (hf : times_cont_diff_at 𝕜 n f x) : times_cont_diff_at 𝕜 n (λx, -f x) x :=
+begin
+  rw ← times_cont_diff_within_at_univ at *,
+  exact hf.neg
 end
 
-/-- The negative of a `C^n`function is `C^n`. -/
+/-- The negative of a `C^n` function on a domain is `C^n`. -/
+lemma times_cont_diff_on.neg {n : with_top ℕ} {s : set E} {f : E → F}
+  (hf : times_cont_diff_on 𝕜 n f s) : times_cont_diff_on 𝕜 n (λx, -f x) s :=
+λ x hx, (hf x hx).neg
+
+/-- The negative of a `C^n` function is `C^n`. -/
 lemma times_cont_diff.neg {n : with_top ℕ} {f : E → F} (hf : times_cont_diff 𝕜 n f) :
   times_cont_diff 𝕜 n (λx, -f x) :=
 begin
-  have : times_cont_diff 𝕜 n (λp : F, -p),
-  { apply is_bounded_linear_map.times_cont_diff,
-    exact is_bounded_linear_map.neg is_bounded_linear_map.id },
-  exact this.comp hf
+  rw ← times_cont_diff_on_univ at *,
+  exact hf.neg
 end
 
-/-- The difference of two `C^n`functions on a domain is `C^n`. -/
+/-! ### Subtraction -/
+
+/-- The difference of two `C^n` functions within a set at a point is `C^n` within this set
+at this point. -/
+lemma times_cont_diff_within_at.sub {n : with_top ℕ} {s : set E} {f g : E → F}
+  (hf : times_cont_diff_within_at 𝕜 n f s x) (hg : times_cont_diff_within_at 𝕜 n g s x) :
+  times_cont_diff_within_at 𝕜 n (λx, f x - g x) s x :=
+hf.add hg.neg
+
+/-- The difference of two `C^n` functions at a point is `C^n` at this point. -/
+lemma times_cont_diff_at.sub {n : with_top ℕ} {f g : E → F}
+  (hf : times_cont_diff_at 𝕜 n f x) (hg : times_cont_diff_at 𝕜 n g x) :
+  times_cont_diff_at 𝕜 n (λx, f x - g x) x :=
+hf.add hg.neg
+
+/-- The difference of two `C^n` functions on a domain is `C^n`. -/
 lemma times_cont_diff_on.sub {n : with_top ℕ} {s : set E} {f g : E → F}
   (hf : times_cont_diff_on 𝕜 n f s) (hg : times_cont_diff_on 𝕜 n g s) :
   times_cont_diff_on 𝕜 n (λx, f x - g x) s :=
-hf.add (hg.neg)
+hf.add hg.neg
 
-/-- The difference of two `C^n`functions is `C^n`. -/
+/-- The difference of two `C^n` functions is `C^n`. -/
 lemma times_cont_diff.sub {n : with_top ℕ} {f g : E → F}
-  (hf : times_cont_diff 𝕜 n f) (hg : times_cont_diff 𝕜 n g) :
-  times_cont_diff 𝕜 n (λx, f x - g x) :=
+  (hf : times_cont_diff 𝕜 n f) (hg : times_cont_diff 𝕜 n g) : times_cont_diff 𝕜 n (λx, f x - g x) :=
 hf.add hg.neg
 
+/-! ### Sum of finitely many functions -/
+
+lemma times_cont_diff_within_at.sum
+  {ι : Type*} {f : ι → E → F} {s : finset ι} {n : with_top ℕ} {t : set E} {x : E}
+  (h : ∀ i ∈ s, times_cont_diff_within_at 𝕜 n (λ x, f i x) t x) :
+  times_cont_diff_within_at 𝕜 n (λ x, (∑ i in s, f i x)) t x :=
+begin
+  classical,
+  induction s using finset.induction_on with i s is IH,
+  { simp [times_cont_diff_within_at_const] },
+  { simp only [is, finset.sum_insert, not_false_iff],
+    exact (h _ (finset.mem_insert_self i s)).add (IH (λ j hj, h _ (finset.mem_insert_of_mem hj))) }
+end
+
+lemma times_cont_diff_at.sum
+  {ι : Type*} {f : ι → E → F} {s : finset ι} {n : with_top ℕ} {x : E}
+  (h : ∀ i ∈ s, times_cont_diff_at 𝕜 n (λ x, f i x) x) :
+  times_cont_diff_at 𝕜 n (λ x, (∑ i in s, f i x)) x :=
+begin
+  rw [← times_cont_diff_within_at_univ] at *,
+  exact times_cont_diff_within_at.sum h
+end
+
+lemma times_cont_diff_on.sum
+  {ι : Type*} {f : ι → E → F} {s : finset ι} {n : with_top ℕ} {t : set E}
+  (h : ∀ i ∈ s, times_cont_diff_on 𝕜 n (λ x, f i x) t) :
+  times_cont_diff_on 𝕜 n (λ x, (∑ i in s, f i x)) t :=
+λ x hx, times_cont_diff_within_at.sum (λ i hi, h i hi x hx)
+
+lemma times_cont_diff.sum
+  {ι : Type*} {f : ι → E → F} {s : finset ι} {n : with_top ℕ}
+  (h : ∀ i ∈ s, times_cont_diff 𝕜 n (λ x, f i x)) :
+  times_cont_diff 𝕜 n (λ x, (∑ i in s, f i x)) :=
+begin
+  simp [← times_cont_diff_on_univ] at *,
+  exact times_cont_diff_on.sum h
+end
+
+/-! ### Cartesian product of two functions-/
+
 /-- The product map of two `C^n` functions is `C^n`. -/
 lemma times_cont_diff_on.map_prod {E' : Type*} [normed_group E'] [normed_space 𝕜 E']
   {F' : Type*} [normed_group F'] [normed_space 𝕜 F']

src/geometry/manifold/times_cont_mdiff.lean

@@ -93,7 +93,7 @@ lemma times_cont_diff_within_at_local_invariant_prop (n : with_top ℕ) :
     rw this at h,
     have : I (e x) ∈ (I.symm) ⁻¹' e.target ∩ range ⇑I, by simp only [hx] with mfld_simps,
     have := ((mem_groupoid_of_pregroupoid.2 he).2.times_cont_diff_within_at this).of_le le_top,
-    convert h.comp' this using 1,
+    convert h.comp' _ this using 1,
     { ext y, simp only with mfld_simps },
     { mfld_set_tac }
   end,
@@ -113,7 +113,7 @@ lemma times_cont_diff_within_at_local_invariant_prop (n : with_top ℕ) :
     have A : (I' ∘ f ∘ I.symm) (I x) ∈ (I'.symm ⁻¹' e'.source ∩ range I'),
       by simp only [hx] with mfld_simps,
     have := ((mem_groupoid_of_pregroupoid.2 he').1.times_cont_diff_within_at A).of_le le_top,
-    convert this.comp h _,
+    convert this.comp _ h _,
     { ext y, simp only with mfld_simps },
     { assume y hy, simp only with mfld_simps at hy, simpa only [hy] with mfld_simps using hs hy.2 }
   end }

src/topology/metric_space/gromov_hausdorff.lean

@@ -409,7 +409,7 @@ instance GH_space_metric_space : metric_space GH_space :=
   end,
   dist_triangle := λx y z, begin
     /- To show the triangular inequality between `X`, `Y` and `Z`, realize an optimal coupling
-    between `X` and `Y` in a space `γ1`, and an optimal coupling between `Y`and `Z` in a space `γ2`.
+    between `X` and `Y` in a space `γ1`, and an optimal coupling between `Y` and `Z` in a space `γ2`.
     Then, glue these metric spaces along `Y`. We get a new space `γ` in which `X` and `Y` are
     optimally coupled, as well as `Y` and `Z`. Apply the triangle inequality for the Hausdorff
     distance in `γ` to conclude. -/

src/topology/metric_space/hausdorff_distance.lean

@@ -211,7 +211,7 @@ exists_edist_lt_of_inf_edist_lt $ calc
   ... ≤ Sup ((λx, inf_edist x t) '' s) ⊔ Sup ((λx, inf_edist x s) '' t) : le_sup_left
   ... < r : by rwa Hausdorff_edist_def at H
 
-/-- The distance from `x` to `s`or `t` is controlled in terms of the Hausdorff distance
+/-- The distance from `x` to `s` or `t` is controlled in terms of the Hausdorff distance
 between `s` and `t` -/
 lemma inf_edist_le_inf_edist_add_Hausdorff_edist :
   inf_edist x t ≤ inf_edist x s + Hausdorff_edist s t :=