feat: regularity of the pullback of a vector field on a manifold

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

@@ -1094,6 +1094,19 @@ theorem hasFDerivAt_zero_of_eventually_const (c : F) (hf : f =ᶠ[𝓝 x] fun _
 
 end Const
 
+theorem differentiableWithinAt_of_isInvertible_fderivWithin
+    (hf : (fderivWithin 𝕜 f s x).IsInvertible) : DifferentiableWithinAt 𝕜 f s x := by
+  contrapose hf
+  rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
+  contrapose! hf
+  rcases isInvertible_zero_iff.1 hf with ⟨hE, hF⟩
+  exact (hasFDerivAt_of_subsingleton _ _).differentiableAt.differentiableWithinAt
+
+theorem differentiableAt_of_isInvertible_fderiv
+    (hf : (fderiv 𝕜 f x).IsInvertible) : DifferentiableAt 𝕜 f x := by
+  simp only [← differentiableWithinAt_univ, ← fderivWithin_univ] at hf ⊢
+  exact differentiableWithinAt_of_isInvertible_fderivWithin hf
+
 section MeanValue
 
 /-- Converse to the mean value inequality: if `f` is differentiable at `x₀` and `C`-lipschitz

Mathlib/Geometry/Manifold/ChartedSpace.lean

@@ -738,6 +738,17 @@ theorem ChartedSpace.t1Space [T1Space H] : T1Space M := by
       exact (chartAt H x).injOn.ne (ChartedSpace.mem_chart_source x) hy hxy
   · exact ⟨(chartAt H x).source, (chartAt H x).open_source, ChartedSpace.mem_chart_source x, hy⟩
 
+/-- A charted space over a discrete space is discrete. -/
+theorem ChartedSpace.discreteTopology [DiscreteTopology H] : DiscreteTopology M := by
+  apply singletons_open_iff_discrete.1 (fun x ↦ ?_)
+  have : IsOpen ((chartAt H x).source ∩ (chartAt H x) ⁻¹' {chartAt H x x}) :=
+    isOpen_inter_preimage _ (isOpen_discrete _)
+  convert this
+  refine Subset.antisymm (by simp) ?_
+  simp only [subset_singleton_iff, mem_inter_iff, mem_preimage, mem_singleton_iff, and_imp]
+  intro y hy h'y
+  exact (chartAt H x).injOn hy (ChartedSpace.mem_chart_source x) h'y
+
 end
 
 library_note "Manifold type tags" /-- For technical reasons we introduce two type tags:

Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

@@ -583,13 +583,41 @@ protected theorem UniqueMDiffOn.eq (U : UniqueMDiffOn I s) (hx : x ∈ s)
 We mimic the API for functions between vector spaces
 -/
 
+@[simp, mfld_simps]
+theorem mfderivWithin_univ : mfderivWithin I I' f univ = mfderiv I I' f := by
+  ext x : 1
+  simp only [mfderivWithin, mfderiv, mfld_simps]
+  rw [mdifferentiableWithinAt_univ]
+
 theorem mfderivWithin_zero_of_not_mdifferentiableWithinAt
     (h : ¬MDifferentiableWithinAt I I' f s x) : mfderivWithin I I' f s x = 0 := by
   simp only [mfderivWithin, h, if_neg, not_false_iff]
 
 theorem mfderiv_zero_of_not_mdifferentiableAt (h : ¬MDifferentiableAt I I' f x) :
     mfderiv I I' f x = 0 := by simp only [mfderiv, h, if_neg, not_false_iff]
 
+theorem mdifferentiable_of_subsingleton [Subsingleton E] : MDifferentiable I I' f := by
+  intro x
+  have : Subsingleton H := I.injective.subsingleton
+  have : DiscreteTopology M := discreteTopology H M
+  have : ContinuousAt f x := continuous_of_discreteTopology.continuousAt
+  simp only [mdifferentiableAt_iff, this, true_and]
+  exact (hasFDerivAt_of_subsingleton _ _).differentiableAt.differentiableWithinAt
+
+theorem mdifferentiableWithinAt_of_isInvertible_mfderivWithin
+    (hf : (mfderivWithin I I' f s x).IsInvertible) : MDifferentiableWithinAt I I' f s x := by
+  contrapose hf
+  rw [mfderivWithin_zero_of_not_mdifferentiableWithinAt hf]
+  contrapose! hf
+  rcases ContinuousLinearMap.isInvertible_zero_iff.1 hf with ⟨hE, hF⟩
+  have : Subsingleton E := hE
+  exact mdifferentiable_of_subsingleton.mdifferentiableAt.mdifferentiableWithinAt
+
+theorem mdifferentiableAt_of_isInvertible_mfderiv
+    (hf : (mfderiv I I' f x).IsInvertible) : MDifferentiableAt I I' f x := by
+  simp only [← mdifferentiableWithinAt_univ, ← mfderivWithin_univ] at hf ⊢
+  exact mdifferentiableWithinAt_of_isInvertible_mfderivWithin hf
+
 theorem HasMFDerivWithinAt.mono (h : HasMFDerivWithinAt I I' f t x f') (hst : s ⊆ t) :
     HasMFDerivWithinAt I I' f s x f' :=
   ⟨ContinuousWithinAt.mono h.1 hst,
@@ -716,12 +744,6 @@ theorem mfderivWithin_subset (st : s ⊆ t) (hs : UniqueMDiffWithinAt I s x)
     mfderivWithin I I' f s x = mfderivWithin I I' f t x :=
   ((MDifferentiableWithinAt.hasMFDerivWithinAt h).mono st).mfderivWithin hs
 
-@[simp, mfld_simps]
-theorem mfderivWithin_univ : mfderivWithin I I' f univ = mfderiv I I' f := by
-  ext x : 1
-  simp only [mfderivWithin, mfderiv, mfld_simps]
-  rw [mdifferentiableWithinAt_univ]
-
 theorem mfderivWithin_inter (ht : t ∈ 𝓝 x) :
     mfderivWithin I I' f (s ∩ t) x = mfderivWithin I I' f s x := by
   rw [mfderivWithin, mfderivWithin, extChartAt_preimage_inter_eq, mdifferentiableWithinAt_inter ht,