English
The constant multiplying the right-hand side in the eLp norm inequality depends only on E, μ and p.
Русский
Константа, выходящая в неравенстве eLpNorm, зависит только от пространства E, меры μ и p.
LaTeX
$$$eLpNormLESNormFDerivOneConst := \\text{constant depending on } E, μ, 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 ≥ 2`, equipped
with Haar measure. Then the Lebesgue integral of the pointwise expression
`|u x| ^ (n / (n - 1))` is bounded above by a constant times the `n / (n - 1)`-th power of the
Lebesgue integral of the Fréchet derivative of `u`. -/
theorem lintegral_pow_le_pow_lintegral_fderiv {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u) {p : ℝ}
(hp : Real.HolderConjugate (finrank ℝ E) p) :
∫⁻ x, ‖u x‖ₑ ^ p ∂μ ≤ lintegralPowLePowLIntegralFDerivConst μ p * (∫⁻ x, ‖fderiv ℝ u x‖ₑ ∂μ) ^ p := by
/- We reduce to the case where `E` is `ℝⁿ`, for which we have already proved the result using
an explicit basis in `MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux`.
This proof is not too hard, but takes quite some steps, reasoning about the equivalence
`e : E ≃ ℝⁿ`, relating the measures on each sides of the equivalence,
and estimating the derivative using the chain rule. -/
set C := lintegralPowLePowLIntegralFDerivConst μ p
let ι := Fin (finrank ℝ E)
have hιcard : #ι = finrank ℝ E := Fintype.card_fin (finrank ℝ E)
have : finrank ℝ E = finrank ℝ (ι → ℝ) := by simp [hιcard]
let e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
have hp : Real.HolderConjugate (#ι) p := by rwa [hιcard]
have h0p : 0 ≤ p := hp.symm.nonneg
let c := addHaarScalarFactor μ ((volume : Measure (ι → ℝ)).map e.symm)
have hc : 0 < c := addHaarScalarFactor_pos_of_isAddHaarMeasure ..
have h2c : μ = c • ((volume : Measure (ι → ℝ)).map e.symm) := isAddLeftInvariant_eq_smul ..
have h3c : (c : ℝ≥0∞) ≠ 0 := by simp_rw [ne_eq, ENNReal.coe_eq_zero, hc.ne', not_false_eq_true]
have h0C : C = (c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p) * (c ^ p)⁻¹ := by
simp_rw [c, ι, C, e, lintegralPowLePowLIntegralFDerivConst]
have hC : C * c ^ p = c * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p := by
rw [h0C, inv_mul_cancel_right₀ (NNReal.rpow_pos hc).ne']
simp only [h2c, ENNReal.smul_def, lintegral_smul_measure, smul_eq_mul]
let v : (ι → ℝ) → F := u ∘ e.symm
have hv : ContDiff ℝ 1 v := hu.comp e.symm.contDiff
have h2v : HasCompactSupport v := h2u.comp_homeomorph e.symm.toHomeomorph
have :=
calc
∫⁻ x, ‖u x‖ₑ ^ p ∂(volume : Measure (ι → ℝ)).map e.symm = ∫⁻ y, ‖v y‖ₑ ^ p :=
by
refine lintegral_map ?_ e.symm.continuous.measurable
borelize F
exact hu.continuous.measurable.nnnorm.coe_nnreal_ennreal.pow_const _
_ ≤ (∫⁻ y, ‖fderiv ℝ v y‖ₑ) ^ p := (lintegral_pow_le_pow_lintegral_fderiv_aux hp hv h2v)
_ = (∫⁻ y, ‖(fderiv ℝ u (e.symm y)).comp (fderiv ℝ e.symm y)‖ₑ) ^ p :=
by
congr! with y
apply fderiv_comp _ (hu.differentiable le_rfl _)
exact e.symm.differentiableAt
_ ≤ (∫⁻ y, ‖fderiv ℝ u (e.symm y)‖ₑ * ‖(e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ) ^ p :=
by
gcongr with y
rw [e.symm.fderiv]
apply ContinuousLinearMap.opENorm_comp_le
_ = (‖(e.symm : (ι → ℝ) →L[ℝ] E)‖ₑ * ∫⁻ y, ‖fderiv ℝ u (e.symm y)‖ₑ) ^ p :=
by
rw [lintegral_mul_const, mul_comm]
fun_prop
_ = (‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p : ℝ≥0) * (∫⁻ y, ‖fderiv ℝ u (e.symm y)‖ₑ) ^ p := by
rw [ENNReal.mul_rpow_of_nonneg _ _ h0p, enorm_eq_nnnorm, ← ENNReal.coe_rpow_of_nonneg _ h0p]
_ =
(‖(e.symm : (ι → ℝ) →L[ℝ] E)‖₊ ^ p : ℝ≥0) *
(∫⁻ x, ‖fderiv ℝ u x‖ₑ ∂(volume : Measure (ι → ℝ)).map e.symm) ^ p :=
by
congr
rw [lintegral_map _ e.symm.continuous.measurable]
fun_prop
rw [← ENNReal.mul_le_mul_left h3c ENNReal.coe_ne_top, ← mul_assoc, ← ENNReal.coe_mul, ← hC, ENNReal.coe_mul] at this
rw [ENNReal.mul_rpow_of_nonneg _ _ h0p, ← mul_assoc, ← ENNReal.coe_rpow_of_ne_zero hc.ne']
exact this
