The parameter derivative of the Koszul expression

Let b_s be a one-parameter family of fields of bilinear forms on TM, jointly C² in (s, x) as a map into the bundle of bilinear forms on TM, with parameter derivative h = ∂ₛ b. This file proves that the Koszul expression TauCeti.Manifold.koszulBilinear of b_s on vector fields that are C² at x is differentiable in s, with derivative the Koszul expression of h. Symmetry, nondegeneracy and finite dimensionality are not needed. The proof commutes the parameter derivative with the differentials of the pairings, TauCeti.Manifold.hasDerivAt_mvfderiv_apply_apply.

Main results

• TauCeti.Manifold.differentiableAt_koszulBilinear: the Koszul expression of a jointly C² family of fields of bilinear forms is differentiable in the parameter.
• TauCeti.Manifold.hasDerivAt_koszulBilinear: its parameter derivative is the Koszul expression of the parameter derivative of the family.

References

• A. L. Besse, Einstein Manifolds, Springer (1987), Section 1.K, Theorem 1.174.

theorem TauCeti.Manifold.differentiableAt_koszulBilinear {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)) {X Y Z : (x : M) → TangentSpace I x} (hX : ContMDiffAt I I.tangent 2 (fun (x : M) => ⟨x, X x⟩) x) (hY : ContMDiffAt I I.tangent 2 (fun (x : M) => ⟨x, Y x⟩) x) (hZ : ContMDiffAt I I.tangent 2 (fun (x : M) => ⟨x, Z x⟩) x) : DifferentiableAt ℝ (fun (s : ℝ) => koszulBilinear I (b s) X Y Z x) t

The Koszul expression K_{b_s}(X, Y, Z) at x of a family of fields of bilinear forms, jointly C² at (t, x), is differentiable in the parameter at t, for vector fields X, Y, Z that are C² at x.

theorem TauCeti.Manifold.hasDerivAt_koszulBilinear {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] (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) {X Y Z : (x : M) → TangentSpace I x} (hX : ContMDiffAt I I.tangent 2 (fun (x : M) => ⟨x, X x⟩) x) (hY : ContMDiffAt I I.tangent 2 (fun (x : M) => ⟨x, Y x⟩) x) (hZ : ContMDiffAt I I.tangent 2 (fun (x : M) => ⟨x, Z x⟩) x) : HasDerivAt (fun (s : ℝ) => koszulBilinear I (b s) X Y Z x) (koszulBilinear I h X Y Z x) t

Variation of the Koszul expression. Let b_s be a family of fields of bilinear forms on TM, jointly C² in (s, y) at (t, x), with parameter derivative h = ∂ₛ b at s = t near x. Then for vector fields X, Y, Z that are C² at x, the parameter derivative of the Koszul expression K_{b_s}(X, Y, Z) at x is the Koszul expression K_h(X, Y, Z) of h.