The Sobolev quotient of the Yamabe bubbles

Let E be a real inner product space of dimension n, with Lebesgue measure, and let U = U_{t,b} be the bubble of scale t > 0 centred at b (TauCeti.Yamabe.bubble). With aₙ = 4 (n - 1) / (n - 2), pₙ = 2 n / (n - 2) and |Sⁿ| the area of the unit round sphere (TauCeti.roundSphereVolume), this file identifies the critical norm and the energy of a bubble with the round sphere:

• ∫ U ^ pₙ = |Sⁿ| for n ≠ 2, n > 0;
• aₙ ∫ ‖dU‖² = n (n - 1) |Sⁿ| for n > 2.

Consequently, for n > 2, the bubbles attain the constant Y(Sⁿ) = n (n - 1) |Sⁿ| ^ (2 / n) (TauCeti.Yamabe.sphereYamabeConstant) in the Sobolev quotient:

aₙ ∫ ‖dU‖² = Y(Sⁿ) (∫ U ^ pₙ) ^ (2 / pₙ).

This is the equality case of the sharp Euclidean Sobolev inequality aₙ ∫ ‖du‖² ≥ Y(Sⁿ) (∫ |u| ^ pₙ) ^ (2 / pₙ); the inequality itself is not proved here. All three identities are independent of the scale t and the centre b.

Main declarations

• TauCeti.Yamabe.integral_bubble_rpow_criticalExponent_eq_roundSphereVolume: ∫ U ^ pₙ = |Sⁿ|.
• TauCeti.Yamabe.conformalCoefficient_mul_integral_norm_fderiv_bubble_sq_eq_roundSphereVolume: aₙ ∫ ‖dU‖² = n (n - 1) |Sⁿ|.
• TauCeti.Yamabe.conformalCoefficient_mul_integral_norm_fderiv_bubble_sq_eq_sphereYamabeConstant: aₙ ∫ ‖dU‖² = Y(Sⁿ) (∫ U ^ pₙ) ^ (2 / pₙ).
• TauCeti.Yamabe.sphereYamabeConstant_eq_div: Y(Sⁿ) = n (n - 1) |Sⁿ| / |Sⁿ| ^ (2 / pₙ).

References

• J. M. Lee and T. H. Parker, The Yamabe problem, Bull. Amer. Math. Soc. 17 (1987), §3.
• T. Aubin, Problèmes isopérimétriques et espaces de Sobolev, J. Differential Geom. 11 (1976).
• G. Talenti, Best constant in Sobolev inequality, Ann. Mat. Pura Appl. 110 (1976).

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

The Yamabe constant of the round sphere as the quotient of the conformal energy n (n - 1) |Sⁿ| of a bubble by the power 2 / pₙ of its critical mass |Sⁿ|.

theorem TauCeti.Yamabe.integral_bubble_rpow_criticalExponent_eq_roundSphereVolume {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (hn₀ : 0 < Module.finrank ℝ E) (hn : Module.finrank ℝ E ≠ 2) {t : ℝ} (ht : 0 < t) (b : E) : ∫ (x : E), bubble t b x ^ criticalExponent (Module.finrank ℝ E) = roundSphereVolume (Module.finrank ℝ E)

The critical norm of a bubble is the area of the round sphere: in every positive dimension n ≠ 2, for Lebesgue measure, ∫ U_{t,b} ^ pₙ = |Sⁿ|.

theorem TauCeti.Yamabe.conformalCoefficient_mul_integral_norm_fderiv_bubble_sq_eq_roundSphereVolume {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (hn : 2 < Module.finrank ℝ E) {t : ℝ} (ht : 0 < t) (b : E) : conformalCoefficient (Module.finrank ℝ E) * ∫ (x : E), ‖fderiv ℝ (bubble t b) x‖ ^ 2 = ↑(Module.finrank ℝ E) * (↑(Module.finrank ℝ E) - 1) * roundSphereVolume (Module.finrank ℝ E)

The energy of a bubble: in dimension n > 2, for Lebesgue measure, aₙ ∫ ‖dU_{t,b}‖² = n (n - 1) |Sⁿ|.

theorem TauCeti.Yamabe.conformalCoefficient_mul_integral_norm_fderiv_bubble_sq_eq_sphereYamabeConstant {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (hn : 2 < Module.finrank ℝ E) {t : ℝ} (ht : 0 < t) (b : E) : conformalCoefficient (Module.finrank ℝ E) * ∫ (x : E), ‖fderiv ℝ (bubble t b) x‖ ^ 2 = sphereYamabeConstant (Module.finrank ℝ E) * (∫ (x : E), bubble t b x ^ criticalExponent (Module.finrank ℝ E)) ^ (2 / criticalExponent (Module.finrank ℝ E))

The bubbles attain the Yamabe constant of the sphere: in dimension n > 2, for Lebesgue measure, aₙ ∫ ‖dU_{t,b}‖² = Y(Sⁿ) (∫ U_{t,b} ^ pₙ) ^ (2 / pₙ). This is the equality case of the sharp Euclidean Sobolev inequality.