English
Similarly, the grid-lines construction preserves oddness: (Φ ↦ 𝓕Φ) preserves oddness equivalence with Φ.
Русский
Свойство нечетности сохраняется под преобразованием: нечетность Φ эквивалентна нечетности 𝓕Φ.
LaTeX
$$$((\\\\mathcal{F}\\\\Phi).\\\\Odd) \\iff (\\\\Phi).\\\\Odd$$$
Lean4
/-- The **Gagliardo-Nirenberg-Sobolev inequality**. Let `u` be a continuously differentiable
compactly-supported function `u` on `ℝⁿ`, for `n ≥ 2`. (More literally we encode `ℝⁿ` as
`ι → ℝ` where `n := #ι` is finite and at least 2.) Then the Lebesgue integral of the pointwise
expression `|u x| ^ (n / (n - 1))` is bounded above by the `n / (n - 1)`-th power of the Lebesgue
integral of the Fréchet derivative of `u`.
For a basis-free version, see `lintegral_pow_le_pow_lintegral_fderiv`. -/
theorem lintegral_pow_le_pow_lintegral_fderiv_aux [Fintype ι] {p : ℝ} (hp : Real.HolderConjugate (#ι) p)
{u : (ι → ℝ) → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u) :
∫⁻ x, ‖u x‖ₑ ^ p ≤ (∫⁻ x, ‖fderiv ℝ u x‖ₑ) ^ p := by
classical
/- For a function `f` in one variable and `t ∈ ℝ` we have
`|f(t)| = `|∫_{-∞}^t Df(s)∂s| ≤ ∫_ℝ |Df(s)| ∂s` where we use the fundamental theorem of calculus.
For each `x ∈ ℝⁿ` we let `u` vary in one of the `n` coordinates and apply the inequality above.
By taking the product over these `n` factors, raising them to the power `(n-1)⁻¹` and integrating,
we get the inequality `∫ |u| ^ (n/(n-1)) ≤ ∫ x, ∏ i, (∫ xᵢ, |Du(update x i xᵢ)|)^(n-1)⁻¹`.
The result then follows from the grid-lines lemma. -/
have : (1 : ℝ) ≤ ↑#ι - 1 := by
have hι : (2 : ℝ) ≤ #ι := by exact_mod_cast hp.lt
linarith
calc
∫⁻ x, ‖u x‖ₑ ^ p = ∫⁻ x, (‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ))) ^ (#ι : ℝ) := by
-- a little algebraic manipulation of the exponent
congr! 2 with x
rw [← ENNReal.rpow_mul, hp.conjugate_eq]
field_simp
_ = ∫⁻ x, ∏ _i : ι, ‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ)) := by
-- express the left-hand integrand as a product of identical factors
congr! 2 with x
simp_rw [prod_const]
norm_cast
_ ≤ ∫⁻ x, ∏ i, (∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ) ^ ((1 : ℝ) / (#ι - 1 : ℝ)) := ?_
_ ≤ (∫⁻ x, ‖fderiv ℝ u x‖ₑ) ^ p := by
-- apply the grid-lines lemma
apply lintegral_prod_lintegral_pow_le _ hp
fun_prop
-- we estimate |u x| using the fundamental theorem of calculus.
gcongr with x i
calc
‖u x‖ₑ
_ ≤ ∫⁻ xᵢ in Iic (x i), ‖deriv (u ∘ update x i) xᵢ‖ₑ :=
by
apply le_trans (by simp) (HasCompactSupport.enorm_le_lintegral_Ici_deriv _ _ _)
· exact hu.comp (by convert contDiff_update 1 x i)
· exact h2u.comp_isClosedEmbedding (isClosedEmbedding_update x i)
_ ≤ ∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ := ?_
gcongr with y
· exact Measure.restrict_le_self
calc
‖deriv (u ∘ update x i) y‖ₑ = ‖fderiv ℝ u (update x i y) (deriv (update x i) y)‖ₑ := by
rw [fderiv_comp_deriv _ (hu.differentiable le_rfl).differentiableAt (hasDerivAt_update x i y).differentiableAt]
_ ≤ ‖fderiv ℝ u (update x i y)‖ₑ * ‖deriv (update x i) y‖ₑ := (ContinuousLinearMap.le_opENorm _ _)
_ ≤ ‖fderiv ℝ u (update x i y)‖ₑ := by simp [deriv_update, Pi.enorm_single]
