feat(geometry/manifold/cont_mdiff): add various properties (#16980)

* More lemmas about `smooth`, more basic lemmas, and some interactions with `cont_diff` and continuous linear maps
* Also add various useful lemmas throughout the manifold directory
* Add me as author to two files (in `local_invariant_properties` for earlier refactoring PRs) 
* From the sphere eversion project

src/geometry/manifold/charted_space.lean

@@ -456,6 +456,7 @@ The model space is written as an explicit parameter as there can be several mode
 given topological space. For instance, a complex manifold (modelled over `ℂ^n`) will also be seen
 sometimes as a real manifold over `ℝ^(2n)`.
 -/
+@[ext]
 class charted_space (H : Type*) [topological_space H] (M : Type*) [topological_space M] :=
 (atlas []            : set (local_homeomorph M H))
 (chart_at []         : M → local_homeomorph M H)
@@ -509,6 +510,9 @@ lemma coe_achart (x : M) : (achart H x : local_homeomorph M H) = chart_at H x :=
 @[simp, mfld_simps]
 lemma achart_val (x : M) : (achart H x).1 = chart_at H x := rfl
 
+lemma mem_achart_source (x : M) : x ∈ (achart H x).1.source :=
+mem_chart_source H x
+
 open topological_space
 
 lemma charted_space.second_countable_of_countable_cover [second_countable_topology H]
@@ -646,6 +650,9 @@ variables [topological_space H] [topological_space M] [charted_space H M]
 @[simp, mfld_simps] lemma prod_charted_space_chart_at :
   (chart_at (model_prod H H') x) = (chart_at H x.fst).prod (chart_at H' x.snd) := rfl
 
+lemma charted_space_self_prod : prod_charted_space H H H' H' = charted_space_self (H × H') :=
+by { ext1, { simp [prod_charted_space, atlas] }, { ext1, simp [chart_at_self_eq], refl } }
+
 end prod_charted_space
 
 /-- The product of a finite family of charted spaces is naturally a charted space, with the

src/geometry/manifold/cont_mdiff.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sébastien Gouëzel
+Authors: Sébastien Gouëzel, Floris van Doorn
 -/
 import geometry.manifold.smooth_manifold_with_corners
 import geometry.manifold.local_invariant_properties
@@ -56,6 +56,10 @@ variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
 {E' : Type*} [normed_add_comm_group E'] [normed_space 𝕜 E']
 {H' : Type*} [topological_space H'] (I' : model_with_corners 𝕜 E' H')
 {M' : Type*} [topological_space M'] [charted_space H' M'] [I's : smooth_manifold_with_corners I' M']
+-- declare a manifold `M''` over the pair `(E'', H'')`.
+{E'' : Type*} [normed_add_comm_group E''] [normed_space 𝕜 E'']
+{H'' : Type*} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''}
+{M'' : Type*} [topological_space M''] [charted_space H'' M'']
 -- declare a smooth manifold `N` over the pair `(F, G)`.
 {F : Type*} [normed_add_comm_group F] [normed_space 𝕜 F]
 {G : Type*} [topological_space G] {J : model_with_corners 𝕜 F G}
@@ -64,6 +68,8 @@ variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
 {F' : Type*} [normed_add_comm_group F'] [normed_space 𝕜 F']
 {G' : Type*} [topological_space G'] {J' : model_with_corners 𝕜 F' G'}
 {N' : Type*} [topological_space N'] [charted_space G' N'] [J's : smooth_manifold_with_corners J' N']
+-- F'' is a normed space
+{F'' : Type*} [normed_add_comm_group F''] [normed_space 𝕜 F'']
 -- declare functions, sets, points and smoothness indices
 {f f₁ : M → M'} {s s₁ t : set M} {x : M} {m n : ℕ∞}
 
@@ -876,10 +882,6 @@ lemma cont_mdiff_of_locally_cont_mdiff_on
 
 section composition
 
-variables {E'' : Type*} [normed_add_comm_group E''] [normed_space 𝕜 E'']
-{H'' : Type*} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''}
-{M'' : Type*} [topological_space M''] [charted_space H'' M'']
-
 /-- The composition of `C^n` functions within domains at points is `C^n`. -/
 lemma cont_mdiff_within_at.comp {t : set M'} {g : M' → M''} (x : M)
   (hg : cont_mdiff_within_at I' I'' n g t (f x))
@@ -914,18 +916,37 @@ begin
   { simp only [written_in_ext_chart_at, (∘), mem_ext_chart_source, e.left_inv, e'.left_inv] }
 end
 
+/-- The composition of `C^∞` functions within domains at points is `C^∞`. -/
+lemma smooth_within_at.comp {t : set M'} {g : M' → M''} (x : M)
+  (hg : smooth_within_at I' I'' g t (f x))
+  (hf : smooth_within_at I I' f s x)
+  (st : maps_to f s t) : smooth_within_at I I'' (g ∘ f) s x :=
+hg.comp x hf st
+
 /-- The composition of `C^n` functions on domains is `C^n`. -/
 lemma cont_mdiff_on.comp {t : set M'} {g : M' → M''}
   (hg : cont_mdiff_on I' I'' n g t) (hf : cont_mdiff_on I I' n f s)
   (st : s ⊆ f ⁻¹' t) : cont_mdiff_on I I'' n (g ∘ f) s :=
 λ x hx, (hg _ (st hx)).comp x (hf x hx) st
 
+/-- The composition of `C^∞` functions on domains is `C^∞`. -/
+lemma smooth_on.comp {t : set M'} {g : M' → M''}
+  (hg : smooth_on I' I'' g t) (hf : smooth_on I I' f s)
+  (st : s ⊆ f ⁻¹' t) : smooth_on I I'' (g ∘ f) s :=
+hg.comp hf st
+
 /-- The composition of `C^n` functions on domains is `C^n`. -/
 lemma cont_mdiff_on.comp' {t : set M'} {g : M' → M''}
   (hg : cont_mdiff_on I' I'' n g t) (hf : cont_mdiff_on I I' n f s) :
   cont_mdiff_on I I'' n (g ∘ f) (s ∩ f ⁻¹' t) :=
 hg.comp (hf.mono (inter_subset_left _ _)) (inter_subset_right _ _)
 
+/-- The composition of `C^∞` functions is `C^∞`. -/
+lemma smooth_on.comp' {t : set M'} {g : M' → M''}
+  (hg : smooth_on I' I'' g t) (hf : smooth_on I I' f s) :
+  smooth_on I I'' (g ∘ f) (s ∩ f ⁻¹' t) :=
+hg.comp' hf
+
 /-- The composition of `C^n` functions is `C^n`. -/
 lemma cont_mdiff.comp {g : M' → M''}
   (hg : cont_mdiff I' I'' n g) (hf : cont_mdiff I I' n f) :
@@ -935,26 +956,51 @@ begin
   exact hg.comp hf subset_preimage_univ,
 end
 
+/-- The composition of `C^∞` functions is `C^∞`. -/
+lemma smooth.comp {g : M' → M''} (hg : smooth I' I'' g) (hf : smooth I I' f) :
+  smooth I I'' (g ∘ f) :=
+hg.comp hf
+
 /-- The composition of `C^n` functions within domains at points is `C^n`. -/
 lemma cont_mdiff_within_at.comp' {t : set M'} {g : M' → M''} (x : M)
   (hg : cont_mdiff_within_at I' I'' n g t (f x))
   (hf : cont_mdiff_within_at I I' n f s x) :
   cont_mdiff_within_at I I'' n (g ∘ f) (s ∩ f⁻¹' t) x :=
 hg.comp x (hf.mono (inter_subset_left _ _)) (inter_subset_right _ _)
 
+/-- The composition of `C^∞` functions within domains at points is `C^∞`. -/
+lemma smooth_within_at.comp' {t : set M'} {g : M' → M''} (x : M)
+  (hg : smooth_within_at I' I'' g t (f x))
+  (hf : smooth_within_at I I' f s x) :
+  smooth_within_at I I'' (g ∘ f) (s ∩ f⁻¹' t) x :=
+hg.comp' x hf
+
 /-- `g ∘ f` is `C^n` within `s` at `x` if `g` is `C^n` at `f x` and
 `f` is `C^n` within `s` at `x`. -/
 lemma cont_mdiff_at.comp_cont_mdiff_within_at {g : M' → M''} (x : M)
   (hg : cont_mdiff_at I' I'' n g (f x)) (hf : cont_mdiff_within_at I I' n f s x) :
   cont_mdiff_within_at I I'' n (g ∘ f) s x :=
 hg.comp x hf (maps_to_univ _ _)
 
+/-- `g ∘ f` is `C^∞` within `s` at `x` if `g` is `C^∞` at `f x` and
+`f` is `C^∞` within `s` at `x`. -/
+lemma smooth_at.comp_smooth_within_at {g : M' → M''} (x : M)
+  (hg : smooth_at I' I'' g (f x)) (hf : smooth_within_at I I' f s x) :
+  smooth_within_at I I'' (g ∘ f) s x :=
+hg.comp_cont_mdiff_within_at x hf
+
 /-- The composition of `C^n` functions at points is `C^n`. -/
 lemma cont_mdiff_at.comp {g : M' → M''} (x : M)
   (hg : cont_mdiff_at I' I'' n g (f x)) (hf : cont_mdiff_at I I' n f x) :
   cont_mdiff_at I I'' n (g ∘ f) x :=
 hg.comp x hf (maps_to_univ _ _)
 
+/-- The composition of `C^∞` functions at points is `C^∞`. -/
+lemma smooth_at.comp {g : M' → M''} (x : M)
+  (hg : smooth_at I' I'' g (f x)) (hf : smooth_at I I' f x) :
+  smooth_at I I'' (g ∘ f) x :=
+hg.comp x hf
+
 lemma cont_mdiff.comp_cont_mdiff_on {f : M → M'} {g : M' → M''} {s : set M}
   (hg : cont_mdiff I' I'' n g) (hf : cont_mdiff_on I I' n f s) :
   cont_mdiff_on I I'' n (g ∘ f) s :=
@@ -1157,6 +1203,29 @@ by rw [← cont_diff_on_univ, ← cont_mdiff_on_univ,
 alias cont_mdiff_iff_cont_diff ↔
   cont_mdiff.cont_diff cont_diff.cont_mdiff
 
+lemma cont_diff_within_at.comp_cont_mdiff_within_at
+  {g : F → F'} {f : M → F} {s : set M} {t : set F} {x : M}
+  (hg : cont_diff_within_at 𝕜 n g t (f x))
+  (hf : cont_mdiff_within_at I 𝓘(𝕜, F) n f s x) (h : s ⊆ f ⁻¹' t) :
+  cont_mdiff_within_at I 𝓘(𝕜, F') n (g ∘ f) s x :=
+begin
+  rw cont_mdiff_within_at_iff at *,
+  refine ⟨hg.continuous_within_at.comp hf.1 h, _⟩,
+  rw [← (ext_chart_at I x).left_inv (mem_ext_chart_source I x)] at hg,
+  apply cont_diff_within_at.comp _ (by exact hg) hf.2 _,
+  exact (inter_subset_left _ _).trans (preimage_mono h)
+end
+
+lemma cont_diff_at.comp_cont_mdiff_at {g : F → F'} {f : M → F} {x : M}
+  (hg : cont_diff_at 𝕜 n g (f x)) (hf : cont_mdiff_at I 𝓘(𝕜, F) n f x) :
+  cont_mdiff_at I 𝓘(𝕜, F') n (g ∘ f) x :=
+hg.comp_cont_mdiff_within_at hf subset.rfl
+
+lemma cont_diff.comp_cont_mdiff {g : F → F'} {f : M → F}
+  (hg : cont_diff 𝕜 n g) (hf : cont_mdiff I 𝓘(𝕜, F) n f) :
+  cont_mdiff I 𝓘(𝕜, F') n (g ∘ f) :=
+λ x, hg.cont_diff_at.comp_cont_mdiff_at (hf x)
+
 end module
 
 /-! ### Smoothness of standard maps associated to the product of manifolds -/
@@ -1293,6 +1362,22 @@ lemma smooth_fst :
   smooth (I.prod J) I (@prod.fst M N) :=
 cont_mdiff_fst
 
+lemma cont_mdiff_at.fst {f : N → M × M'} {x : N} (hf : cont_mdiff_at J (I.prod I') n f x) :
+  cont_mdiff_at J I n (λ x, (f x).1) x :=
+cont_mdiff_at_fst.comp x hf
+
+lemma cont_mdiff.fst {f : N → M × M'} (hf : cont_mdiff J (I.prod I') n f) :
+  cont_mdiff J I n (λ x, (f x).1) :=
+cont_mdiff_fst.comp hf
+
+lemma smooth_at.fst {f : N → M × M'} {x : N} (hf : smooth_at J (I.prod I') f x) :
+  smooth_at J I (λ x, (f x).1) x :=
+smooth_at_fst.comp x hf
+
+lemma smooth.fst {f : N → M × M'} (hf : smooth J (I.prod I') f) :
+  smooth J I (λ x, (f x).1) :=
+smooth_fst.comp hf
+
 lemma cont_mdiff_within_at_snd {s : set (M × N)} {p : M × N} :
   cont_mdiff_within_at (I.prod J) J n prod.snd s p :=
 begin
@@ -1332,6 +1417,22 @@ lemma smooth_snd :
   smooth (I.prod J) J (@prod.snd M N) :=
 cont_mdiff_snd
 
+lemma cont_mdiff_at.snd {f : N → M × M'} {x : N} (hf : cont_mdiff_at J (I.prod I') n f x) :
+  cont_mdiff_at J I' n (λ x, (f x).2) x :=
+cont_mdiff_at_snd.comp x hf
+
+lemma cont_mdiff.snd {f : N → M × M'} (hf : cont_mdiff J (I.prod I') n f) :
+  cont_mdiff J I' n (λ x, (f x).2) :=
+cont_mdiff_snd.comp hf
+
+lemma smooth_at.snd {f : N → M × M'} {x : N} (hf : smooth_at J (I.prod I') f x) :
+  smooth_at J I' (λ x, (f x).2) x :=
+smooth_at_snd.comp x hf
+
+lemma smooth.snd {f : N → M × M'} (hf : smooth J (I.prod I') f) :
+  smooth J I' (λ x, (f x).2) :=
+smooth_snd.comp hf
+
 lemma smooth_iff_proj_smooth {f : M → M' × N'} :
   (smooth I (I'.prod J') f) ↔ (smooth I I' (prod.fst ∘ f)) ∧ (smooth I J' (prod.snd ∘ f)) :=
 begin
@@ -1340,6 +1441,10 @@ begin
   { rintro ⟨h_fst, h_snd⟩, simpa only [prod.mk.eta] using h_fst.prod_mk h_snd, }
 end
 
+lemma smooth_prod_assoc :
+  smooth ((I.prod I').prod J) (I.prod (I'.prod J)) (λ x : (M × M') × N, (x.1.1, x.1.2, x.2)) :=
+smooth_fst.fst.prod_mk $ smooth_fst.snd.prod_mk smooth_snd
+
 end projections
 
 section prod_map
@@ -1474,6 +1579,21 @@ lemma continuous_linear_map.cont_mdiff (L : E →L[𝕜] F) :
   cont_mdiff 𝓘(𝕜, E) 𝓘(𝕜, F) n L :=
 L.cont_diff.cont_mdiff
 
+-- the following proof takes very long to elaborate in pure term mode
+lemma cont_mdiff_at.clm_comp {g : M → F →L[𝕜] F''} {f : M → F' →L[𝕜] F} {x : M}
+  (hg : cont_mdiff_at I 𝓘(𝕜, F →L[𝕜] F'') n g x) (hf : cont_mdiff_at I 𝓘(𝕜, F' →L[𝕜] F) n f x) :
+  cont_mdiff_at I 𝓘(𝕜, F' →L[𝕜] F'') n (λ x, (g x).comp (f x)) x :=
+@cont_diff_at.comp_cont_mdiff_at _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
+  (λ x : (F →L[𝕜] F'') × (F' →L[𝕜] F), x.1.comp x.2) (λ x, (g x, f x)) x
+  (by { apply cont_diff.cont_diff_at, apply is_bounded_bilinear_map.cont_diff,
+    exact is_bounded_bilinear_map_comp }) -- todo: simplify after #16946
+  (hg.prod_mk_space hf)
+
+lemma cont_mdiff.clm_comp {g : M → F →L[𝕜] F''} {f : M → F' →L[𝕜] F}
+  (hg : cont_mdiff I 𝓘(𝕜, F →L[𝕜] F'') n g) (hf : cont_mdiff I 𝓘(𝕜, F' →L[𝕜] F) n f) :
+  cont_mdiff I 𝓘(𝕜, F' →L[𝕜] F'') n (λ x, (g x).comp (f x)) :=
+λ x, (hg x).clm_comp (hf x)
+
 /-! ### Smoothness of standard operations -/
 
 variables {V : Type*} [normed_add_comm_group V] [normed_space 𝕜 V]

src/geometry/manifold/cont_mdiff_mfderiv.lean

@@ -72,6 +72,16 @@ lemma cont_mdiff.mdifferentiable (hf : cont_mdiff I I' n f) (hn : 1 ≤ n) :
   mdifferentiable I I' f :=
 λ x, (hf x).mdifferentiable_at hn
 
+lemma smooth_within_at.mdifferentiable_within_at
+  (hf : smooth_within_at I I' f s x) : mdifferentiable_within_at I I' f s x :=
+hf.mdifferentiable_within_at le_top
+
+lemma smooth_at.mdifferentiable_at (hf : smooth_at I I' f x) : mdifferentiable_at I I' f x :=
+hf.mdifferentiable_at le_top
+
+lemma smooth_on.mdifferentiable_on (hf : smooth_on I I' f s) : mdifferentiable_on I I' f s :=
+hf.mdifferentiable_on le_top
+
 lemma smooth.mdifferentiable (hf : smooth I I' f) : mdifferentiable I I' f :=
 cont_mdiff.mdifferentiable hf le_top
 
@@ -445,6 +455,12 @@ begin
     .continuous_at_of_comp_left h (mem_chart_source _ _) (h.prod hf.continuous_at.snd)
 end
 
+lemma smooth_iff_target {f : N → Z.to_topological_vector_bundle_core.total_space} :
+  smooth J (I.prod 𝓘(𝕜, E')) f ↔ continuous (bundle.total_space.proj ∘ f) ∧
+  ∀ x, smooth_at J 𝓘(𝕜, E × E') (ext_chart_at (I.prod 𝓘(𝕜, E')) (f x) ∘ f) x :=
+by simp_rw [smooth, smooth_at, cont_mdiff, Z.cont_mdiff_at_iff_target, forall_and_distrib,
+  continuous_iff_continuous_at]
+
 lemma cont_mdiff_proj :
   cont_mdiff (I.prod 𝓘(𝕜, E')) I n Z.to_topological_vector_bundle_core.proj :=
 begin

src/geometry/manifold/local_invariant_properties.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sébastien Gouëzel
+Authors: Sébastien Gouëzel, Floris van Doorn
 -/
 import geometry.manifold.charted_space
 

src/geometry/manifold/smooth_manifold_with_corners.lean

@@ -124,7 +124,7 @@ localized "notation (name := with_top.nat.top) `∞` := (⊤ : ℕ∞)" in manif
 model vector space `E` over the field `𝕜`. This is all what is needed to
 define a smooth manifold with model space `H`, and model vector space `E`.
 -/
-@[nolint has_nonempty_instance]
+@[ext, nolint has_nonempty_instance]
 structure model_with_corners (𝕜 : Type*) [nontrivially_normed_field 𝕜]
   (E : Type*) [normed_add_comm_group E] [normed_space 𝕜 E] (H : Type*) [topological_space H]
   extends local_equiv H E :=
@@ -228,6 +228,9 @@ I.left_inverse.right_inv_on_range
 @[simp, mfld_simps] protected lemma right_inv {x : E} (hx : x ∈ range I) : I (I.symm x) = x :=
 I.right_inv_on hx
 
+lemma preimage_image (s : set H) : I ⁻¹' (I '' s) = s :=
+I.injective.preimage_image s
+
 protected lemma image_eq (s : set H) : I '' s = I.symm ⁻¹' s ∩ range I :=
 begin
   refine (I.to_local_equiv.image_eq_target_inter_inv_preimage _).trans _,
@@ -365,6 +368,12 @@ rfl
   (I : model_with_corners 𝕜 E H) (I' : model_with_corners 𝕜 E' H') :
   ((I.prod I').symm : _ × _ → _ × _) = prod.map I.symm I'.symm := rfl
 
+lemma model_with_corners_self_prod : 𝓘(𝕜, E × F) = 𝓘(𝕜, E).prod 𝓘(𝕜, F) :=
+by { ext1, simp }
+
+lemma model_with_corners.range_prod : range (I.prod J) = range I ×ˢ range J :=
+by { simp_rw [← model_with_corners.target_eq], refl }
+
 end model_with_corners_prod
 
 section boundaryless
@@ -955,4 +964,10 @@ by simp only with mfld_simps
 
 lemma ext_chart_model_space_apply {x y : E} : ext_chart_at 𝓘(𝕜, E) x y = y := rfl
 
+variable {𝕜}
+
+lemma ext_chart_at_prod (x : M × M') :
+  ext_chart_at (I.prod I') x = (ext_chart_at I x.1).prod (ext_chart_at I' x.2) :=
+by simp only with mfld_simps
+
 end extended_charts