English
Defining the constant SNormFDerivConst in terms of a projection of a wrapped object, reflecting the way the Sobolev-type bound factors into the inequality.
Русский
Определяем константу SNormFDerivConst через проекцию обёрнутого объекта, чтобы отражать структуру границы Соболева внутри неравенства.
LaTeX
$$$$ SNormFDerivConst(F, μ, p) = \\operatorname{val\_proj}(\\text{wrapped✝}) . $$$$
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`.
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 finite-dimensional normed space.
-/
theorem eLpNorm_le_eLpNorm_fderiv [FiniteDimensional ℝ F] {u : E → F} {s : Set E} (hu : ContDiff ℝ 1 u)
(h2u : u.support ⊆ s) {p : ℝ≥0} (hp : 1 ≤ p) (h2p : p < finrank ℝ E) (hs : Bornology.IsBounded s) :
eLpNorm u p μ ≤ eLpNormLESNormFDerivOfLeConst F μ s p p * eLpNorm (fderiv ℝ u) p μ :=
by
refine eLpNorm_le_eLpNorm_fderiv_of_le μ hu h2u hp h2p ?_ hs
norm_cast
simp only [tsub_le_iff_right, le_add_iff_nonneg_right]
positivity
