Integrability results #
theorem
MeasureTheory.integrable_toReal_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
(hf : AEMeasurable f μ)
(hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤)
:
MeasureTheory.Integrable (fun (x : α) => (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ⊤
theorem
MeasureTheory.Integrable.neg'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (x : α) => -f x) μ
@[simp]
theorem
MeasureTheory.integrable_add_iff_integrable_left'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → β}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (x : α) => g x + f x) μ ↔ MeasureTheory.Integrable g μ
@[simp]
theorem
MeasureTheory.integrable_add_iff_integrable_right'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → β}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (x : α) => f x + g x) μ ↔ MeasureTheory.Integrable g μ
theorem
MeasureTheory.Integrable.rnDeriv_smul
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[μ.HaveLebesgueDecomposition ν]
(hμν : μ.AbsolutelyContinuous ν)
[MeasureTheory.SigmaFinite μ]
{f : α → E}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal • f x) ν
theorem
MeasureTheory.integrable_of_le_of_le
{α : Type u_3}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
{g₁ : α → ℝ}
{g₂ : α → ℝ}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(h_le₁ : g₁ ≤ᵐ[μ] f)
(h_le₂ : f ≤ᵐ[μ] g₂)
(h_int₁ : MeasureTheory.Integrable g₁ μ)
(h_int₂ : MeasureTheory.Integrable g₂ μ)
: