The Euclidean Yamabe bubbles

On a real inner product space E of dimension n, the conformal coefficient and the critical Sobolev exponent are

aₙ = 4 (n - 1) / (n - 2), pₙ = 2 n / (n - 2),

so that, for n > 2, the conformal Laplacian of a metric g is aₙ Δ⁺_g + Scal_g, with Δ⁺ = -Δ the nonnegative Laplacian. The bubble of scale t > 0 centred at b is

U_{t,b}(x) = (2 t / (t² + ‖x - b‖²)) ^ ((n - 2) / 2).

The definitions are total: they make sense in every dimension, and at n = 2 the divisions by n - 2 evaluate to 0 by Lean's convention. Their geometric and analytic meaning is classical only for n > 2, which is the setting of the Yamabe problem.

Classically, for n > 2, U_{t,b} ^ (4 / (n - 2)) times the Euclidean metric is the pullback of the unit round metric of Sⁿ under x ↦ σ⁻¹ ((2 / t) • (x - b)), where σ = stereographic' n v is Mathlib's stereographic chart from a unit vector v; this identification is TauCeti.Yamabe.inner_mfderiv_stereographic'_symm_smul_sub. Accordingly, the bubble solves the conformal Laplacian equation whose right-hand side carries the scalar curvature n (n - 1) of the unit sphere:

aₙ (-Δ U_{t,b}) = n (n - 1) U_{t,b} ^ (pₙ - 1).

As stated, this equation is proved here for every n ≠ 2; in dimensions 0 and 1 both sides vanish, and it carries no geometric content.

For n > 2, these functions are the extremals of the sharp Euclidean Sobolev inequality and the local models for the test functions of the Yamabe problem.

Main declarations

• TauCeti.Yamabe.conformalCoefficient, TauCeti.Yamabe.criticalExponent: the constants aₙ and pₙ.
• TauCeti.Yamabe.bubble: the bubble U_{t,b}.
• TauCeti.Yamabe.bubble_pos, TauCeti.Yamabe.contDiff_bubble: positivity and smoothness.
• TauCeti.Yamabe.bubble_zero_sub, TauCeti.Yamabe.bubble_zero_smul: every bubble is a translate of a rescaled standard bubble U_{1,0}.
• TauCeti.Yamabe.bubble_rpow_criticalExponent, TauCeti.Yamabe.bubble_rpow_criticalExponent_eq_mul_rpow_neg_one_add_norm_sq: the critical power of a bubble, and its form as a rescaled translate of a Japanese bracket power.
• TauCeti.Yamabe.bubble_sq: the square of a bubble as a power of its profile.
• TauCeti.Yamabe.bubble_rpow_four_div_finrank_sub_two: the conformal factor U_{t,b} ^ (4 / (n - 2)) of a bubble.
• TauCeti.Yamabe.hasFDerivAt_bubble: the differential of a bubble without completeness.
• TauCeti.Yamabe.hasGradientAt_bubble, TauCeti.Yamabe.norm_fderiv_bubble, TauCeti.Yamabe.norm_fderiv_bubble_sq: the gradient of a bubble and the norm and squared norm of its differential.
• TauCeti.Yamabe.laplacian_div_add_norm_sub_sq_rpow: the Laplacian of an arbitrary real power of the bubble profile y ↦ 2 t / (t² + ‖y - b‖²).
• TauCeti.Yamabe.laplacian_bubble: Δ U_{t,b} = -(n (n - 2) / 4) U_{t,b} ^ (pₙ - 1).
• TauCeti.Yamabe.conformalCoefficient_mul_neg_laplacian_bubble: the bubble equation aₙ (-Δ U_{t,b}) = n (n - 1) U_{t,b} ^ (pₙ - 1).

References

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

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

The exponent pₙ = 2 n / (n - 2); for n > 2 it is the critical Sobolev exponent of H¹ in dimension n. At n = 2 it is 0 by the convention for division by zero.

theorem TauCeti.Yamabe.criticalExponent_def (n : ℕ) : criticalExponent n = 2 * ↑n / (↑n - 2)

Unfolding lemma for TauCeti.Yamabe.criticalExponent.

theorem TauCeti.Yamabe.criticalExponent_pos {n : ℕ} (hn : 2 < n) : 0 < criticalExponent n

The critical exponent is positive in every dimension n > 2.

theorem TauCeti.Yamabe.two_lt_criticalExponent {n : ℕ} (hn : 2 < n) : 2 < criticalExponent n

The critical exponent exceeds 2 in every dimension n > 2.

theorem TauCeti.Yamabe.two_div_criticalExponent (n : ℕ) : 2 / criticalExponent n = (↑n - 2) / ↑n

The exponent 2 / pₙ of the critical norm is (n - 2) / n; at n = 0 and n = 2 both sides vanish by the convention for division by zero.

theorem TauCeti.Yamabe.inv_ofReal_criticalExponent_add_inv_eq_inv {n : ℕ} (hn : 2 < n) : (ENNReal.ofReal (criticalExponent n))⁻¹ + (↑n)⁻¹ = 2⁻¹

The critical exponent, viewed in ℝ≥0∞, is Sobolev conjugate to 2.

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

The coefficient aₙ = 4 (n - 1) / (n - 2); for n > 2 it is the coefficient of the nonnegative Laplacian in the conformal Laplacian aₙ Δ⁺ + Scal in dimension n. At n = 2 it is 0 by the convention for division by zero.

theorem TauCeti.Yamabe.conformalCoefficient_def (n : ℕ) : conformalCoefficient n = 4 * (↑n - 1) / (↑n - 2)

Unfolding lemma for TauCeti.Yamabe.conformalCoefficient.

theorem TauCeti.Yamabe.conformalCoefficient_pos {n : ℕ} (hn : 2 < n) : 0 < conformalCoefficient n

The conformal coefficient is positive in every dimension n > 2.

noncomputable def TauCeti.Yamabe.bubble {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (t : ℝ) (b x : E) : ℝ

The bubble U_{t,b}(x) = (2 t / (t² + ‖x - b‖²)) ^ ((n - 2) / 2) of scale t centred at b, where n is the dimension of E.

theorem TauCeti.Yamabe.bubble_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (t : ℝ) (b x : E) : bubble t b x = (2 * t / (t ^ 2 + ‖x - b‖ ^ 2)) ^ ((↑(Module.finrank ℝ E) - 2) / 2)

Unfolding lemma for TauCeti.Yamabe.bubble.

theorem TauCeti.Yamabe.bubble_pos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (b x : E) : 0 < bubble t b x

A bubble of positive scale is positive.

theorem TauCeti.Yamabe.contDiff_bubble {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : t ≠ 0) (b : E) {m : WithTop ℕ∞} : ContDiff ℝ m (bubble t b)

A bubble of nonzero scale is smooth.

theorem TauCeti.Yamabe.bubble_zero_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (t : ℝ) (b x : E) : bubble t 0 (x - b) = bubble t b x

The bubble centred at b is the translate by b of the bubble centred at the origin.

theorem TauCeti.Yamabe.bubble_zero_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (x : E) : bubble t 0 (t • x) = t ^ (-((↑(Module.finrank ℝ E) - 2) / 2)) * bubble 1 0 x

The bubble of scale t centred at the origin is the rescaled standard bubble: U_{t,0}(t x) = t ^ (-(n - 2) / 2) U_{1,0}(x).

theorem TauCeti.Yamabe.bubble_sq_add_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (b x : E) : bubble t b (b + t • x) ^ 2 = t ^ (-(↑(Module.finrank ℝ E) - 2)) * bubble 1 0 x ^ 2

The square of a bubble under translation and dilation: U_{t,b}(b + t x)² = t ^ (-(n - 2)) U_{1,0}(x)².

theorem TauCeti.Yamabe.bubble_rpow_criticalExponent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (hn : Module.finrank ℝ E ≠ 2) {t : ℝ} (ht : 0 < t) (b x : E) : bubble t b x ^ criticalExponent (Module.finrank ℝ E) = (2 * t / (t ^ 2 + ‖x - b‖ ^ 2)) ^ Module.finrank ℝ E

In dimension n ≠ 2, the critical power of a bubble is U_{t,b} ^ pₙ = (2 t / (t² + ‖x - b‖²)) ^ n.

theorem TauCeti.Yamabe.bubble_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (hn : 2 ≤ Module.finrank ℝ E) {t : ℝ} (ht : 0 ≤ t) (b x : E) : bubble t b x ^ 2 = (2 * t / (t ^ 2 + ‖x - b‖ ^ 2)) ^ (Module.finrank ℝ E - 2)

In dimension n ≥ 2, the square of a bubble is a power of its profile: U_{t,b} ^ 2 = (2 t / (t² + ‖x - b‖²)) ^ (n - 2).

theorem TauCeti.Yamabe.bubble_rpow_criticalExponent_eq_mul_rpow_neg_one_add_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (hn : Module.finrank ℝ E ≠ 2) {t : ℝ} (ht : 0 < t) (b x : E) : bubble t b x ^ criticalExponent (Module.finrank ℝ E) = (2 / t) ^ Module.finrank ℝ E * (1 + ‖t⁻¹ • (x - b)‖ ^ 2) ^ (-↑(Module.finrank ℝ E))

In dimension n ≠ 2, the critical power of a bubble is a rescaled translate of a power of the Japanese bracket: U_{t,b}(x) ^ pₙ = (2 / t) ^ n (1 + ‖t⁻¹ (x - b)‖²) ^ (-n).

theorem TauCeti.Yamabe.bubble_rpow_four_div_finrank_sub_two {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (hn : Module.finrank ℝ E ≠ 2) {t : ℝ} (ht : 0 < t) (b x : E) : bubble t b x ^ (4 / (↑(Module.finrank ℝ E) - 2)) = (2 * t / (t ^ 2 + ‖x - b‖ ^ 2)) ^ 2

In dimension n ≠ 2, the Yamabe conformal factor of a bubble is U_{t,b} ^ (4 / (n - 2)) = (2 t / (t² + ‖x - b‖²)) ^ 2.

theorem TauCeti.Yamabe.hasFDerivAt_bubble {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (b x : E) : HasFDerivAt (bubble t b) ((InnerProductSpace.toDualMap ℝ E) (-((↑(Module.finrank ℝ E) - 2) / (t ^ 2 + ‖x - b‖ ^ 2) * bubble t b x) • (x - b))) x

The differential of a bubble: D U_{t,b}(x)[v] = -((n - 2) / (t² + ‖x - b‖²)) U_{t,b}(x) ⟪x - b, v⟫, where n = finrank ℝ E. The canonical map to the dual gives this formula without completeness; only its Riesz inverse, used to define the gradient, needs completeness.

theorem TauCeti.Yamabe.hasGradientAt_bubble {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {t : ℝ} (ht : 0 < t) (b x : E) : HasGradientAt (bubble t b) (-((↑(Module.finrank ℝ E) - 2) / (t ^ 2 + ‖x - b‖ ^ 2) * bubble t b x) • (x - b)) x

The gradient of a bubble: ∇U_{t,b}(x) = -((n - 2) / (t² + ‖x - b‖²)) U_{t,b}(x) (x - b), where n is the dimension of E.

theorem TauCeti.Yamabe.gradient_bubble {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {t : ℝ} (ht : 0 < t) (b x : E) : gradient (bubble t b) x = -((↑(Module.finrank ℝ E) - 2) / (t ^ 2 + ‖x - b‖ ^ 2) * bubble t b x) • (x - b)

The gradient of a bubble, as a value of gradient.

theorem TauCeti.Yamabe.norm_fderiv_bubble {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (b x : E) : ‖fderiv ℝ (bubble t b) x‖ = |↑(Module.finrank ℝ E) - 2| * bubble t b x * ‖x - b‖ / (t ^ 2 + ‖x - b‖ ^ 2)

The exact norm of the first differential, including the dimensions below two.

theorem TauCeti.Yamabe.norm_fderiv_bubble_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (b x : E) : ‖fderiv ℝ (bubble t b) x‖ ^ 2 = ((↑(Module.finrank ℝ E) - 2) / (2 * t)) ^ 2 * ‖x - b‖ ^ 2 * (2 * t / (t ^ 2 + ‖x - b‖ ^ 2)) ^ Module.finrank ℝ E

The squared norm of the differential of a bubble is the radial function ((n - 2) / (2 t)) ² ‖x - b‖² (2 t / (t² + ‖x - b‖²)) ^ n.

theorem TauCeti.Yamabe.laplacian_div_add_norm_sub_sq_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {t : ℝ} (ht : 0 < t) (k : ℝ) (b x : E) : Laplacian.laplacian (fun (y : E) => (2 * t / (t ^ 2 + ‖y - b‖ ^ 2)) ^ k) x = (2 * t) ^ k * (t ^ 2 + ‖x - b‖ ^ 2) ^ (-k - 2) * (4 * k * (k + 1) * ‖x - b‖ ^ 2 - 2 * ↑(Module.finrank ℝ E) * k * (t ^ 2 + ‖x - b‖ ^ 2))

The Laplacian of a real power of the bubble profile y ↦ 2 t / (t² + ‖y - b‖²), by the chain rule through the squared distance to b.

theorem TauCeti.Yamabe.laplacian_bubble {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {t : ℝ} (ht : 0 < t) (b x : E) : Laplacian.laplacian (bubble t b) x = -(↑(Module.finrank ℝ E) * (↑(Module.finrank ℝ E) - 2) / 4) * bubble t b x ^ (criticalExponent (Module.finrank ℝ E) - 1)

The Laplacian of a bubble: Δ U_{t,b} = -(n (n - 2) / 4) U_{t,b} ^ (pₙ - 1), where n is the dimension of E and pₙ = 2 n / (n - 2) is the exponent criticalExponent n. The identity holds in every dimension; at n = 2 both sides vanish.

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

The bubble equation: in dimension n ≠ 2, every bubble of positive scale solves the Yamabe equation of the unit round sphere, aₙ (-Δ U_{t,b}) = n (n - 1) U_{t,b} ^ (pₙ - 1).