Families of fields of bilinear forms on the tangent bundle

This file collects regularity results for a one-parameter family b_s of fields of bilinear forms on TM, jointly C^n in (s, x) as a map into the bundle of bilinear forms on TM. No metric, symmetry or nondegeneracy is assumed.

Main results

• TauCeti.Manifold.contMDiffAt_uncurry_apply_apply: pairing two C^n vector fields with a jointly C^n family of fields of bilinear forms gives a jointly C^n family of functions.
• TauCeti.Manifold.differentiableAt_apply_apply_of_contMDiffAt: the parameter curves at x of a jointly C¹ family are differentiable.
• TauCeti.Manifold.hasDerivAt_mvfderiv_apply_apply: for a jointly C² family, the parameter derivative commutes with the differential of the pairing with two vector fields.
• TauCeti.Manifold.contMDiffAt_of_hasDerivAt_family: the parameter derivative of a jointly C^n family of fields of bilinear forms is a C^m field for m + 1 ≤ n.
• TauCeti.Manifold.mdifferentiableAt_apply_apply_of_hasDerivAt_family: the parameter derivative of a jointly C² family pairs differentiable vector fields to a differentiable function.

theorem TauCeti.Manifold.contMDiffAt_uncurry_apply_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {b : ℝ → (x : M) → TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ} {t : ℝ} {x : M} [IsManifold I (↑⊤) M] {n : WithTop ℕ∞} (hb : ContMDiffAt ((modelWithCornersSelf ℝ ℝ).prod I) (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) n (fun (q : ℝ × M) => ⟨q.2, b q.1 q.2⟩) (t, x)) {V W : (x : M) → TangentSpace I x} (hV : ContMDiffAt I I.tangent n (fun (x : M) => ⟨x, V x⟩) x) (hW : ContMDiffAt I I.tangent n (fun (x : M) => ⟨x, W x⟩) x) : ContMDiffAt ((modelWithCornersSelf ℝ ℝ).prod I) (modelWithCornersSelf ℝ ℝ) n (Function.uncurry fun (s : ℝ) (y : M) => ((b s y) (V y)) (W y)) (t, x)

Pairing two C^n vector fields with a jointly C^n family of fields of bilinear forms gives a jointly C^n family of functions.

theorem TauCeti.Manifold.differentiableAt_apply_apply_of_contMDiffAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {b : ℝ → (x : M) → TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ} {t : ℝ} {x : M} [IsManifold I (↑⊤) M] {n : WithTop ℕ∞} (hn : 1 ≤ n) (hb : ContMDiffAt ((modelWithCornersSelf ℝ ℝ).prod I) (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) n (fun (q : ℝ × M) => ⟨q.2, b q.1 q.2⟩) (t, x)) (u w : TangentSpace I x) : DifferentiableAt ℝ (fun (s : ℝ) => ((b s x) u) w) t

The parameter curve s ↦ b s x u w of a family of fields of bilinear forms, jointly C¹ at (t, x), is differentiable at t.

theorem TauCeti.Manifold.hasDerivAt_mvfderiv_apply_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {b : ℝ → (x : M) → TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ} {t : ℝ} {x : M} [IsManifold I (↑⊤) M] (hb : ContMDiffAt ((modelWithCornersSelf ℝ ℝ).prod I) (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) 2 (fun (q : ℝ × M) => ⟨q.2, b q.1 q.2⟩) (t, x)) {V W : (x : M) → TangentSpace I x} (hV : ContMDiffAt I I.tangent 2 (fun (x : M) => ⟨x, V x⟩) x) (hW : ContMDiffAt I I.tangent 2 (fun (x : M) => ⟨x, W x⟩) x) (u : TangentSpace I x) : HasDerivAt (fun (s : ℝ) => ((d% fun (y : M) => ((b s y) (V y)) (W y)) x) u) (((d% fun (y : M) => deriv (fun (s : ℝ) => ((b s y) (V y)) (W y)) t) x) u) t

For a family of fields of bilinear forms, jointly C² at (t, x), and vector fields V, W that are C² at x, the parameter derivative of the differential at x of the pairing y ↦ b_s(V, W) is the differential of the parameter derivative of the pairing.

theorem TauCeti.Manifold.contMDiffAt_of_hasDerivAt_family {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {b : ℝ → (x : M) → TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ} {h : (x : M) → TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ} {t : ℝ} {x : M} [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E] {m n : WithTop ℕ∞} (hb : ContMDiffAt ((modelWithCornersSelf ℝ ℝ).prod I) (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) n (fun (q : ℝ × M) => ⟨q.2, b q.1 q.2⟩) (t, x)) (hmn : m + 1 ≤ n) (hh : ∀ᶠ (y : M) in nhds x, ∀ (v w : TangentSpace I y), HasDerivAt (fun (s : ℝ) => ((b s y) v) w) (((h y) v) w) t) : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) m (fun (y : M) => ⟨y, h y⟩) x

Regularity of the parameter derivative of a family of bilinear forms. Let b_s be a family of fields of bilinear forms on TM, jointly C^n in (s, y) at (t, x), and let h be its parameter derivative at s = t near x. Then h is a C^m field of bilinear forms at x whenever m + 1 ≤ n.

theorem TauCeti.Manifold.mdifferentiableAt_apply_apply_of_hasDerivAt_family {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {b : ℝ → (x : M) → TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ} {h : (x : M) → TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ} {t : ℝ} {x : M} [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E] (hb : ContMDiffAt ((modelWithCornersSelf ℝ ℝ).prod I) (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) 2 (fun (q : ℝ × M) => ⟨q.2, b q.1 q.2⟩) (t, x)) (hh : ∀ᶠ (y : M) in nhds x, ∀ (v w : TangentSpace I y), HasDerivAt (fun (s : ℝ) => ((b s y) v) w) (((h y) v) w) t) {V W : (x : M) → TangentSpace I x} (hV : (MDiffAt fun (x : M) => ⟨x, V x⟩) x) (hW : (MDiffAt fun (x : M) => ⟨x, W x⟩) x) : (MDiffAt fun (y : M) => ((h y) (V y)) (W y)) x

The parameter derivative h of a family of fields of bilinear forms, jointly C² at (t, x), pairs vector fields differentiable at x to a function differentiable at x.