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 #
noncomputable 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₁}
[TopologicalSpace E₁]
[ESeminormedAddMonoid E₁]
(hg : AEStronglyMeasurable g μ)
(tc : ToneCouple)
:
theorem
MeasureTheory.indicator_ton_measurable_lt
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{g : α → E₁}
[TopologicalSpace E₁]
[ESeminormedAddMonoid E₁]
(hg : AEStronglyMeasurable g μ)
(tc : ToneCouple)
:
theorem
MeasureTheory.AEStronglyMeasurable.trunc_ton_norm
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → E₁}
[TopologicalSpace E₁]
[ESeminormedAddMonoid E₁]
(hf : AEStronglyMeasurable f μ)
(tc : ToneCouple)
:
AEStronglyMeasurable (fun (a : ENNReal × α) => MeasureTheory.trunc f (tc.ton a.1) a.2)
((volume.restrict (Set.Ioi 0)).prod (μ.restrict (Function.support fun (x : α) => ‖f x‖ₑ)))
theorem
MeasureTheory.AEStronglyMeasurable.trunc_ton
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → E₁}
[TopologicalSpace E₁]
[ESeminormedAddMonoid E₁]
(hf : AEStronglyMeasurable f μ)
(tc : ToneCouple)
:
AEStronglyMeasurable (fun (a : ENNReal × α) => MeasureTheory.trunc f (tc.ton a.1) a.2)
((volume.restrict (Set.Ioi 0)).prod (μ.restrict (Function.support f)))
theorem
MeasureTheory.AEStronglyMeasurable.truncCompl_ton
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → E₁}
[TopologicalSpace E₁]
[ESeminormedAddMonoid E₁]
(hf : AEStronglyMeasurable f μ)
(tc : ToneCouple)
:
AEStronglyMeasurable (fun (a : ENNReal × α) => MeasureTheory.truncCompl f (tc.ton a.1) a.2)
((volume.restrict (Set.Ioi 0)).prod (μ.restrict (Function.support f)))
theorem
MeasureTheory.AEStronglyMeasurable.truncCompl_ton_norm
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → E₁}
[TopologicalSpace E₁]
[ESeminormedAddMonoid E₁]
(hf : AEStronglyMeasurable f μ)
(tc : ToneCouple)
:
AEStronglyMeasurable (fun (a : ENNReal × α) => MeasureTheory.truncCompl f (tc.ton a.1) a.2)
((volume.restrict (Set.Ioi 0)).prod (μ.restrict (Function.support fun (x : α) => ‖f x‖ₑ)))
theorem
MeasureTheory.restrict_to_support
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{p : ℝ}
(hp : 0 < p)
[TopologicalSpace E₁]
[ESeminormedAddMonoid E₁]
(f : α → E₁)
:
theorem
MeasureTheory.restrict_to_support_truncCompl
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{t : ENNReal}
{p : ℝ}
[TopologicalSpace E₁]
[ESeminormedAddMonoid 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₁]
[ESeminormedAddMonoid E₁]
(hp : 0 < p)
(f : α → E₁)
:
theorem
MeasureTheory.AEStronglyMeasurable.trnc_restrict
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → E₁}
[TopologicalSpace E₁]
[ESeminormedAddMonoid E₁]
{j : Bool}
(hf : AEStronglyMeasurable f μ)
(tc : ToneCouple)
:
theorem
MeasureTheory.AEStronglyMeasurable.trnc_restrict_norm
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → E₁}
[TopologicalSpace E₁]
[ESeminormedAddMonoid E₁]
{j : Bool}
(hf : AEStronglyMeasurable f μ)
(tc : ToneCouple)
:
theorem
MeasureTheory.lintegral_lintegral_pow_swap_truncCompl_old
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → E₁}
{q q₀ p₀ : ℝ}
[TopologicalSpace E₁]
[ESeminormedAddMonoid 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_lintegral_pow_swap_truncCompl
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → E₁}
{q q₀ p₀ : ℝ}
[TopologicalSpace E₁]
[ESeminormedAddMonoid E₁]
{j : Bool}
{hμ : SigmaFinite (μ.restrict (Function.support fun (x : α) => ‖f x‖ₑ))}
(hp₀ : 0 < p₀)
(hp₀q₀ : p₀ ≤ q₀)
(hf : AEStronglyMeasurable f μ)
(tc : ToneCouple)
:
∫⁻ (s : ℝ) in Set.Ioi 0, (∫⁻ (a : α) in Function.support fun (x : α) => ‖f x‖ₑ, ENNReal.ofReal (s ^ (q - q₀ - 1)) ^ (p₀⁻¹ * q₀)⁻¹ * ‖trnc j f (tc.ton (ENNReal.ofReal s)) a‖ₑ ^ p₀ ∂μ) ^ (p₀⁻¹ * q₀) ≤ (∫⁻ (a : α) in Function.support fun (x : α) => ‖f x‖ₑ, (∫⁻ (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₁]
[ESeminormedAddMonoid E₁]
(hf : AEStronglyMeasurable f μ)
(hgh : ∀ x ∈ Function.support fun (x : α) => ‖f x‖ₑ, 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₁]
[ESeminormedAddMonoid E₁]
(hp₀ : 0 < p₀)
(hq₀ : 0 < q₀)
(hp₀q₀ : p₀ ≤ q₀)
(hf : AEStronglyMeasurable f μ)
(hf₂ : SigmaFinite (μ.restrict (Function.support fun (x : α) => ‖f x‖ₑ)))
(hpowers : if (j ^^ (spf_to_tc spf).mon) = true then q₀ < q else q < q₀)
(hpow_pos : 0 < q₀ + spf.σ⁻¹ * (q - q₀))
:
∫⁻ (s : ℝ) in Set.Ioi 0, eLpNorm (trnc j f ((spf_to_tc spf).ton (ENNReal.ofReal s))) (ENNReal.ofReal p₀) μ ^ q₀ * ENNReal.ofReal (s ^ (q - q₀ - 1)) ≤ spf.d ^ (q - q₀) * ENNReal.ofReal |q - q₀|⁻¹ * (∫⁻ (a : α) in Function.support fun (x : α) => ‖f x‖ₑ, ‖f a‖ₑ ^ (p₀ + spf.σ⁻¹ * (q - q₀) * (p₀ / q₀)) ∂μ) ^ (p₀⁻¹ * 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₁]
[ESeminormedAddMonoid 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 fun (x : α) => ‖f x‖ₑ)))
(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.
Weaktype estimates applied to truncations #
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}
[ENorm ε₁]
[ENorm ε₂]
{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}
[ENorm ε₁]
[ENorm ε₂]
{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.eLpNorm_eq_zero_of_eLpNorm_eq_zero
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{p q : ENNReal}
{μ : Measure α}
[TopologicalSpace E₁]
[ContinuousENorm E₁]
{f : α → E₁}
(hf : AEStronglyMeasurable f μ)
(hp : p ≠ 0)
:
theorem
MeasureTheory.eLpNormEssSup_eq_zero_of_eLpNorm_eq_zero
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[TopologicalSpace E₁]
[ContinuousENorm E₁]
{f : α → E₁}
(hf : AEStronglyMeasurable f μ)
(hp : p ≠ 0)
:
eLpNorm f p μ = 0 → eLpNormEssSup f μ = 0
theorem
MeasureTheory.eLpNorm_eq_zero_of_eLpNormEssSup_eq_zero
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[TopologicalSpace E₁]
[ContinuousENorm E₁]
{f : α → E₁}
(hf : AEStronglyMeasurable f μ)
:
eLpNormEssSup f μ = 0 → eLpNorm f p μ = 0
theorem
MeasureTheory.eLpNorm_trnc_est
{α : Type u_1}
{E₁ : Type u_4}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{t : ENNReal}
[TopologicalSpace E₁]
[ESeminormedAddMonoid E₁]
{f : α → E₁}
{j : Bool}
:
theorem
MeasureTheory.weaktype_aux₀
{α : Type u_1}
{α' : Type u_2}
{m : MeasurableSpace α}
{m' : MeasurableSpace α'}
{ε₁ : Type u_8}
{ε₂ : Type u_9}
[TopologicalSpace ε₁]
[TopologicalSpace ε₂]
{μ : Measure α}
{ν : Measure α'}
[ESeminormedAddMonoid ε₁]
[ENorm ε₂]
{f : α → ε₁}
{T : (α → ε₁) → α' → ε₂}
{q₀ p : ENNReal}
(p₀ q : ENNReal)
(hq₀ : 0 < q₀)
(hp : 0 < p)
{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₁]
[ESeminormedAddMonoid E₁]
{T : (α → E₁) → α' → E₂}
[TopologicalSpace E₂]
[ENorm 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₁']
[ESeminormedAddMonoid E₁']
{T' : (α → E₁') → α' → E₂'}
[TopologicalSpace E₂']
[ENorm 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₁']
[ESeminormedAddMonoid E₁']
{T' : (α → E₁') → α' → E₂'}
[TopologicalSpace E₂']
[ENorm 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₁']
[ESeminormedAddMonoid E₁']
{T' : (α → E₁') → α' → E₂'}
[TopologicalSpace E₂']
[ENorm 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₁']
[ESeminormedAddMonoid E₁']
{T' : (α → E₁') → α' → E₂'}
[TopologicalSpace E₂']
[ENorm 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⁻¹)
: