English
Let F be finite-dimensional, E a real finite-dimensional normed space, and u: E → F a ContDiff function with compact support. For u, there holds eLpNorm u p′ ≤ SNormLESNormFDerivOfLeConst(F, μ, s, p, q) · eLpNorm (fderiv u) p, under appropriate p, p′ and q relations.
Русский
Пусть F фиксировано размерности m, E — реальное конечномерное нормированное пространство, и u: E → F непрерывно дифференцируемая с компактной опорой. Тогда соблюдается неравенство eLpNorm с параметрами p′ и p с константой SNormFDerivOfLeConst.
LaTeX
$$$$ \\|u\\|_{p'} \\le SNormLESNormFDerivOfEqConst(F,\\mu,p) \\cdot \\|fderiv u\\|_{p}. $$$$
Lean4
/-- The **Gagliardo-Nirenberg-Sobolev inequality**. Let `u` be a continuously differentiable
function `u` supported in a bounded set `s` in a normed space `E` of finite dimension
`n`, equipped with Haar measure, and let `1 < p < n` and `0 < q ≤ (p⁻¹ - (finrank ℝ E : ℝ)⁻¹)⁻¹`.
Then the `L^q` norm of `u` is bounded above by a constant times the `Lᵖ` norm of
the Fréchet derivative of `u`.
Note: The codomain of `u` needs to be a finite-dimensional normed space.
-/
theorem eLpNorm_le_eLpNorm_fderiv_of_le [FiniteDimensional ℝ F] {u : E → F} {s : Set E} (hu : ContDiff ℝ 1 u)
(h2u : u.support ⊆ s) {p q : ℝ≥0} (hp : 1 ≤ p) (h2p : p < finrank ℝ E) (hpq : p⁻¹ - (finrank ℝ E : ℝ)⁻¹ ≤ (q : ℝ)⁻¹)
(hs : Bornology.IsBounded s) : eLpNorm u q μ ≤ eLpNormLESNormFDerivOfLeConst F μ s p q * eLpNorm (fderiv ℝ u) p μ :=
by
by_cases hq0 : q = 0
· simp [hq0]
let p' : ℝ≥0 := (p⁻¹ - (finrank ℝ E : ℝ≥0)⁻¹)⁻¹
have hp' : p'⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹ :=
by
rw [inv_inv, NNReal.coe_sub]
· simp
· gcongr
have : (q : ℝ≥0∞) ≤ p' := by
have H : (p' : ℝ)⁻¹ ≤ (↑q)⁻¹ := trans hp' hpq
norm_cast at H ⊢
rwa [inv_le_inv₀] at H
· dsimp
have : 0 < p⁻¹ - (finrank ℝ E : ℝ≥0)⁻¹ := by
simp only [tsub_pos_iff_lt]
gcongr
positivity
· positivity
set t := (μ s).toNNReal ^ (1 / q - 1 / p' : ℝ)
let C := SNormLESNormFDerivOfEqConst F μ p
calc
eLpNorm u q μ = eLpNorm u q (μ.restrict s) := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
_ ≤ eLpNorm u p' (μ.restrict s) * t :=
by
convert eLpNorm_le_eLpNorm_mul_rpow_measure_univ this hu.continuous.aestronglyMeasurable
rw [ENNReal.coe_rpow_of_nonneg]
· simp [ENNReal.coe_toNNReal hs.measure_lt_top.ne]
· rw [one_div, one_div]
norm_cast
rw [hp']
simpa using hpq
_ = eLpNorm u p' μ * t := by rw [eLpNorm_restrict_eq_of_support_subset h2u]
_ ≤ (C * eLpNorm (fderiv ℝ u) p μ) * t :=
by
have h2u' : HasCompactSupport u :=
by
apply HasCompactSupport.of_support_subset_isCompact hs.isCompact_closure
exact h2u.trans subset_closure
rel [eLpNorm_le_eLpNorm_fderiv_of_eq μ hu h2u' hp (mod_cast (zero_le p).trans_lt h2p) hp']
_ = eLpNormLESNormFDerivOfLeConst F μ s p q * eLpNorm (fderiv ℝ u) p μ := by
simp_rw [eLpNormLESNormFDerivOfLeConst, ENNReal.coe_mul]; ring
