The first variation of a smooth family of nondegenerate metrics

Let g be a smooth family of nondegenerate metrics on M parametrized by a manifold P, as bundled by TauCeti.Manifold.ContMDiffNondegenerateMetricFamily. At every point y : M the forms g (p, y) all live on the single tangent space T_y M, so p ↦ g (p, y) is a smooth map from P to a fixed space of bilinear forms. Its differential at p in the direction of a parameter tangent vector u ∈ T_p P is the first variation δ_u g of the family, a field of symmetric bilinear forms on M.

Along a parameter curve c : ℝ → P, the parameter derivative ∂ₜ g_{c t} of the restricted family is the variation of g at c t in the direction of the velocity c'(t). This is the symmetric field h = ∂ₜ g_t entering the first variation formula of the Levi-Civita connection.

Main definitions and results

In the namespace TauCeti.Manifold.ContMDiffNondegenerateMetricFamily:

• variation: the first variation δ_u g of a family at a parameter p in the direction u ∈ T_p P.
• variation_eq_mfderiv: the variation at y is the differential of p ↦ g (p, y).
• variation_zero, variation_add, variation_smul: the variation is linear in the parameter direction.
• variation_apply_comm: the variation is a field of symmetric bilinear forms.
• contMDiff_variation: in any parameter tangent direction, it is a smooth tensor field.
• hasDerivAt_apply_apply_comp: along a differentiable parameter curve c, the derivative at t of s ↦ g (c s, y) (v, w) is δ_{c'(t)} g (v, w).
• variation_comp and variation_const: the variation of a restricted family is given by the chain rule, and the variation of a constant family vanishes.

References

• A. L. Besse, Einstein Manifolds, Springer (1987), Section 1.K: variations of metrics.

noncomputable def TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.variation {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] [IsManifold I (↑⊤) M] {EP : Type u_4} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_5} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_6} [TopologicalSpace P] [ChartedSpace HP P] (g : ContMDiffNondegenerateMetricFamily I M IP P) (p : P) (u : TangentSpace IP p) (y : M) : TangentSpace I y →L[ℝ] TangentSpace I y →L[ℝ] ℝ

The first variation δ_u g of a smooth nondegenerate metric family at the parameter p in the direction u ∈ T_p P. Its value at y : M is the differential at p of the smooth map p' ↦ g (p', y) into the bilinear forms on T_y M, applied to u.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.variation_eq_mfderiv {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] [IsManifold I (↑⊤) M] {EP : Type u_4} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_5} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_6} [TopologicalSpace P] [ChartedSpace HP P] (g : ContMDiffNondegenerateMetricFamily I M IP P) (p : P) (u : TangentSpace IP p) (y : M) : g.variation p u y = ((mfderiv% fun (p' : P) => (g.metric p').toContMDiffSection y) p) u

The first variation at y is the differential at p of the smooth map p' ↦ g_{p'} y, with values typed as bilinear forms on the model space, applied to u.

@[simp]

theorem TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.variation_zero {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] [IsManifold I (↑⊤) M] {EP : Type u_4} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_5} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_6} [TopologicalSpace P] [ChartedSpace HP P] (g : ContMDiffNondegenerateMetricFamily I M IP P) (p : P) : g.variation p 0 = 0

The first variation in the zero direction vanishes.

@[simp]

theorem TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.variation_add {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] [IsManifold I (↑⊤) M] {EP : Type u_4} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_5} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_6} [TopologicalSpace P] [ChartedSpace HP P] (g : ContMDiffNondegenerateMetricFamily I M IP P) (p : P) (u₁ u₂ : TangentSpace IP p) : g.variation p (u₁ + u₂) = g.variation p u₁ + g.variation p u₂

The first variation is additive in the parameter direction.

@[simp]

theorem TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.variation_smul {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] [IsManifold I (↑⊤) M] {EP : Type u_4} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_5} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_6} [TopologicalSpace P] [ChartedSpace HP P] (g : ContMDiffNondegenerateMetricFamily I M IP P) (p : P) (a : ℝ) (u : TangentSpace IP p) : g.variation p (a • u) = a • g.variation p u

The first variation is homogeneous in the parameter direction.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.contMDiff_variation {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] [IsManifold I (↑⊤) M] {EP : Type u_4} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_5} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_6} [TopologicalSpace P] [ChartedSpace HP P] (g : ContMDiffNondegenerateMetricFamily I M IP P) [IsManifold IP 1 P] (p : P) (u : TangentSpace IP p) : ContMDiff I (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) ↑⊤ fun (y : M) => ⟨y, g.variation p u y⟩

The first variation in an arbitrary parameter tangent direction is a smooth section of the tangent bilinear-form bundle.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.variation_apply_comm {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] [IsManifold I (↑⊤) M] {EP : Type u_4} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_5} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_6} [TopologicalSpace P] [ChartedSpace HP P] (g : ContMDiffNondegenerateMetricFamily I M IP P) (p : P) (u : TangentSpace IP p) (y : M) (v w : TangentSpace I y) : ((g.variation p u y) v) w = ((g.variation p u y) w) v

The first variation of a smooth nondegenerate metric family is a field of symmetric bilinear forms.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.hasDerivAt_apply_apply_comp {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] [IsManifold I (↑⊤) M] {EP : Type u_4} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_5} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_6} [TopologicalSpace P] [ChartedSpace HP P] (g : ContMDiffNondegenerateMetricFamily I M IP P) {c : ℝ → P} {t : ℝ} (hc : MDiffAt c t) (y : M) (v w : TangentSpace I y) : HasDerivAt (fun (s : ℝ) => ((↑g (c s, y)) v) w) (((g.variation (c t) ((mfderiv% c t) 1) y) v) w) t

The variation along a parameter curve. For a parameter curve c differentiable at t, the derivative at t of s ↦ g (c s, y) (v, w) is the first variation of g at c t in the direction of the velocity c'(t), evaluated at (v, w).

@[simp]

theorem TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.variation_comp {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] [IsManifold I (↑⊤) M] {EP : Type u_4} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_5} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_6} [TopologicalSpace P] [ChartedSpace HP P] (g : ContMDiffNondegenerateMetricFamily I M IP P) {EP' : Type u_7} [NormedAddCommGroup EP'] [NormedSpace ℝ EP'] {HP' : Type u_8} [TopologicalSpace HP'] {IP' : ModelWithCorners ℝ EP' HP'} {P' : Type u_9} [TopologicalSpace P'] [ChartedSpace HP' P'] (c : ContMDiffMap IP' IP P' P ↑⊤) (p' : P') (u : TangentSpace IP' p') : (g.comp c).variation p' u = g.variation (c p') ((mfderiv% ⇑c p') u)

Chain rule. The first variation of a family restricted along a smooth parameter map c is the variation of the original family in the direction of the image of u under dc.

@[simp]

theorem TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.variation_const {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] [IsManifold I (↑⊤) M] {EP : Type u_4} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_5} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_6} [TopologicalSpace P] [ChartedSpace HP P] (g₀ : ContMDiffNondegenerateMetric) (p : P) (u : TangentSpace IP p) : (const g₀).variation p u = 0

The first variation of a constant family vanishes.