Regularity of covariant derivatives along vector fields

This file records the regularity of evaluating a smooth covariant derivative on a smooth vector field. It turns the hom-bundle-valued regularity supplied by CovariantDerivative.ContMDiffCovariantDerivative into regularity of the resulting section. That class asks for regularity of ∇σ only for sections σ which are regular everywhere, and ContMDiffCovariantDerivativeOn on a set s only for sections regular on all of s; on a smooth real manifold, cutting off by bump functions shows that this gives the same regularity of ∇σ on every open subset where σ is regular, which is the form used to read a connection in a local frame.

Main results

• CovariantDerivative.contMDiff_apply: applying a C^n covariant derivative to a C^(n + 1) section along a C^n vector field produces a C^n section.
• ContMDiffCovariantDerivativeOn.mono_of_isOpen: on a smooth real manifold, a covariant derivative which is C^n on a set is C^n on each open subset where it is a covariant derivative.
• CovariantDerivative.contMDiffCovariantDerivativeOn_of_isOpen: a C^n covariant derivative is C^n on every open set.

theorem CovariantDerivative.contMDiff_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul 𝕜 (V x)] [FiberBundle F V] [IsManifold I 1 M] [VectorBundle 𝕜 F V] {n : WithTop ℕ∞} (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative n] {X : (x : M) → TangentSpace I x} {σ : (x : M) → V x} (hX : ContMDiff I I.tangent n fun (x : M) => ⟨x, X x⟩) (hσ : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) (n + 1) fun (x : M) => ⟨x, σ x⟩) : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨x, (↑cov σ x) (X x)⟩

Applying a C^n covariant derivative to a C^(n + 1) section along a C^n vector field produces a C^n section.

theorem ContMDiffCovariantDerivativeOn.mono_of_isOpen {E : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_8} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] {F : Type u_10} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_11} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] {n : ℕ∞} {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[ℝ] V x} {s u : Set M} (h : ContMDiffCovariantDerivativeOn F (↑n) cov s) (hcov : IsCovariantDerivativeOn F cov u) (hu : IsOpen u) (hus : u ⊆ s) : ContMDiffCovariantDerivativeOn F (↑n) cov u

Locality of the regularity of a connection. On a smooth real manifold, if cov is C^n on a set s and is a covariant derivative on an open subset u ⊆ s, then cov is also C^n on u: it sends sections which are C^(n + 1) on u to covariant derivatives which are C^n on u.

theorem CovariantDerivative.contMDiffCovariantDerivativeOn_of_isOpen {E : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_8} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] {F : Type u_10} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_11} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] {n : ℕ∞} (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑n] {u : Set M} (hu : IsOpen u) : ContMDiffCovariantDerivativeOn F (↑n) (↑cov) u

Locality of the regularity of a connection. A C^n covariant derivative on a smooth real manifold is C^n on every open set u: it sends sections which are C^(n + 1) on u to covariant derivatives which are C^n on u.