Iterated derivative seminorms: linear changes of variables and the Euclidean Hessian

Composing a vector-valued function with a linear automorphism e multiplies the Lᵖ seminorm of its i-th derivative by at most ‖e‖ ^ i * |det e|^(-1 / p). The estimate compares a set with its preimage under e, works against any additive Haar measure on a finite-dimensional real normed space, and requires no differentiability of the function. Only the derivative of the composite must be a.e. strongly measurable on the preimage.

For a finite-dimensional real normed space it also records the consequence for second derivatives of a C² function on a thickening: the L² norm of D²u on a thickening of a bounded set is finite (MeasureTheory.Measure.eLpNorm_iteratedFDeriv_two_thickening_ne_top), and D²(u ∘ e) on the preimage thickening is controlled by D²u through the ellipticity constants of e (MeasureTheory.Measure.toReal_eLpNorm_iteratedFDeriv_two_comp_le).

On a finite-dimensional inner product space with an additive Haar measure, the Lᵖ norm of the Hessian of a function with continuous second derivative supported in a closed ball, with all second partial derivatives along an orthonormal basis bounded by B, is at most the 1/p-th power of the measure of the ball times (card ι)² B (MeasureTheory.Measure.toReal_eLpNorm_iteratedFDeriv_two_le_of_support_subset_closedBall).

theorem ContinuousLinearEquiv.eLpNorm_iteratedFDeriv_comp_right_restrict_preimage_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃L[ℝ] E) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E → F) {s : Set E} (i : ℕ) (p : ENNReal) (hm : MeasureTheory.AEStronglyMeasurable (iteratedFDeriv ℝ i (f ∘ ⇑e)) (μ.restrict (⇑e ⁻¹' s))) : MeasureTheory.eLpNorm (iteratedFDeriv ℝ i (f ∘ ⇑e)) p (μ.restrict (⇑e ⁻¹' s)) ≤ ENNReal.ofReal (‖↑e‖ ^ i) * (ENNReal.ofReal |(LinearMap.det ↑↑e)⁻¹| ^ (1 / p).toReal * MeasureTheory.eLpNorm (iteratedFDeriv ℝ i f) p (μ.restrict s))

Under a linear change of variables e, the Lᵖ seminorm of Dⁱ(f ∘ e) on e ⁻¹' s is at most ‖e‖ⁱ |det e|^(-1/p) times the Lᵖ seminorm of Dⁱf on s, against any additive Haar measure. The set need not be measurable, and no differentiability of f is required.

theorem MeasureTheory.Measure.eLpNorm_iteratedFDeriv_two_thickening_ne_top {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [IsFiniteMeasureOnCompacts μ] {U S : Set E} {u : E → ℝ} {R : ℝ} (hU : IsOpen U) (hu : ContDiffOn ℝ 2 u U) (hS : Bornology.IsBounded S) (hSU : Metric.cthickening R S ⊆ U) : eLpNorm (iteratedFDeriv ℝ 2 u) 2 (μ.restrict (Metric.thickening R S)) ≠ ⊤

The L² norm of D²u on the open R-thickening of a bounded set S is finite when u is C² on an open set containing the closed R-thickening.

theorem MeasureTheory.Measure.toReal_eLpNorm_iteratedFDeriv_two_comp_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] {e : E ≃L[ℝ] E} {lam Lam R : ℝ} {U S : Set E} {u : E → ℝ} (hlam : 0 < lam) (hLam : 0 < Lam) (he' : ∀ (ξ : E), ‖e ξ‖ ≤ √Lam * ‖ξ‖) (hesn : ‖↑e.symm‖ ≤ (√lam)⁻¹) (hU : IsOpen U) (hu : ContDiffOn ℝ 2 u U) (hS : Bornology.IsBounded S) (hSU : Metric.cthickening R S ⊆ U) : (eLpNorm (iteratedFDeriv ℝ 2 (u ∘ ⇑e)) 2 (μ.restrict (Metric.thickening (R / √Lam) (⇑e ⁻¹' S)))).toReal ≤ Lam * lam ^ (-(↑(Module.finrank ℝ E) / 4)) * (eLpNorm (iteratedFDeriv ℝ 2 u) 2 (μ.restrict (Metric.thickening R S))).toReal

The L² norm of D²(u ∘ e) on the R / √Λ-thickening of e ⁻¹' S is at most Λ λ^{-d/4} times the L² norm of D²u on the R-thickening of S, where d is the dimension of E.

theorem MeasureTheory.Measure.toReal_eLpNorm_iteratedFDeriv_two_le_of_support_subset_closedBall {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] [Fintype ι] [Nonempty ι] (b : OrthonormalBasis ι ℝ E) {w : E → ℝ} (hw : Continuous (iteratedFDeriv ℝ 2 w)) {x₀ : E} {R B : ℝ} {p : ENNReal} (hsupp : Function.support (iteratedFDeriv ℝ 2 w) ⊆ Metric.closedBall x₀ R) (hB : ∀ (x : E) (i j : ι), |((fderiv ℝ (fderiv ℝ w) x) (b i)) (b j)| ≤ B) : (eLpNorm (iteratedFDeriv ℝ 2 w) p μ).toReal ≤ (μ (Metric.closedBall 0 R)).toReal ^ p.toReal⁻¹ * (↑(Fintype.card ι) ^ 2 * B)

The Lᵖ norm of the second derivative of a function w with continuous second derivative on a finite-dimensional real inner product space with an additive Haar measure μ is at most μ (closedBall 0 R) ^ (1/p) * (card ι) ^ 2 * B, when the second derivative of w is supported in the closed ball closedBall x₀ R and all its second partial derivatives along an orthonormal basis b are bounded by B. Only the second derivative needs to be supported there, so w itself may be nonzero outside.