feat: expand API of ContMDiff and MFDeriv (#18623)

Sequel to #17927 and #18447.

Author: sgouezel

Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

@@ -99,6 +99,17 @@ theorem contMDiffOn_extChartAt_symm (x : M) :
   convert contMDiffOn_extend_symm (chart_mem_maximalAtlas (I := I) x)
   rw [extChartAt_target, I.image_eq]
 
+theorem contMDiffWithinAt_extChartAt_symm_target
+    (x : M) {y : E} (hy : y ∈ (extChartAt I x).target) :
+    ContMDiffWithinAt 𝓘(𝕜, E) I n (extChartAt I x).symm (extChartAt I x).target y :=
+  contMDiffOn_extChartAt_symm x y hy
+
+theorem contMDiffWithinAt_extChartAt_symm_range
+    (x : M) {y : E} (hy : y ∈ (extChartAt I x).target) :
+    ContMDiffWithinAt 𝓘(𝕜, E) I n (extChartAt I x).symm (range I) y :=
+  (contMDiffWithinAt_extChartAt_symm_target x hy).mono_of_mem_nhdsWithin
+    (extChartAt_target_mem_nhdsWithin_of_mem hy)
+
 /-- An element of `contDiffGroupoid ⊤ I` is `C^n` for any `n`. -/
 theorem contMDiffOn_of_mem_contDiffGroupoid {e' : PartialHomeomorph H H}
     (h : e' ∈ contDiffGroupoid ⊤ I) : ContMDiffOn I I n e' e'.source :=

Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

@@ -654,10 +654,16 @@ theorem ContMDiffWithinAt.mono (hf : ContMDiffWithinAt I I' n f s x) (hts : t 
     ContMDiffWithinAt I I' n f t x :=
   hf.mono_of_mem_nhdsWithin <| mem_of_superset self_mem_nhdsWithin hts
 
-theorem contMDiffWithinAt_congr_nhds (hst : 𝓝[s] x = 𝓝[t] x) :
+theorem contMDiffWithinAt_congr_set (h : s =ᶠ[𝓝 x] t) :
     ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt I I' n f t x :=
-  ⟨fun h => h.mono_of_mem_nhdsWithin <| hst ▸ self_mem_nhdsWithin, fun h =>
-    h.mono_of_mem_nhdsWithin <| hst.symm ▸ self_mem_nhdsWithin⟩
+  (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_set h
+
+theorem ContMDiffWithinAt.congr_set (h : ContMDiffWithinAt I I' n f s x) (hst : s =ᶠ[𝓝 x] t) :
+    ContMDiffWithinAt I I' n f t x :=
+  (contMDiffWithinAt_congr_set hst).1 h
+
+@[deprecated (since := "2024-10-23")]
+alias contMDiffWithinAt_congr_nhds := contMDiffWithinAt_congr_set
 
 theorem contMDiffWithinAt_insert_self :
     ContMDiffWithinAt I I' n f (insert x s) x ↔ ContMDiffWithinAt I I' n f s x := by
@@ -669,24 +675,32 @@ theorem contMDiffWithinAt_insert_self :
 alias ⟨ContMDiffWithinAt.of_insert, _⟩ := contMDiffWithinAt_insert_self
 
 -- TODO: use `alias` again once it can make protected theorems
-theorem ContMDiffWithinAt.insert (h : ContMDiffWithinAt I I' n f s x) :
+protected theorem ContMDiffWithinAt.insert (h : ContMDiffWithinAt I I' n f s x) :
     ContMDiffWithinAt I I' n f (insert x s) x :=
   contMDiffWithinAt_insert_self.2 h
 
-theorem ContMDiffAt.contMDiffWithinAt (hf : ContMDiffAt I I' n f x) :
+/-- Being `C^n` in a set only depends on the germ of the set. Version where one only requires
+the two sets to coincide locally in the complement of a point `y`. -/
+theorem contMDiffWithinAt_congr_set' (y : M) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
+    ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt I I' n f t x := by
+  have : T1Space M := I.t1Space M
+  rw [← contMDiffWithinAt_insert_self (s := s), ← contMDiffWithinAt_insert_self (s := t)]
+  exact contMDiffWithinAt_congr_set (eventuallyEq_insert h)
+
+protected theorem ContMDiffAt.contMDiffWithinAt (hf : ContMDiffAt I I' n f x) :
     ContMDiffWithinAt I I' n f s x :=
   ContMDiffWithinAt.mono hf (subset_univ _)
 
-theorem SmoothAt.smoothWithinAt (hf : SmoothAt I I' f x) : SmoothWithinAt I I' f s x :=
+protected theorem SmoothAt.smoothWithinAt (hf : SmoothAt I I' f x) : SmoothWithinAt I I' f s x :=
   ContMDiffAt.contMDiffWithinAt hf
 
 theorem ContMDiffOn.mono (hf : ContMDiffOn I I' n f s) (hts : t ⊆ s) : ContMDiffOn I I' n f t :=
   fun x hx => (hf x (hts hx)).mono hts
 
-theorem ContMDiff.contMDiffOn (hf : ContMDiff I I' n f) : ContMDiffOn I I' n f s := fun x _ =>
-  (hf x).contMDiffWithinAt
+protected theorem ContMDiff.contMDiffOn (hf : ContMDiff I I' n f) : ContMDiffOn I I' n f s :=
+  fun x _ => (hf x).contMDiffWithinAt
 
-theorem Smooth.smoothOn (hf : Smooth I I' f) : SmoothOn I I' f s :=
+protected theorem Smooth.smoothOn (hf : Smooth I I' f) : SmoothOn I I' f s :=
   ContMDiff.contMDiffOn hf
 
 theorem contMDiffWithinAt_inter' (ht : t ∈ 𝓝[s] x) :
@@ -697,19 +711,20 @@ theorem contMDiffWithinAt_inter (ht : t ∈ 𝓝 x) :
     ContMDiffWithinAt I I' n f (s ∩ t) x ↔ ContMDiffWithinAt I I' n f s x :=
   (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_inter ht
 
-theorem ContMDiffWithinAt.contMDiffAt (h : ContMDiffWithinAt I I' n f s x) (ht : s ∈ 𝓝 x) :
+protected theorem ContMDiffWithinAt.contMDiffAt
+    (h : ContMDiffWithinAt I I' n f s x) (ht : s ∈ 𝓝 x) :
     ContMDiffAt I I' n f x :=
   (contDiffWithinAt_localInvariantProp n).liftPropAt_of_liftPropWithinAt h ht
 
-theorem SmoothWithinAt.smoothAt (h : SmoothWithinAt I I' f s x) (ht : s ∈ 𝓝 x) :
+protected theorem SmoothWithinAt.smoothAt (h : SmoothWithinAt I I' f s x) (ht : s ∈ 𝓝 x) :
     SmoothAt I I' f x :=
   ContMDiffWithinAt.contMDiffAt h ht
 
-theorem ContMDiffOn.contMDiffAt (h : ContMDiffOn I I' n f s) (hx : s ∈ 𝓝 x) :
+protected theorem ContMDiffOn.contMDiffAt (h : ContMDiffOn I I' n f s) (hx : s ∈ 𝓝 x) :
     ContMDiffAt I I' n f x :=
   (h x (mem_of_mem_nhds hx)).contMDiffAt hx
 
-theorem SmoothOn.smoothAt (h : SmoothOn I I' f s) (hx : s ∈ 𝓝 x) : SmoothAt I I' f x :=
+protected theorem SmoothOn.smoothAt (h : SmoothOn I I' f s) (hx : s ∈ 𝓝 x) : SmoothAt I I' f x :=
   h.contMDiffAt hx
 
 theorem contMDiffOn_iff_source_of_mem_maximalAtlas [SmoothManifoldWithCorners I M]
@@ -719,9 +734,8 @@ theorem contMDiffOn_iff_source_of_mem_maximalAtlas [SmoothManifoldWithCorners I
   simp_rw [ContMDiffOn, Set.forall_mem_image]
   refine forall₂_congr fun x hx => ?_
   rw [contMDiffWithinAt_iff_source_of_mem_maximalAtlas he (hs hx)]
-  apply contMDiffWithinAt_congr_nhds
-  simp_rw [nhdsWithin_eq_iff_eventuallyEq,
-    e.extend_symm_preimage_inter_range_eventuallyEq hs (hs hx)]
+  apply contMDiffWithinAt_congr_set
+  simp_rw [e.extend_symm_preimage_inter_range_eventuallyEq hs (hs hx)]
 
 -- Porting note: didn't compile; fixed by golfing the proof and moving parts to lemmas
 /-- A function is `C^n` within a set at a point, for `n : ℕ`, if and only if it is `C^n` on
@@ -757,6 +771,29 @@ theorem contMDiffWithinAt_iff_contMDiffOn_nhds
     rwa [contMDiffOn_iff_of_subset_source' hv₁ hv₂, PartialEquiv.image_symm_image_of_subset_target]
     exact hsub.trans inter_subset_left
 
+/-- If a function is `C^m` within a set at a point, for some finite `m`, then it is `C^m` within
+this set on an open set around the basepoint.
+-/
+theorem ContMDiffWithinAt.contMDiffOn'
+    [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M']
+    {m : ℕ} (hm : (m : ℕ∞) ≤ n)
+    (h : ContMDiffWithinAt I I' n f s x) :
+    ∃ u, IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I' m f (insert x s ∩ u) := by
+  rcases contMDiffWithinAt_iff_contMDiffOn_nhds.1 (h.of_le hm) with ⟨t, ht, h't⟩
+  rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩
+  rw [inter_comm] at hu
+  exact ⟨u, u_open, xu, h't.mono hu⟩
+
+/-- If a function is `C^m` within a set at a point, for some finite `m`, then it is `C^m` within
+this set on a neighborhood of the basepoint. -/
+theorem ContMDiffWithinAt.contMDiffOn
+    [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M']
+    {m : ℕ} (hm : (m : ℕ∞) ≤ n)
+    (h : ContMDiffWithinAt I I' n f s x) :
+    ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContMDiffOn I I' m f u := by
+  let ⟨_u, uo, xu, h⟩ := h.contMDiffOn' hm
+  exact ⟨_, inter_mem_nhdsWithin _ (uo.mem_nhds xu), inter_subset_left, h⟩
+
 /-- A function is `C^n` at a point, for `n : ℕ`, if and only if it is `C^n` on
 a neighborhood of this point. -/
 theorem contMDiffAt_iff_contMDiffOn_nhds
@@ -775,6 +812,19 @@ theorem contMDiffAt_iff_contMDiffAt_nhds
   refine (eventually_mem_nhds_iff.mpr hu).mono fun x' hx' => ?_
   exact (h x' <| mem_of_mem_nhds hx').contMDiffAt hx'
 
+/-- Note: This does not hold for `n = ∞`. `f` being `C^∞` at `x` means that for every `n`, `f` is
+`C^n` on some neighborhood of `x`, but this neighborhood can depend on `n`. -/
+theorem contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin
+    [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {n : ℕ} :
+    ContMDiffWithinAt I I' n f s x ↔
+      ∀ᶠ x' in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x' := by
+  refine ⟨?_, fun h ↦ mem_of_mem_nhdsWithin (mem_insert x s) h⟩
+  rw [contMDiffWithinAt_iff_contMDiffOn_nhds]
+  rintro ⟨u, hu, h⟩
+  filter_upwards [hu, eventually_mem_nhdsWithin_iff.mpr hu] with x' h'x' hx'
+  apply (h x' h'x').mono_of_mem_nhdsWithin
+  exact nhdsWithin_mono _ (subset_insert x s) hx'
+
 /-! ### Congruence lemmas -/
 
 theorem ContMDiffWithinAt.congr (h : ContMDiffWithinAt I I' n f s x) (h₁ : ∀ y ∈ s, f₁ y = f y)
@@ -785,10 +835,23 @@ theorem contMDiffWithinAt_congr (h₁ : ∀ y ∈ s, f₁ y = f y) (hx : f₁ x
     ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x :=
   (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_iff h₁ hx
 
+theorem ContMDiffWithinAt.congr_of_mem
+    (h : ContMDiffWithinAt I I' n f s x) (h₁ : ∀ y ∈ s, f₁ y = f y) (hx : x ∈ s) :
+    ContMDiffWithinAt I I' n f₁ s x :=
+  (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_of_mem h h₁ hx
+
+theorem contMDiffWithinAt_congr_of_mem (h₁ : ∀ y ∈ s, f₁ y = f y) (hx : x ∈ s) :
+    ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x :=
+  (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_iff_of_mem h₁ hx
+
 theorem ContMDiffWithinAt.congr_of_eventuallyEq (h : ContMDiffWithinAt I I' n f s x)
     (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : ContMDiffWithinAt I I' n f₁ s x :=
   (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_of_eventuallyEq h h₁ hx
 
+theorem ContMDiffWithinAt.congr_of_eventuallyEq_of_mem (h : ContMDiffWithinAt I I' n f s x)
+    (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : x ∈ s) : ContMDiffWithinAt I I' n f₁ s x :=
+  (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_of_eventuallyEq_of_mem h h₁ hx
+
 theorem Filter.EventuallyEq.contMDiffWithinAt_iff (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
     ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x :=
   (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_iff_of_eventuallyEq h₁ hx

Mathlib/Geometry/Manifold/ContMDiff/Product.lean

@@ -36,6 +36,9 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {F' : Type*}
   [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type*} [TopologicalSpace G']
   {J' : ModelWithCorners 𝕜 F' G'} {N' : Type*} [TopologicalSpace N'] [ChartedSpace G' N']
+  -- declare a few vector spaces
+  {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁]
+  {F₂ : Type*} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂]
   -- declare functions, sets, points and smoothness indices
   {f : M → M'} {s : Set M} {x : M} {n : ℕ∞}
 
@@ -229,21 +232,53 @@ theorem Smooth.snd {f : N → M × M'} (hf : Smooth J (I.prod I') f) : Smooth J
 
 end Projections
 
-theorem contMDiffWithinAt_prod_iff (f : M → M' × N') {s : Set M} {x : M} :
+theorem contMDiffWithinAt_prod_iff (f : M → M' × N') :
     ContMDiffWithinAt I (I'.prod J') n f s x ↔
       ContMDiffWithinAt I I' n (Prod.fst ∘ f) s x ∧ ContMDiffWithinAt I J' n (Prod.snd ∘ f) s x :=
   ⟨fun h => ⟨h.fst, h.snd⟩, fun h => h.1.prod_mk h.2⟩
 
-theorem contMDiffAt_prod_iff (f : M → M' × N') {x : M} :
+theorem contMDiffWithinAt_prod_module_iff (f : M → F₁ × F₂) :
+    ContMDiffWithinAt I 𝓘(𝕜, F₁ × F₂) n f s x ↔
+      ContMDiffWithinAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s x ∧
+      ContMDiffWithinAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s x := by
+  rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
+  exact contMDiffWithinAt_prod_iff f
+
+theorem contMDiffAt_prod_iff (f : M → M' × N') :
     ContMDiffAt I (I'.prod J') n f x ↔
       ContMDiffAt I I' n (Prod.fst ∘ f) x ∧ ContMDiffAt I J' n (Prod.snd ∘ f) x := by
   simp_rw [← contMDiffWithinAt_univ]; exact contMDiffWithinAt_prod_iff f
 
+theorem contMDiffAt_prod_module_iff (f : M → F₁ × F₂) :
+    ContMDiffAt I 𝓘(𝕜, F₁ × F₂) n f x ↔
+      ContMDiffAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) x ∧ ContMDiffAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) x := by
+  rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
+  exact contMDiffAt_prod_iff f
+
+theorem contMDiffOn_prod_iff (f : M → M' × N') :
+    ContMDiffOn I (I'.prod J') n f s ↔
+      ContMDiffOn I I' n (Prod.fst ∘ f) s ∧ ContMDiffOn I J' n (Prod.snd ∘ f) s :=
+  ⟨fun h ↦ ⟨fun x hx ↦ ((contMDiffWithinAt_prod_iff f).1 (h x hx)).1,
+      fun x hx ↦ ((contMDiffWithinAt_prod_iff f).1 (h x hx)).2⟩ ,
+    fun h x hx ↦ (contMDiffWithinAt_prod_iff f).2 ⟨h.1 x hx, h.2 x hx⟩⟩
+
+theorem contMDiffOn_prod_module_iff (f : M → F₁ × F₂) :
+    ContMDiffOn I 𝓘(𝕜, F₁ × F₂) n f s ↔
+      ContMDiffOn I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) s ∧ ContMDiffOn I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) s := by
+  rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
+  exact contMDiffOn_prod_iff f
+
 theorem contMDiff_prod_iff (f : M → M' × N') :
     ContMDiff I (I'.prod J') n f ↔
       ContMDiff I I' n (Prod.fst ∘ f) ∧ ContMDiff I J' n (Prod.snd ∘ f) :=
   ⟨fun h => ⟨h.fst, h.snd⟩, fun h => by convert h.1.prod_mk h.2⟩
 
+theorem contMDiff_prod_module_iff (f : M → F₁ × F₂) :
+    ContMDiff I 𝓘(𝕜, F₁ × F₂) n f ↔
+      ContMDiff I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) ∧ ContMDiff I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) := by
+  rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
+  exact contMDiff_prod_iff f
+
 theorem smoothAt_prod_iff (f : M → M' × N') {x : M} :
     SmoothAt I (I'.prod J') f x ↔ SmoothAt I I' (Prod.fst ∘ f) x ∧ SmoothAt I J' (Prod.snd ∘ f) x :=
   contMDiffAt_prod_iff f

Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

@@ -338,6 +338,13 @@ theorem liftPropWithinAt_inter (ht : t ∈ 𝓝 x) :
     LiftPropWithinAt P g (s ∩ t) x ↔ LiftPropWithinAt P g s x :=
   hG.liftPropWithinAt_inter' (mem_nhdsWithin_of_mem_nhds ht)
 
+theorem liftPropWithinAt_congr_set (hu : s =ᶠ[𝓝 x] t) :
+    LiftPropWithinAt P g s x ↔ LiftPropWithinAt P g t x := by
+  rw [← hG.liftPropWithinAt_inter (s := s) hu, ← hG.liftPropWithinAt_inter (s := t) hu,
+    ← eq_iff_iff]
+  congr 1
+  aesop
+
 theorem liftPropAt_of_liftPropWithinAt (h : LiftPropWithinAt P g s x) (hs : s ∈ 𝓝 x) :
     LiftPropAt P g x := by
   rwa [← univ_inter s, hG.liftPropWithinAt_inter hs] at h
@@ -370,6 +377,10 @@ theorem liftPropWithinAt_congr_of_eventuallyEq (h : LiftPropWithinAt P g s x) (h
     (fun y ↦ chartAt H' (g' x) (g' y) = chartAt H' (g x) (g y)) (mem_chart_source H x)]
   exact h₁.mono fun y hy ↦ by rw [hx, hy]
 
+theorem liftPropWithinAt_congr_of_eventuallyEq_of_mem (h : LiftPropWithinAt P g s x)
+    (h₁ : g' =ᶠ[𝓝[s] x] g) (h₂ : x ∈ s) : LiftPropWithinAt P g' s x :=
+  liftPropWithinAt_congr_of_eventuallyEq hG h h₁ (mem_of_mem_nhdsWithin h₂ h₁ : _)
+
 theorem liftPropWithinAt_congr_iff_of_eventuallyEq (h₁ : g' =ᶠ[𝓝[s] x] g) (hx : g' x = g x) :
     LiftPropWithinAt P g' s x ↔ LiftPropWithinAt P g s x :=
   ⟨fun h ↦ hG.liftPropWithinAt_congr_of_eventuallyEq h h₁.symm hx.symm,
@@ -379,10 +390,18 @@ theorem liftPropWithinAt_congr_iff (h₁ : ∀ y ∈ s, g' y = g y) (hx : g' x =
     LiftPropWithinAt P g' s x ↔ LiftPropWithinAt P g s x :=
   hG.liftPropWithinAt_congr_iff_of_eventuallyEq (eventually_nhdsWithin_of_forall h₁) hx
 
+theorem liftPropWithinAt_congr_iff_of_mem (h₁ : ∀ y ∈ s, g' y = g y) (hx : x ∈ s) :
+    LiftPropWithinAt P g' s x ↔ LiftPropWithinAt P g s x :=
+  hG.liftPropWithinAt_congr_iff_of_eventuallyEq (eventually_nhdsWithin_of_forall h₁) (h₁ _ hx)
+
 theorem liftPropWithinAt_congr (h : LiftPropWithinAt P g s x) (h₁ : ∀ y ∈ s, g' y = g y)
     (hx : g' x = g x) : LiftPropWithinAt P g' s x :=
   (hG.liftPropWithinAt_congr_iff h₁ hx).mpr h
 
+theorem liftPropWithinAt_congr_of_mem (h : LiftPropWithinAt P g s x) (h₁ : ∀ y ∈ s, g' y = g y)
+    (hx : x ∈ s) : LiftPropWithinAt P g' s x :=
+  (hG.liftPropWithinAt_congr_iff h₁ (h₁ _ hx)).mpr h
+
 theorem liftPropAt_congr_iff_of_eventuallyEq (h₁ : g' =ᶠ[𝓝 x] g) :
     LiftPropAt P g' x ↔ LiftPropAt P g x :=
   hG.liftPropWithinAt_congr_iff_of_eventuallyEq (by simp_rw [nhdsWithin_univ, h₁]) h₁.eq_of_nhds