English
Let u: E → F' be a continuously differentiable function with compact support on a finite-dimensional real normed space E, where the codomain F' is a Hilbert space. For 1 ≤ p < n (n = dimℝ E) and p′ defined by 1/p′ = 1/p − 1/n, we have a bound of the Lp′-norm of u by a constant times the Lp-norm of its Frechet derivative: ||u||p′ ≤ C · ||fderiv u||p.
Русский
Пусть u: E → F' непрерывно дифференцируема с компактной опорой на конечномерном вещественном нормированном пространстве E, где F' являeтся гильбертовым пространством. Пусть 1 ≤ p < n (n = dimℝ E) и 1/p′ = 1/p − 1/n. Тогда существует константа C such that норма Lp′ элемента u управляется по неравенству: ||u||p′ ≤ C · ||fderiv u||p.
LaTeX
$$$$ \\|u\\|_{p'} \\le C_{F,\\mu,p} \\cdot \\|fderiv\\,u\\|_{p}.$$$$
Lean4
/-- The **Gagliardo-Nirenberg-Sobolev inequality**. Let `u` be a continuously differentiable
compactly-supported function `u` on a normed space `E` of finite dimension `n`, equipped
with Haar measure, let `1 ≤ p < n` and let `p'⁻¹ := p⁻¹ - n⁻¹`.
Then the `Lᵖ'` 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 Hilbert space.
-/
theorem eLpNorm_le_eLpNorm_fderiv_of_eq_inner {u : E → F'} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u)
{p p' : ℝ≥0} (hp : 1 ≤ p) (hn : 0 < finrank ℝ E) (hp' : (p' : ℝ)⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹) :
eLpNorm u p' μ ≤ eLpNormLESNormFDerivOfEqInnerConst μ p * eLpNorm (fderiv ℝ u) p μ := by
/- Here we derive the GNS-inequality for `p ≥ 1` from the version with `p = 1`.
For `p > 1` we apply the previous version to the function `|u|^γ` for a suitably chosen `γ`.
The proof requires that `x ↦ |x|^p` is smooth in the codomain, so we require that it is a
Hilbert space. -/
by_cases hp'0 : p' = 0
· simp [hp'0]
set n := finrank ℝ E
let n' := NNReal.conjExponent n
have h2p : (p : ℝ) < n :=
by
have : 0 < p⁻¹ - (n : ℝ)⁻¹ := NNReal.coe_lt_coe.mpr (pos_iff_ne_zero.mpr (inv_ne_zero hp'0)) |>.trans_eq hp'
rwa [NNReal.coe_inv, sub_pos, inv_lt_inv₀ _ (zero_lt_one.trans_le (NNReal.coe_le_coe.mpr hp))] at this
exact_mod_cast hn
have h0n : 2 ≤ n := Nat.succ_le_of_lt <| Nat.one_lt_cast.mp <| hp.trans_lt h2p
have hn : NNReal.HolderConjugate n n' := .conjExponent (by norm_cast)
have h1n : 1 ≤ (n : ℝ≥0) := hn.lt.le
have h2n : (0 : ℝ) < n - 1 := by simp_rw [sub_pos]; exact hn.coe.lt
have hnp : (0 : ℝ) < n - p := by simp_rw [sub_pos]; exact h2p
rcases hp.eq_or_lt with rfl | hp
· convert eLpNorm_le_eLpNorm_fderiv_one μ hu h2u hn using 2
· suffices (p' : ℝ) = n' by simpa using this
rw [← inv_inj, hp']
simp [field, n', NNReal.conjExponent, *]
· norm_cast
simp_rw [n', n, eLpNormLESNormFDerivOfEqInnerConst]
simp only [n, NNReal.coe_one] at hnp
field_simp
simp
-- the case `p > 1`
let q := Real.conjExponent p
have hq : Real.HolderConjugate p q := .conjExponent hp
have h0p : p ≠ 0 := zero_lt_one.trans hp |>.ne'
have h1p : (p : ℝ) ≠ 1 := hq.lt.ne'
have h3p : (p : ℝ) - 1 ≠ 0 := sub_ne_zero_of_ne h1p
have h2q : 1 / n' - 1 / q = 1 / p' := by
simp_rw -zeta [one_div, hp']
rw [← hq.one_sub_inv, ← hn.coe.one_sub_inv, sub_sub_sub_cancel_left]
simp only [NNReal.coe_natCast, NNReal.coe_inv]
let γ : ℝ≥0 := ⟨p * (n - 1) / (n - p), by positivity⟩
have h0γ : (γ : ℝ) = p * (n - 1) / (n - p) := rfl
have h1γ : 1 < (γ : ℝ) :=
by
rwa [h0γ, one_lt_div hnp, mul_sub, mul_one, sub_lt_sub_iff_right, lt_mul_iff_one_lt_left]
exact hn.coe.pos
have h2γ : γ * n' = p' :=
by
rw [← NNReal.coe_inj, ← inv_inj, hp', NNReal.coe_mul, h0γ, hn.coe.conjugate_eq]
simp [field]
have h3γ : (γ - 1) * q = p' := by
rw [← inv_inj, hp', h0γ, hq.conjugate_eq]
have : (p : ℝ) * (n - 1) - (n - p) = n * (p - 1) := by ring
simp [field, this]
have h4γ : (γ : ℝ) ≠ 0 := (zero_lt_one.trans h1γ).ne'
by_cases h3u : ∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ = 0
· rw [eLpNorm_nnreal_eq_lintegral hp'0, h3u, ENNReal.zero_rpow_of_pos] <;> positivity
have h4u : ∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ ≠ ∞ :=
by
refine lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top ((NNReal.coe_pos.trans pos_iff_ne_zero).mpr hp'0) ?_ |>.ne
rw [← eLpNorm_nnreal_eq_eLpNorm' hp'0]
exact hu.continuous.memLp_of_hasCompactSupport (μ := μ) h2u |>.eLpNorm_lt_top
have h5u : (∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ) ^ (1 / q) ≠ 0 := ENNReal.rpow_pos (pos_iff_ne_zero.mpr h3u) h4u |>.ne'
have h6u : (∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ) ^ (1 / q) ≠ ∞ := by finiteness
have h7u := hu.continuous
let v : E → ℝ := fun x ↦ ‖u x‖ ^ (γ : ℝ)
have hv : ContDiff ℝ 1 v := hu.norm_rpow h1γ
have h2v : HasCompactSupport v := h2u.norm.rpow_const h4γ
set C := eLpNormLESNormFDerivOneConst μ n'
have :=
calc
(∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ) ^ (1 / (n' : ℝ)) = eLpNorm v n' μ :=
by
rw [← h2γ, eLpNorm_nnreal_eq_lintegral hn.symm.pos.ne']
simp (discharger := positivity) [v, Real.enorm_rpow_of_nonneg, ENNReal.rpow_mul]
_ ≤ C * eLpNorm (fderiv ℝ v) 1 μ := (eLpNorm_le_eLpNorm_fderiv_one μ hv h2v hn)
_ = C * ∫⁻ x, ‖fderiv ℝ v x‖ₑ ∂μ := by rw [eLpNorm_one_eq_lintegral_enorm]
_ ≤ C * γ * ∫⁻ x, ‖u x‖ₑ ^ ((γ : ℝ) - 1) * ‖fderiv ℝ u x‖ₑ ∂μ :=
by
rw [mul_assoc, ← lintegral_const_mul γ]
gcongr
simp_rw [← mul_assoc]
exact enorm_fderiv_norm_rpow_le (hu.differentiable le_rfl) h1γ
dsimp [enorm]
fun_prop
_ ≤ C * γ * ((∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ) ^ (1 / q) * (∫⁻ x, ‖fderiv ℝ u x‖ₑ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ))) :=
by
gcongr
convert ENNReal.lintegral_mul_le_Lp_mul_Lq μ (.symm <| .conjExponent <| show 1 < (p : ℝ) from hp) ?_ ?_ using 5
· simp [γ, n, q, ← ENNReal.rpow_mul, ← h3γ]
· borelize F'
fun_prop
· fun_prop
_ = C * γ * (∫⁻ x, ‖fderiv ℝ u x‖ₑ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ)) * (∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ) ^ (1 / q) := by
ring
calc
eLpNorm u p' μ = (∫⁻ x, ‖u x‖ₑ ^ (p' : ℝ) ∂μ) ^ (1 / (p' : ℝ)) := eLpNorm_nnreal_eq_lintegral hp'0
_ ≤ C * γ * (∫⁻ x, ‖fderiv ℝ u x‖ₑ ^ (p : ℝ) ∂μ) ^ (1 / (p : ℝ)) := by
rwa [← h2q, ENNReal.rpow_sub _ _ h3u h4u, ENNReal.div_le_iff h5u h6u]
_ = eLpNormLESNormFDerivOfEqInnerConst μ p * eLpNorm (fderiv ℝ u) (↑p) μ :=
by
suffices (C : ℝ) * γ = eLpNormLESNormFDerivOfEqInnerConst μ p
by
rw [eLpNorm_nnreal_eq_lintegral h0p]
congr
norm_cast at this ⊢
simp_rw [eLpNormLESNormFDerivOfEqInnerConst, γ]
refold_let n n' C
rw [NNReal.coe_mul, NNReal.coe_mk, Real.coe_toNNReal', mul_eq_mul_left_iff, eq_comm, max_eq_left_iff]
left
positivity
