Documentation

Mathlib.MeasureTheory.Function.L1Space

Integrable functions and space #

In the first part of this file, the predicate Integrable is defined and basic properties of integrable functions are proved.

Such a predicate is already available under the name Memℒp 1. We give a direct definition which is easier to use, and show that it is equivalent to Memℒp 1

In the second part, we establish an API between Integrable and the space of equivalence classes of integrable functions, already defined as a special case of L^p spaces for p = 1.

Notation #

Main definitions #

Implementation notes #

To prove something for an arbitrary integrable function, a useful theorem is Integrable.induction in the file SetIntegral.

Tags #

integrable, function space, l1

Some results about the Lebesgue integral involving a normed group #

theorem MeasureTheory.lintegral_nnnorm_eq_lintegral_edist {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : αβ) :
∫⁻ (a : α), f a‖₊μ = ∫⁻ (a : α), edist (f a) 0μ
theorem MeasureTheory.lintegral_norm_eq_lintegral_edist {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : αβ) :
∫⁻ (a : α), ENNReal.ofReal f aμ = ∫⁻ (a : α), edist (f a) 0μ
theorem MeasureTheory.lintegral_edist_triangle {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} {g : αβ} {h : αβ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hh : MeasureTheory.AEStronglyMeasurable h μ) :
∫⁻ (a : α), edist (f a) (g a)μ ∫⁻ (a : α), edist (f a) (h a)μ + ∫⁻ (a : α), edist (g a) (h a)μ
theorem MeasureTheory.lintegral_nnnorm_zero {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] :
∫⁻ (x : α), 0‖₊μ = 0
theorem MeasureTheory.lintegral_nnnorm_add_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : αβ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (g : αγ) :
∫⁻ (a : α), f a‖₊ + g a‖₊μ = ∫⁻ (a : α), f a‖₊μ + ∫⁻ (a : α), g a‖₊μ
theorem MeasureTheory.lintegral_nnnorm_add_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] (f : αβ) {g : αγ} (hg : MeasureTheory.AEStronglyMeasurable g μ) :
∫⁻ (a : α), f a‖₊ + g a‖₊μ = ∫⁻ (a : α), f a‖₊μ + ∫⁻ (a : α), g a‖₊μ
theorem MeasureTheory.lintegral_nnnorm_neg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} :
∫⁻ (a : α), (-f) a‖₊μ = ∫⁻ (a : α), f a‖₊μ

The predicate HasFiniteIntegral #

def MeasureTheory.HasFiniteIntegral {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] :
{x : MeasurableSpace α} → (αβ)autoParam (MeasureTheory.Measure α) _auto✝Prop

HasFiniteIntegral f μ means that the integral ∫⁻ a, ‖f a‖ ∂μ is finite. HasFiniteIntegral f means HasFiniteIntegral f volume.

Equations
Instances For
    theorem MeasureTheory.hasFiniteIntegral_def {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] :
    ∀ {x : MeasurableSpace α} (f : αβ) (μ : MeasureTheory.Measure α), MeasureTheory.HasFiniteIntegral f μ ∫⁻ (a : α), f a‖₊μ <
    theorem MeasureTheory.hasFiniteIntegral_iff_norm {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : αβ) :
    theorem MeasureTheory.hasFiniteIntegral_iff_edist {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : αβ) :
    MeasureTheory.HasFiniteIntegral f μ ∫⁻ (a : α), edist (f a) 0μ <
    theorem MeasureTheory.hasFiniteIntegral_iff_ofReal {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (h : 0 ≤ᵐ[μ] f) :
    MeasureTheory.HasFiniteIntegral f μ ∫⁻ (a : α), ENNReal.ofReal (f a)μ <
    theorem MeasureTheory.hasFiniteIntegral_iff_ofNNReal {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αNNReal} :
    MeasureTheory.HasFiniteIntegral (fun (x : α) => (f x)) μ ∫⁻ (a : α), (f a)μ <
    theorem MeasureTheory.HasFiniteIntegral.mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : αβ} {g : αγ} (hg : MeasureTheory.HasFiniteIntegral g μ) (h : ∀ᵐ (a : α) ∂μ, f a g a) :
    theorem MeasureTheory.HasFiniteIntegral.mono' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} {g : α} (hg : MeasureTheory.HasFiniteIntegral g μ) (h : ∀ᵐ (a : α) ∂μ, f a g a) :
    theorem MeasureTheory.HasFiniteIntegral.congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : αβ} {g : αγ} (hf : MeasureTheory.HasFiniteIntegral f μ) (h : ∀ᵐ (a : α) ∂μ, f a = g a) :
    theorem MeasureTheory.hasFiniteIntegral_congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : αβ} {g : αγ} (h : ∀ᵐ (a : α) ∂μ, f a = g a) :
    theorem MeasureTheory.HasFiniteIntegral.congr {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} {g : αβ} (hf : MeasureTheory.HasFiniteIntegral f μ) (h : f =ᵐ[μ] g) :
    theorem MeasureTheory.hasFiniteIntegral_congr {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} {g : αβ} (h : f =ᵐ[μ] g) :
    theorem MeasureTheory.hasFiniteIntegral_const_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {c : β} :
    MeasureTheory.HasFiniteIntegral (fun (x : α) => c) μ c = 0 μ Set.univ <
    theorem MeasureTheory.hasFiniteIntegral_of_bounded {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [MeasureTheory.IsFiniteMeasure μ] {f : αβ} {C : } (hC : ∀ᵐ (a : α) ∂μ, f a C) :
    @[deprecated MeasureTheory.HasFiniteIntegral.of_finite]

    Alias of MeasureTheory.HasFiniteIntegral.of_finite.

    @[simp]
    theorem MeasureTheory.HasFiniteIntegral.norm {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} (hfi : MeasureTheory.HasFiniteIntegral f μ) :
    MeasureTheory.HasFiniteIntegral (fun (a : α) => f a) μ
    theorem MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} (hf : ∫⁻ (x : α), f xμ ) :
    MeasureTheory.HasFiniteIntegral (fun (x : α) => (f x).toReal) μ
    theorem MeasureTheory.all_ae_ofReal_F_le_bound {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {F : αβ} {bound : α} (h : ∀ (n : ), ∀ᵐ (a : α) ∂μ, F n a bound a) (n : ) :
    ∀ᵐ (a : α) ∂μ, ENNReal.ofReal F n a ENNReal.ofReal (bound a)
    theorem MeasureTheory.all_ae_tendsto_ofReal_norm {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {F : αβ} {f : αβ} (h : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ) => F n a) Filter.atTop (nhds (f a))) :
    ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ) => ENNReal.ofReal F n a) Filter.atTop (nhds (ENNReal.ofReal f a))
    theorem MeasureTheory.all_ae_ofReal_f_le_bound {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {F : αβ} {f : αβ} {bound : α} (h_bound : ∀ (n : ), ∀ᵐ (a : α) ∂μ, F n a bound a) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ) => F n a) Filter.atTop (nhds (f a))) :
    ∀ᵐ (a : α) ∂μ, ENNReal.ofReal f a ENNReal.ofReal (bound a)
    theorem MeasureTheory.hasFiniteIntegral_of_dominated_convergence {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {F : αβ} {f : αβ} {bound : α} (bound_hasFiniteIntegral : MeasureTheory.HasFiniteIntegral bound μ) (h_bound : ∀ (n : ), ∀ᵐ (a : α) ∂μ, F n a bound a) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ) => F n a) Filter.atTop (nhds (f a))) :
    theorem MeasureTheory.tendsto_lintegral_norm_of_dominated_convergence {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {F : αβ} {f : αβ} {bound : α} (F_measurable : ∀ (n : ), MeasureTheory.AEStronglyMeasurable (F n) μ) (bound_hasFiniteIntegral : MeasureTheory.HasFiniteIntegral bound μ) (h_bound : ∀ (n : ), ∀ᵐ (a : α) ∂μ, F n a bound a) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ) => F n a) Filter.atTop (nhds (f a))) :
    Filter.Tendsto (fun (n : ) => ∫⁻ (a : α), ENNReal.ofReal F n a - f aμ) Filter.atTop (nhds 0)

    Lemmas used for defining the positive part of an function

    theorem MeasureTheory.HasFiniteIntegral.smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 β] [BoundedSMul 𝕜 β] (c : 𝕜) {f : αβ} :
    theorem MeasureTheory.hasFiniteIntegral_smul_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedRing 𝕜] [MulActionWithZero 𝕜 β] [BoundedSMul 𝕜 β] {c : 𝕜} (hc : IsUnit c) (f : αβ) :
    theorem MeasureTheory.HasFiniteIntegral.const_mul {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [NormedRing 𝕜] {f : α𝕜} (h : MeasureTheory.HasFiniteIntegral f μ) (c : 𝕜) :
    MeasureTheory.HasFiniteIntegral (fun (x : α) => c * f x) μ
    theorem MeasureTheory.HasFiniteIntegral.mul_const {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [NormedRing 𝕜] {f : α𝕜} (h : MeasureTheory.HasFiniteIntegral f μ) (c : 𝕜) :
    MeasureTheory.HasFiniteIntegral (fun (x : α) => f x * c) μ

    The predicate Integrable #

    def MeasureTheory.Integrable {β : Type u_2} [NormedAddCommGroup β] {α : Type u_5} :
    {x : MeasurableSpace α} → (αβ)autoParam (MeasureTheory.Measure α) _auto✝Prop

    Integrable f μ means that f is measurable and that the integral ∫⁻ a, ‖f a‖ ∂μ is finite. Integrable f means Integrable f volume.

    Equations
    Instances For
      theorem MeasureTheory.Integrable.mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : αβ} {g : αγ} (hg : MeasureTheory.Integrable g μ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (h : ∀ᵐ (a : α) ∂μ, f a g a) :
      theorem MeasureTheory.Integrable.mono' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} {g : α} (hg : MeasureTheory.Integrable g μ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (h : ∀ᵐ (a : α) ∂μ, f a g a) :
      theorem MeasureTheory.Integrable.congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : αβ} {g : αγ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (h : ∀ᵐ (a : α) ∂μ, f a = g a) :
      theorem MeasureTheory.integrable_congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : αβ} {g : αγ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (h : ∀ᵐ (a : α) ∂μ, f a = g a) :
      theorem MeasureTheory.Integrable.congr {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} {g : αβ} (hf : MeasureTheory.Integrable f μ) (h : f =ᵐ[μ] g) :
      theorem MeasureTheory.integrable_congr {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} {g : αβ} (h : f =ᵐ[μ] g) :
      theorem MeasureTheory.integrable_const_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {c : β} :
      MeasureTheory.Integrable (fun (x : α) => c) μ c = 0 μ Set.univ <
      @[simp]
      theorem MeasureTheory.integrable_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [MeasureTheory.IsFiniteMeasure μ] (c : β) :
      MeasureTheory.Integrable (fun (x : α) => c) μ
      @[simp]
      @[deprecated MeasureTheory.Integrable.of_finite]

      Alias of MeasureTheory.Integrable.of_finite.

      theorem MeasureTheory.Memℒp.integrable_norm_rpow {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} {p : ENNReal} (hf : MeasureTheory.Memℒp f p μ) (hp_ne_zero : p 0) (hp_ne_top : p ) :
      MeasureTheory.Integrable (fun (x : α) => f x ^ p.toReal) μ
      theorem MeasureTheory.Memℒp.integrable_norm_rpow' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [MeasureTheory.IsFiniteMeasure μ] {f : αβ} {p : ENNReal} (hf : MeasureTheory.Memℒp f p μ) :
      MeasureTheory.Integrable (fun (x : α) => f x ^ p.toReal) μ
      theorem MeasureTheory.Integrable.mono_measure {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} (h : MeasureTheory.Integrable f ν) (hμ : μ ν) :
      theorem MeasureTheory.Integrable.of_measure_le_smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {μ' : MeasureTheory.Measure α} (c : ENNReal) (hc : c ) (hμ'_le : μ' c μ) {f : αβ} (hf : MeasureTheory.Integrable f μ) :
      @[simp]
      theorem MeasureTheory.integrable_zero_measure {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] :
      ∀ {x : MeasurableSpace α} {f : αβ}, MeasureTheory.Integrable f 0
      theorem MeasureTheory.integrable_finset_sum_measure {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {ι : Type u_5} {m : MeasurableSpace α} {f : αβ} {μ : ιMeasureTheory.Measure α} {s : Finset ι} :
      MeasureTheory.Integrable f (is, μ i) is, MeasureTheory.Integrable f (μ i)
      theorem MeasureTheory.Integrable.smul_measure {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} (h : MeasureTheory.Integrable f μ) {c : ENNReal} (hc : c ) :
      theorem MeasureTheory.integrable_smul_measure {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} {c : ENNReal} (h₁ : c 0) (h₂ : c ) :
      theorem MeasureTheory.integrable_inv_smul_measure {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} {c : ENNReal} (h₁ : c 0) (h₂ : c ) :
      theorem MeasureTheory.Integrable.to_average {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} (h : MeasureTheory.Integrable f μ) :
      MeasureTheory.Integrable f ((μ Set.univ)⁻¹ μ)
      theorem MeasureTheory.Integrable.comp_aemeasurable {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace δ] [NormedAddCommGroup β] {f : αδ} {g : δβ} (hg : MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) :
      theorem MeasureTheory.Integrable.comp_measurable {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace δ] [NormedAddCommGroup β] {f : αδ} {g : δβ} (hg : MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ)) (hf : Measurable f) :
      theorem MeasureTheory.integrable_map_equiv {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace δ] [NormedAddCommGroup β] (f : α ≃ᵐ δ) (g : δβ) :
      theorem MeasureTheory.lintegral_edist_lt_top {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} {g : αβ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
      ∫⁻ (a : α), edist (f a) (g a)μ <
      @[simp]
      theorem MeasureTheory.integrable_zero (α : Type u_1) (β : Type u_2) {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [NormedAddCommGroup β] :
      MeasureTheory.Integrable (fun (x : α) => 0) μ
      theorem MeasureTheory.Integrable.add' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} {g : αβ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
      theorem MeasureTheory.Integrable.add {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} {g : αβ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
      theorem MeasureTheory.integrable_finset_sum' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {ι : Type u_5} (s : Finset ι) {f : ιαβ} (hf : is, MeasureTheory.Integrable (f i) μ) :
      MeasureTheory.Integrable (is, f i) μ
      theorem MeasureTheory.integrable_finset_sum {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {ι : Type u_5} (s : Finset ι) {f : ιαβ} (hf : is, MeasureTheory.Integrable (f i) μ) :
      MeasureTheory.Integrable (fun (a : α) => is, f i a) μ
      theorem MeasureTheory.Integrable.neg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} (hf : MeasureTheory.Integrable f μ) :
      @[simp]
      @[simp]
      theorem MeasureTheory.integrable_left_of_integrable_add_of_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {g : α} (h_meas : MeasureTheory.AEStronglyMeasurable f μ) (hf : 0 ≤ᵐ[μ] f) (hg : 0 ≤ᵐ[μ] g) (h_int : MeasureTheory.Integrable (f + g) μ) :
      theorem MeasureTheory.integrable_right_of_integrable_add_of_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} {g : α} (h_meas : MeasureTheory.AEStronglyMeasurable f μ) (hf : 0 ≤ᵐ[μ] f) (hg : 0 ≤ᵐ[μ] g) (h_int : MeasureTheory.Integrable (f + g) μ) :
      @[simp]
      theorem MeasureTheory.integrable_add_const_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [MeasureTheory.IsFiniteMeasure μ] {f : αβ} {c : β} :
      MeasureTheory.Integrable (fun (x : α) => f x + c) μ MeasureTheory.Integrable f μ
      @[simp]
      theorem MeasureTheory.integrable_const_add_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [MeasureTheory.IsFiniteMeasure μ] {f : αβ} {c : β} :
      MeasureTheory.Integrable (fun (x : α) => c + f x) μ MeasureTheory.Integrable f μ
      theorem MeasureTheory.Integrable.sub {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} {g : αβ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
      theorem MeasureTheory.Integrable.norm {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} (hf : MeasureTheory.Integrable f μ) :
      MeasureTheory.Integrable (fun (a : α) => f a) μ
      theorem MeasureTheory.Integrable.inf {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [NormedLatticeAddCommGroup β] {f : αβ} {g : αβ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
      theorem MeasureTheory.Integrable.sup {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [NormedLatticeAddCommGroup β] {f : αβ} {g : αβ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
      theorem MeasureTheory.Integrable.abs {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [NormedLatticeAddCommGroup β] {f : αβ} (hf : MeasureTheory.Integrable f μ) :
      MeasureTheory.Integrable (fun (a : α) => |f a|) μ
      theorem MeasureTheory.Integrable.bdd_mul {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {F : Type u_5} [NormedDivisionRing F] {f : αF} {g : αF} (hint : MeasureTheory.Integrable g μ) (hm : MeasureTheory.AEStronglyMeasurable f μ) (hfbdd : ∃ (C : ), ∀ (x : α), f x C) :
      MeasureTheory.Integrable (fun (x : α) => f x * g x) μ
      theorem MeasureTheory.Integrable.essSup_smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 β] {f : αβ} (hf : MeasureTheory.Integrable f μ) {g : α𝕜} (g_aestronglyMeasurable : MeasureTheory.AEStronglyMeasurable g μ) (ess_sup_g : essSup (fun (x : α) => g x‖₊) μ ) :
      MeasureTheory.Integrable (fun (x : α) => g x f x) μ

      Hölder's inequality for integrable functions: the scalar multiplication of an integrable vector-valued function by a scalar function with finite essential supremum is integrable.

      theorem MeasureTheory.Integrable.smul_essSup {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 β] [BoundedSMul 𝕜 β] {f : α𝕜} (hf : MeasureTheory.Integrable f μ) {g : αβ} (g_aestronglyMeasurable : MeasureTheory.AEStronglyMeasurable g μ) (ess_sup_g : essSup (fun (x : α) => g x‖₊) μ ) :
      MeasureTheory.Integrable (fun (x : α) => f x g x) μ

      Hölder's inequality for integrable functions: the scalar multiplication of an integrable scalar-valued function by a vector-value function with finite essential supremum is integrable.

      theorem MeasureTheory.integrable_of_norm_sub_le {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f₀ : αβ} {f₁ : αβ} {g : α} (hf₁_m : MeasureTheory.AEStronglyMeasurable f₁ μ) (hf₀_i : MeasureTheory.Integrable f₀ μ) (hg_i : MeasureTheory.Integrable g μ) (h : ∀ᵐ (a : α) ∂μ, f₀ a - f₁ a g a) :
      theorem MeasureTheory.Integrable.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : αβ} {g : αγ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
      MeasureTheory.Integrable (fun (x : α) => (f x, g x)) μ
      theorem MeasureTheory.Memℒp.integrable {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {q : ENNReal} (hq1 : 1 q) {f : αβ} [MeasureTheory.IsFiniteMeasure μ] (hfq : MeasureTheory.Memℒp f q μ) :
      theorem MeasureTheory.Integrable.measure_norm_ge_lt_top {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} (hf : MeasureTheory.Integrable f μ) {ε : } (hε : 0 < ε) :
      μ {x : α | ε f x} <

      A non-quantitative version of Markov inequality for integrable functions: the measure of points where ‖f x‖ ≥ ε is finite for all positive ε.

      theorem MeasureTheory.Integrable.measure_norm_gt_lt_top {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} (hf : MeasureTheory.Integrable f μ) {ε : } (hε : 0 < ε) :
      μ {x : α | ε < f x} <

      A non-quantitative version of Markov inequality for integrable functions: the measure of points where ‖f x‖ > ε is finite for all positive ε.

      theorem MeasureTheory.Integrable.measure_ge_lt_top {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : MeasureTheory.Integrable f μ) {ε : } (ε_pos : 0 < ε) :
      μ {a : α | ε f a} <

      If f is -valued and integrable, then for any c > 0 the set {x | f x ≥ c} has finite measure.

      theorem MeasureTheory.Integrable.measure_le_lt_top {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : MeasureTheory.Integrable f μ) {c : } (c_neg : c < 0) :
      μ {a : α | f a c} <

      If f is -valued and integrable, then for any c < 0 the set {x | f x ≤ c} has finite measure.

      theorem MeasureTheory.Integrable.measure_gt_lt_top {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : MeasureTheory.Integrable f μ) {ε : } (ε_pos : 0 < ε) :
      μ {a : α | ε < f a} <

      If f is -valued and integrable, then for any c > 0 the set {x | f x > c} has finite measure.

      theorem MeasureTheory.Integrable.measure_lt_lt_top {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : MeasureTheory.Integrable f μ) {c : } (c_neg : c < 0) :
      μ {a : α | f a < c} <

      If f is -valued and integrable, then for any c < 0 the set {x | f x < c} has finite measure.

      theorem MeasureTheory.LipschitzWith.integrable_comp_iff_of_antilipschitz {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {K : NNReal} {K' : NNReal} {f : αβ} {g : βγ} (hg : LipschitzWith K g) (hg' : AntilipschitzWith K' g) (g0 : g 0 = 0) :
      theorem MeasureTheory.Integrable.real_toNNReal {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : MeasureTheory.Integrable f μ) :
      MeasureTheory.Integrable (fun (x : α) => (f x).toNNReal) μ
      theorem MeasureTheory.ofReal_toReal_ae_eq {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} (hf : ∀ᵐ (x : α) ∂μ, f x < ) :
      (fun (x : α) => ENNReal.ofReal (f x).toReal) =ᵐ[μ] f
      theorem MeasureTheory.coe_toNNReal_ae_eq {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} (hf : ∀ᵐ (x : α) ∂μ, f x < ) :
      (fun (x : α) => (f x).toNNReal) =ᵐ[μ] f
      theorem MeasureTheory.hasFiniteIntegral_count_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup β] [MeasurableSingletonClass α] {f : αβ} :
      MeasureTheory.HasFiniteIntegral f MeasureTheory.Measure.count Summable fun (x : α) => f x

      A function has finite integral for the counting measure iff its norm is summable.

      theorem MeasureTheory.integrable_count_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup β] [MeasurableSingletonClass α] {f : αβ} :
      MeasureTheory.Integrable f MeasureTheory.Measure.count Summable fun (x : α) => f x

      A function is integrable for the counting measure iff its norm is summable.

      theorem MeasureTheory.integrable_withDensity_iff_integrable_coe_smul {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] [NormedSpace E] {f : αNNReal} (hf : Measurable f) {g : αE} :
      MeasureTheory.Integrable g (μ.withDensity fun (x : α) => (f x)) MeasureTheory.Integrable (fun (x : α) => (f x) g x) μ
      theorem MeasureTheory.integrable_withDensity_iff_integrable_smul {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] [NormedSpace E] {f : αNNReal} (hf : Measurable f) {g : αE} :
      MeasureTheory.Integrable g (μ.withDensity fun (x : α) => (f x)) MeasureTheory.Integrable (fun (x : α) => f x g x) μ
      theorem MeasureTheory.integrable_withDensity_iff_integrable_smul' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] [NormedSpace E] {f : αENNReal} (hf : Measurable f) (hflt : ∀ᵐ (x : α) ∂μ, f x < ) {g : αE} :
      MeasureTheory.Integrable g (μ.withDensity f) MeasureTheory.Integrable (fun (x : α) => (f x).toReal g x) μ
      theorem MeasureTheory.integrable_withDensity_iff_integrable_coe_smul₀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] [NormedSpace E] {f : αNNReal} (hf : AEMeasurable f μ) {g : αE} :
      MeasureTheory.Integrable g (μ.withDensity fun (x : α) => (f x)) MeasureTheory.Integrable (fun (x : α) => (f x) g x) μ
      theorem MeasureTheory.integrable_withDensity_iff_integrable_smul₀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] [NormedSpace E] {f : αNNReal} (hf : AEMeasurable f μ) {g : αE} :
      MeasureTheory.Integrable g (μ.withDensity fun (x : α) => (f x)) MeasureTheory.Integrable (fun (x : α) => f x g x) μ
      theorem MeasureTheory.integrable_withDensity_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} (hf : Measurable f) (hflt : ∀ᵐ (x : α) ∂μ, f x < ) {g : α} :
      MeasureTheory.Integrable g (μ.withDensity f) MeasureTheory.Integrable (fun (x : α) => g x * (f x).toReal) μ
      theorem MeasureTheory.memℒ1_smul_of_L1_withDensity {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] [NormedSpace E] {f : αNNReal} (f_meas : Measurable f) (u : (MeasureTheory.Lp E 1 (μ.withDensity fun (x : α) => (f x)))) :
      MeasureTheory.Memℒp (fun (x : α) => f x u x) 1 μ
      noncomputable def MeasureTheory.withDensitySMulLI {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {E : Type u_5} [NormedAddCommGroup E] [NormedSpace E] {f : αNNReal} (f_meas : Measurable f) :
      (MeasureTheory.Lp E 1 (μ.withDensity fun (x : α) => (f x))) →ₗᵢ[] (MeasureTheory.Lp E 1 μ)

      The map u ↦ f • u is an isometry between the L^1 spaces for μ.withDensity f and μ.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem MeasureTheory.withDensitySMulLI_apply {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {E : Type u_5} [NormedAddCommGroup E] [NormedSpace E] {f : αNNReal} (f_meas : Measurable f) (u : (MeasureTheory.Lp E 1 (μ.withDensity fun (x : α) => (f x)))) :
        (MeasureTheory.withDensitySMulLI μ f_meas) u = MeasureTheory.Memℒp.toLp (fun (x : α) => f x u x)
        theorem MeasureTheory.mem_ℒ1_toReal_of_lintegral_ne_top {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} (hfm : AEMeasurable f μ) (hfi : ∫⁻ (x : α), f xμ ) :
        MeasureTheory.Memℒp (fun (x : α) => (f x).toReal) 1 μ
        theorem MeasureTheory.integrable_toReal_of_lintegral_ne_top {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} (hfm : AEMeasurable f μ) (hfi : ∫⁻ (x : α), f xμ ) :
        MeasureTheory.Integrable (fun (x : α) => (f x).toReal) μ

        Lemmas used for defining the positive part of an function #

        theorem MeasureTheory.Integrable.pos_part {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : MeasureTheory.Integrable f μ) :
        MeasureTheory.Integrable (fun (a : α) => max (f a) 0) μ
        theorem MeasureTheory.Integrable.neg_part {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : MeasureTheory.Integrable f μ) :
        MeasureTheory.Integrable (fun (a : α) => max (-f a) 0) μ
        theorem MeasureTheory.Integrable.smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 β] [BoundedSMul 𝕜 β] (c : 𝕜) {f : αβ} (hf : MeasureTheory.Integrable f μ) :
        theorem IsUnit.integrable_smul_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 β] [BoundedSMul 𝕜 β] {c : 𝕜} (hc : IsUnit c) (f : αβ) :
        theorem MeasureTheory.integrable_smul_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedDivisionRing 𝕜] [Module 𝕜 β] [BoundedSMul 𝕜 β] {c : 𝕜} (hc : c 0) (f : αβ) :
        theorem MeasureTheory.Integrable.smul_of_top_right {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 β] [BoundedSMul 𝕜 β] {f : αβ} {φ : α𝕜} (hf : MeasureTheory.Integrable f μ) (hφ : MeasureTheory.Memℒp φ μ) :
        theorem MeasureTheory.Integrable.smul_of_top_left {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 β] [BoundedSMul 𝕜 β] {f : αβ} {φ : α𝕜} (hφ : MeasureTheory.Integrable φ μ) (hf : MeasureTheory.Memℒp f μ) :
        theorem MeasureTheory.Integrable.smul_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 β] [BoundedSMul 𝕜 β] {f : α𝕜} (hf : MeasureTheory.Integrable f μ) (c : β) :
        MeasureTheory.Integrable (fun (x : α) => f x c) μ
        theorem MeasureTheory.integrable_smul_const {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : α𝕜} {c : E} (hc : c 0) :
        theorem MeasureTheory.Integrable.const_mul {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [NormedRing 𝕜] {f : α𝕜} (h : MeasureTheory.Integrable f μ) (c : 𝕜) :
        MeasureTheory.Integrable (fun (x : α) => c * f x) μ
        theorem MeasureTheory.Integrable.const_mul' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [NormedRing 𝕜] {f : α𝕜} (h : MeasureTheory.Integrable f μ) (c : 𝕜) :
        MeasureTheory.Integrable ((fun (x : α) => c) * f) μ
        theorem MeasureTheory.Integrable.mul_const {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [NormedRing 𝕜] {f : α𝕜} (h : MeasureTheory.Integrable f μ) (c : 𝕜) :
        MeasureTheory.Integrable (fun (x : α) => f x * c) μ
        theorem MeasureTheory.Integrable.mul_const' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [NormedRing 𝕜] {f : α𝕜} (h : MeasureTheory.Integrable f μ) (c : 𝕜) :
        MeasureTheory.Integrable (f * fun (x : α) => c) μ
        theorem MeasureTheory.integrable_const_mul_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [NormedRing 𝕜] {c : 𝕜} (hc : IsUnit c) (f : α𝕜) :
        MeasureTheory.Integrable (fun (x : α) => c * f x) μ MeasureTheory.Integrable f μ
        theorem MeasureTheory.integrable_mul_const_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [NormedRing 𝕜] {c : 𝕜} (hc : IsUnit c) (f : α𝕜) :
        MeasureTheory.Integrable (fun (x : α) => f x * c) μ MeasureTheory.Integrable f μ
        theorem MeasureTheory.Integrable.bdd_mul' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [NormedRing 𝕜] {f : α𝕜} {g : α𝕜} {c : } (hg : MeasureTheory.Integrable g μ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hf_bound : ∀ᵐ (x : α) ∂μ, f x c) :
        MeasureTheory.Integrable (fun (x : α) => f x * g x) μ
        theorem MeasureTheory.Integrable.div_const {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [NormedDivisionRing 𝕜] {f : α𝕜} (h : MeasureTheory.Integrable f μ) (c : 𝕜) :
        MeasureTheory.Integrable (fun (x : α) => f x / c) μ
        theorem MeasureTheory.Integrable.ofReal {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [RCLike 𝕜] {f : α} (hf : MeasureTheory.Integrable f μ) :
        MeasureTheory.Integrable (fun (x : α) => (f x)) μ
        theorem MeasureTheory.Integrable.re_im_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [RCLike 𝕜] {f : α𝕜} :
        MeasureTheory.Integrable (fun (x : α) => RCLike.re (f x)) μ MeasureTheory.Integrable (fun (x : α) => RCLike.im (f x)) μ MeasureTheory.Integrable f μ
        theorem MeasureTheory.Integrable.re {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [RCLike 𝕜] {f : α𝕜} (hf : MeasureTheory.Integrable f μ) :
        MeasureTheory.Integrable (fun (x : α) => RCLike.re (f x)) μ
        theorem MeasureTheory.Integrable.im {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [RCLike 𝕜] {f : α𝕜} (hf : MeasureTheory.Integrable f μ) :
        MeasureTheory.Integrable (fun (x : α) => RCLike.im (f x)) μ
        theorem MeasureTheory.Integrable.trim {α : Type u_1} {m : MeasurableSpace α} {H : Type u_5} [NormedAddCommGroup H] {m0 : MeasurableSpace α} {μ' : MeasureTheory.Measure α} {f : αH} (hm : m m0) (hf_int : MeasureTheory.Integrable f μ') (hf : MeasureTheory.StronglyMeasurable f) :
        MeasureTheory.Integrable f (μ'.trim hm)
        theorem MeasureTheory.integrable_of_integrable_trim {α : Type u_1} {m : MeasurableSpace α} {H : Type u_5} [NormedAddCommGroup H] {m0 : MeasurableSpace α} {μ' : MeasureTheory.Measure α} {f : αH} (hm : m m0) (hf_int : MeasureTheory.Integrable f (μ'.trim hm)) :
        theorem MeasureTheory.integrable_of_forall_fin_meas_le' {α : Type u_1} {m : MeasurableSpace α} {E : Type u_5} {m0 : MeasurableSpace α} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} (hm : m m0) [MeasureTheory.SigmaFinite (μ.trim hm)] (C : ENNReal) (hC : C < ) {f : αE} (hf_meas : MeasureTheory.AEStronglyMeasurable f μ) (hf : ∀ (s : Set α), MeasurableSet sμ s ∫⁻ (x : α) in s, f x‖₊μ C) :
        theorem MeasureTheory.integrable_of_forall_fin_meas_le {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] [MeasureTheory.SigmaFinite μ] (C : ENNReal) (hC : C < ) {f : αE} (hf_meas : MeasureTheory.AEStronglyMeasurable f μ) (hf : ∀ (s : Set α), MeasurableSet sμ s ∫⁻ (x : α) in s, f x‖₊μ C) :

        The predicate Integrable on measurable functions modulo a.e.-equality #

        def MeasureTheory.AEEqFun.Integrable {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : α →ₘ[μ] β) :

        A class of almost everywhere equal functions is Integrable if its function representative is integrable.

        Equations
        Instances For
          theorem MeasureTheory.AEEqFun.integrable_coeFn {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α →ₘ[μ] β} :
          MeasureTheory.Integrable (f) μ f.Integrable
          theorem MeasureTheory.AEEqFun.Integrable.neg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α →ₘ[μ] β} :
          f.Integrable(-f).Integrable
          theorem MeasureTheory.AEEqFun.integrable_iff_mem_L1 {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α →ₘ[μ] β} :
          f.Integrable f MeasureTheory.Lp β 1 μ
          theorem MeasureTheory.AEEqFun.Integrable.add {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α →ₘ[μ] β} {g : α →ₘ[μ] β} :
          f.Integrableg.Integrable(f + g).Integrable
          theorem MeasureTheory.AEEqFun.Integrable.sub {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α →ₘ[μ] β} {g : α →ₘ[μ] β} (hf : f.Integrable) (hg : g.Integrable) :
          (f - g).Integrable
          theorem MeasureTheory.AEEqFun.Integrable.smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 β] [BoundedSMul 𝕜 β] {c : 𝕜} {f : α →ₘ[μ] β} :
          f.Integrable(c f).Integrable
          theorem MeasureTheory.L1.integrable_coeFn {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : (MeasureTheory.Lp β 1 μ)) :
          theorem MeasureTheory.L1.aemeasurable_coeFn {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [MeasurableSpace β] [BorelSpace β] (f : (MeasureTheory.Lp β 1 μ)) :
          AEMeasurable (f) μ
          theorem MeasureTheory.L1.edist_def {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : (MeasureTheory.Lp β 1 μ)) (g : (MeasureTheory.Lp β 1 μ)) :
          edist f g = ∫⁻ (a : α), edist (f a) (g a)μ
          theorem MeasureTheory.L1.dist_def {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : (MeasureTheory.Lp β 1 μ)) (g : (MeasureTheory.Lp β 1 μ)) :
          dist f g = (∫⁻ (a : α), edist (f a) (g a)μ).toReal
          theorem MeasureTheory.L1.norm_def {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : (MeasureTheory.Lp β 1 μ)) :
          f = (∫⁻ (a : α), f a‖₊μ).toReal
          theorem MeasureTheory.L1.norm_sub_eq_lintegral {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : (MeasureTheory.Lp β 1 μ)) (g : (MeasureTheory.Lp β 1 μ)) :
          f - g = (∫⁻ (x : α), f x - g x‖₊μ).toReal

          Computing the norm of a difference between two L¹-functions. Note that this is not a special case of norm_def since (f - g) x and f x - g x are not equal (but only a.e.-equal).

          theorem MeasureTheory.L1.ofReal_norm_eq_lintegral {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : (MeasureTheory.Lp β 1 μ)) :
          ENNReal.ofReal f = ∫⁻ (x : α), f x‖₊μ
          theorem MeasureTheory.L1.ofReal_norm_sub_eq_lintegral {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : (MeasureTheory.Lp β 1 μ)) (g : (MeasureTheory.Lp β 1 μ)) :
          ENNReal.ofReal f - g = ∫⁻ (x : α), f x - g x‖₊μ

          Computing the norm of a difference between two L¹-functions. Note that this is not a special case of ofReal_norm_eq_lintegral since (f - g) x and f x - g x are not equal (but only a.e.-equal).

          def MeasureTheory.Integrable.toL1 {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : αβ) (hf : MeasureTheory.Integrable f μ) :
          (MeasureTheory.Lp β 1 μ)

          Construct the equivalence class [f] of an integrable function f, as a member of the space L1 β 1 μ.

          Equations
          Instances For
            @[simp]
            theorem MeasureTheory.Integrable.toL1_coeFn {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : (MeasureTheory.Lp β 1 μ)) (hf : MeasureTheory.Integrable (f) μ) :
            theorem MeasureTheory.Integrable.coeFn_toL1 {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} (hf : MeasureTheory.Integrable f μ) :
            theorem MeasureTheory.Integrable.norm_toL1 {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : αβ) (hf : MeasureTheory.Integrable f μ) :
            MeasureTheory.Integrable.toL1 f hf = (∫⁻ (a : α), edist (f a) 0μ).toReal
            theorem MeasureTheory.Integrable.nnnorm_toL1 {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : αβ} (hf : MeasureTheory.Integrable f μ) :
            MeasureTheory.Integrable.toL1 f hf‖₊ = ∫⁻ (a : α), f a‖₊μ
            @[simp]
            theorem MeasureTheory.Integrable.edist_toL1_toL1 {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : αβ) (g : αβ) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) :
            edist (MeasureTheory.Integrable.toL1 f hf) (MeasureTheory.Integrable.toL1 g hg) = ∫⁻ (a : α), edist (f a) (g a)μ
            @[simp]
            theorem MeasureTheory.Integrable.edist_toL1_zero {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : αβ) (hf : MeasureTheory.Integrable f μ) :
            edist (MeasureTheory.Integrable.toL1 f hf) 0 = ∫⁻ (a : α), edist (f a) 0μ
            theorem MeasureTheory.Integrable.toL1_smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 β] [BoundedSMul 𝕜 β] (f : αβ) (hf : MeasureTheory.Integrable f μ) (k : 𝕜) :
            theorem MeasureTheory.Integrable.toL1_smul' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 β] [BoundedSMul 𝕜 β] (f : αβ) (hf : MeasureTheory.Integrable f μ) (k : 𝕜) :
            theorem MeasureTheory.Integrable.restrict {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] {f : αE} (f_intble : MeasureTheory.Integrable f μ) {s : Set α} :
            MeasureTheory.Integrable f (μ.restrict s)
            theorem ContinuousLinearMap.integrable_comp {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {φ : αH} (L : H →L[𝕜] E) (φ_int : MeasureTheory.Integrable φ μ) :
            MeasureTheory.Integrable (fun (a : α) => L (φ a)) μ
            @[simp]
            theorem ContinuousLinearEquiv.integrable_comp_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {φ : αH} (L : H ≃L[𝕜] E) :
            MeasureTheory.Integrable (fun (a : α) => L (φ a)) μ MeasureTheory.Integrable φ μ
            @[simp]
            theorem LinearIsometryEquiv.integrable_comp_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {φ : αH} (L : H ≃ₗᵢ[𝕜] E) :
            MeasureTheory.Integrable (fun (a : α) => L (φ a)) μ MeasureTheory.Integrable φ μ
            theorem MeasureTheory.Integrable.apply_continuousLinearMap {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {φ : αH →L[𝕜] E} (φ_int : MeasureTheory.Integrable φ μ) (v : H) :
            MeasureTheory.Integrable (fun (a : α) => (φ a) v) μ
            theorem MeasureTheory.Integrable.fst {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {f : αE × F} (hf : MeasureTheory.Integrable f μ) :
            MeasureTheory.Integrable (fun (x : α) => (f x).1) μ
            theorem MeasureTheory.Integrable.snd {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {f : αE × F} (hf : MeasureTheory.Integrable f μ) :
            MeasureTheory.Integrable (fun (x : α) => (f x).2) μ
            theorem MeasureTheory.integrable_prod {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {f : αE × F} :
            MeasureTheory.Integrable f μ MeasureTheory.Integrable (fun (x : α) => (f x).1) μ MeasureTheory.Integrable (fun (x : α) => (f x).2) μ