English
Define the constant SNormLESNormFDerivOfEqConst and show that it decomposes as the product of the norm of the linear part e and the Sobolev-derived factor, matching the inner-derivative bound.
Русский
Задаётся константа SNormLESNormFDerivOfEqConst и демонстрируется её разложение на произведение нормы линейной части и фактора, полученного изSobolev-предусловий.
LaTeX
$$$$ \\text{SNormLESNormFDerivOfEqConst}(F,\\mu,p) = \\|e\\| \\cdot \\text{SobolevFactor}(F,\\mu,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`.
This is the version where the codomain of `u` is a finite-dimensional normed space.
-/
theorem eLpNorm_le_eLpNorm_fderiv_of_eq [FiniteDimensional ℝ F] {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' μ ≤ SNormLESNormFDerivOfEqConst F μ p * eLpNorm (fderiv ℝ u) p μ := by
/- Here we reduce the GNS-inequality with a Hilbert space as codomain to the case with a
finite-dimensional normed space as codomain, by transferring the result along the equivalence
`F ≃ ℝᵐ`. -/
let F' := EuclideanSpace ℝ <| Fin <| finrank ℝ F
let e : F ≃L[ℝ] F' := toEuclidean
let C₁ : ℝ≥0 := ‖(e.symm : F' →L[ℝ] F)‖₊
let C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ p
let C₂ : ℝ≥0 := ‖(e : F →L[ℝ] F')‖₊
let v := e ∘ u
have hv : ContDiff ℝ 1 v := e.contDiff.comp hu
have h2v : HasCompactSupport v := h2u.comp_left e.map_zero
have := eLpNorm_le_eLpNorm_fderiv_of_eq_inner μ hv h2v hp hn hp'
have h4v : ∀ x, ‖fderiv ℝ v x‖ ≤ C₂ * ‖fderiv ℝ u x‖ := fun x ↦
calc
‖fderiv ℝ v x‖ = ‖(fderiv ℝ e (u x)).comp (fderiv ℝ u x)‖ := by
rw [fderiv_comp x e.differentiableAt (hu.differentiable le_rfl x)]
_ ≤ ‖fderiv ℝ e (u x)‖ * ‖fderiv ℝ u x‖ := ((fderiv ℝ e (u x)).opNorm_comp_le (fderiv ℝ u x))
_ = C₂ * ‖fderiv ℝ u x‖ := by simp_rw [e.fderiv, C₂, coe_nnnorm]
calc
eLpNorm u p' μ = eLpNorm (e.symm ∘ v) p' μ := by simp_rw [v, Function.comp_def, e.symm_apply_apply]
_ ≤ C₁ • eLpNorm v p' μ := by
apply eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
exact Eventually.of_forall (fun x ↦ (e.symm : F' →L[ℝ] F).le_opNNNorm _)
_ = C₁ * eLpNorm v p' μ := rfl
_ ≤ C₁ * C * eLpNorm (fderiv ℝ v) p μ := by rw [mul_assoc]; gcongr
_ ≤ C₁ * C * (C₂ * eLpNorm (fderiv ℝ u) p μ) := by gcongr;
exact eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul (Eventually.of_forall h4v) p
_ = SNormLESNormFDerivOfEqConst F μ p * eLpNorm (fderiv ℝ u) p μ :=
by
simp_rw [C₂, C₁, C, e, SNormLESNormFDerivOfEqConst]
push_cast
simp_rw [mul_assoc]
