The Yamabe constant of the sphere

Let |Sⁿ| be the area of the unit round sphere Sⁿ ⊆ ℝⁿ⁺¹ (TauCeti.roundSphereVolume), its normalized n-dimensional Hausdorff measure. The Yamabe constant of the sphere is

Y(Sⁿ) = n (n - 1) |Sⁿ| ^ (2 / n).

For n > 2 it is the value of the Yamabe quotient Q(u) = ∫ (aₙ |du|² + Scal u²) / ‖u‖_{pₙ}² of the round metric (scalar curvature n (n - 1)) at a constant function u; it is the sharp constant of the Euclidean Sobolev inequality aₙ ∫ |du|² ≥ Y(Sⁿ) ‖u‖_{pₙ}² and the upper bound for the Yamabe invariant of every closed n-manifold. Neither of these facts is proved here; they are the reasons for introducing the constant.

Main declarations

• TauCeti.Yamabe.sphereYamabeConstant: the constant Y(Sⁿ), with its positivity for n > 1.

References

• J. M. Lee and T. H. Parker, The Yamabe problem, Bull. Amer. Math. Soc. 17 (1987), §2–§3.

noncomputable def TauCeti.Yamabe.sphereYamabeConstant (n : ℕ) : ℝ

The Yamabe constant of the sphere, Y(Sⁿ) = n (n - 1) |Sⁿ| ^ (2 / n), where |Sⁿ| is the area TauCeti.roundSphereVolume n of the unit round sphere.

theorem TauCeti.Yamabe.sphereYamabeConstant_def (n : ℕ) : sphereYamabeConstant n = ↑n * (↑n - 1) * roundSphereVolume n ^ (2 / ↑n)

Unfolding lemma for TauCeti.Yamabe.sphereYamabeConstant.

theorem TauCeti.Yamabe.sphereYamabeConstant_pos {n : ℕ} (hn : 1 < n) : 0 < sphereYamabeConstant n

The Yamabe constant of the sphere is positive in every dimension n > 1.

theorem TauCeti.Yamabe.sphereYamabeConstant_mul_roundSphereVolume_rpow {n : ℕ} (hn : n ≠ 0) : sphereYamabeConstant n * roundSphereVolume n ^ ((↑n - 2) / ↑n) = ↑n * (↑n - 1) * roundSphereVolume n

In dimension n ≠ 0, Y(Sⁿ) |Sⁿ| ^ ((n - 2) / n) = n (n - 1) |Sⁿ|. For n > 2 the exponent (n - 2) / n is 2 / pₙ, with pₙ = 2 n / (n - 2).