Gagliardo-Nirenberg-Sobolev inequality #
In this file we prove the Gagliardo-Nirenberg-Sobolev inequality.
This states that for compactly supported C¹-functions between finite dimensional vector spaces,
we can bound the L^p-norm of u by the L^q norm of the derivative of u.
The bound is up to a constant that is independent of the function u.
Let n be the dimension of the domain.
The main step in the proof, which we dubbed the "grid-lines lemma" below, is a complicated
inductive argument that involves manipulating an n+1-fold iterated integral and a product of
n+2 factors. In each step, one pushes one of the integral inside (all but one of)
the factors of the product using Hölder's inequality. The precise formulation of the induction
hypothesis (MeasureTheory.GridLines.T_insert_le_T_lmarginal_singleton) is tricky,
and none of the 5 sources we referenced stated it.
In the formalization we use the operation MeasureTheory.lmarginal to work with the iterated
integrals, and use MeasureTheory.lmarginal_insert' to conveniently push one of the integrals
inside. The Hölder's inequality step is done using ENNReal.lintegral_mul_prod_norm_pow_le.
The conclusions of the main results below are an estimation up to a constant multiple.
We don't really care about this constant, other than that it only depends on some pieces of data,
typically E, μ, p and sometimes also the codomain of u or the support of u.
We state these constants as separate definitions.
Main results #
MeasureTheory.snorm_le_snorm_fderiv_of_eq: The bound holds for1 ≤ p,0 < nandq⁻¹ = p⁻¹ - n⁻¹MeasureTheory.snorm_le_snorm_fderiv_of_le: The bound holds when1 ≤ p < n,0 ≤ qandp⁻¹ - n⁻¹ ≤ q⁻¹. Note that in this case the constant depends on the support ofu.
Potentially also useful:
MeasureTheory.snorm_le_snorm_fderiv_one: this is the inequality forq = 1. In this version, the codomain can be an arbitrary Banach space.MeasureTheory.snorm_le_snorm_fderiv_of_eq_inner: in this version the codomain is assumed to be a Hilbert space, without restrictions on its dimension.
The grid-lines lemma #
The "grid-lines operation" (not a standard name) which is central in the inductive proof of the Sobolev inequality.
For a finite dependent product Π i : ι, A i of sigma-finite measure spaces, a finite set s of
indices from ι, and a (later assumed nonnegative) real number p, this operation acts on a
function f from Π i, A i into the extended nonnegative reals. The operation is to partially
integrate, in the s co-ordinates, the function whose value at x : Π i, A i is obtained by
multiplying a certain power of f with the product, for each co-ordinate i in s, of a certain
power of the integral of f along the "grid line" in the i direction through x.
We are most interested in this operation when the set s is the universe in ι, but as a proxy for
"induction on dimension" we define it for a general set s of co-ordinates: the s-grid-lines
operation on a function f which is constant along the co-ordinates in sᶜ is morally (that is, up
to type-theoretic nonsense) the same thing as the universe-grid-lines operation on the associated
function on the "lower-dimensional" space Π i : s, A i.
Equations
Instances For
The main inductive step in the grid-lines lemma for the Gagliardo-Nirenberg-Sobolev inequality.
The grid-lines operation GridLines.T on a nonnegative function on a finitary product type is
less than or equal to the grid-lines operation of its partial integral in one co-ordinate
(the latter intuitively considered as a function on a space "one dimension down").
Auxiliary result for the grid-lines lemma. Given a nonnegative function on a finitary product
type indexed by ι, and a set s in ι, consider partially integrating over the variables in
sᶜ and performing the "grid-lines operation" (see GridLines.T) to the resulting function in the
variables s. This theorem states that this operation decreases as the number of grid-lines taken
increases.
The "grid-lines lemma" (not a standard name), stated with a general parameter p as the
exponent. Compare with lintegral_prod_lintegral_pow_le.
For any finite dependent product Π i : ι, A i of sigma-finite measure spaces, for any
nonnegative real number p such that (#ι - 1) * p ≤ 1, for any function f from Π i, A i into
the extended nonnegative reals, we consider an associated "grid-lines quantity", the integral of an
associated function from Π i, A i into the extended nonnegative reals. The value of this function
at x : Π i, A i is obtained by multiplying a certain power of f with the product, for each
co-ordinate i, of a certain power of the integral of f along the "grid line" in the i
direction through x.
This lemma bounds the Lebesgue integral of the grid-lines quantity by a power of the Lebesgue
integral of f.
Special case of the grid-lines lemma lintegral_mul_prod_lintegral_pow_le, taking the extremal
exponent p = (#ι - 1)⁻¹.
The Gagliardo-Nirenberg-Sobolev inequality #
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.
The constant factor occurring in the conclusion of lintegral_pow_le_pow_lintegral_fderiv.
It only depends on E, μ and p.
It is determined by the ratio of the measures on E and ℝⁿ and
the operator norm of a chosen equivalence E ≃ ℝⁿ (raised to suitable powers involving p).
Instances For
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.
The constant factor occurring in the conclusion of snorm_le_snorm_fderiv_one.
It only depends on E, μ and p.
Instances For
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.
The constant factor occurring in the conclusion of snorm_le_snorm_fderiv_of_eq_inner.
It only depends on E, μ and p.
Equations
- MeasureTheory.snormLESNormFDerivOfEqInnerConst μ p = let n := FiniteDimensional.finrank ℝ E; MeasureTheory.snormLESNormFDerivOneConst μ ↑(↑n).conjExponent * (p * (↑n - 1) / (↑n - p)).toNNReal
Instances For
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.
Note: The codomain of u needs to be a Hilbert space.
The constant factor occurring in the conclusion of snorm_le_snorm_fderiv_of_eq.
It only depends on E, F, μ and p.
Instances For
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.
The constant factor occurring in the conclusion of snorm_le_snorm_fderiv_of_le.
It only depends on F, μ, s, p and q.
Instances For
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 and 0 < q ≤ (p⁻¹ - (finrank ℝ E : ℝ)⁻¹)⁻¹.
Then the L^q 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.
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.