The Levi-Civita connection under a conformal change of metric

Let g be a Riemannian metric on M and f a positive function, and let ĝ = f g be the conformally rescaled metric Bundle.ContMDiffRiemannianMetric.rescale. The Levi-Civita connections of g and ĝ differ by the tensor

A(Y, X) = (2 f)⁻¹ (df(X) Y + df(Y) X - g(X, Y) grad_g f),

that is, ∇^ĝ_X Y = ∇^g_X Y + A(Y, X) for every vector field Y differentiable at the point. Writing f = e^(2φ), this is the classical formula ∇^ĝ_X Y = ∇^g_X Y + dφ(X) Y + dφ(Y) X - g(X, Y) grad_g φ. It is the first-order input for the transformation laws of curvature under conformal change, and hence for the conformal Laplacian. For the metrics u ^ p g of the Yamabe problem, with p = 4 / (n - 2), the tensor is p times the tensor of u (TauCeti.Manifold.conformalConnectionTensor_rpow).

The tensor A is built from g alone and the difference is added to a connection with Mathlib's CovariantDerivative.addOneForm. Adding A to a Levi-Civita connection of g gives a torsion-free connection, since A is symmetric, compatible with f g, by a direct computation with the product rule. Uniqueness of the Levi-Civita connection on differentiable vector fields, CovariantDerivative.IsLeviCivitaConnection.uniqueness, then identifies it with Mathlib's Levi-Civita connection of f g. As in TauCeti.Geometry.Manifold.Riemannian.Scaling, connections do not depend on a metric, so each metric is installed in turn as the RiemannianBundle instance of the tangent bundle of M and the connections are compared directly on M.

Main definitions and results

• TauCeti.Manifold.conformalConnectionTensor: the tensor A above, for the metric of the RiemannianBundle instance; TauCeti.Manifold.conformalConnectionTensor_apply evaluates it, and TauCeti.Manifold.inner_conformalConnectionTensor pairs it with a third vector.
• TauCeti.Manifold.contMDiff_conformalConnectionTensor_apply: evaluated on C^n vector fields, the tensor of a nowhere vanishing C^(n + 1) function is a C^n vector field.
• TauCeti.Manifold.conformalConnectionTensor_rpow: the tensor of u ^ p is p times the tensor of u.
• Bundle.ContMDiffRiemannianMetric.isLeviCivitaConnection_rescale_addOneForm: adding the tensor of f to a Levi-Civita connection of g gives a Levi-Civita connection of f g.
• Bundle.ContMDiffRiemannianMetric.leviCivitaConnection_rescale_apply: the Levi-Civita connection of f g is that of g plus the tensor of f, on differentiable vector fields.

References

• A. L. Besse, Einstein Manifolds, Springer (1987), Section 1.J.
• J. M. Lee and T. H. Parker, The Yamabe problem, Bull. Amer. Math. Soc. 17 (1987), 37–91, Section 2.

noncomputable def TauCeti.Manifold.conformalConnectionTensor {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (f : M → ℝ) (x : M) : TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] TangentSpace I x

The difference between the Levi-Civita connections of the metric g of the RiemannianBundle instance and of its conformal rescaling f g: A(v, w) = (2 f)⁻¹ (df(w) v + df(v) w - ⟪v, w⟫ grad f). As for CovariantDerivative.addOneForm, the first argument v is the value of the vector field being differentiated and the second argument w is the direction of differentiation.

@[simp]

theorem TauCeti.Manifold.conformalConnectionTensor_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (f : M → ℝ) (x : M) (v w : TangentSpace I x) : ((conformalConnectionTensor I f x) v) w = (2 * f x)⁻¹ • ((d% f x) w • v + (d% f x) v • w - inner ℝ v w • mgradient I f x)

theorem TauCeti.Manifold.conformalConnectionTensor_comm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (f : M → ℝ) (x : M) (v w : TangentSpace I x) : ((conformalConnectionTensor I f x) v) w = ((conformalConnectionTensor I f x) w) v

The conformal connection tensor is symmetric, which is why the conformally changed connection stays torsion free.

theorem TauCeti.Manifold.inner_conformalConnectionTensor {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (f : M → ℝ) (x : M) (v w z : TangentSpace I x) : inner ℝ (((conformalConnectionTensor I f x) v) w) z = (2 * f x)⁻¹ * ((d% f x) w * inner ℝ v z + (d% f x) v * inner ℝ w z - (d% f x) z * inner ℝ v w)

The pairing of the conformal connection tensor with a third vector: ⟪A(v, w), z⟫ = (2 f)⁻¹ (df(w) ⟪v, z⟫ + df(v) ⟪w, z⟫ - df(z) ⟪v, w⟫).

theorem TauCeti.Manifold.contMDiff_conformalConnectionTensor_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] [IsContMDiffRiemannianBundle I n E fun (x : M) => TangentSpace I x] {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (n + 1) f) (hf₀ : ∀ (x : M), f x ≠ 0) {Y Z : (x : M) → TangentSpace I x} (hY : ContMDiff I I.tangent n fun (x : M) => ⟨x, Y x⟩) (hZ : ContMDiff I I.tangent n fun (x : M) => ⟨x, Z x⟩) : ContMDiff I I.tangent n fun (y : M) => ⟨y, ((conformalConnectionTensor I f y) (Y y)) (Z y)⟩

The conformal connection tensor of a nowhere vanishing C^(n + 1) function, evaluated on two C^n vector fields, is a C^n vector field for a C^n metric.

theorem TauCeti.Manifold.conformalConnectionTensor_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {u : M → ℝ} {x : M} (hu : MDiffAt u x) (hux : 0 < u x) (p : ℝ) : conformalConnectionTensor I (fun (y : M) => u y ^ p) x = p • conformalConnectionTensor I u x

The conformal connection tensor of a real power u ^ p of a positive function is p times that of u. For p = 4 / (n - 2) this is the conformal factor of the Yamabe problem.

theorem TauCeti.Manifold.conformalConnectionTensor_exp_two_mul_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {φ : M → ℝ} {x : M} (hφ : MDiffAt φ x) (v w : TangentSpace I x) : ((conformalConnectionTensor I (fun (y : M) => Real.exp (2 * φ y)) x) v) w = (d% φ x) w • v + (d% φ x) v • w - inner ℝ v w • mgradient I φ x

The conformal connection tensor of an exponential factor e^(2φ) is the classical tensor A(v, w) = dφ(w) v + dφ(v) w - ⟪v, w⟫ grad φ of the conformal change e^(2φ) g.

theorem Bundle.ContMDiffRiemannianMetric.isLeviCivitaConnection_rescale_addOneForm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] {n : WithTop ℕ∞} (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (hn : 1 ≤ n) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f) (hf_pos : ∀ (x : M), 0 < f x) {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} (hcov : CovariantDerivative.IsLeviCivitaConnection I cov) : CovariantDerivative.IsLeviCivitaConnection I (cov.addOneForm (TauCeti.Manifold.conformalConnectionTensor I f))

Conformal change of the Levi-Civita connection. If ∇ is a Levi-Civita connection of a C¹ metric g, then ∇ + A is a Levi-Civita connection of f g for every positive function f of the same regularity, where A is the conformal connection tensor of f for g.

theorem Bundle.ContMDiffRiemannianMetric.leviCivitaConnection_rescale_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] {n : WithTop ℕ∞} (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (hn : 1 ≤ n) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f) (hf_pos : ∀ (x : M), 0 < f x) {Y : (x : M) → TangentSpace I x} {x : M} (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (v : TangentSpace I x) : (↑(CovariantDerivative.leviCivitaConnection I M) Y x) v = (↑(CovariantDerivative.leviCivitaConnection I M) Y x) v + ((TauCeti.Manifold.conformalConnectionTensor I f x) (Y x)) v

Levi-Civita connection under conformal change. For a positive function f, the Levi-Civita connection of f g is the Levi-Civita connection of g plus the conformal connection tensor of f, ∇^(f g)_v Y = ∇^g_v Y + (2 f)⁻¹ (df(v) Y + df(Y) v - g(Y, v) grad_g f), on every vector field Y differentiable at the point.