The conformal Laplacian

On a Riemannian manifold (M, g) of dimension n, the conformal Laplacian is the second-order operator

L_g u = aₙ Δ⁺_g u + Scal_g u,

where aₙ = 4 (n - 1) / (n - 2) (TauCeti.Yamabe.conformalCoefficient), Δ⁺_g = -Δ_g is the nonnegative Laplacian (TauCeti.Manifold.laplaceBeltrami is Δ_g = div ∘ grad) and Scal_g is the scalar curvature of the Levi-Civita connection. It is the operator of the Yamabe problem: for n > 2 and u > 0, the metric u ^ (4 / (n - 2)) g has scalar curvature u ^ (-(n + 2) / (n - 2)) L_g u, so u gives a metric of constant scalar curvature λ exactly when L_g u = λ u ^ (pₙ - 1).

The definition is total in the dimension; at n = 2 the coefficient aₙ is 0 by the convention for division by zero, and the operator has its classical meaning only for n > 2. The metric is the RiemannianBundle instance of the tangent bundle, as for TauCeti.Manifold.laplaceBeltrami. This file develops the operator itself, its two basic examples, and the transformation law of scalar curvature:

• on Euclidean space, which is flat, L u = aₙ (-Δ u) for Mathlib's Laplacian Δ, so the bubble equation aₙ (-Δ U) = n (n - 1) U ^ (pₙ - 1) says that every bubble U solves the Yamabe equation L U = n (n - 1) U ^ (pₙ - 1) of the unit round sphere;
• under multiplication of the metric by a positive constant c, both Δ and Scal are multiplied by c⁻¹, so L_{c g} = c⁻¹ L_g;
• for n ≠ 2 and u > 0, writing u ^ (4 / (n - 2)) = e^(2φ) with φ = (2 / (n - 2)) log u, the conformal change formula Scal_ĝ = e^(-2φ) (Scal_g - 2 (n - 1) Δφ - (n - 1) (n - 2) |dφ|²) and the chain rule for Δ log u combine into Scal_ĝ = u ^ (-(n + 2) / (n - 2)) L_g u: the first-order terms |du|² / u² cancel exactly for the coefficient aₙ.

Main declarations

• TauCeti.Yamabe.conformalLaplacian: the conformal Laplacian L_g.
• TauCeti.Yamabe.conformalLaplacian_add, TauCeti.Yamabe.conformalLaplacian_smul: linearity on C² functions; TauCeti.Yamabe.conformalLaplacian_const: L_g c = c Scal_g.
• TauCeti.Yamabe.contMDiff_conformalLaplacian: L_g maps C^(k + 2) functions to C^k functions.
• TauCeti.Yamabe.conformalLaplacian_eq_conformalCoefficient_mul_neg_laplacian: on Euclidean space, L u = aₙ (-Δ u).
• TauCeti.Yamabe.conformalLaplacian_bubble: the bubbles solve L U = n (n - 1) U ^ (pₙ - 1).
• TauCeti.Yamabe.conformalLaplacian_rescale_const: L_{c g} = c⁻¹ L_g for a constant c > 0.
• TauCeti.Yamabe.scalarCurvature_rescale_eq_rpow_mul_conformalLaplacian: the scalar curvature of ĝ = u ^ (4 / (n - 2)) g is u ^ (-(n + 2) / (n - 2)) L_g u.
• TauCeti.Yamabe.scalarCurvature_rescale_eq_iff_conformalLaplacian_eq: ĝ has scalar curvature c exactly where L_g u = c u ^ (pₙ - 1).
• TauCeti.Yamabe.conformalLaplacian_rescale: the conformal covariance L_ĝ v = u ^ (-(n + 2) / (n - 2)) L_g (u v).
• Bundle.ContMDiffRiemannianMetric.scalarCurvature_rescale_of_conformalLaplacian_eq_mul: if L_g u = λ u, then Scal_ĝ = λ u ^ (-4 / (n - 2)), and Bundle.ContMDiffRiemannianMetric.sign_scalarCurvature_rescale_of_conformalLaplacian_eq_mul: its sign is that of λ.

References

• J. M. Lee and T. H. Parker, The Yamabe problem, Bull. Amer. Math. Soc. 17 (1987), §2 (the conformal Laplacian and its conventions) and §3 (the Euclidean bubbles).

noncomputable def TauCeti.Yamabe.conformalLaplacian {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] [T2Space M] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] (u : M → ℝ) (x : M) : ℝ

The conformal Laplacian L_g u = aₙ Δ⁺_g u + Scal_g u of a function u on a smooth Riemannian manifold of dimension n, where aₙ = 4 (n - 1) / (n - 2), Δ⁺_g = -Δ_g is the nonnegative Laplacian and Scal_g is the scalar curvature.

theorem TauCeti.Yamabe.conformalLaplacian_def {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] [T2Space M] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] (u : M → ℝ) (x : M) : conformalLaplacian I u x = conformalCoefficient (Module.finrank ℝ E) * -Manifold.laplaceBeltrami I u x + (CovariantDerivative.leviCivitaConnection I M).scalarCurvature x * u x

Unfolding lemma for TauCeti.Yamabe.conformalLaplacian.

@[simp]

theorem TauCeti.Yamabe.conformalLaplacian_const {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] [T2Space M] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] (c : ℝ) (x : M) : conformalLaplacian I (fun (x : M) => c) x = (CovariantDerivative.leviCivitaConnection I M).scalarCurvature x * c

The conformal Laplacian of a constant c is c times the scalar curvature.

@[simp]

theorem TauCeti.Yamabe.conformalLaplacian_zero {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] [T2Space M] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] (x : M) : conformalLaplacian I 0 x = 0

The conformal Laplacian of the zero function vanishes.

theorem TauCeti.Yamabe.conformalLaplacian_add {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] [T2Space M] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {u v : M → ℝ} (hu : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 u) (hv : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 v) (x : M) : conformalLaplacian I (u + v) x = conformalLaplacian I u x + conformalLaplacian I v x

The conformal Laplacian is additive on C² functions.

theorem TauCeti.Yamabe.conformalLaplacian_smul {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] [T2Space M] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] (c : ℝ) {u : M → ℝ} (hu : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 u) (x : M) : conformalLaplacian I (c • u) x = c * conformalLaplacian I u x

The conformal Laplacian commutes with multiplication by a real constant on C² functions.

theorem TauCeti.Yamabe.contMDiff_conformalLaplacian {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] [T2Space M] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {k : WithTop ℕ∞} (hk : k ≤ ↑⊤) {u : M → ℝ} (hu : ContMDiff I (modelWithCornersSelf ℝ ℝ) (k + 2) u) : ContMDiff I (modelWithCornersSelf ℝ ℝ) k (conformalLaplacian I u)

The conformal Laplacian of a C^(k + 2) function is C^k.

theorem TauCeti.Yamabe.conformalLaplacian_eq_conformalCoefficient_mul_neg_laplacian {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {u : F → ℝ} {x : F} (hu : DifferentiableAt ℝ (gradient u) x) : conformalLaplacian (modelWithCornersSelf ℝ F) u x = conformalCoefficient (Module.finrank ℝ F) * -Laplacian.laplacian u x

The conformal Laplacian of Euclidean space. Euclidean space is flat, so its conformal Laplacian is L u = aₙ (-Δ u), for Mathlib's Laplacian Δ, at every point where the gradient of u is differentiable.

theorem TauCeti.Yamabe.conformalLaplacian_bubble {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (hn : Module.finrank ℝ F ≠ 2) {t : ℝ} (ht : 0 < t) (b x : F) : conformalLaplacian (modelWithCornersSelf ℝ F) (bubble t b) x = ↑(Module.finrank ℝ F) * (↑(Module.finrank ℝ F) - 1) * bubble t b x ^ (criticalExponent (Module.finrank ℝ F) - 1)

The bubbles solve the Yamabe equation of the sphere. In dimension n ≠ 2, every bubble U = U_{t,b} of positive scale satisfies L U = n (n - 1) U ^ (pₙ - 1) for the conformal Laplacian L of Euclidean space.

theorem TauCeti.Yamabe.conformalLaplacian_rescale_const {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] [T2Space M] [IsManifold I (↑⊤) M] (g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {c : ℝ} (hc : 0 < c) {u : M → ℝ} (hu : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 u) (x : M) : conformalLaplacian I u x = c⁻¹ * conformalLaplacian I u x

Scaling of the conformal Laplacian. Multiplying a smooth metric g by a positive constant c multiplies its conformal Laplacian by c⁻¹ on C² functions: L_{c g} u = c⁻¹ L_g u.

theorem TauCeti.Yamabe.scalarCurvature_rescale_eq_rpow_mul_conformalLaplacian {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] [T2Space M] [IsManifold I (↑⊤) M] (g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hn : Module.finrank ℝ E ≠ 2) {u : M → ℝ} (hu_pos : ∀ (x : M), 0 < u x) {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ fun (x : M) => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))} {hf_pos : ∀ (x : M), 0 < u x ^ (4 / (↑(Module.finrank ℝ E) - 2))} (x : M) : (g.rescale (fun (x : M) => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))) hf hf_pos).scalarCurvature x = u x ^ (-(↑(Module.finrank ℝ E) + 2) / (↑(Module.finrank ℝ E) - 2)) * conformalLaplacian I u x

Scalar curvature of a conformal metric. In dimension n ≠ 2, let u be a positive function such that ĝ = u ^ (4 / (n - 2)) g is a smooth metric. Then the scalar curvature of ĝ is Scal_ĝ = u ^ (-(n + 2) / (n - 2)) L_g u, where L_g is the conformal Laplacian of g. Such a u is automatically smooth.

theorem TauCeti.Yamabe.scalarCurvature_rescale_eq_iff_conformalLaplacian_eq {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] [T2Space M] [IsManifold I (↑⊤) M] (g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hn : Module.finrank ℝ E ≠ 2) {u : M → ℝ} (hu_pos : ∀ (x : M), 0 < u x) {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ fun (x : M) => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))} {hf_pos : ∀ (x : M), 0 < u x ^ (4 / (↑(Module.finrank ℝ E) - 2))} (c : ℝ) (x : M) : (g.rescale (fun (x : M) => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))) hf hf_pos).scalarCurvature x = c ↔ conformalLaplacian I u x = c * u x ^ (criticalExponent (Module.finrank ℝ E) - 1)

The Yamabe equation. In dimension n ≠ 2, let u be a positive function such that ĝ = u ^ (4 / (n - 2)) g is a smooth metric. Then ĝ has scalar curvature c at a point exactly when u solves the Yamabe equation L_g u = c u ^ (pₙ - 1) there, where pₙ = 2 n / (n - 2).

theorem TauCeti.Yamabe.conformalLaplacian_rescale {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] [T2Space M] [IsManifold I (↑⊤) M] (g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hn : Module.finrank ℝ E ≠ 2) {u : M → ℝ} (hu_pos : ∀ (x : M), 0 < u x) {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ fun (x : M) => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))} {hf_pos : ∀ (x : M), 0 < u x ^ (4 / (↑(Module.finrank ℝ E) - 2))} {v : M → ℝ} (hv : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 v) (x : M) : conformalLaplacian I v x = u x ^ (-(↑(Module.finrank ℝ E) + 2) / (↑(Module.finrank ℝ E) - 2)) * conformalLaplacian I (u * v) x

The conformal Laplacian of a conformal metric. In dimension n ≠ 2, let u be a positive function such that ĝ = u ^ (4 / (n - 2)) g is a smooth metric. Then the conformal Laplacians of ĝ and g are related by L_ĝ v = u ^ (-(n + 2) / (n - 2)) L_g (u v) for every C² function v. For v = 1 this is the scalar curvature law scalarCurvature_rescale_eq_rpow_mul_conformalLaplacian.

theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_rescale_of_conformalLaplacian_eq_mul {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] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hn : Module.finrank ℝ E ≠ 2) {u : M → ℝ} (hu_pos : ∀ (x : M), 0 < u x) {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ fun (x : M) => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))} {hf_pos : ∀ (x : M), 0 < u x ^ (4 / (↑(Module.finrank ℝ E) - 2))} {c : ℝ} {x : M} (h : TauCeti.Yamabe.conformalLaplacian I u x = c * u x) : (g.rescale (fun (x : M) => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))) hf hf_pos).scalarCurvature x = c * u x ^ (-(4 / (↑(Module.finrank ℝ E) - 2)))

Scalar curvature from an eigenfunction of the conformal Laplacian. In dimension n ≠ 2, let u be a positive function such that ĝ = u ^ (4 / (n - 2)) g is a smooth metric. At a point where L_g u = λ u, the scalar curvature of ĝ is Scal_ĝ = λ u ^ (-4 / (n - 2)).

theorem Bundle.ContMDiffRiemannianMetric.sign_scalarCurvature_rescale_of_conformalLaplacian_eq_mul {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] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hn : Module.finrank ℝ E ≠ 2) {u : M → ℝ} (hu_pos : ∀ (x : M), 0 < u x) {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ fun (x : M) => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))} {hf_pos : ∀ (x : M), 0 < u x ^ (4 / (↑(Module.finrank ℝ E) - 2))} {c : ℝ} {x : M} (h : TauCeti.Yamabe.conformalLaplacian I u x = c * u x) : SignType.sign ((g.rescale (fun (x : M) => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))) hf hf_pos).scalarCurvature x) = SignType.sign c

The sign of the scalar curvature from an eigenfunction. In dimension n ≠ 2, let u be a positive function such that ĝ = u ^ (4 / (n - 2)) g is a smooth metric. At a point where L_g u = λ u, the scalar curvature of ĝ has the sign of λ.