Minkowski's integral inequality #
In this file, we prove Minkowski's integral inequality and apply it to truncations. We use this to deduce weak type estimates for truncations.
Upstreaming status:
- Minkowski's integral inequality belongs into mathlib, and is mostly ready
- applying it to truncations needs truncations upstreamed first
- weak type estimates are also desirable
Lemma names often need to be improved a bit; perhaps the code can also be golfed.
Minkowski's integral inequality #
def
MeasureTheory.truncCut
{α : Type u_1}
{m : MeasurableSpace α}
(f : α → ENNReal)
(μ : Measure α)
[SigmaFinite μ]
(n : ℕ)
(x : α)
:
Equations
- MeasureTheory.truncCut f μ n = (MeasureTheory.spanningSets μ n).indicator fun (x : α) => min (f x) ↑n
Instances For
theorem
MeasureTheory.truncCut_mono
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
{f : α → ENNReal}
(x : α)
:
theorem
MeasureTheory.truncCut_mono₀
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
{f : α → ENNReal}
:
theorem
MeasureTheory.truncCut_sup
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
{f : α → ENNReal}
(x : α)
:
theorem
MeasureTheory.representationLp
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
[SigmaFinite μ]
{f : α → ENNReal}
(hf : AEMeasurable f μ)
{p q : ℝ}
(hp : p > 1)
(hq : q ≥ 1)
(hpq : p⁻¹ + q⁻¹ = 1)
:
Characterization of ∫⁻ x : α, f x ^ p ∂μ by a duality argument.
theorem
MeasureTheory.aemeasurability_prod₁
{α : Type u_1}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{ν : Measure β}
[SFinite ν]
⦃f : α × β → ENNReal⦄
(hf : AEMeasurable f (μ.prod ν))
:
theorem
MeasureTheory.aemeasurability_prod₂
{α : Type u_1}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{ν : Measure β}
[SFinite ν]
[SFinite μ]
⦃f : α × β → ENNReal⦄
(hf : AEMeasurable f (μ.prod ν))
:
theorem
MeasureTheory.aemeasurable_integral_component
{α : Type u_1}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{ν : Measure β}
[SFinite ν]
⦃f : α × β → ENNReal⦄
(hf : AEMeasurable f (μ.prod ν))
:
theorem
MeasureTheory.lintegral_lintegral_pow_swap
{α : Type u_1}
{β : Type u_3}
{p : ℝ}
(hp : 1 ≤ p)
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{ν : Measure β}
[SFinite ν]
[SigmaFinite μ]
⦃f : α → β → ENNReal⦄
(hf : AEMeasurable (Function.uncurry f) (μ.prod ν))
:
Minkowsi's integral inequality: TODO describe what it does
theorem
MeasureTheory.lintegral_lintegral_pow_swap_rpow
{α : Type u_1}
{β : Type u_3}
{p : ℝ}
(hp : p ≥ 1)
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{ν : Measure β}
[SFinite ν]
[SigmaFinite μ]
⦃f : α → β → ENNReal⦄
(hf : AEMeasurable (Function.uncurry f) (μ.prod ν))
:
Apply Minkowski's integral inequality to truncations #
theorem
MeasureTheory.aemeasurable_ton
(tc : ToneCouple)
:
AEMeasurable tc.ton (volume.restrict (Set.Ioi 0))
theorem
MeasureTheory.indicator_ton_measurable
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{g : α → E₁}
[MeasurableSpace E₁]
[TopologicalSpace E₁]
[ESeminormedAddCommMonoid E₁]
[BorelSpace E₁]
(hg : AEMeasurable g μ)
(tc : ToneCouple)
:
theorem
MeasureTheory.indicator_ton_measurable_lt
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{g : α → E₁}
[MeasurableSpace E₁]
[TopologicalSpace E₁]
[ESeminormedAddCommMonoid E₁]
[BorelSpace E₁]
(hg : AEMeasurable g μ)
(tc : ToneCouple)
:
theorem
MeasureTheory.AEMeasurable.trunc_ton
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → E₁}
[MeasurableSpace E₁]
[TopologicalSpace E₁]
[ESeminormedAddCommMonoid E₁]
[BorelSpace E₁]
(hf : AEMeasurable f μ)
(tc : ToneCouple)
:
theorem
MeasureTheory.AEMeasurable.truncCompl_ton
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → E₁}
[MeasurableSpace E₁]
[TopologicalSpace E₁]
[ESeminormedAddCommMonoid E₁]
[BorelSpace E₁]
(hf : AEMeasurable f μ)
(tc : ToneCouple)
:
AEMeasurable (fun (a : ENNReal × α) => truncCompl f (tc.ton a.1) a.2)
((volume.restrict (Set.Ioi 0)).prod (μ.restrict (Function.support f)))
theorem
MeasureTheory.restrict_to_support
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{p : ℝ}
(hp : 0 < p)
[TopologicalSpace E₁]
[ESeminormedAddCommMonoid E₁]
(f : α → E₁)
:
theorem
MeasureTheory.restrict_to_support_truncCompl
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{p : ℝ}
[TopologicalSpace E₁]
[ESeminormedAddCommMonoid E₁]
(hp : 0 < p)
(f : α → E₁)
:
theorem
MeasureTheory.restrict_to_support_trnc
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{p : ℝ}
{j : Bool}
[TopologicalSpace E₁]
[ESeminormedAddCommMonoid E₁]
(hp : 0 < p)
(f : α → E₁)
:
theorem
MeasureTheory.AEMeasurable.trnc_restrict
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → E₁}
[MeasurableSpace E₁]
[TopologicalSpace E₁]
[ESeminormedAddCommMonoid E₁]
[BorelSpace E₁]
{j : Bool}
(hf : AEMeasurable f μ)
(tc : ToneCouple)
:
theorem
MeasureTheory.lintegral_lintegral_pow_swap_truncCompl
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → E₁}
{q q₀ p₀ : ℝ}
[MeasurableSpace E₁]
[TopologicalSpace E₁]
[ESeminormedAddCommMonoid E₁]
[TopologicalSpace.PseudoMetrizableSpace E₁]
[BorelSpace E₁]
{j : Bool}
{hμ : SigmaFinite (μ.restrict (Function.support f))}
(hp₀ : 0 < p₀)
(hp₀q₀ : p₀ ≤ q₀)
(hf : AEStronglyMeasurable f μ)
(tc : ToneCouple)
:
∫⁻ (s : ℝ) in Set.Ioi 0, (∫⁻ (a : α) in Function.support f, ENNReal.ofReal (s ^ (q - q₀ - 1)) ^ (p₀⁻¹ * q₀)⁻¹ * ‖trnc j f (tc.ton (ENNReal.ofReal s)) a‖ₑ ^ p₀ ∂μ) ^ (p₀⁻¹ * q₀) ≤ (∫⁻ (a : α) in Function.support f, (∫⁻ (s : ℝ) in Set.Ioi 0, (ENNReal.ofReal (s ^ (q - q₀ - 1)) ^ (p₀⁻¹ * q₀)⁻¹ * ‖trnc j f (tc.ton (ENNReal.ofReal s)) a‖ₑ ^ p₀) ^ (p₀⁻¹ * q₀)) ^ (p₀⁻¹ * q₀)⁻¹ ∂μ) ^ (p₀⁻¹ * q₀)
theorem
MeasureTheory.lintegral_congr_support
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → E₁}
{g h : α → ENNReal}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
(hf : AEStronglyMeasurable f μ)
(hgh : ∀ x ∈ Function.support f, g x = h x)
:
theorem
MeasureTheory.estimate_trnc
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → E₁}
{p₀ q₀ q : ℝ}
{spf : ScaledPowerFunction}
{j : Bool}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
[MeasurableSpace E₁]
[BorelSpace E₁]
[TopologicalSpace.PseudoMetrizableSpace E₁]
(hp₀ : 0 < p₀)
(hq₀ : 0 < q₀)
(hp₀q₀ : p₀ ≤ q₀)
(hf : AEStronglyMeasurable f μ)
(hf₂ : SigmaFinite (μ.restrict (Function.support f)))
(hpowers : if (j ^^ (spf_to_tc spf).mon) = true then q₀ < q else q < q₀)
(hpow_pos : 0 < q₀ + spf.σ⁻¹ * (q - q₀))
:
One of the key estimates for the real interpolation theorem, not yet using
the particular choice of exponent and scale in the ScaledPowerFunction.
Equations
- MeasureTheory.sel true p₀ p₁ = p₁
- MeasureTheory.sel false p₀ p₁ = p₀
Instances For
theorem
MeasureTheory.estimate_trnc₁
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{p q p₀ q₀ p₁ q₁ : ENNReal}
{μ : Measure α}
{f : α → E₁}
{t : ENNReal}
{spf : ScaledPowerFunction}
{j : Bool}
[TopologicalSpace E₁]
[ENormedAddCommMonoid E₁]
[MeasurableSpace E₁]
[BorelSpace E₁]
[TopologicalSpace.PseudoMetrizableSpace E₁]
(ht : t ∈ Set.Ioo 0 1)
(hp₀ : 0 < p₀)
(hq₀ : 0 < q₀)
(hp₁ : 0 < p₁)
(hq₁ : 0 < q₁)
(hpq : sel j p₀ p₁ ≤ sel j q₀ q₁)
(hp' : sel j p₀ p₁ ≠ ⊤)
(hq' : sel j q₀ q₁ ≠ ⊤)
(hp₀p₁ : p₀ < p₁)
(hq₀q₁ : q₀ ≠ q₁)
(hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
(hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹)
(hf : AEStronglyMeasurable f μ)
(hf₂ : SigmaFinite (μ.restrict (Function.support f)))
(hspf : spf.σ = ComputationsChoiceExponent.ζ p₀ q₀ p₁ q₁ t.toReal)
:
∫⁻ (s : ℝ) in Set.Ioi 0, eLpNorm (trnc j f ((spf_to_tc spf).ton (ENNReal.ofReal s))) (sel j p₀ p₁) μ ^ (sel j q₀ q₁).toReal * ENNReal.ofReal (s ^ (q.toReal - (sel j q₀ q₁).toReal - 1)) ≤ spf.d ^ (q.toReal - (sel j q₀ q₁).toReal) * ENNReal.ofReal |q.toReal - (sel j q₀ q₁).toReal|⁻¹ * (eLpNorm f p μ ^ p.toReal) ^ ((sel j p₀ p₁).toReal⁻¹ * (sel j q₀ q₁).toReal)
One of the key estimates for the real interpolation theorem, now using
the particular choice of exponent, but not yet using the
particular choice of scale in the ScaledPowerFunction.
theorem
MeasureTheory.wnorm_eq_zero_iff
{α : Type u_1}
{m : MeasurableSpace α}
{ε : Type u_7}
[TopologicalSpace ε]
{μ : Measure α}
[ENormedAddMonoid ε]
{f : α → ε}
{p : ENNReal}
(hp : p ≠ 0)
:
Weaktype estimates applied to truncations #
theorem
MeasureTheory.eLpNorm_trnc_est
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{t : ENNReal}
[TopologicalSpace E₁]
[ESeminormedAddCommMonoid E₁]
{f : α → E₁}
{j : Bool}
:
theorem
MeasureTheory.weaktype_estimate
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{ε₁ : Type u_8}
{ε₂ : Type u_9}
[TopologicalSpace ε₁]
[TopologicalSpace ε₂]
{μ : Measure α}
{ν : Measure α'}
{t : ENNReal}
[ContinuousENorm ε₁]
[ContinuousENorm ε₂]
{T : (α → ε₁) → α' → ε₂}
{C₀ : NNReal}
{p q : ENNReal}
{f : α → ε₁}
(hq : 0 < q)
(hq' : q < ⊤)
(hf : MemLp f p μ)
(h₀T : HasWeakType T p q μ ν ↑C₀)
(ht : 0 < t)
:
theorem
MeasureTheory.weaktype_estimate_top
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{ε₁ : Type u_8}
{ε₂ : Type u_9}
[TopologicalSpace ε₁]
[TopologicalSpace ε₂]
{μ : Measure α}
{ν : Measure α'}
{t : ENNReal}
[ContinuousENorm ε₁]
[ContinuousENorm ε₂]
{T : (α → ε₁) → α' → ε₂}
{C : NNReal}
{p q : ENNReal}
(hq' : q = ⊤)
{f : α → ε₁}
(hf : MemLp f p μ)
(hT : HasWeakType T p q μ ν ↑C)
(ht : ↑C * eLpNorm f p μ ≤ t)
:
theorem
MeasureTheory.weaktype_aux₀
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{ε₁ : Type u_8}
{ε₂ : Type u_9}
[TopologicalSpace ε₁]
[TopologicalSpace ε₂]
{μ : Measure α}
{ν : Measure α'}
[ENormedAddMonoid ε₁]
[ENormedAddMonoid ε₂]
{f : α → ε₁}
{T : (α → ε₁) → α' → ε₂}
{p₀ q₀ p q : ENNReal}
(hp₀ : 0 < p₀)
(hq₀ : 0 < q₀)
(hp : 0 < p)
(hq : 0 < q)
{C₀ : NNReal}
(h₀T : HasWeakType T p₀ q₀ μ ν ↑C₀)
(hf : AEStronglyMeasurable f μ)
(hF : eLpNorm f p μ = 0)
:
If T has weaktype p₀-p₁, f is AEStronglyMeasurable and the p-norm of f
vanishes, then the q-norm of T f vanishes.
theorem
MeasureTheory.weaktype_estimate_truncCompl
{α : Type u_1}
{α' : Type u_2}
{E₁ : Type u_4}
{E₂ : Type u_5}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{t : ENNReal}
[TopologicalSpace E₁]
[ESeminormedAddCommMonoid E₁]
[TopologicalSpace E₂]
[ESeminormedAddCommMonoid E₂]
{T : (α → E₁) → α' → E₂}
{C₀ : NNReal}
{p p₀ : ENNReal}
{f : α → E₁}
(hp₀ : 0 < p₀)
{q₀ : ENNReal}
(hp : p ≠ ⊤)
(hq₀ : 0 < q₀)
(hq₀' : q₀ < ⊤)
(hp₀p : p₀ ≤ p)
(hf : MemLp f p μ)
(h₀T : HasWeakType T p₀ q₀ μ ν ↑C₀)
(ht : 0 < t)
{a : ENNReal}
(ha : 0 < a)
:
distribution (T (truncCompl f a)) t ν ≤ ↑C₀ ^ q₀.toReal * eLpNorm (truncCompl f a) p₀ μ ^ q₀.toReal * t ^ (-q₀.toReal)
theorem
MeasureTheory.weaktype_estimate_trunc
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{t : ENNReal}
{E₁' : Type u_10}
{E₂' : Type u_11}
[TopologicalSpace E₁']
[ENormedAddCommMonoid E₁']
[TopologicalSpace E₂']
[ENormedAddCommMonoid E₂']
{T' : (α → E₁') → α' → E₂'}
{C₁ : NNReal}
{p p₁ q₁ : ENNReal}
{f : α → E₁'}
(hp : 0 < p)
(hq₁ : 0 < q₁)
(hq₁' : q₁ < ⊤)
(hp₁p : p ≤ p₁)
(hf : MemLp f p μ)
(h₁T : HasWeakType T' p₁ q₁ μ ν ↑C₁)
(ht : 0 < t)
{a : ENNReal}
(ha : a ≠ ⊤)
:
theorem
MeasureTheory.weaktype_estimate_trunc_top_top
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{t : ENNReal}
{E₁' : Type u_10}
{E₂' : Type u_11}
[TopologicalSpace E₁']
[ENormedAddCommMonoid E₁']
[TopologicalSpace E₂']
[ENormedAddCommMonoid E₂']
{T' : (α → E₁') → α' → E₂'}
{a : ENNReal}
{C₁ : NNReal}
(hC₁ : 0 < C₁)
{p p₁ q₁ : ENNReal}
(hp : 0 < p)
(hp₁ : p₁ = ⊤)
(hq₁ : q₁ = ⊤)
(hp₁p : p ≤ p₁)
{f : α → E₁'}
(hf : MemLp f p μ)
(h₁T : HasWeakType T' p₁ q₁ μ ν ↑C₁)
(ha : a = t / ↑C₁)
:
theorem
MeasureTheory.weaktype_estimate_truncCompl_top
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{t : ENNReal}
{E₁' : Type u_10}
{E₂' : Type u_11}
[TopologicalSpace E₁']
[ENormedAddCommMonoid E₁']
[TopologicalSpace E₂']
[ENormedAddCommMonoid E₂']
{T' : (α → E₁') → α' → E₂'}
{C₀ : NNReal}
(hC₀ : 0 < C₀)
{p p₀ q₀ : ENNReal}
(hp₀ : 0 < p₀)
(hq₀ : q₀ = ⊤)
(hp₀p : p₀ < p)
(hp : p ≠ ⊤)
{f : α → E₁'}
(hf : MemLp f p μ)
(h₀T : HasWeakType T' p₀ q₀ μ ν ↑C₀)
(ht : 0 < t)
{a d : ENNReal}
(ha : a = (t / d) ^ (p₀.toReal / (p₀.toReal - p.toReal)))
(hdeq : d = (↑C₀ ^ p₀.toReal * eLpNorm f p μ ^ p.toReal) ^ p₀.toReal⁻¹)
:
theorem
MeasureTheory.weaktype_estimate_trunc_top
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{μ : Measure α}
{ν : Measure α'}
{t : ENNReal}
{E₁' : Type u_10}
{E₂' : Type u_11}
[TopologicalSpace E₁']
[ENormedAddCommMonoid E₁']
[TopologicalSpace E₂']
[ENormedAddCommMonoid E₂']
{T' : (α → E₁') → α' → E₂'}
{C₁ : NNReal}
(hC₁ : 0 < C₁)
{p p₁ q₁ : ENNReal}
(hp : 0 < p)
(hp₁ : p₁ < ⊤)
(hq₁ : q₁ = ⊤)
(hp₁p : p < p₁)
{f : α → E₁'}
(hf : MemLp f p μ)
(h₁T : HasWeakType T' p₁ q₁ μ ν ↑C₁)
(ht : 0 < t)
{a d : ENNReal}
(hd : 0 < d)
(ha : a = (t / d) ^ (p₁.toReal / (p₁.toReal - p.toReal)))
(hdeq : d = (↑C₁ ^ p₁.toReal * eLpNorm f p μ ^ p.toReal) ^ p₁.toReal⁻¹)
: