Gradient, integrability and energy of the Yamabe bubbles

Let E be a real inner product space of dimension n > 2, and let U = U_{t,b}, U(x) = (2 t / (t² + ‖x - b‖²)) ^ ((n - 2) / 2), be the bubble of scale t > 0 centred at b (TauCeti.Yamabe.bubble). With aₙ = 4 (n - 1) / (n - 2) and pₙ = 2 n / (n - 2), this file proves:

• U ∈ L^{pₙ} and dU ∈ L² for every additive Haar measure, with U ^ pₙ = (2 t / (t² + ‖x - b‖²)) ^ n;
• the energy identity aₙ ∫ ‖dU‖² = n (n - 1) ∫ U ^ pₙ, again for every additive Haar measure;
• the value ∫ U ^ pₙ = 2 π ^ ((n + 1) / 2) / Γ((n + 1) / 2) for Lebesgue measure.

The integrability of U ^ pₙ and its value hold more generally in every positive dimension n ≠ 2, including n = 1.

The value is the classical surface area |Sⁿ| of the unit sphere Sⁿ ⊆ ℝⁿ⁺¹, as it must be, since U ^ (4 / (n - 2)) times the Euclidean metric is the pullback of the round metric of Sⁿ; neither the sphere nor the stereographic projection is formalized here. Classically, the two identities together say that aₙ ∫ ‖dU‖² = n (n - 1) |Sⁿ|, so that the Sobolev quotient of U is n (n - 1) |Sⁿ| ^ (2 / n), the Yamabe invariant of the round sphere; this is the equality case of the sharp Euclidean Sobolev inequality, which is not proved here.

The energy identity is proved in polar coordinates. Both integrands are radial about b, and the radial integrals are related by integrating the derivative of r ↦ r ^ n (t² + r²) (2 t / (t² + r²)) ^ n, which vanishes at 0 and at infinity exactly because n > 2. This gives the energy identity directly, without a whole-space integration by parts. The integrability of U ^ pₙ and ‖dU‖² and the value of ∫ U ^ pₙ are the moments of order 0 of TauCeti.Analysis.PDE.Yamabe.Bubble.Moments; the value then follows from Legendre's duplication formula.

Main declarations

• TauCeti.Yamabe.memLp_bubble, TauCeti.Yamabe.memLp_fderiv_bubble: U ∈ L^{pₙ}, dU ∈ L².
• TauCeti.Yamabe.conformalCoefficient_mul_integral_norm_fderiv_bubble_sq: the energy identity.
• TauCeti.Yamabe.integral_bubble_rpow_criticalExponent: the value of ∫ U ^ 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).

theorem TauCeti.Yamabe.integrable_bubble_rpow_criticalExponent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hn₀ : 0 < Module.finrank ℝ E) (hn : Module.finrank ℝ E ≠ 2) {t : ℝ} (ht : 0 < t) (b : E) : MeasureTheory.Integrable (fun (x : E) => bubble t b x ^ criticalExponent (Module.finrank ℝ E)) μ

In every positive dimension n ≠ 2, the critical power U_{t,b} ^ pₙ of a bubble is integrable for every additive Haar measure.

theorem TauCeti.Yamabe.integrable_norm_fderiv_bubble_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hn : 2 < Module.finrank ℝ E) {t : ℝ} (ht : 0 < t) (b : E) : MeasureTheory.Integrable (fun (x : E) => ‖fderiv ℝ (bubble t b) x‖ ^ 2) μ

In dimension n > 2, the squared norm of the differential of a bubble is integrable for every additive Haar measure.

theorem TauCeti.Yamabe.memLp_bubble {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hn : 2 < Module.finrank ℝ E) {t : ℝ} (ht : 0 < t) (b : E) : MeasureTheory.MemLp (bubble t b) (ENNReal.ofReal (criticalExponent (Module.finrank ℝ E))) μ

In dimension n > 2, a bubble lies in L^{pₙ} for every additive Haar measure.

theorem TauCeti.Yamabe.memLp_fderiv_bubble {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hn : 2 < Module.finrank ℝ E) {t : ℝ} (ht : 0 < t) (b : E) : MeasureTheory.MemLp (fderiv ℝ (bubble t b)) 2 μ

In dimension n > 2, the differential of a bubble lies in L² for every additive Haar measure.

theorem TauCeti.Yamabe.conformalCoefficient_mul_integral_norm_fderiv_bubble_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (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) * ∫ (x : E), bubble t b x ^ criticalExponent (Module.finrank ℝ E) ∂μ

The energy identity of a bubble: in dimension n > 2, aₙ ∫ ‖dU_{t,b}‖² = n (n - 1) ∫ U_{t,b} ^ pₙ for every additive Haar measure.

theorem TauCeti.Yamabe.integral_bubble_rpow_criticalExponent {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) = 2 * Real.pi ^ ((↑(Module.finrank ℝ E) + 1) / 2) / Real.Gamma ((↑(Module.finrank ℝ E) + 1) / 2)

The critical norm of a bubble: in every positive dimension n ≠ 2, for Lebesgue measure, ∫ U_{t,b} ^ pₙ = 2 π ^ ((n + 1) / 2) / Γ((n + 1) / 2), independently of the scale and the centre. The right-hand side is the classical surface area of the unit sphere Sⁿ ⊆ ℝⁿ⁺¹.