Dilation scaling of the Lᵖ seminorm #
Dilating the variable of a function on a finite-dimensional real normed space E by r⁻¹, for
r > 0, multiplies its Lᵖ seminorm against an additive Haar measure by r ^ (n / p), where
n is the dimension of E. 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, so at those two exponents
the factor is 1. This is the eLpNorm counterpart of the lower Lebesgue integral law
TauCeti.lintegral_comp_inv_smul.
Main declarations #
TauCeti.eLpNorm_comp_inv_smul:‖u (r⁻¹ • ·)‖_p = r ^ (n / p) * ‖u‖_p.
theorem
TauCeti.eLpNorm_comp_inv_smul
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[FiniteDimensional ℝ E]
(μ : MeasureTheory.Measure E)
[μ.IsAddHaarMeasure]
{G : Type u_2}
[TopologicalSpace G]
[ContinuousENorm G]
(u : E → G)
{r : ℝ}
(hr : 0 < r)
(p : ENNReal)
:
MeasureTheory.eLpNorm (fun (x : E) => u (r⁻¹ • x)) p μ = ENNReal.ofReal (r ^ (↑(Module.finrank ℝ E) / p.toReal)) * MeasureTheory.eLpNorm u p μ
Dilation scaling of the Lᵖ seminorm: ‖u (r⁻¹ • ·)‖_p = r ^ (n / p) * ‖u‖_p, where
n is the dimension of the ambient space. The exponent n / p is n / p.toReal, which is 0 at
p = 0 and p = ∞, where the factor is thus 1.