Duality arguments for L^p spaces #
This auxiliary file collects statements describing how duality interacts
with L^p spaces. The full proofs are deferred, but the theorem
signatures are provided so that other files (notably the Minkowski
integral inequality) can depend on them while development is in
progress.
theorem
Newton.lp_duality_pairing
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
(p q : ENNReal)
(_hp : 1 < p)
(_hq : 1 < q)
(hpq : IsConjugateExponent p q)
{f g : α → ℝ}
(hf : MeasureTheory.MemLp f p μ)
(hg : MeasureTheory.MemLp g q μ)
:
Hölder's inequality expressed as a dual pairing between L^p and L^q.
theorem
Newton.normalized_eLpNorm_toReal_eq_one
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
(p : ENNReal)
{f : α → ℝ}
(hf_ne_zero : (MeasureTheory.eLpNorm f p μ).toReal ≠ 0)
:
(MeasureTheory.eLpNorm (fun (x : α) => 1 / (MeasureTheory.eLpNorm f p μ).toReal * f x) p μ).toReal = 1
Scaling f by the reciprocal of its L^p norm yields a unit eLpNorm.
theorem
Newton.dual_candidate_memLp
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
(p q : ENNReal)
(hp : 1 < p)
(hq : 1 < q)
(hpq : IsConjugateExponent p q)
{f : α → ℝ}
(hf : MeasureTheory.MemLp f p μ)
:
The standard Hölder extremiser associated to f lies in L^q.
theorem
Newton.dual_candidate_pairing_eq
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
(p q : ENNReal)
(hp : 1 < p)
(hq : 1 < q)
(hpq : IsConjugateExponent p q)
{f : α → ℝ}
(hf : MeasureTheory.MemLp f p μ)
(hf_norm : (MeasureTheory.eLpNorm f p μ).toReal = 1)
:
The Hölder extremiser realises the dual pairing for a unit L^p function.
theorem
Newton.exists_dual_pair_for_unit
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
(p q : ENNReal)
(hp : 1 < p)
(hq : 1 < q)
(hpq : IsConjugateExponent p q)
{f : α → ℝ}
(hf : MeasureTheory.MemLp f p μ)
(hf_norm : (MeasureTheory.eLpNorm f p μ).toReal = 1)
:
∃ (g : α → ℝ),
MeasureTheory.MemLp g q μ ∧ (MeasureTheory.eLpNorm g q μ).toReal = 1 ∧ MeasureTheory.Integrable (fun (x : α) => f x * g x) μ ∧ ∫ (x : α), f x * g x ∂μ = (MeasureTheory.eLpNorm f p μ).toReal * (MeasureTheory.eLpNorm g q μ).toReal
For a unit L^p element, produce a dual element saturating Hölder's inequality.
theorem
Newton.integral_scaling_of_normalization
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{f g : α → ℝ}
{c : ℝ}
(hc_ne_zero : c ≠ 0)
(h_int : MeasureTheory.Integrable (fun (x : α) => f x * g x) μ)
:
Pulling out a scalar when comparing f and its normalisation.
theorem
Newton.lp_duality_exists_norm_one_attainer
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
(p q : ENNReal)
(hp : 1 < p)
(hq : 1 < q)
(hpq : IsConjugateExponent p q)
{f : α → ℝ}
(hf : MeasureTheory.MemLp f p μ)
(hf_ne_zero : (MeasureTheory.eLpNorm f p μ).toReal ≠ 0)
:
∃ (g : α → ℝ),
MeasureTheory.MemLp g q μ ∧ (MeasureTheory.eLpNorm g q μ).toReal = 1 ∧ MeasureTheory.Integrable (fun (x : α) => f x * g x) μ ∧ ∫ (x : α), f x * g x ∂μ = (MeasureTheory.eLpNorm f p μ).toReal
Produce a dual element with unit L^q norm attaining the L^p norm of f.
theorem
Newton.lp_duality_norm_le_of_pairing_bound
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
(p q : ENNReal)
(hp : 1 < p)
(hq : 1 < q)
(hpq : IsConjugateExponent p q)
{f : α → ℝ}
(hf : MeasureTheory.MemLp f p μ)
{B : ℝ}
(hB :
∀ (g : α → ℝ),
MeasureTheory.MemLp g q μ →
(MeasureTheory.eLpNorm g q μ).toReal ≤ 1 →
MeasureTheory.Integrable (fun (x : α) => f x * g x) μ → |∫ (x : α), f x * g x ∂μ| ≤ B)
:
Control the L^p norm of f by bounding pairings against the unit ball of L^q.
theorem
Newton.eLpNorm_norm_integral_lt_top
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{β : Type u_2}
[MeasurableSpace β]
{ν : MeasureTheory.Measure β}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasureTheory.SFinite μ]
[MeasureTheory.SFinite ν]
(p : ENNReal)
(hp : 1 < p)
(hp_ne_top : p ≠ ⊤)
{F : α → β → E}
(hF_meas : MeasureTheory.AEStronglyMeasurable (Function.uncurry F) (μ.prod ν))
(hF_prod : MeasureTheory.Integrable (Function.uncurry F) (μ.prod ν))
(hF_memLp : ∀ᵐ (y : β) ∂ν, MeasureTheory.MemLp (fun (x : α) => F x y) p μ)
(hF_norm : MeasureTheory.Integrable (fun (y : β) => (MeasureTheory.eLpNorm (fun (x : α) => F x y) p μ).toReal) ν)
:
theorem
Newton.memLp_norm_integral
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{β : Type u_4}
[MeasurableSpace β]
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite μ]
[MeasureTheory.SFinite ν]
(p : ENNReal)
(hp : 1 ≤ p)
(hp_ne_top : p ≠ ⊤)
{F : α → β → E}
(hF_meas : MeasureTheory.AEStronglyMeasurable (Function.uncurry F) (μ.prod ν))
(hF_prod : MeasureTheory.Integrable (Function.uncurry F) (μ.prod ν))
(hF_memLp : ∀ᵐ (y : β) ∂ν, MeasureTheory.MemLp (fun (x : α) => F x y) p μ)
(hF_norm : MeasureTheory.Integrable (fun (y : β) => (MeasureTheory.eLpNorm (fun (x : α) => F x y) p μ).toReal) ν)
: