The Yamabe bubbles as stereographic pullbacks of the round sphere

Let n ≠ 2 and let U_{t,b} be the Yamabe bubble of scale t > 0 centred at b on ℝⁿ (TauCeti.Yamabe.bubble). This file proves that its Yamabe conformal factor U_{t,b} ^ (4 / (n - 2)) is the round metric of the unit sphere Sⁿ read in rescaled stereographic coordinates: if σ = stereographic' n v is Mathlib's stereographic chart from a unit vector v and Φ(x) = σ⁻¹((2 / t) (x - b)), then for all tangent vectors a, c at x,

⟪dΦ_x a, dΦ_x c⟫_{Sⁿ} = U_{t,b}(x) ^ (4 / (n - 2)) ⟪a, c⟫.

In other words, Φ is an isometry from (ℝⁿ, U_{t,b} ^ (4 / (n - 2)) δ) onto the round sphere minus the point v. Classically, this identification explains why the metric U_{t,b} ^ (4 / (n - 2)) δ has constant scalar curvature n (n - 1), matching the bubble equation aₙ Δ⁺ U = n (n - 1) U ^ (pₙ - 1) (TauCeti.Yamabe.conformalCoefficient_mul_neg_laplacian_bubble), and why the Sobolev quotient of a bubble is the Yamabe constant of the sphere; neither consequence is derived from it here. The scale 2 / t reflects Mathlib's normalization of σ, whose inverse chart alone pulls the round metric back to U_{2,0} ^ (4 / (n - 2)) δ.

Main results

• TauCeti.Yamabe.inner_mfderiv_stereographic'_symm_smul_sub: the pullback of the round metric along x ↦ σ⁻¹((2 / t) (x - b)) is U_{t,b} ^ (4 / (n - 2)) times the Euclidean metric.

References

• J. M. Lee and T. H. Parker, The Yamabe problem, Bull. Amer. Math. Soc. 17 (1987), 37–91, Section 3.
• T. Aubin, Problèmes isopérimétriques et espaces de Sobolev, J. Differential Geom. 11 (1976).

theorem TauCeti.Yamabe.inner_mfderiv_stereographic'_symm_smul_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (hn : n ≠ 2) (v : ↑(Metric.sphere 0 1)) {t : ℝ} (ht : 0 < t) (b x a c : EuclideanSpace ℝ (Fin n)) : inner ℝ ((mfderiv% (↑(stereographic' n v).symm ∘ fun (y : EuclideanSpace ℝ (Fin n)) => (2 / t) • (y - b)) x) a) ((mfderiv% (↑(stereographic' n v).symm ∘ fun (y : EuclideanSpace ℝ (Fin n)) => (2 / t) • (y - b)) x) c) = bubble t b x ^ (4 / (↑n - 2)) * inner ℝ a c

The bubbles are stereographic pullbacks of the round metric. In dimension n ≠ 2, let σ = stereographic' n v be a stereographic chart of the unit sphere Sⁿ. The round metric pulled back along x ↦ σ⁻¹((2 / t) (x - b)) is U_{t,b} ^ (4 / (n - 2)) times the Euclidean metric of ℝⁿ, where U_{t,b} is the bubble of scale t > 0 centred at b.