[placeholder PR uniting ongoing work on connections and geodesics]

Mathlib.lean

@@ -4463,6 +4463,7 @@ public import Mathlib.Geometry.Manifold.Notation
 public import Mathlib.Geometry.Manifold.PartitionOfUnity
 public import Mathlib.Geometry.Manifold.PoincareConjecture
 public import Mathlib.Geometry.Manifold.Riemannian.Basic
+public import Mathlib.Geometry.Manifold.Riemannian.ExistsRiemannianMetric
 public import Mathlib.Geometry.Manifold.Riemannian.PathELength
 public import Mathlib.Geometry.Manifold.Sheaf.Basic
 public import Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
@@ -4472,16 +4473,31 @@ public import Mathlib.Geometry.Manifold.SmoothEmbedding
 public import Mathlib.Geometry.Manifold.StructureGroupoid
 public import Mathlib.Geometry.Manifold.VectorBundle.Basic
 public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.ChristoffelSymbols
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Curvature
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Ehresmann
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Geodesics
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.IntegralCurvePrelim
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.LeviCivita
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Lift
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Prelim
 public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion2
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.TrivPrelim
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Trivial
 public import Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
+public import Mathlib.Geometry.Manifold.VectorBundle.GramSchmidtOrtho
 public import Mathlib.Geometry.Manifold.VectorBundle.Hom
 public import Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
 public import Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
+public import Mathlib.Geometry.Manifold.VectorBundle.OrthonormalFrame
 public import Mathlib.Geometry.Manifold.VectorBundle.Pullback
 public import Mathlib.Geometry.Manifold.VectorBundle.Riemannian
 public import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
 public import Mathlib.Geometry.Manifold.VectorBundle.Tangent
 public import Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
+public import Mathlib.Geometry.Manifold.VectorBundle.Unused
 public import Mathlib.Geometry.Manifold.VectorField.LieBracket
 public import Mathlib.Geometry.Manifold.VectorField.Pullback
 public import Mathlib.Geometry.Manifold.WhitneyEmbedding

Mathlib/Geometry/Manifold/CheatSheet.md

@@ -0,0 +1,127 @@
+## Differential geometry cheat sheet
+
+How do I say certain basic things in Lean?
+For each of them, include a variable block. Can verso do this already?
+
+
+Let M be a C^k manifold.
+```
+variable {𝕜 E M H : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
+  [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {k : ℕ} -- more general: take k : WithTop ℕ∞, allows smooth and analytic; remove WithTop to exclude analyticity
+  {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] [IsManifold I k M]
+```
+
+Let M be a smooth manifold
+```
+variable {𝕜 E M H : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
+  [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M]
+  {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] [IsManifold I ∞ M]
+```
+
+Let M be a smooth real manifold.
+```
+variable {E M H : Type*} [NormedAddCommGroup E]
+  [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M]
+  {I : ModelWithCorners ℝ E H} [ChartedSpace H M] [IsManifold I ∞ M] -- test, needs open scoped Manifold??
+```
+
+Let M be an analytic manifold
+```
+open scoped Manifold -- test, necessary?
+
+variable {𝕜 E M H : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
+  [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M]
+  {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] [IsManifold I ω M]
+```
+
+Differentiability of functions between manifolds
+```
+import Mathlib.Geometry.Manifold.MFDeriv.Defs
+import Mathlib.Geometry.Manifold.ContMDiff.Defs
+
+variable
+  -- Given a non-trivially normed field 𝕜
+  {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+  -- A manifold M over 𝕜
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+  {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
+  {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
+  -- A manifold M' over 𝕜
+  {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
+  {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
+  {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
+  -- A function from M to M' and x in M
+  (f : M → M') (x : M)
+
+variable (x : M) in
+-- f is differentiable at x
+#check MDifferentiableAt I I' f x
+
+variable (n : WithTop ℕ∞) in -- A natural number or ∞ or ω
+#check ContMDiff I I' n f
+
+
+variable
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+  (g : M → F) in
+open scoped Manifold in
+#check ContMDiff I 𝓘(𝕜, F) n g  -- g is n times continuously differentiable
+```
+
+Consider the product manifold M \times N.
+
+
+Let \phi be the preferred chart at x\in M.
+
+Let \phi be any (compatible) chart on M.
+
+--------
+
+Let E\to M be a topological vector bundle.
+
+Let E\to M be a smooth vector bundle.
+
+Let s be a section of E.
+```
+variable (s : Π x : M, V x)
+```
+Let X be a vector field on `M`
+```
+(X : Π x : M, TangentSpace I x)
+```
+
+Let s be a C^k section of E. / The section s of E is C^k.
+```
+ContMDiff I (I.prod 𝓘(𝕜, F)) (k + 1) (fun x ↦ TotalSpace.mk' F x (σ x))
+```
+
+Let `X` be a C^k vector field on M.
+```
+variable {X : Π x : M, TangentSpace I x}
+-- TODO: this doesn't work!
+-- variable (___hX: ContMDiff I I.tangent 2 (fun x ↦ (X x : TangentBundle I M)))
+```
+
+Let \phi be the preferred local trivialisation at x\in E.
+Let \phi be any compatible trivialisation on M.
+
+Consider the tangent bundle TM of M.
+
+Let X be a C^k vector field on M.
+
+explain TotalSpace.mk' somewhere in here...
+
+
+
+**Basic API lemmas**
+- testing smoothness of a map in charts: the standard charts; any charts
+
+- testing smoothness of a section in trivialisations: the standard charts; any charts
+
+
+**constructions**
+- product manifold (tricky!)
+- disjoint union
+
+- product bundle (how difficult?)
+- Lie bracket of vector fields

Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

@@ -83,7 +83,7 @@ theorem Differentiable.comp_mdifferentiable {g : F → F'} {f : M → F}
 
 end Module
 
-section ExtChartAt
+section extChartAt
 
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : M → F}
 
@@ -101,7 +101,7 @@ theorem DifferentiableWithinAt.mdifferentiableWithinAt_of_comp_extChartAt_symm [
   refine (mdifferentiableWithinAt_iff_source_of_mem_source (mem_chart_source H x)).2 ?_
   simpa [extChartAt_self_eq] using hf.mdifferentiableWithinAt
 
-end ExtChartAt
+end extChartAt
 
 /-! ### Linear maps between normed spaces are differentiable -/
 
@@ -398,20 +398,20 @@ end smul
 /-! ### Exterior derivative of a scalar function -/
 
 /-- The exterior derivative of a scalar function on `M`, as a section of the cotangent bundle. -/
-noncomputable abbrev extDerivFun (g : M → 𝕜) :
-    Π x : M, TangentSpace I x →L[𝕜] 𝕜 :=
+noncomputable abbrev extDerivFun (g : M → F) :
+    Π x : M, TangentSpace I x →L[𝕜] F :=
   fun x ↦ (NormedSpace.fromTangentSpace <| g x).toContinuousLinearMap ∘L (mfderiv% g x)
 
 @[simp]
-lemma extDerivFun_add {g g' : M → 𝕜} {x : M} (hg : MDiffAt g x) (hg' : MDiffAt g' x) :
+lemma extDerivFun_add {g g' : M → F} {x : M} (hg : MDiffAt g x) (hg' : MDiffAt g' x) :
     extDerivFun (g + g') x = extDerivFun (I := I) g x + extDerivFun g' x := by
   simp [extDerivFun, mfderiv_add hg hg']
   congr
 
 @[simp]
-lemma extDerivFun_zero {x : M} : extDerivFun (I := I) (0 : M → 𝕜) x = 0 := by
-  have : extDerivFun (0 : M → 𝕜) x + extDerivFun (0 : M → 𝕜) x =
-      extDerivFun (I := I) (0 : M → 𝕜) x := by
+lemma extDerivFun_zero {x : M} : extDerivFun (I := I) (0 : M → F) x = 0 := by
+  have : extDerivFun (0 : M → F) x + extDerivFun (0 : M → F) x =
+      extDerivFun (I := I) (0 : M → F) x := by
     rw [← extDerivFun_add (by exact mdifferentiable_const ..) (by exact mdifferentiable_const ..)]
     simp
   simpa using this

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

@@ -790,6 +790,20 @@ theorem mfderiv_add (hf : MDiffAt f z) (hg : MDiffAt g z) :
       (by exact mfderiv% f z) + (by exact mfderiv% g z) :=
   (hf.hasMFDerivAt.add hg.hasMFDerivAt).mfderiv
 
+open NormedSpace in
+theorem fromTangentSpace_mfderiv_add (hf : MDiffAt f z) (hg : MDiffAt g z) :
+    (fromTangentSpace _).toContinuousLinearMap ∘L (mfderiv% (f + g) z)
+    = (fromTangentSpace _).toContinuousLinearMap ∘L (mfderiv% f z)
+    + (fromTangentSpace _).toContinuousLinearMap ∘L (mfderiv% g z) :=
+  (hf.hasMFDerivAt.add hg.hasMFDerivAt).mfderiv
+
+open NormedSpace in
+theorem fromTangentSpace_mfderiv_add_apply (hf : MDiffAt f z) (hg : MDiffAt g z)
+    (v : TangentSpace I x) :
+    fromTangentSpace _ (mfderiv% (f + g) z v)
+    = fromTangentSpace _ (mfderiv% f z v) + fromTangentSpace _ (mfderiv% g z v) :=
+  congr($(fromTangentSpace_mfderiv_add hf hg) v)
+
 section sum
 variable {ι : Type} {t : Finset ι} {f : ι → M → E'} {f' : ι → TangentSpace I z →L[𝕜] E'}