First-order quantities 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 two metrics live on the copies TauCeti.WithMetric g and TauCeti.WithMetric ĝ of M, so that each carries its own RiemannianBundle instance. This file compares the quantities of first order in the metric:

• the inner product: ⟪v, w⟫_ĝ = f ⟪v, w⟫_g;
• the inverse metric on arbitrary covectors: raising an index and pairing covectors scale by f⁻¹, and the covector operator norm scales by 1 / √f;
• the gradient, through the inverse metric: grad_ĝ u = f⁻¹ grad_g u, and hence ⟪grad_ĝ u, grad_ĝ w⟫_ĝ = f⁻¹ ⟪grad_g u, grad_g w⟫_g;
• the chart Gram matrix and its inverse, G_ĝ = f G_g and G_ĝ⁻¹ = f⁻¹ G_g⁻¹, and the volume density, dV_ĝ = f ^ (n / 2) dV_g in real dimension n.

Tangent vectors of the copies are compared with tangent vectors of M through the differential of TauCeti.WithMetric.ofWithMetric, which is the identity of the model space. Covectors on M are pulled back by that same differential, so each copy carries its own metric norm. Index raising uses Riemannian.Tensor.rieszDual. The inverse-metric laws hold for Cⁿ metrics and positive Cⁿ factors, including n = 0.

For the Yamabe problem, f = u ^ (4 / (n - 2)) with u positive, so that f ^ (n / 2) = u ^ (2 n / (n - 2)).

Main results

• TauCeti.WithMetric.inner_rescale: the inner product of the rescaled metric.
• TauCeti.WithMetric.mfderiv_ofWithMetric_rieszDual_rescale: raising a covector's index for the rescaled metric multiplies its transported Riesz dual by f⁻¹.
• TauCeti.WithMetric.apply_rieszDual_rescale: the inverse-metric pairing scales by f⁻¹.
• TauCeti.WithMetric.norm_sq_covector_rescale and TauCeti.WithMetric.norm_covector_rescale: the squared covector norm scales by f⁻¹, and the norm by 1 / √f.
• TauCeti.WithMetric.mfderiv_ofWithMetric_mgradient_rescale: the gradient for the rescaled metric is f⁻¹ times the gradient for g.
• TauCeti.WithMetric.inner_mgradient_rescale: the corresponding identity for the pointwise Dirichlet energy density.
• TauCeti.WithMetric.chartGramMatrix_rescale and TauCeti.WithMetric.chartInvGramMatrix_rescale: the chart Gram matrix scales by f, and its inverse by f⁻¹.
• TauCeti.WithMetric.chartVolumeDensity_rescale: the volume density of the rescaled metric is f ^ (n / 2) times that of g.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 2 (conformal metrics, dual metric, gradient and volume form).
• J. M. Lee and T. H. Parker, The Yamabe problem, Bull. Amer. Math. Soc. 17 (1987), 37–91, Section 2.

theorem TauCeti.WithMetric.inner_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {f : M → ℝ} {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f} {hf_pos : ∀ (x : M), 0 < f x} (x : WithMetric (g.rescale f hf hf_pos)) (v w : TangentSpace I x) : inner ℝ v w = f x.ofWithMetric * ((g.inner x.ofWithMetric) ((mfderiv% ofWithMetric x) v)) ((mfderiv% ofWithMetric x) w)

The inner product of the rescaled metric f g is f times that of g.

theorem TauCeti.WithMetric.mfderiv_ofWithMetric_rieszDual_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {f : M → ℝ} {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f} {hf_pos : ∀ (x : M), 0 < f x} (x : M) (φ : TangentSpace I x →L[ℝ] ℝ) : (mfderiv% ofWithMetric { ofWithMetric := x }) ((Riemannian.Tensor.rieszDual { ofWithMetric := x }) (φ ∘SL mfderiv% ofWithMetric { ofWithMetric := x })) = (f x)⁻¹ • (mfderiv% ofWithMetric { ofWithMetric := x }) ((Riemannian.Tensor.rieszDual { ofWithMetric := x }) (φ ∘SL mfderiv% ofWithMetric { ofWithMetric := x }))

Raising the index of a covector for f g gives f⁻¹ times its Riesz dual for g, with both vectors transported to the underlying manifold.

theorem TauCeti.WithMetric.apply_rieszDual_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {f : M → ℝ} {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f} {hf_pos : ∀ (x : M), 0 < f x} (x : M) (φ ψ : TangentSpace I x →L[ℝ] ℝ) : (φ ∘SL mfderiv% ofWithMetric { ofWithMetric := x }) ((Riemannian.Tensor.rieszDual { ofWithMetric := x }) (ψ ∘SL mfderiv% ofWithMetric { ofWithMetric := x })) = (f x)⁻¹ * (φ ∘SL mfderiv% ofWithMetric { ofWithMetric := x }) ((Riemannian.Tensor.rieszDual { ofWithMetric := x }) (ψ ∘SL mfderiv% ofWithMetric { ofWithMetric := x }))

The inverse-metric pairing φ(ψ♯) of two covectors scales by f⁻¹ under g ↦ f g.

theorem TauCeti.WithMetric.norm_sq_covector_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {f : M → ℝ} {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f} {hf_pos : ∀ (x : M), 0 < f x} (x : M) (φ : TangentSpace I x →L[ℝ] ℝ) : ‖φ ∘SL mfderiv% ofWithMetric { ofWithMetric := x }‖ ^ 2 = (f x)⁻¹ * ‖φ ∘SL mfderiv% ofWithMetric { ofWithMetric := x }‖ ^ 2

The squared operator norm of an arbitrary covector scales by f⁻¹ under g ↦ f g.

theorem TauCeti.WithMetric.norm_covector_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {f : M → ℝ} {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f} {hf_pos : ∀ (x : M), 0 < f x} (x : M) (φ : TangentSpace I x →L[ℝ] ℝ) : ‖φ ∘SL mfderiv% ofWithMetric { ofWithMetric := x }‖ = (√(f x))⁻¹ * ‖φ ∘SL mfderiv% ofWithMetric { ofWithMetric := x }‖

The operator norm of a covector for f g is its norm for g divided by √f.

theorem TauCeti.WithMetric.mfderiv_ofWithMetric_mgradient_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {f : M → ℝ} {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f} {hf_pos : ∀ (x : M), 0 < f x} (u : M → ℝ) (x : M) : (mfderiv% ofWithMetric { ofWithMetric := x }) (Manifold.mgradient I (u ∘ ofWithMetric) { ofWithMetric := x }) = (f x)⁻¹ • (mfderiv% ofWithMetric { ofWithMetric := x }) (Manifold.mgradient I (u ∘ ofWithMetric) { ofWithMetric := x })

Gradient under conformal change. The gradient of a function for the rescaled metric f g is f⁻¹ times its gradient for g, both read as tangent vectors of M.

theorem TauCeti.WithMetric.inner_mgradient_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {f : M → ℝ} {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f} {hf_pos : ∀ (x : M), 0 < f x} (u w : M → ℝ) (x : M) : inner ℝ (Manifold.mgradient I (u ∘ ofWithMetric) { ofWithMetric := x }) (Manifold.mgradient I (w ∘ ofWithMetric) { ofWithMetric := x }) = (f x)⁻¹ * inner ℝ (Manifold.mgradient I (u ∘ ofWithMetric) { ofWithMetric := x }) (Manifold.mgradient I (w ∘ ofWithMetric) { ofWithMetric := x })

The inner product of two gradients for the rescaled metric f g is f⁻¹ times the inner product of the gradients for g. With u = w, this is the pointwise Dirichlet energy density |du|²_{f g} = f⁻¹ |du|²_g.

theorem TauCeti.WithMetric.chartGramMatrix_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {f : M → ℝ} {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f} {hf_pos : ∀ (x : M), 0 < f x} (α x : M) : Riemannian.Tensor.chartGramMatrix { ofWithMetric := α } { ofWithMetric := x } = f x • Riemannian.Tensor.chartGramMatrix { ofWithMetric := α } { ofWithMetric := x }

The chart Gram matrix of the rescaled metric f g is f times that of g.

theorem TauCeti.WithMetric.chartInvGramMatrix_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {f : M → ℝ} {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f} {hf_pos : ∀ (x : M), 0 < f x} (α x : M) : Riemannian.Tensor.chartInvGramMatrix { ofWithMetric := α } { ofWithMetric := x } = (f x)⁻¹ • Riemannian.Tensor.chartInvGramMatrix { ofWithMetric := α } { ofWithMetric := x }

In chart coordinates, the inverse Gram matrix of f g is f⁻¹ times that of g.

theorem TauCeti.WithMetric.chartVolumeDensity_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} {f : M → ℝ} {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f} {hf_pos : ∀ (x : M), 0 < f x} (α x : M) : chartVolumeDensity { ofWithMetric := α } { ofWithMetric := x } = f x ^ (↑(Module.finrank ℝ E) / 2) * chartVolumeDensity { ofWithMetric := α } { ofWithMetric := x }

Volume density under conformal change. In real dimension n, the volume density of the rescaled metric f g in any chart is f ^ (n / 2) times that of g.