English
The constant used in the main inequality is defined via a wrapping construction; this lemma states the definitional equality.
Русский
Задаваемая константа в главном неравенстве определяется через обёртывающую конструкцию; лемма устанавливает определение.
LaTeX
$$$lintegralPowLePowLIntegralFDerivConst_def := \\eta\\!\\text{-helper}(...)$$$
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 ≥ 2`, equipped
with Haar measure. Then the `Lᵖ` norm of `u`, where `p := n / (n - 1)`, is bounded above by
a constant times the `L¹` norm of the Fréchet derivative of `u`. -/
theorem eLpNorm_le_eLpNorm_fderiv_one {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u) {p : ℝ≥0}
(hp : NNReal.HolderConjugate (finrank ℝ E) p) :
eLpNorm u p μ ≤ eLpNormLESNormFDerivOneConst μ p * eLpNorm (fderiv ℝ u) 1 μ :=
by
have h0p : 0 < (p : ℝ) := hp.coe.symm.pos
rw [eLpNorm_one_eq_lintegral_enorm, ← ENNReal.rpow_le_rpow_iff h0p, ENNReal.mul_rpow_of_nonneg _ _ h0p.le, ←
ENNReal.coe_rpow_of_nonneg _ h0p.le, eLpNormLESNormFDerivOneConst, ← NNReal.rpow_mul,
eLpNorm_nnreal_pow_eq_lintegral hp.symm.pos.ne', inv_mul_cancel₀ h0p.ne', NNReal.rpow_one]
exact lintegral_pow_le_pow_lintegral_fderiv μ hu h2u hp.coe
