This file contains some miscellaneous prerequisites for proving the Marcinkiewisz real interpolation theorem. There are the following sections:
- Interface for using cutoff functions
- Results about the particular choice of scale
- Some tools for measure theory computations
- Results about truncations of a function
- Measurability properties of truncations
- Truncations and Lp spaces
Interface for using cutoff functions #
A ToneCouple is a couple of two monotone functions that are practically inverses of each
other. It is used in the proof of the real interpolation theorem.
Note: originally it seemed useful to make the possible choice of this function general in the proof of the real inteprolation theorem. However, in the end really only one function works for all the different cases. This infrastructure, however, could potentially still be useful, if one would like to try to improve the constant.
- mon : Bool
Instances For
A StrictRangeToneCouple is a ToneCouple for which the functions in the couple, when
restricted to Ioo 0 ∞, map to Ioo 0 ∞.
Instances For
A scaled power function gives rise to a ToneCouple.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Results about the particular choice of scale #
The proof of the real interpolation theorem will estimate
`distribution (trunc f A(t)) t` and `distribution (truncCompl f A(t)) t` for a
function `A`. The function `A` can be given a closed-form expression that works for
_all_ cases in the real interpolation theorem, because of the computation rules available
for elements in `ℝ≥0∞` that avoid the need for a limiting procedure, e.g. `⊤⁻¹ = 0`.
The function `A` will be of the form `A(t) = (t / d) ^ σ` for particular choices of `d` and
`σ`. This section contatins results about the scale `d`.
def
ChoiceScale.d
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p p₀ q₀ p₁ q₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ChoiceScale.d_pos_aux₀
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
(hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
:
theorem
ChoiceScale.d_ne_zero_aux₀
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
{b : ℝ}
(hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
:
theorem
ChoiceScale.d_ne_zero_aux₂
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
{C : NNReal}
{b c : ℝ}
(hC : 0 < C)
(hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
:
theorem
ChoiceScale.d_ne_top_aux₂
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
{b : ℝ}
(hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
:
theorem
ChoiceScale.d_ne_top_aux₃
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
{C : NNReal}
{b c : ℝ}
(hC : 0 < C)
(hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
:
theorem
ChoiceScale.d_ne_zero_aux₃
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{C₀ C₁ : NNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
{b₀ c₀ b₁ c₁ : ℝ}
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
:
theorem
ChoiceScale.d_ne_top_aux₄
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{C₀ C₁ : NNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
{b₀ c₀ b₁ c₁ : ℝ}
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
:
theorem
ChoiceScale.d_pos
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p p₀ q₀ p₁ q₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
:
theorem
ChoiceScale.d_ne_top
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p p₀ q₀ p₁ q₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
:
theorem
ChoiceScale.d_eq_top₀
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p p₀ q₀ p₁ q₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
(hp₀ : 0 < p₀)
(hq₁ : 0 < q₁)
(hp₀' : p₀ ≠ ⊤)
(hq₀' : q₀ = ⊤)
(hq₀q₁ : q₀ ≠ q₁)
:
theorem
ChoiceScale.d_eq_top₁
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p p₀ q₀ p₁ q₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
(hq₀ : 0 < q₀)
(hp₁ : 0 < p₁)
(hp₁' : p₁ ≠ ⊤)
(hq₁' : q₁ = ⊤)
(hq₀q₁ : q₀ ≠ q₁)
(hC₁ : 0 < C₁)
:
theorem
ChoiceScale.d_eq_top_of_eq
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p p₀ q₀ p₁ q₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
(hC₁ : 0 < C₁)
(hp₀ : 0 < p₀)
(hq₀ : 0 < q₀)
(hq₀' : q₀ ≠ ⊤)
(hp₀' : p₀ ≠ ⊤)
(hp₁ : 0 < p₁)
(hp₀p₁ : p₀ = p₁)
(hpp₀ : p = p₀)
(hq₁' : q₁ = ⊤)
:
theorem
ChoiceScale.d_eq_top_top
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p p₀ q₀ p₁ q₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
(hq₀ : 0 < q₀)
(hq₀q₁ : q₀ ≠ q₁)
(hp₁' : p₁ = ⊤)
(hq₁' : q₁ = ⊤)
:
def
ChoiceScale.spf_ch
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p p₀ q₀ p₁ q₁ : ENNReal}
{C₀ C₁ : NNReal}
{μ : MeasureTheory.Measure α}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
{t : ℝ}
(ht : t ∈ Set.Ioo 0 1)
(hq₀q₁ : q₀ ≠ q₁)
(hp₀ : 0 < p₀)
(hq₀ : 0 < q₀)
(hp₁ : 0 < p₁)
(hq₁ : 0 < q₁)
(hp₀p₁ : p₀ ≠ p₁)
(hC₀ : 0 < C₀)
(hC₁ : 0 < C₁)
(hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤)
:
The particular choice of scaled power function that works in the proof of the real interpolation theorem.
Equations
- ChoiceScale.spf_ch ht hq₀q₁ hp₀ hq₀ hp₁ hq₁ hp₀p₁ hC₀ hC₁ hF = { σ := ComputationsChoiceExponent.ζ p₀ q₀ p₁ q₁ t, d := ChoiceScale.d, hd := ⋯, hd' := ⋯, hσ := ⋯ }
Instances For
Some tools for measure theory computations #
A collection of small lemmas to help with integral manipulations.
theorem
MeasureTheory.measure_preserving_shift
{a : ℝ}
:
MeasurePreserving (fun (x : ℝ) => a + x) volume volume
theorem
MeasureTheory.measure_preserving_scaling
{a : ℝ}
(ha : a ≠ 0)
:
MeasurePreserving (fun (x : ℝ) => a * x) volume (ENNReal.ofReal |a⁻¹| • volume)
Results about truncations of a function #
def
MeasureTheory.trunc
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
(f : α → ε)
(t : ENNReal)
(x : α)
:
ε
The t-truncation of a function f.
Instances For
@[simp]
theorem
MeasureTheory.trunc_top
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
:
def
MeasureTheory.truncCompl
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
(f : α → ε)
(t : ENNReal)
(x : α)
:
ε
The complement of a t-truncation of a function f.
Instances For
theorem
MeasureTheory.truncCompl_eq_indicator
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
:
@[simp]
theorem
MeasureTheory.truncCompl_top
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
:
theorem
MeasureTheory.truncCompl_eq
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{t : ENNReal}
{f : α → ε}
:
def
MeasureTheory.trnc
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
(j : Bool)
(f : α → ε)
(t : ENNReal)
:
α → ε
A function to deal with truncations and complement of truncations in one go.
Equations
Instances For
@[simp]
theorem
MeasureTheory.trnc_false
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
:
@[simp]
theorem
MeasureTheory.trnc_true
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
:
@[simp]
theorem
MeasureTheory.trunc_add_truncCompl
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
:
A function is the complement if its truncation and the complement of the truncation.
theorem
MeasureTheory.trnc_true_add_trnc_false
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
:
Alias of MeasureTheory.trunc_add_truncCompl.
A function is the complement if its truncation and the complement of the truncation.
theorem
MeasureTheory.trunc_of_nonpos
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{t : ENNReal}
{f : α → ε}
(ht : t ≤ 0)
:
If the truncation parameter is non-positive, the truncation vanishes.
theorem
MeasureTheory.truncCompl_of_nonpos
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{t : ENNReal}
{f : α → ε}
(ht : t ≤ 0)
:
If the truncation parameter is non-positive, the complement of the truncation is the function itself.
Measurability properties of truncations #
theorem
MeasureTheory.StronglyMeasurable.trunc
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
(hf : StronglyMeasurable f)
:
StronglyMeasurable (trunc f t)
theorem
MeasureTheory.StronglyMeasurable.truncCompl
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
(hf : StronglyMeasurable f)
:
StronglyMeasurable (truncCompl f t)
theorem
MeasureTheory.AEStronglyMeasurable.trunc
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.AEStronglyMeasurable.truncCompl
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.aestronglyMeasurable_trnc
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
{j : Bool}
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (trnc j f t) μ
theorem
MeasureTheory.trunc_le
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{t : ENNReal}
{f : α → ε}
(x : α)
:
A small lemma that is helpful for rewriting
theorem
MeasureTheory.trunc_eLpNormEssSup_le
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
(a : ENNReal)
:
theorem
MeasureTheory.trunc_mono
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{a b : ENNReal}
(hab : a ≤ b)
{x : α}
:
theorem
MeasureTheory.eLpNorm_trunc_mono
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
:
The norm of the truncation is monotone in the truncation parameter
theorem
MeasureTheory.trunc_buildup_enorm
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
{x : α}
:
theorem
MeasureTheory.trunc_le_func
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
{x : α}
:
theorem
MeasureTheory.truncCompl_le_func
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
{x : α}
:
theorem
MeasureTheory.truncCompl_anti
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{s t : ENNReal}
{x : α}
(hab : t ≤ s)
(hf : ‖trunc f t x‖ₑ ≠ ⊤)
:
theorem
MeasureTheory.eLpNorm_truncCompl_anti
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
(hf : eLpNorm f 1 μ ≠ ⊤)
(mf : AEStronglyMeasurable f μ)
:
Antitone fun (s : ENNReal) => eLpNorm (truncCompl f s) p μ
The norm of the complement of the truncation is antitone in the truncation parameter
theorem
MeasureTheory.eLpNorm_trunc_measurable
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
:
Measurable fun (s : ENNReal) => eLpNorm (trunc f s) p μ
The norm of the truncation is meaurable in the truncation parameter
theorem
MeasureTheory.eLpNorm_truncCompl_measurable
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
(hf : eLpNorm f 1 μ ≠ ⊤)
(mf : AEStronglyMeasurable f μ)
:
Measurable fun (s : ENNReal) => eLpNorm (truncCompl f s) p μ
The norm of the complement of the truncation is measurable in the truncation parameter
theorem
MeasureTheory.trnc_le_func
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{j : Bool}
{a : ENNReal}
{x : α}
:
Truncations and L-p spaces #
theorem
MeasureTheory.rpow_le_rpow_of_exponent_le_base_le
{a b t γ : ℝ}
(ht : 0 < t)
(htγ : t ≤ γ)
(hab : a ≤ b)
:
theorem
MeasureTheory.rpow_le_rpow_of_exponent_le_base_ge
{a b t γ : ℝ}
(hγ : 0 < γ)
(htγ : γ ≤ t)
(hab : a ≤ b)
:
theorem
MeasureTheory.trunc_preserves_Lp
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t p : ENNReal}
(hf : MemLp f p μ)
:
theorem
MeasureTheory.truncCompl_preserves_Lp
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t p : ENNReal}
(hf : MemLp f p μ)
:
MemLp (truncCompl f t) p μ
theorem
MeasureTheory.eLpNorm_truncCompl_le
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t q : ENNReal}
(q_ne_zero : ¬q = 0)
(q_ne_top : q ≠ ⊤)
:
theorem
MeasureTheory.estimate_eLpNorm_truncCompl
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t p q : ENNReal}
(p_ne_top : p ≠ ⊤)
(hpq : q ∈ Set.Ioc 0 p)
(hf : AEStronglyMeasurable f μ)
(ht : 0 < t)
:
theorem
MeasureTheory.estimate_eLpNorm_trunc
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t p q : ENNReal}
(hq : q ≠ ⊤)
(hpq : p ∈ Set.Ioc 0 q)
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.trunc_Lp_Lq_higher
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p q : ENNReal}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
(hpq : p ∈ Set.Ioc 0 q)
(hf : MemLp f p μ)
(ht : t ≠ ⊤)
:
If f is in Lp, the truncation is element of Lq for q ≥ p.
theorem
MeasureTheory.truncCompl_Lp_Lq_lower
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p q : ENNReal}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
{t : ENNReal}
(hp : p ≠ ⊤)
(hpq : q ∈ Set.Ioc 0 p)
(ht : 0 < t)
(hf : MemLp f p μ)
:
If f is in Lp, the complement of the truncation is in Lq for q ≤ p.
theorem
MeasureTheory.memLp_of_memLp_le_of_memLp_ge
{α : Type u_1}
{ε : Type u_3}
{m : MeasurableSpace α}
{p q : ENNReal}
{μ : Measure α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
{f : α → ε}
[ContinuousAdd ε]
{r : ENNReal}
(hp : 0 < p)
(hr' : q ∈ Set.Icc p r)
(hf : MemLp f p μ)
(hf' : MemLp f r μ)
:
MemLp f q μ
Some results about the integrals of truncations #
Equations
theorem
MeasureTheory.lintegral_trunc_mul₀
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
{g : ℝ → ENNReal}
{j : Bool}
{x : α}
{tc : ToneCouple}
{p : ℝ}
(hp : 0 < p)
:
theorem
MeasureTheory.lintegral_trunc_mul₁
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
{g : ℝ → ENNReal}
{j : Bool}
{x : α}
{p : ℝ}
{tc : ToneCouple}
:
theorem
MeasureTheory.lintegral_trunc_mul₂
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
{g : ℝ → ENNReal}
{j : Bool}
{x : α}
{p : ℝ}
{tc : ToneCouple}
:
theorem
MeasureTheory.lintegral_trunc_mul
{α : Type u_1}
{ε : Type u_3}
[TopologicalSpace ε]
[ENormedAddCommMonoid ε]
{f : α → ε}
{g : ℝ → ENNReal}
(hg : AEMeasurable g volume)
{j : Bool}
{x : α}
{tc : ToneCouple}
{p : ℝ}
(hp : 0 < p)
:
Extract expressions for the lower Lebesgue integral of power functions
theorem
MeasureTheory.AEStronglyMeasurable.induction
{α : Type u_4}
{β : Type u_5}
{mα : MeasurableSpace α}
[TopologicalSpace β]
{μ : Measure α}
{motive : (α → β) → Prop}
(ae_eq_implies : ∀ ⦃f g : α → β⦄, StronglyMeasurable f → f =ᶠ[ae μ] g → motive f → motive g)
(measurable : ∀ ⦃f : α → β⦄, StronglyMeasurable f → motive f)
⦃f : α → β⦄
(hf : AEStronglyMeasurable f μ)
:
motive f