wip

Author: grunweg

Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

@@ -161,18 +161,22 @@ theorem contDiffWithinAtProp_id (x : H) : ContDiffWithinAtProp I I n id univ x :
   · simp only [mfld_simps]
 
 variable (I I') in
-/-- A function is `n` times continuously differentiable within a set at a point in a manifold if
-it is continuous and it is `n` times continuously differentiable in this set around this point, when
-read in the preferred chart at this point.
+/-- `ContMDiffWithinAt I I' n f x` indicates that the function `f : M → M'` between manifolds
+is `n` times continuously differentiable at `x : M` within the set `s`.
+
+`f` is `n` times continuously differentiable within `s` at `x` if it is continuous and it is `n`
+times continuously differentiable in this set around `x`, when read in the preferred chart at `x`.
 The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
 number, `∞`, or `ω`, where `C^ω` corresponds to analytic functions. -/
 def ContMDiffWithinAt (n : ℕ∞ω) (f : M → M') (s : Set M) (x : M) :=
   LiftPropWithinAt (ContDiffWithinAtProp I I' n) f s x
 
 variable (I I') in
-/-- A function is `n` times continuously differentiable at a point in a manifold if
-it is continuous and it is `n` times continuously differentiable around this point, when
-read in the preferred chart at this point.
+/-- `ContMDiffAt I I' n f x` indicates that the function `f : M → M'` between manifolds
+is `n` times continuously differentiable at `x : M`.
+
+`f` is `n` times continuously differentiable at `x` if it is continuous and it is `n` times
+continuously differentiable around `x`, when read in the preferred chart at `x`.
 The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
 number, `∞`, or `ω`, where `C^ω` corresponds to analytic functions. -/
 def ContMDiffAt (n : ℕ∞ω) (f : M → M') (x : M) :=
@@ -186,18 +190,23 @@ theorem contMDiffAt_iff {n : ℕ∞ω} {f : M → M'} {x : M} :
   liftPropAt_iff.trans <| by rw [ContDiffWithinAtProp, preimage_univ, univ_inter]; rfl
 
 variable (I I') in
-/-- A function is `n` times continuously differentiable in a set of a manifold if it is continuous
-and, for any pair of points, it is `n` times continuously differentiable on this set in the charts
+/-- `ContMDiffOn I I' n f s` indicates that the function `f : M → M'` between manifolds
+is `n` times continuously differentiable in a set `s : Set M`.
+
+`f` is `n` times continuously differentiable on `s` if it is continuous on `s` and,
+for any pair of points, it is `n` times continuously differentiable `s` in the charts
 around these points.
 The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
 number, `∞`, or `ω`, where `C^ω` corresponds to analytic functions. -/
 def ContMDiffOn (n : ℕ∞ω) (f : M → M') (s : Set M) :=
   ∀ x ∈ s, ContMDiffWithinAt I I' n f s x
 
 variable (I I') in
-/-- A function is `n` times continuously differentiable in a manifold if it is continuous
-and, for any pair of points, it is `n` times continuously differentiable in the charts
-around these points.
+/-- `ContMDiff I I' n f` indicates that the function `f : M → M'` between manifolds
+is `n` times continuously differentiable.
+
+`f` is `n` times continuously differentiable if it is continuous and, for any pair of points,
+it is `n` times continuously differentiable in the charts around these points.
 The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
 number, `∞`, or `ω`, where `C^ω` corresponds to analytic functions. -/
 def ContMDiff (n : ℕ∞ω) (f : M → M') :=

Mathlib/Geometry/Manifold/MFDeriv/Defs.lean

@@ -316,9 +316,9 @@ def HasMFDerivAt (f : M → M') (x : M) (f' : TangentSpace I x →L[𝕜] Tangen
 
 open Classical in
 variable (I I') in
-/-- Let `f` be a function between two manifolds. Then `mfderivWithin I I' f s x` is the
-derivative of `f` at `x` within `s`, as a continuous linear map from the tangent space at `x` to the
-tangent space at `f x`. -/
+/-- `mfderivWithin I I' f s x`, given a function `f` between two manifolds,
+is the derivative of `f` at `x` within `s`,
+as a continuous linear map from the tangent space at `x` to the tangent space at `f x`. -/
 def mfderivWithin (f : M → M') (s : Set M) (x : M) : TangentSpace I x →L[𝕜] TangentSpace I' (f x) :=
   if MDifferentiableWithinAt I I' f s x then
     (fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((extChartAt I x).symm ⁻¹' s ∩ range I)
@@ -328,21 +328,22 @@ def mfderivWithin (f : M → M') (s : Set M) (x : M) : TangentSpace I x →L[
 
 open Classical in
 variable (I I') in
-/-- Let `f` be a function between two manifolds. Then `mfderiv I I' f x` is the derivative of
-`f` at `x`, as a continuous linear map from the tangent space at `x` to the tangent space at
-`f x`. -/
+/-- `mfderiv I I' f x`, given a function `f` between two manifolds, is the derivative of `f` at `x`,
+as a continuous linear map from the tangent space at `x` to the tangent space at `f x`. -/
 def mfderiv (f : M → M') (x : M) : TangentSpace I x →L[𝕜] TangentSpace I' (f x) :=
   if MDifferentiableAt I I' f x then
     (fderivWithin 𝕜 (writtenInExtChartAt I I' x f : E → E') (range I) ((extChartAt I x) x) :)
   else 0
 
 variable (I I') in
-/-- The derivative within a set, as a map between the tangent bundles -/
+/-- `tangentMapWithin I I' f s` is the derivative of `f : M → M'` within a set `s`,
+as a map between the tangent bundles `TM` and `TM'`. -/
 def tangentMapWithin (f : M → M') (s : Set M) : TangentBundle I M → TangentBundle I' M' := fun p =>
   ⟨f p.1, (mfderivWithin I I' f s p.1 : TangentSpace I p.1 → TangentSpace I' (f p.1)) p.2⟩
 
 variable (I I') in
-/-- The derivative, as a map between the tangent bundles -/
+/-- `tangentMap I I' f` is the derivative of `f : M → M'` as a map between the tangent bundles
+`TM` and `TM'`. -/
 def tangentMap (f : M → M') : TangentBundle I M → TangentBundle I' M' := fun p =>
   ⟨f p.1, (mfderiv I I' f p.1 : TangentSpace I p.1 → TangentSpace I' (f p.1)) p.2⟩