Dilations of a function on ℝ^d

Scaling x ↦ f (r • x) multiplies the Lᵖ seminorm by |r|^{-d/p} and each partial derivative by r, and it shrinks the support by |r|⁻¹. These are the three identities the sharpness of the Sobolev embedding turns on: the exponent p⋆ is the one at which the two factors cancel, so a dilated family keeps its L^{p⋆} norm while its L² norm tends to zero.

Main declarations

• EllipticPdes.Analysis.eLpNorm_comp_smul: the Lᵖ seminorm of a dilate.
• EllipticPdes.Analysis.partialD_comp_smul: the partial derivatives of a dilate.
• EllipticPdes.Analysis.tsupport_comp_smul_subset: the support of a dilate.

References

James Guo, Partial Differential Equations, Example IV.2.11.

theorem EllipticPdes.Analysis.eLpNorm_comp_smul {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : Measurable f) {r : ℝ} (hr : r ≠ 0) {p : ENNReal} (hp0 : p ≠ 0) (hpt : p ≠ ⊤) : MeasureTheory.eLpNorm (fun (x : EuclideanSpace ℝ (Fin d)) => f (r • x)) p MeasureTheory.volume = ENNReal.ofReal |(r ^ d)⁻¹| ^ (1 / p.toReal) * MeasureTheory.eLpNorm f p MeasureTheory.volume

Lᵖ seminorm of a dilate. Scaling the argument by r multiplies the seminorm by |r^d|^{-1/p}.

theorem EllipticPdes.Analysis.partialD_comp_smul {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : Differentiable ℝ f) (r : ℝ) (i : Fin d) : (Sobolev.partialD i fun (x : EuclideanSpace ℝ (Fin d)) => f (r • x)) = fun (x : EuclideanSpace ℝ (Fin d)) => r * Sobolev.partialD i f (r • x)

Partial derivatives of a dilate.

theorem EllipticPdes.Analysis.tsupport_comp_smul_subset {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} {r : ℝ} (hr : 0 < r) (hf : tsupport f ⊆ Metric.closedBall 0 1) : (tsupport fun (x : EuclideanSpace ℝ (Fin d)) => f (r • x)) ⊆ Metric.closedBall 0 r⁻¹

Support of a dilate. For 1 ≤ r, a function supported in the unit ball dilates to one supported in the ball of radius r⁻¹.