feat(analysis/calculus/cont_diff): add more prod lemmas (#13521)

* Add `cont_diff.fst`, `cont_diff.comp₂`, `cont_diff_prod_mk_left` and many variants.
* From the sphere eversion project
* Required for convolutions
* PR #13423 is similar for continuity

src/analysis/calculus/cont_diff.lean

@@ -1273,13 +1273,12 @@ variable (𝕜)
 order `n`, which are continuous. Contrary to the case of definitions in domains (where derivatives
 might not be unique) we do not need to localize the definition in space or time.
 -/
-definition cont_diff (n : with_top ℕ) (f : E → F)  :=
+definition cont_diff (n : with_top ℕ) (f : E → F) :=
 ∃ p : E → formal_multilinear_series 𝕜 E F, has_ftaylor_series_up_to n f p
 
 variable {𝕜}
 
-theorem cont_diff_on_univ :
-  cont_diff_on 𝕜 n f univ ↔ cont_diff 𝕜 n f :=
+theorem cont_diff_on_univ : cont_diff_on 𝕜 n f univ ↔ cont_diff 𝕜 n f :=
 begin
   split,
   { assume H,
@@ -1290,39 +1289,31 @@ begin
     exact ⟨univ, filter.univ_sets _, p, (hp.has_ftaylor_series_up_to_on univ).of_le hm⟩ }
 end
 
-lemma cont_diff_iff_cont_diff_at :
-  cont_diff 𝕜 n f ↔ ∀ x, cont_diff_at 𝕜 n f x :=
+lemma cont_diff_iff_cont_diff_at : cont_diff 𝕜 n f ↔ ∀ x, cont_diff_at 𝕜 n f x :=
 by simp [← cont_diff_on_univ, cont_diff_on, cont_diff_at]
 
-lemma cont_diff.cont_diff_at (h : cont_diff 𝕜 n f) :
-  cont_diff_at 𝕜 n f x :=
+lemma cont_diff.cont_diff_at (h : cont_diff 𝕜 n f) : cont_diff_at 𝕜 n f x :=
 cont_diff_iff_cont_diff_at.1 h x
 
-lemma cont_diff.cont_diff_within_at (h : cont_diff 𝕜 n f) :
-  cont_diff_within_at 𝕜 n f s x :=
+lemma cont_diff.cont_diff_within_at (h : cont_diff 𝕜 n f) : cont_diff_within_at 𝕜 n f s x :=
 h.cont_diff_at.cont_diff_within_at
 
-lemma cont_diff_top :
-  cont_diff 𝕜 ∞ f ↔ ∀ (n : ℕ), cont_diff 𝕜 n f :=
+lemma cont_diff_top : cont_diff 𝕜 ∞ f ↔ ∀ (n : ℕ), cont_diff 𝕜 n f :=
 by simp [cont_diff_on_univ.symm, cont_diff_on_top]
 
-lemma cont_diff_all_iff_nat :
-  (∀ n, cont_diff 𝕜 n f) ↔ (∀ n : ℕ, cont_diff 𝕜 n f) :=
+lemma cont_diff_all_iff_nat : (∀ n, cont_diff 𝕜 n f) ↔ (∀ n : ℕ, cont_diff 𝕜 n f) :=
 by simp only [← cont_diff_on_univ, cont_diff_on_all_iff_nat]
 
-lemma cont_diff.cont_diff_on
-  (h : cont_diff 𝕜 n f) : cont_diff_on 𝕜 n f s :=
+lemma cont_diff.cont_diff_on (h : cont_diff 𝕜 n f) : cont_diff_on 𝕜 n f s :=
 (cont_diff_on_univ.2 h).mono (subset_univ _)
 
-@[simp] lemma cont_diff_zero :
-  cont_diff 𝕜 0 f ↔ continuous f :=
+@[simp] lemma cont_diff_zero : cont_diff 𝕜 0 f ↔ continuous f :=
 begin
   rw [← cont_diff_on_univ, continuous_iff_continuous_on_univ],
   exact cont_diff_on_zero
 end
 
-lemma cont_diff_at_zero :
-  cont_diff_at 𝕜 0 f x ↔ ∃ u ∈ 𝓝 x, continuous_on f u :=
+lemma cont_diff_at_zero : cont_diff_at 𝕜 0 f x ↔ ∃ u ∈ 𝓝 x, continuous_on f u :=
 by { rw ← cont_diff_within_at_univ, simp [cont_diff_within_at_zero, nhds_within_univ] }
 
 theorem cont_diff_at_one_iff : cont_diff_at 𝕜 1 f x ↔
@@ -1331,18 +1322,20 @@ by simp_rw [show (1 : with_top ℕ) = (0 + 1 : ℕ), from (zero_add 1).symm,
   cont_diff_at_succ_iff_has_fderiv_at, show ((0 : ℕ) : with_top ℕ) = 0, from rfl,
   cont_diff_at_zero, exists_mem_and_iff antitone_bforall antitone_continuous_on, and_comm]
 
-lemma cont_diff.of_le
-  (h : cont_diff 𝕜 n f) (hmn : m ≤ n) :
-  cont_diff 𝕜 m f :=
+lemma cont_diff.of_le (h : cont_diff 𝕜 n f) (hmn : m ≤ n) : cont_diff 𝕜 m f :=
 cont_diff_on_univ.1 $ (cont_diff_on_univ.2 h).of_le hmn
 
-lemma cont_diff.continuous
-  (h : cont_diff 𝕜 n f) : continuous f :=
+lemma cont_diff.of_succ {n : ℕ} (h : cont_diff 𝕜 (n + 1) f) : cont_diff 𝕜 n f :=
+h.of_le $ with_top.coe_le_coe.mpr le_self_add
+
+lemma cont_diff.one_of_succ {n : ℕ} (h : cont_diff 𝕜 (n + 1) f) : cont_diff 𝕜 1 f :=
+h.of_le $ with_top.coe_le_coe.mpr le_add_self
+
+lemma cont_diff.continuous (h : cont_diff 𝕜 n f) : continuous f :=
 cont_diff_zero.1 (h.of_le bot_le)
 
 /-- If a function is `C^n` with `n ≥ 1`, then it is differentiable. -/
-lemma cont_diff.differentiable
-  (h : cont_diff 𝕜 n f) (hn : 1 ≤ n) : differentiable 𝕜 f :=
+lemma cont_diff.differentiable (h : cont_diff 𝕜 n f) (hn : 1 ≤ n) : differentiable 𝕜 f :=
 differentiable_on_univ.1 $ (cont_diff_on_univ.2 h).differentiable_on hn
 
 
@@ -2020,27 +2013,53 @@ begin
   exact this.comp x hf (subset_univ _),
 end
 
-lemma cont_diff.comp_cont_diff_at
-  {g : F → G} {f : E → F} (x : E)
-  (hg : cont_diff 𝕜 n g)
-  (hf : cont_diff_at 𝕜 n f x) :
-  cont_diff_at 𝕜 n (g ∘ f) x :=
+lemma cont_diff.comp_cont_diff_at {g : F → G} {f : E → F} (x : E)
+  (hg : cont_diff 𝕜 n g) (hf : cont_diff_at 𝕜 n f x) : cont_diff_at 𝕜 n (g ∘ f) x :=
 hg.comp_cont_diff_within_at hf
 
+/-!
+### Smoothness of projections
+-/
+
 /-- The first projection in a product is `C^∞`. -/
 lemma cont_diff_fst : cont_diff 𝕜 n (prod.fst : E × F → E) :=
 is_bounded_linear_map.cont_diff is_bounded_linear_map.fst
 
+/-- Postcomposing `f` with `prod.fst` is `C^n` -/
+lemma cont_diff.fst {f : E → F × G} (hf : cont_diff 𝕜 n f) : cont_diff 𝕜 n (λ x, (f x).1) :=
+cont_diff_fst.comp hf
+
+/-- Precomposing `f` with `prod.fst` is `C^n` -/
+lemma cont_diff.fst' {f : E → G} (hf : cont_diff 𝕜 n f) : cont_diff 𝕜 n (λ x : E × F, f x.1) :=
+hf.comp cont_diff_fst
+
 /-- The first projection on a domain in a product is `C^∞`. -/
-lemma cont_diff_on_fst {s : set (E×F)} :
-  cont_diff_on 𝕜 n (prod.fst : E × F → E) s :=
+lemma cont_diff_on_fst {s : set (E × F)} : cont_diff_on 𝕜 n (prod.fst : E × F → E) s :=
 cont_diff.cont_diff_on cont_diff_fst
 
+lemma cont_diff_on.fst {f : E → F × G} {s : set E} (hf : cont_diff_on 𝕜 n f s) :
+  cont_diff_on 𝕜 n (λ x, (f x).1) s :=
+cont_diff_fst.comp_cont_diff_on hf
+
 /-- The first projection at a point in a product is `C^∞`. -/
-lemma cont_diff_at_fst {p : E × F} :
-  cont_diff_at 𝕜 n (prod.fst : E × F → E) p :=
+lemma cont_diff_at_fst {p : E × F} : cont_diff_at 𝕜 n (prod.fst : E × F → E) p :=
 cont_diff_fst.cont_diff_at
 
+/-- Postcomposing `f` with `prod.fst` is `C^n` at `(x, y)` -/
+lemma cont_diff_at.fst {f : E → F × G} {x : E} (hf : cont_diff_at 𝕜 n f x) :
+  cont_diff_at 𝕜 n (λ x, (f x).1) x :=
+cont_diff_at_fst.comp x hf
+
+/-- Precomposing `f` with `prod.fst` is `C^n` at `(x, y)` -/
+lemma cont_diff_at.fst' {f : E → G} {x : E} {y : F} (hf : cont_diff_at 𝕜 n f x) :
+  cont_diff_at 𝕜 n (λ x : E × F, f x.1) (x, y) :=
+cont_diff_at.comp (x, y) hf cont_diff_at_fst
+
+/-- Precomposing `f` with `prod.fst` is `C^n` at `x : E × F` -/
+lemma cont_diff_at.fst'' {f : E → G} {x : E × F} (hf : cont_diff_at 𝕜 n f x.1) :
+  cont_diff_at 𝕜 n (λ x : E × F, f x.1) x :=
+hf.comp x cont_diff_at_fst
+
 /-- The first projection within a domain at a point in a product is `C^∞`. -/
 lemma cont_diff_within_at_fst {s : set (E × F)} {p : E × F} :
   cont_diff_within_at 𝕜 n (prod.fst : E × F → E) s p :=
@@ -2050,21 +2069,64 @@ cont_diff_fst.cont_diff_within_at
 lemma cont_diff_snd : cont_diff 𝕜 n (prod.snd : E × F → F) :=
 is_bounded_linear_map.cont_diff is_bounded_linear_map.snd
 
+/-- Postcomposing `f` with `prod.snd` is `C^n` -/
+lemma cont_diff.snd {f : E → F × G} (hf : cont_diff 𝕜 n f) : cont_diff 𝕜 n (λ x, (f x).2) :=
+cont_diff_snd.comp hf
+
+/-- Precomposing `f` with `prod.snd` is `C^n` -/
+lemma cont_diff.snd' {f : F → G} (hf : cont_diff 𝕜 n f) : cont_diff 𝕜 n (λ x : E × F, f x.2) :=
+hf.comp cont_diff_snd
+
 /-- The second projection on a domain in a product is `C^∞`. -/
-lemma cont_diff_on_snd {s : set (E×F)} :
-  cont_diff_on 𝕜 n (prod.snd : E × F → F) s :=
+lemma cont_diff_on_snd {s : set (E × F)} : cont_diff_on 𝕜 n (prod.snd : E × F → F) s :=
 cont_diff.cont_diff_on cont_diff_snd
 
+lemma cont_diff_on.snd {f : E → F × G} {s : set E} (hf : cont_diff_on 𝕜 n f s) :
+  cont_diff_on 𝕜 n (λ x, (f x).2) s :=
+cont_diff_snd.comp_cont_diff_on hf
+
 /-- The second projection at a point in a product is `C^∞`. -/
-lemma cont_diff_at_snd {p : E × F} :
-  cont_diff_at 𝕜 n (prod.snd : E × F → F) p :=
+lemma cont_diff_at_snd {p : E × F} : cont_diff_at 𝕜 n (prod.snd : E × F → F) p :=
 cont_diff_snd.cont_diff_at
 
+/-- Postcomposing `f` with `prod.snd` is `C^n` at `x` -/
+lemma cont_diff_at.snd {f : E → F × G} {x : E} (hf : cont_diff_at 𝕜 n f x) :
+  cont_diff_at 𝕜 n (λ x, (f x).2) x :=
+cont_diff_at_snd.comp x hf
+
+/-- Precomposing `f` with `prod.snd` is `C^n` at `(x, y)` -/
+lemma cont_diff_at.snd' {f : F → G} {x : E} {y : F} (hf : cont_diff_at 𝕜 n f y) :
+  cont_diff_at 𝕜 n (λ x : E × F, f x.2) (x, y) :=
+cont_diff_at.comp (x, y) hf cont_diff_at_snd
+
+/-- Precomposing `f` with `prod.snd` is `C^n` at `x : E × F` -/
+lemma cont_diff_at.snd'' {f : F → G} {x : E × F} (hf : cont_diff_at 𝕜 n f x.2) :
+  cont_diff_at 𝕜 n (λ x : E × F, f x.2) x :=
+hf.comp x cont_diff_at_snd
+
 /-- The second projection within a domain at a point in a product is `C^∞`. -/
 lemma cont_diff_within_at_snd {s : set (E × F)} {p : E × F} :
   cont_diff_within_at 𝕜 n (prod.snd : E × F → F) s p :=
 cont_diff_snd.cont_diff_within_at
 
+section n_ary
+
+variables {E₁ E₂ E₃ E₄ : Type*}
+variables [normed_group E₁] [normed_group E₂] [normed_group E₃] [normed_group E₄]
+variables [normed_space 𝕜 E₁] [normed_space 𝕜 E₂] [normed_space 𝕜 E₃] [normed_space 𝕜 E₄]
+
+lemma cont_diff.comp₂ {g : E₁ × E₂ → G} {f₁ : F → E₁} {f₂ : F → E₂}
+  (hg : cont_diff 𝕜 n g) (hf₁ : cont_diff 𝕜 n f₁) (hf₂ : cont_diff 𝕜 n f₂) :
+  cont_diff 𝕜 n (λ x, g (f₁ x, f₂ x)) :=
+hg.comp $ hf₁.prod hf₂
+
+lemma cont_diff.comp₃ {g : E₁ × E₂ × E₃ → G} {f₁ : F → E₁} {f₂ : F → E₂} {f₃ : F → E₃}
+  (hg : cont_diff 𝕜 n g) (hf₁ : cont_diff 𝕜 n f₁) (hf₂ : cont_diff 𝕜 n f₂)
+  (hf₃ : cont_diff 𝕜 n f₃) : cont_diff 𝕜 n (λ x, g (f₁ x, f₂ x, f₃ x)) :=
+hg.comp₂ hf₁ $ hf₂.prod hf₃
+
+end n_ary
+
 /--
 The natural equivalence `(E × F) × G ≃ E × (F × G)` is smooth.
 
@@ -2083,6 +2145,8 @@ 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 -/
+
 /-- 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}
   {f : E → F} (hf : cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) (hmn : m + 1 ≤ n) :
@@ -2121,7 +2185,7 @@ end
 
 section pi
 
-variables {ι : Type*} [fintype ι] {F' : ι → Type*} [Π i, normed_group (F' i)]
+variables {ι ι' : Type*} [fintype ι] [fintype ι'] {F' : ι → Type*} [Π i, normed_group (F' i)]
   [Π i, normed_space 𝕜 (F' i)] {φ : Π i, E → F' i}
   {p' : Π i, E → formal_multilinear_series 𝕜 E (F' i)}
   {Φ : E → Π i, F' i} {P' : E → formal_multilinear_series 𝕜 E (Π i, F' i)}
@@ -2179,6 +2243,15 @@ lemma cont_diff_pi :
   cont_diff 𝕜 n Φ ↔ ∀ i, cont_diff 𝕜 n (λ x, Φ x i) :=
 by simp only [← cont_diff_on_univ, cont_diff_on_pi]
 
+variables (𝕜 E)
+lemma cont_diff_apply (i : ι) : cont_diff 𝕜 n (λ (f : ι → E), f i) :=
+cont_diff_pi.mp cont_diff_id i
+
+lemma cont_diff_apply_apply (i : ι) (j : ι') : cont_diff 𝕜 n (λ (f : ι → ι' → E), f i j) :=
+cont_diff_pi.mp (cont_diff_apply 𝕜 (ι' → E) i) j
+
+variables {𝕜 E}
+
 end pi
 
 /-! ### Sum of two functions -/
@@ -2391,13 +2464,12 @@ lemma cont_diff_on.smul {s : set E} {f : E → 𝕜} {g : E → F}
   cont_diff_on 𝕜 n (λ x, f x • g x) s :=
 λ x hx, (hf x hx).smul (hg x hx)
 
-/-! ### Cartesian product of two functions-/
+/-! ### Cartesian product of two functions -/
 
 section prod_map
 variables {E' : Type*} [normed_group E'] [normed_space 𝕜 E']
 variables {F' : Type*} [normed_group F'] [normed_space 𝕜 F']
 
-
 /-- The product map of two `C^n` functions within a set at a point is `C^n`
 within the product set at the product point. -/
 lemma cont_diff_within_at.prod_map'
@@ -2452,6 +2524,12 @@ begin
   exact λ ⟨x, y⟩, (hf x).prod_map (hg y)
 end
 
+lemma cont_diff_prod_mk_left (f₀ : F) : cont_diff 𝕜 n (λ e : E, (e, f₀)) :=
+cont_diff_id.prod cont_diff_const
+
+lemma cont_diff_prod_mk_right (e₀ : E) : cont_diff 𝕜 n (λ f : F, (e₀, f)) :=
+cont_diff_const.prod cont_diff_id
+
 end prod_map
 
 /-! ### Inversion in a complete normed algebra -/

src/analysis/calculus/fderiv.lean

@@ -1230,9 +1230,17 @@ lemma has_fderiv_within_at.prod
 hf₁.prod hf₂
 
 lemma has_fderiv_at.prod (hf₁ : has_fderiv_at f₁ f₁' x) (hf₂ : has_fderiv_at f₂ f₂' x) :
-  has_fderiv_at (λx, (f₁ x, f₂ x)) (continuous_linear_map.prod f₁' f₂') x :=
+  has_fderiv_at (λx, (f₁ x, f₂ x)) (f₁'.prod f₂') x :=
 hf₁.prod hf₂
 
+lemma has_fderiv_at_prod_mk_left (e₀ : E) (f₀ : F) :
+  has_fderiv_at (λ e : E, (e, f₀)) (inl 𝕜 E F) e₀ :=
+(has_fderiv_at_id e₀).prod (has_fderiv_at_const f₀ e₀)
+
+lemma has_fderiv_at_prod_mk_right (e₀ : E) (f₀ : F) :
+  has_fderiv_at (λ f : F, (e₀, f)) (inr 𝕜 E F) f₀ :=
+(has_fderiv_at_const e₀ f₀).prod (has_fderiv_at_id f₀)
+
 lemma differentiable_within_at.prod
   (hf₁ : differentiable_within_at 𝕜 f₁ s x) (hf₂ : differentiable_within_at 𝕜 f₂ s x) :
   differentiable_within_at 𝕜 (λx:E, (f₁ x, f₂ x)) s x :=