Dilation scaling of the Sobolev seminorms

Fix a finite-dimensional real normed space E of dimension n carrying an additive Haar measure μ, and dilate the variable of a function by r > 0, i.e. replace u by x ↦ u (r⁻¹ • x). This file records how that operation rescales the Lᵖ seminorm of the derivative, the second of the two quantities a first-order Sobolev estimate compares; the first, the Lᵖ seminorm of the function itself, is TauCeti.eLpNorm_comp_inv_smul.

For every exponent p the two scaling laws are

‖u (r⁻¹ • ·)‖_p = r ^ (n / p) * ‖u‖_p and ‖D(u (r⁻¹ • ·))‖_p = r ^ (n / p - 1) * ‖Du‖_p,

the extra r⁻¹ in the second coming from the chain rule, in the shape of Mathlib's fderiv_comp_smul. Here n / p stands for n / p.toReal, which is 0 at p = 0 and p = ∞ by Lean's conventions ENNReal.toReal ∞ = 0 and x / 0 = 0; at those two exponents the factors are therefore 1 and r⁻¹. The mismatch of the two exponents is the scaling obstruction behind TauCeti.not_exists_eLpNorm_le_const_mul_eLpNorm_fderiv: a Poincaré-type inequality cannot hold with one constant for all compactly supported functions on the whole space.

Main declarations

• TauCeti.eLpNorm_fderiv_comp_inv_smul: ‖D(u (r⁻¹ • ·))‖_p = r ^ (n / p - 1) * ‖Du‖_p.

theorem TauCeti.eLpNorm_fderiv_comp_inv_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (u : E → F) {r : ℝ} (hr : 0 < r) (p : ENNReal) : MeasureTheory.eLpNorm (fderiv ℝ fun (y : E) => u (r⁻¹ • y)) p μ = ENNReal.ofReal (r ^ (↑(Module.finrank ℝ E) / p.toReal - 1)) * MeasureTheory.eLpNorm (fderiv ℝ u) p μ

Dilation scaling of the Lᵖ seminorm of the derivative: ‖D(u (r⁻¹ • ·))‖_p = r ^ (n / p - 1) * ‖Du‖_p. The exponent drops by one relative to TauCeti.eLpNorm_comp_inv_smul because the chain rule contributes a factor r⁻¹. The exponent n / p is n / p.toReal, which is 0 at p = 0 and p = ∞, where the factor is thus r⁻¹.