# Integrable functions #

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

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

## Main definition #

- Let `f : α → β` be a function, where `α` is a `MeasureSpace` and `β` a `NormedAddCommGroup` which also a `MeasurableSpace`. Then `f` is called `Integrable` if `f` is `Measurable` and `HasFiniteIntegral f` holds.

## Implementation notes #

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

## Tags #

integrable

### The predicate `Integrable` #

source
def MeasureTheory.Integrable {ε : Type u_5} [TopologicalSpace ε] [ContinuousENorm ε] {α : Type u_8} {x✝ : MeasurableSpace α} (f : α → ε) (μ : Measure α := by volume_tac) :
Prop

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

Equations

- MeasureTheory.Integrable f μ = (MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.HasFiniteIntegral f μ)

Instances For

source
def MeasureTheory.«termIntegrable[_]» :
Lean.ParserDescr

Notation for `Integrable` with respect to a non-standard σ-algebra.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem MeasureTheory.memLp_one_iff_integrable {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} :
MemLp f 1 μ ↔ Integrable f μ
source
theorem MeasureTheory.Integrable.aestronglyMeasurable {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (hf : Integrable f μ) :
AEStronglyMeasurable f μ
source
theorem MeasureTheory.Integrable.aemeasurable {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] [MeasurableSpace ε] [BorelSpace ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : α → ε} (hf : Integrable f μ) :
AEMeasurable f μ
source
theorem MeasureTheory.Integrable.hasFiniteIntegral {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (hf : Integrable f μ) :
HasFiniteIntegral f μ
source
theorem MeasureTheory.Integrable.mono_enorm {α : Type u_1} {ε : Type u_5} {ε' : Type u_6} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] [TopologicalSpace ε'] [ContinuousENorm ε'] {f : α → ε} {g : α → ε'} (hg : Integrable g μ) (hf : AEStronglyMeasurable f μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ ‖g a‖ₑ) :
Integrable f μ
source
theorem MeasureTheory.Integrable.mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : α → β} {g : α → γ} (hg : Integrable g μ) (hf : AEStronglyMeasurable f μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖) :
Integrable f μ
source
theorem MeasureTheory.Integrable.mono'_enorm {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} {g : α → ENNReal} (hg : Integrable g μ) (hf : AEStronglyMeasurable f μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ g a) :
Integrable f μ
source
theorem MeasureTheory.Integrable.mono' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} {g : α → ℝ} (hg : Integrable g μ) (hf : AEStronglyMeasurable f μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a) :
Integrable f μ
source
theorem MeasureTheory.Integrable.congr'_enorm {α : Type u_1} {ε : Type u_5} {ε' : Type u_6} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] [TopologicalSpace ε'] [ContinuousENorm ε'] {f : α → ε} {g : α → ε'} (hf : Integrable f μ) (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) :
Integrable g μ
source
theorem MeasureTheory.Integrable.congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : α → β} {g : α → γ} (hf : Integrable f μ) (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) :
Integrable g μ
source
theorem MeasureTheory.integrable_congr'_enorm {α : Type u_1} {ε : Type u_5} {ε' : Type u_6} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] [TopologicalSpace ε'] [ContinuousENorm ε'] {f : α → ε} {g : α → ε'} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) :
Integrable f μ ↔ Integrable g μ
source
theorem MeasureTheory.integrable_congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : α → β} {g : α → γ} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) :
Integrable f μ ↔ Integrable g μ
source
theorem MeasureTheory.Integrable.congr {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f g : α → ε} (hf : Integrable f μ) (h : f =ᶠ[ae μ] g) :
Integrable g μ
source
theorem MeasureTheory.integrable_congr {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f g : α → ε} (h : f =ᶠ[ae μ] g) :
Integrable f μ ↔ Integrable g μ
source
theorem MeasureTheory.integrable_const_iff_enorm {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {c : ε} (hc : ‖c‖ₑ ≠ ⊤) :
Integrable (fun (x : α) => c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ
source
theorem MeasureTheory.integrable_const_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {c : β} :
Integrable (fun (x : α) => c) μ ↔ c = 0 ∨ IsFiniteMeasure μ
source
theorem MeasureTheory.integrable_const_iff_isFiniteMeasure_enorm {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {c : ε} (hc : ‖c‖ₑ ≠ 0) (hc' : ‖c‖ₑ ≠ ⊤) :
Integrable (fun (x : α) => c) μ ↔ IsFiniteMeasure μ
source
theorem MeasureTheory.integrable_const_iff_isFiniteMeasure {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {c : β} (hc : c ≠ 0) :
Integrable (fun (x : α) => c) μ ↔ IsFiniteMeasure μ
source
theorem MeasureTheory.Integrable.of_mem_Icc_enorm {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) {X : α → ENNReal} (hX : AEMeasurable X μ) (h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Set.Icc a b) :
Integrable X μ
source
theorem MeasureTheory.Integrable.of_mem_Icc {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] (a b : ℝ) {X : α → ℝ} (hX : AEMeasurable X μ) (h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Set.Icc a b) :
Integrable X μ
source
@[simp]
theorem MeasureTheory.integrable_const_enorm {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] [IsFiniteMeasure μ] {c : ε} (hc : ‖c‖ₑ ≠ ⊤) :
Integrable (fun (x : α) => c) μ
source
theorem MeasureTheory.integrable_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [IsFiniteMeasure μ] (c : β) :
Integrable (fun (x : α) => c) μ
source
@[simp]
theorem MeasureTheory.Integrable.of_finite {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [Finite α] [MeasurableSingletonClass α] [IsFiniteMeasure μ] {f : α → β} :
Integrable f μ
source
theorem MeasureTheory.Integrable.of_isEmpty {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [IsEmpty α] {f : α → β} :
Integrable f μ

This lemma is a special case of `Integrable.of_finite`.

source
theorem MeasureTheory.Integrable.of_subsingleton {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [Subsingleton α] [IsFiniteMeasure μ] {f : α → β} :
Integrable f μ

This lemma is a special case of `Integrable.of_finite`.

source
theorem MeasureTheory.MemLp.integrable_enorm_rpow {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} {p : ENNReal} (hf : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) :
Integrable (fun (x : α) => ‖f x‖ₑ ^ p.toReal) μ
source
theorem MeasureTheory.MemLp.integrable_norm_rpow {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} {p : ENNReal} (hf : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) :
Integrable (fun (x : α) => ‖f x‖ ^ p.toReal) μ
source
theorem MeasureTheory.MemLp.integrable_enorm_rpow' {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] [IsFiniteMeasure μ] {f : α → ε} {p : ENNReal} (hf : MemLp f p μ) :
Integrable (fun (x : α) => ‖f x‖ₑ ^ p.toReal) μ
source
theorem MeasureTheory.MemLp.integrable_norm_rpow' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [IsFiniteMeasure μ] {f : α → β} {p : ENNReal} (hf : MemLp f p μ) :
Integrable (fun (x : α) => ‖f x‖ ^ p.toReal) μ
source
theorem MeasureTheory.MemLp.integrable_enorm_pow {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} {p : ℕ} (hf : MemLp f (↑p) μ) (hp : p ≠ 0) :
Integrable (fun (x : α) => ‖f x‖ₑ ^ p) μ
source
theorem MeasureTheory.MemLp.integrable_norm_pow {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} {p : ℕ} (hf : MemLp f (↑p) μ) (hp : p ≠ 0) :
Integrable (fun (x : α) => ‖f x‖ ^ p) μ
source
theorem MeasureTheory.MemLp.integrable_enorm_pow' {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] [IsFiniteMeasure μ] {f : α → ε} {p : ℕ} (hf : MemLp f (↑p) μ) :
Integrable (fun (x : α) => ‖f x‖ₑ ^ p) μ
source
theorem MeasureTheory.MemLp.integrable_norm_pow' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [IsFiniteMeasure μ] {f : α → β} {p : ℕ} (hf : MemLp f (↑p) μ) :
Integrable (fun (x : α) => ‖f x‖ ^ p) μ
source
theorem MeasureTheory.integrable_enorm_rpow_iff {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} {p : ENNReal} (hf : AEStronglyMeasurable f μ) (p_zero : p ≠ 0) (p_top : p ≠ ⊤) :
Integrable (fun (x : α) => ‖f x‖ₑ ^ p.toReal) μ ↔ MemLp f p μ
source
theorem MeasureTheory.integrable_norm_rpow_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} {p : ENNReal} (hf : AEStronglyMeasurable f μ) (p_zero : p ≠ 0) (p_top : p ≠ ⊤) :
Integrable (fun (x : α) => ‖f x‖ ^ p.toReal) μ ↔ MemLp f p μ
source
theorem MeasureTheory.Integrable.mono_measure {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ ν : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (h : Integrable f ν) (hμ : μ ≤ ν) :
Integrable f μ
source
theorem MeasureTheory.Integrable.of_measure_le_smul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_8} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {μ' : Measure α} {c : ENNReal} (hc : c ≠ ⊤) (hμ'_le : μ' ≤ c • μ) {f : α → ε} (hf : Integrable f μ) :
Integrable f μ'
source
theorem MeasureTheory.Integrable.add_measure {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ ν : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : α → ε} (hμ : Integrable f μ) (hν : Integrable f ν) :
Integrable f (μ + ν)
source
theorem MeasureTheory.Integrable.left_of_add_measure {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ ν : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (h : Integrable f (μ + ν)) :
Integrable f μ
source
theorem MeasureTheory.Integrable.right_of_add_measure {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ ν : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (h : Integrable f (μ + ν)) :
Integrable f ν
source
@[simp]
theorem MeasureTheory.integrable_add_measure {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ ν : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : α → ε} :
Integrable f (μ + ν) ↔ Integrable f μ ∧ Integrable f ν
source
@[simp]
theorem MeasureTheory.integrable_zero_measure {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} :
Integrable f 0
source
theorem MeasureTheory.integrable_dirac {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} [TopologicalSpace ε] [ContinuousENorm ε] [MeasurableSingletonClass α] {a : α} {f : α → ε} (hfa : ‖f a‖ₑ < ⊤) :
Integrable f (Measure.dirac a)

In a measurable space with measurable singletons, every function is integrable with respect to a Dirac measure. See `integrable_dirac'` for a version which requires `f` to be strongly measurable but does not need singletons to be measurable.

source
theorem MeasureTheory.integrable_dirac' {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} [TopologicalSpace ε] [ContinuousENorm ε] {a : α} {f : α → ε} (hf : StronglyMeasurable f) (hfa : ‖f a‖ₑ < ⊤) :
Integrable f (Measure.dirac a)

Every strongly measurable function is integrable with respect to a Dirac measure. See `integrable_dirac` for a version which requires that singletons are measurable sets but has no hypothesis on `f`.

source
theorem MeasureTheory.integrable_finset_sum_measure {α : Type u_1} {ε : Type u_5} [TopologicalSpace ε] [ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε] {ι : Type u_8} {m : MeasurableSpace α} {f : α → ε} {μ : ι → Measure α} {s : Finset ι} :
Integrable f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)
source
theorem MeasureTheory.Integrable.smul_measure {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_8} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} (h : Integrable f μ) {c : ENNReal} (hc : c ≠ ⊤) :
Integrable f (c • μ)
source
theorem MeasureTheory.Integrable.smul_measure_nnreal {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_8} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} (h : Integrable f μ) {c : NNReal} :
Integrable f (c • μ)
source
theorem MeasureTheory.integrable_smul_measure {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_8} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} {c : ENNReal} (h₁ : c ≠ 0) (h₂ : c ≠ ⊤) :
Integrable f (c • μ) ↔ Integrable f μ
source
theorem MeasureTheory.integrable_inv_smul_measure {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_8} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} {c : ENNReal} (h₁ : c ≠ 0) (h₂ : c ≠ ⊤) :
Integrable f (c⁻¹ • μ) ↔ Integrable f μ
source
theorem MeasureTheory.Integrable.to_average {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_8} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} (h : Integrable f μ) :
Integrable f ((μ Set.univ)⁻¹ • μ)
source
theorem MeasureTheory.integrable_average {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_8} [TopologicalSpace ε] [ESeminormedAddMonoid ε] [IsFiniteMeasure μ] {f : α → ε} :
Integrable f ((μ Set.univ)⁻¹ • μ) ↔ Integrable f μ
source
theorem MeasureTheory.integrable_map_measure {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {α' : Type u_8} [MeasurableSpace α'] {f : α → α'} {g : α' → ε} (hg : AEStronglyMeasurable g (Measure.map f μ)) (hf : AEMeasurable f μ) :
Integrable g (Measure.map f μ) ↔ Integrable (g ∘ f) μ
source
theorem MeasureTheory.Integrable.comp_aemeasurable {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {α' : Type u_8} [MeasurableSpace α'] {f : α → α'} {g : α' → ε} (hg : Integrable g (Measure.map f μ)) (hf : AEMeasurable f μ) :
Integrable (g ∘ f) μ
source
theorem MeasureTheory.Integrable.comp_measurable {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {α' : Type u_8} [MeasurableSpace α'] {f : α → α'} {g : α' → ε} (hg : Integrable g (Measure.map f μ)) (hf : Measurable f) :
Integrable (g ∘ f) μ
source
theorem MeasurableEmbedding.integrable_map_iff {α : Type u_1} {δ : Type u_4} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace δ] [TopologicalSpace ε] [ContinuousENorm ε] {f : α → δ} (hf : MeasurableEmbedding f) {g : δ → ε} :
MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Integrable (g ∘ f) μ
source
theorem MeasureTheory.integrable_map_equiv {α : Type u_1} {δ : Type u_4} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [MeasurableSpace δ] [TopologicalSpace ε] [ContinuousENorm ε] (f : α ≃ᵐ δ) (g : δ → ε) :
Integrable g (Measure.map (⇑f) μ) ↔ Integrable (g ∘ ⇑f) μ
source
theorem MeasureTheory.MeasurePreserving.integrable_comp {α : Type u_1} {δ : Type u_4} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [MeasurableSpace δ] [TopologicalSpace ε] [ContinuousENorm ε] {ν : Measure δ} {g : δ → ε} {f : α → δ} (hf : MeasurePreserving f μ ν) (hg : AEStronglyMeasurable g ν) :
Integrable (g ∘ f) μ ↔ Integrable g ν
source
theorem MeasureTheory.MeasurePreserving.integrable_comp_of_integrable {α : Type u_1} {δ : Type u_4} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [MeasurableSpace δ] [TopologicalSpace ε] [ContinuousENorm ε] {ν : Measure δ} {g : δ → ε} {f : α → δ} (hf : MeasurePreserving f μ ν) (hg : Integrable g ν) :
Integrable (g ∘ f) μ
source
theorem MeasureTheory.MeasurePreserving.integrable_comp_emb {α : Type u_1} {δ : Type u_4} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [MeasurableSpace δ] [TopologicalSpace ε] [ContinuousENorm ε] {f : α → δ} {ν : Measure δ} (h₁ : MeasurePreserving f μ ν) (h₂ : MeasurableEmbedding f) {g : δ → ε} :
Integrable (g ∘ f) μ ↔ Integrable g ν
source
theorem MeasureTheory.lintegral_edist_lt_top {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f g : α → β} (hf : Integrable f μ) (hg : Integrable g μ) :
∫⁻ (a : α), edist (f a) (g a) ∂μ < ⊤
source
@[simp]
theorem MeasureTheory.integrable_zero (α : Type u_1) {m : MeasurableSpace α} (ε' : Type u_8) [TopologicalSpace ε'] [ESeminormedAddMonoid ε'] (μ : Measure α) :
Integrable (fun (x : α) => 0) μ
source
theorem MeasureTheory.Integrable.add' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε' : Type u_8} [TopologicalSpace ε'] [ESeminormedAddMonoid ε'] {f g : α → ε'} (hf : Integrable f μ) (hg : Integrable g μ) :
HasFiniteIntegral (f + g) μ
source
theorem MeasureTheory.Integrable.add {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε' : Type u_8} [TopologicalSpace ε'] [ESeminormedAddMonoid ε'] [ContinuousAdd ε'] {f g : α → ε'} (hf : Integrable f μ) (hg : Integrable g μ) :
Integrable (f + g) μ
source
theorem MeasureTheory.Integrable.add'' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε' : Type u_8} [TopologicalSpace ε'] [ESeminormedAddMonoid ε'] [ContinuousAdd ε'] {f g : α → ε'} (hf : Integrable f μ) (hg : Integrable g μ) :
Integrable (fun (x : α) => f x + g x) μ
source
@[simp]
theorem MeasureTheory.Integrable.of_subsingleton_codomain {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε' : Type u_8} [TopologicalSpace ε'] [ESeminormedAddMonoid ε'] [Subsingleton ε'] {f : α → ε'} :
Integrable f μ
source
theorem MeasureTheory.integrable_finset_sum' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε' : Type u_8} [TopologicalSpace ε'] [ESeminormedAddCommMonoid ε'] [ContinuousAdd ε'] {ι : Type u_9} (s : Finset ι) {f : ι → α → ε'} (hf : ∀ i ∈ s, Integrable (f i) μ) :
Integrable (∑ i ∈ s, f i) μ
source
theorem MeasureTheory.integrable_finset_sum {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε' : Type u_8} [TopologicalSpace ε'] [ESeminormedAddCommMonoid ε'] [ContinuousAdd ε'] {ι : Type u_9} (s : Finset ι) {f : ι → α → ε'} (hf : ∀ i ∈ s, Integrable (f i) μ) :
Integrable (fun (a : α) => ∑ i ∈ s, f i a) μ
source
theorem MeasureTheory.Integrable.neg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} (hf : Integrable f μ) :
Integrable (-f) μ

If `f` is integrable, then so is `-f`. See `Integrable.neg'` for the same statement, but formulated with `x ↦ - f x` instead of `-f`.

source
theorem MeasureTheory.Integrable.neg' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} (hf : Integrable f μ) :
Integrable (fun (x : α) => -f x) μ

If `f` is integrable, then so is `fun x ↦ - f x`. See `Integrable.neg` for the same statement, but formulated with `-f` instead of `fun x ↦ - f x`.

source
@[simp]
theorem MeasureTheory.integrable_neg_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} :
Integrable (-f) μ ↔ Integrable f μ
source
@[simp]
theorem MeasureTheory.integrable_add_iff_integrable_right {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f g : α → β} (hf : Integrable f μ) :
Integrable (f + g) μ ↔ Integrable g μ

if `f` is integrable, then `f + g` is integrable iff `g` is. See `integrable_add_iff_integrable_right'` for the same statement with `fun x ↦ f x + g x` instead of `f + g`.

source
@[simp]
theorem MeasureTheory.integrable_add_iff_integrable_right' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f g : α → β} (hf : Integrable f μ) :
Integrable (fun (x : α) => f x + g x) μ ↔ Integrable g μ

if `f` is integrable, then `fun x ↦ f x + g x` is integrable iff `g` is. See `integrable_add_iff_integrable_right` for the same statement with `f + g` instead of `fun x ↦ f x + g x`.

source
@[simp]
theorem MeasureTheory.integrable_add_iff_integrable_left {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f g : α → β} (hf : Integrable f μ) :
Integrable (g + f) μ ↔ Integrable g μ

if `f` is integrable, then `g + f` is integrable iff `g` is. See `integrable_add_iff_integrable_left'` for the same statement with `fun x ↦ g x + f x` instead of `g + f`.

source
@[simp]
theorem MeasureTheory.integrable_add_iff_integrable_left' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f g : α → β} (hf : Integrable f μ) :
Integrable (fun (x : α) => g x + f x) μ ↔ Integrable g μ

if `f` is integrable, then `fun x ↦ g x + f x` is integrable iff `g` is. See `integrable_add_iff_integrable_left'` for the same statement with `g + f` instead of `fun x ↦ g x + f x`.

source
theorem MeasureTheory.integrable_left_of_integrable_add_of_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f g : α → ℝ} (h_meas : AEStronglyMeasurable f μ) (hf : 0 ≤ᶠ[ae μ] f) (hg : 0 ≤ᶠ[ae μ] g) (h_int : Integrable (f + g) μ) :
Integrable f μ
source
theorem MeasureTheory.integrable_right_of_integrable_add_of_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f g : α → ℝ} (h_meas : AEStronglyMeasurable f μ) (hf : 0 ≤ᶠ[ae μ] f) (hg : 0 ≤ᶠ[ae μ] g) (h_int : Integrable (f + g) μ) :
Integrable g μ
source
theorem MeasureTheory.integrable_add_iff_of_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f g : α → ℝ} (h_meas : AEStronglyMeasurable f μ) (hf : 0 ≤ᶠ[ae μ] f) (hg : 0 ≤ᶠ[ae μ] g) :
Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ
source
theorem MeasureTheory.integrable_add_iff_of_nonpos {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f g : α → ℝ} (h_meas : AEStronglyMeasurable f μ) (hf : f ≤ᶠ[ae μ] 0) (hg : g ≤ᶠ[ae μ] 0) :
Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ
source
theorem MeasureTheory.integrable_add_const_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [IsFiniteMeasure μ] {f : α → β} {c : β} :
Integrable (fun (x : α) => f x + c) μ ↔ Integrable f μ
source
theorem MeasureTheory.integrable_const_add_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [IsFiniteMeasure μ] {f : α → β} {c : β} :
Integrable (fun (x : α) => c + f x) μ ↔ Integrable f μ
source
theorem MeasureTheory.Integrable.sub {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f g : α → β} (hf : Integrable f μ) (hg : Integrable g μ) :
Integrable (f - g) μ
source
theorem MeasureTheory.Integrable.sub' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f g : α → β} (hf : Integrable f μ) (hg : Integrable g μ) :
Integrable (fun (a : α) => f a - g a) μ
source
theorem MeasureTheory.Integrable.enorm {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (hf : Integrable f μ) :
Integrable (fun (x : α) => ‖f x‖ₑ) μ
source
theorem MeasureTheory.Integrable.norm {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} (hf : Integrable f μ) :
Integrable (fun (a : α) => ‖f a‖) μ
source
theorem MeasureTheory.Integrable.inf {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_8} [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] {f g : α → β} (hf : Integrable f μ) (hg : Integrable g μ) :
Integrable (f ⊓ g) μ
source
theorem MeasureTheory.Integrable.sup {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_8} [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] {f g : α → β} (hf : Integrable f μ) (hg : Integrable g μ) :
Integrable (f ⊔ g) μ
source
theorem MeasureTheory.Integrable.abs {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {β : Type u_8} [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [IsOrderedAddMonoid β] {f : α → β} (hf : Integrable f μ) :
Integrable (fun (a : α) => |f a|) μ
source
theorem MeasureTheory.Integrable.bdd_mul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {F : Type u_8} [NormedDivisionRing F] {f g : α → F} (hint : Integrable g μ) (hm : AEStronglyMeasurable f μ) (hfbdd : ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C) :
Integrable (fun (x : α) => f x * g x) μ
source
theorem MeasureTheory.Integrable.essSup_smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {R : Type u_8} [NormedRing R] [Module R β] [IsBoundedSMul R β] {f : α → β} (hf : Integrable f μ) {g : α → R} (g_aestronglyMeasurable : AEStronglyMeasurable g μ) (ess_sup_g : essSup (fun (x : α) => ‖g x‖ₑ) μ ≠ ⊤) :
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.

source
theorem MeasureTheory.Integrable.smul_essSup {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {𝕜 : Type u_8} [NormedRing 𝕜] [MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β] {f : α → 𝕜} (hf : Integrable f μ) {g : α → β} (g_aestronglyMeasurable : AEStronglyMeasurable g μ) (ess_sup_g : essSup (fun (x : α) => ‖g x‖ₑ) μ ≠ ⊤) :
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.

source
theorem MeasureTheory.integrable_enorm_iff {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) :
Integrable (fun (x : α) => ‖f x‖ₑ) μ ↔ Integrable f μ
source
theorem MeasureTheory.integrable_norm_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} (hf : AEStronglyMeasurable f μ) :
Integrable (fun (a : α) => ‖f a‖) μ ↔ Integrable f μ
source
theorem MeasureTheory.integrable_of_norm_sub_le {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f₀ f₁ : α → β} {g : α → ℝ} (hf₁_m : AEStronglyMeasurable f₁ μ) (hf₀_i : Integrable f₀ μ) (hg_i : Integrable g μ) (h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a) :
Integrable f₁ μ
source
theorem MeasureTheory.integrable_of_le_of_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f g₁ g₂ : α → ℝ} (hf : AEStronglyMeasurable f μ) (h_le₁ : g₁ ≤ᶠ[ae μ] f) (h_le₂ : f ≤ᶠ[ae μ] g₂) (h_int₁ : Integrable g₁ μ) (h_int₂ : Integrable g₂ μ) :
Integrable f μ
source
theorem MeasureTheory.Integrable.prodMk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : α → β} {g : α → γ} (hf : Integrable f μ) (hg : Integrable g μ) :
Integrable (fun (x : α) => (f x, g x)) μ
source
theorem MeasureTheory.MemLp.integrable {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {q : ENNReal} (hq1 : 1 ≤ q) {f : α → ε} [IsFiniteMeasure μ] (hfq : MemLp f q μ) :
Integrable f μ
source
theorem MeasureTheory.Integrable.measure_enorm_ge_lt_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_8} [TopologicalSpace E] [ContinuousENorm E] {f : α → E} (hf : Integrable f μ) {ε : ENNReal} (hε : 0 < ε) (hε' : ε ≠ ⊤) :
μ {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 `ε`.

source
theorem MeasureTheory.Integrable.measure_norm_ge_lt_top {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} (hf : 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 `ε`.

source
theorem MeasureTheory.Integrable.measure_norm_gt_lt_top_enorm {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_8} [TopologicalSpace E] [ContinuousENorm E] {f : α → E} (hf : Integrable f μ) {ε : ENNReal} (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 `ε`.

source
theorem MeasureTheory.Integrable.measure_norm_gt_lt_top {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} (hf : 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 `ε`.

source
theorem MeasureTheory.Integrable.measure_ge_lt_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hf : 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.

source
theorem MeasureTheory.Integrable.measure_le_lt_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hf : 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.

source
theorem MeasureTheory.Integrable.measure_gt_lt_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hf : 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.

source
theorem MeasureTheory.Integrable.measure_lt_lt_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hf : 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.

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

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

source
theorem MeasureTheory.integrable_withDensity_iff_integrable_coe_smul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → NNReal} (hf : Measurable f) {g : α → E} :
Integrable g (μ.withDensity fun (x : α) => ↑(f x)) ↔ Integrable (fun (x : α) => ↑(f x) • g x) μ
source
theorem MeasureTheory.integrable_withDensity_iff_integrable_smul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → NNReal} (hf : Measurable f) {g : α → E} :
Integrable g (μ.withDensity fun (x : α) => ↑(f x)) ↔ Integrable (fun (x : α) => f x • g x) μ
source
theorem MeasureTheory.integrable_withDensity_iff_integrable_smul' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → ENNReal} (hf : Measurable f) (hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤) {g : α → E} :
Integrable g (μ.withDensity f) ↔ Integrable (fun (x : α) => (f x).toReal • g x) μ
source
theorem MeasureTheory.integrable_withDensity_iff_integrable_coe_smul₀ {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → NNReal} (hf : AEMeasurable f μ) {g : α → E} :
Integrable g (μ.withDensity fun (x : α) => ↑(f x)) ↔ Integrable (fun (x : α) => ↑(f x) • g x) μ
source
theorem MeasureTheory.integrable_withDensity_iff_integrable_smul₀' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → ENNReal} (hf : AEMeasurable f μ) (hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤) {g : α → E} :
Integrable g (μ.withDensity f) ↔ Integrable (fun (x : α) => (f x).toReal • g x) μ
source
theorem MeasureTheory.integrable_withDensity_iff_integrable_smul₀ {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → NNReal} (hf : AEMeasurable f μ) {g : α → E} :
Integrable g (μ.withDensity fun (x : α) => ↑(f x)) ↔ Integrable (fun (x : α) => f x • g x) μ
source
theorem MeasureTheory.integrable_withDensity_iff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : Measurable f) (hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤) {g : α → ℝ} :
Integrable g (μ.withDensity f) ↔ Integrable (fun (x : α) => g x * (f x).toReal) μ
source
theorem MeasureTheory.memL1_smul_of_L1_withDensity {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → NNReal} (f_meas : Measurable f) (u : ↥(Lp E 1 (μ.withDensity fun (x : α) => ↑(f x)))) :
MemLp (fun (x : α) => f x • ↑↑u x) 1 μ
source
noncomputable def MeasureTheory.withDensitySMulLI {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → NNReal} (f_meas : Measurable f) :
↥(Lp E 1 (μ.withDensity fun (x : α) => ↑(f x))) →ₗᵢ[ℝ] ↥(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

source
@[simp]
theorem MeasureTheory.withDensitySMulLI_apply {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → NNReal} (f_meas : Measurable f) (u : ↥(Lp E 1 (μ.withDensity fun (x : α) => ↑(f x)))) :
(withDensitySMulLI μ f_meas) u = MemLp.toLp (fun (x : α) => f x • ↑↑u x) ⋯
source
theorem MeasureTheory.mem_L1_toReal_of_lintegral_ne_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hfm : AEMeasurable f μ) (hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) :
MemLp (fun (x : α) => (f x).toReal) 1 μ
source
theorem MeasureTheory.integrable_toReal_of_lintegral_ne_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hfm : AEMeasurable f μ) (hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) :
Integrable (fun (x : α) => (f x).toReal) μ
source
theorem MeasureTheory.integrable_toReal_iff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) :
Integrable (fun (x : α) => (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ⊤
source
theorem MeasureTheory.lintegral_ofReal_ne_top_iff_integrable {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hfm : AEStronglyMeasurable f μ) (hf : 0 ≤ᶠ[ae μ] f) :
∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ ≠ ⊤ ↔ Integrable f μ

### Lemmas used for defining the positive part of an `L¹` function #

source
theorem MeasureTheory.Integrable.pos_part {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hf : Integrable f μ) :
Integrable (fun (a : α) => max (f a) 0) μ
source
theorem MeasureTheory.Integrable.neg_part {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hf : Integrable f μ) :
Integrable (fun (a : α) => max (-f a) 0) μ
source
theorem MeasureTheory.Integrable.smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {𝕜 : Type u_8} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 β] [IsBoundedSMul 𝕜 β] (c : 𝕜) {f : α → β} (hf : Integrable f μ) :
Integrable (c • f) μ
source
theorem MeasureTheory.Integrable.fun_smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {𝕜 : Type u_8} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 β] [IsBoundedSMul 𝕜 β] (c : 𝕜) {f : α → β} (hf : Integrable f μ) :
Integrable (fun (x : α) => c • f x) μ
source
theorem MeasureTheory.Integrable.smul_enorm {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} {ε : Type u_9} [TopologicalSpace ε] [ESeminormedAddMonoid ε] [NormedAddCommGroup 𝕜] [SMul 𝕜 ε] [ContinuousConstSMul 𝕜 ε] [ENormSMulClass 𝕜 ε] (c : 𝕜) {f : α → ε} (hf : Integrable f μ) :
Integrable (c • f) μ
source
theorem MeasureTheory.Integrable.fun_smul_enorm {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} {ε : Type u_9} [TopologicalSpace ε] [ESeminormedAddMonoid ε] [NormedAddCommGroup 𝕜] [SMul 𝕜 ε] [ContinuousConstSMul 𝕜 ε] [ENormSMulClass 𝕜 ε] (c : 𝕜) {f : α → ε} (hf : Integrable f μ) :
Integrable (fun (x : α) => c • f x) μ
source
theorem IsUnit.integrable_smul_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {𝕜 : Type u_8} [NormedRing 𝕜] [MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β] {c : 𝕜} (hc : IsUnit c) (f : α → β) :
MeasureTheory.Integrable (c • f) μ ↔ MeasureTheory.Integrable f μ
source
theorem MeasureTheory.integrable_smul_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {𝕜 : Type u_8} [NormedDivisionRing 𝕜] [MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β] {c : 𝕜} (hc : c ≠ 0) (f : α → β) :
Integrable (c • f) μ ↔ Integrable f μ
source
theorem MeasureTheory.integrable_fun_smul_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {𝕜 : Type u_8} [NormedDivisionRing 𝕜] [MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β] {c : 𝕜} (hc : c ≠ 0) (f : α → β) :
Integrable (fun (x : α) => c • f x) μ ↔ Integrable f μ
source
theorem MeasureTheory.Integrable.smul_of_top_right {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {𝕜 : Type u_8} [NormedRing 𝕜] [Module 𝕜 β] [IsBoundedSMul 𝕜 β] {f : α → β} {φ : α → 𝕜} (hf : Integrable f μ) (hφ : MemLp φ ⊤ μ) :
Integrable (φ • f) μ
source
theorem MeasureTheory.Integrable.smul_of_top_left {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {𝕜 : Type u_8} [NormedRing 𝕜] [Module 𝕜 β] [IsBoundedSMul 𝕜 β] {f : α → β} {φ : α → 𝕜} (hφ : Integrable φ μ) (hf : MemLp f ⊤ μ) :
Integrable (φ • f) μ
source
theorem MeasureTheory.Integrable.smul_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {𝕜 : Type u_8} [NormedRing 𝕜] [Module 𝕜 β] [IsBoundedSMul 𝕜 β] {f : α → 𝕜} (hf : Integrable f μ) (c : β) :
Integrable (fun (x : α) => f x • c) μ
source
theorem MeasureTheory.integrable_smul_const {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_9} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : α → 𝕜} {c : E} (hc : c ≠ 0) :
Integrable (fun (x : α) => f x • c) μ ↔ Integrable f μ
source
theorem MeasureTheory.Integrable.const_mul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [NormedRing 𝕜] {f : α → 𝕜} (h : Integrable f μ) (c : 𝕜) :
Integrable (fun (x : α) => c * f x) μ
source
theorem MeasureTheory.Integrable.const_mul' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [NormedRing 𝕜] {f : α → 𝕜} (h : Integrable f μ) (c : 𝕜) :
Integrable ((fun (x : α) => c) * f) μ
source
theorem MeasureTheory.Integrable.mul_const {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [NormedRing 𝕜] {f : α → 𝕜} (h : Integrable f μ) (c : 𝕜) :
Integrable (fun (x : α) => f x * c) μ
source
theorem MeasureTheory.Integrable.mul_const' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [NormedRing 𝕜] {f : α → 𝕜} (h : Integrable f μ) (c : 𝕜) :
Integrable (f * fun (x : α) => c) μ
source
theorem MeasureTheory.integrable_const_mul_iff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [NormedRing 𝕜] {c : 𝕜} (hc : IsUnit c) (f : α → 𝕜) :
Integrable (fun (x : α) => c * f x) μ ↔ Integrable f μ
source
theorem MeasureTheory.integrable_mul_const_iff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [NormedRing 𝕜] {c : 𝕜} (hc : IsUnit c) (f : α → 𝕜) :
Integrable (fun (x : α) => f x * c) μ ↔ Integrable f μ
source
theorem MeasureTheory.Integrable.bdd_mul' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [NormedRing 𝕜] {f g : α → 𝕜} {c : ℝ} (hg : Integrable g μ) (hf : AEStronglyMeasurable f μ) (hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c) :
Integrable (fun (x : α) => f x * g x) μ
source
theorem MeasureTheory.Integrable.mul_of_top_right {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [NormedRing 𝕜] {f φ : α → 𝕜} (hf : Integrable f μ) (hφ : MemLp φ ⊤ μ) :
Integrable (φ * f) μ
source
theorem MeasureTheory.Integrable.mul_of_top_left {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [NormedRing 𝕜] {f φ : α → 𝕜} (hφ : Integrable φ μ) (hf : MemLp f ⊤ μ) :
Integrable (φ * f) μ
source
theorem MeasureTheory.MemLp.integrable_mul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [NormedRing 𝕜] {p q : ENNReal} {f g : α → 𝕜} (hf : MemLp f p μ) (hg : MemLp g q μ) [p.HolderTriple q 1] :
Integrable (f * g) μ
source
theorem MeasureTheory.Integrable.div_const {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [NormedDivisionRing 𝕜] {f : α → 𝕜} (h : Integrable f μ) (c : 𝕜) :
Integrable (fun (x : α) => f x / c) μ
source
theorem MeasureTheory.Integrable.ofReal {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [RCLike 𝕜] {f : α → ℝ} (hf : Integrable f μ) :
Integrable (fun (x : α) => ↑(f x)) μ
source
theorem MeasureTheory.Integrable.re_im_iff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [RCLike 𝕜] {f : α → 𝕜} :
Integrable (fun (x : α) => RCLike.re (f x)) μ ∧ Integrable (fun (x : α) => RCLike.im (f x)) μ ↔ Integrable f μ
source
theorem MeasureTheory.Integrable.re {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [RCLike 𝕜] {f : α → 𝕜} (hf : Integrable f μ) :
Integrable (fun (x : α) => RCLike.re (f x)) μ
source
theorem MeasureTheory.Integrable.im {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_8} [RCLike 𝕜] {f : α → 𝕜} (hf : Integrable f μ) :
Integrable (fun (x : α) => RCLike.im (f x)) μ
source
theorem MeasureTheory.Integrable.trim {α : Type u_1} {m : MeasurableSpace α} {H : Type u_8} [NormedAddCommGroup H] {m0 : MeasurableSpace α} {μ' : Measure α} {f : α → H} (hm : m ≤ m0) (hf_int : Integrable f μ') (hf : StronglyMeasurable f) :
Integrable f (μ'.trim hm)
source
theorem MeasureTheory.integrable_of_integrable_trim {α : Type u_1} {m : MeasurableSpace α} {H : Type u_8} [NormedAddCommGroup H] {m0 : MeasurableSpace α} {μ' : Measure α} {f : α → H} (hm : m ≤ m0) (hf_int : Integrable f (μ'.trim hm)) :
Integrable f μ'
source
theorem MeasureTheory.integrable_of_forall_fin_meas_le' {α : Type u_1} {m m0 : MeasurableSpace α} {ε : Type u_9} [TopologicalSpace ε] [ContinuousENorm ε] {μ : Measure α} (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (C : ENNReal) (hC : C < ⊤) {f : α → ε} (hf_meas : AEStronglyMeasurable f μ) (hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ ≤ C) :
Integrable f μ
source
theorem MeasureTheory.integrable_of_forall_fin_meas_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_9} [TopologicalSpace ε] [ContinuousENorm ε] [SigmaFinite μ] (C : ENNReal) (hC : C < ⊤) {f : α → ε} (hf_meas : AEStronglyMeasurable f μ) (hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ ≤ C) :
Integrable f μ
source
theorem MeasureTheory.Integrable.restrict {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_8} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (hf : Integrable f μ) {s : Set α} :
Integrable f (μ.restrict s)

One should usually use `MeasureTheory.Integrable.integrableOn` instead.

source
theorem ContinuousLinearMap.integrable_comp {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} {H : Type u_9} [NormedAddCommGroup E] [NormedAddCommGroup H] {𝕜 : Type u_10} {𝕜' : Type u_11} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedSpace 𝕜' E] [NormedSpace 𝕜 H] {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] {φ : α → H} (L : H →SL[σ] E) (φ_int : MeasureTheory.Integrable φ μ) :
MeasureTheory.Integrable (fun (a : α) => L (φ a)) μ
source
@[simp]
theorem ContinuousLinearEquiv.integrable_comp_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} {H : Type u_9} [NormedAddCommGroup E] [NormedAddCommGroup H] {𝕜 : Type u_10} {𝕜' : Type u_11} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedSpace 𝕜' E] [NormedSpace 𝕜 H] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [RingHomIsometric σ] [RingHomIsometric σ'] [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {φ : α → H} (L : H ≃SL[σ] E) :
MeasureTheory.Integrable (fun (a : α) => L (φ a)) μ ↔ MeasureTheory.Integrable φ μ
source
@[simp]
theorem LinearIsometryEquiv.integrable_comp_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} {H : Type u_9} [NormedAddCommGroup E] [NormedAddCommGroup H] {𝕜 : Type u_10} {𝕜' : Type u_11} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedSpace 𝕜' E] [NormedSpace 𝕜 H] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [RingHomIsometric σ] [RingHomIsometric σ'] [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {φ : α → H} (L : H ≃ₛₗᵢ[σ] E) :
MeasureTheory.Integrable (fun (a : α) => L (φ a)) μ ↔ MeasureTheory.Integrable φ μ
source
theorem MeasureTheory.Integrable.apply_continuousLinearMap {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_8} {H : Type u_9} [NormedAddCommGroup E] [NormedAddCommGroup H] {𝕜 : Type u_10} {𝕜' : Type u_11} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedSpace 𝕜' E] [NormedSpace 𝕜 H] {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] {φ : α → H →SL[σ] E} (φ_int : Integrable φ μ) (v : H) :
Integrable (fun (a : α) => (φ a) v) μ
source
theorem MeasureTheory.Integrable.fst {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_8} {F : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : α → E × F} (hf : Integrable f μ) :
Integrable (fun (x : α) => (f x).1) μ
source
theorem MeasureTheory.Integrable.snd {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_8} {F : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : α → E × F} (hf : Integrable f μ) :
Integrable (fun (x : α) => (f x).2) μ
source
theorem MeasureTheory.integrable_prod {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_8} {F : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : α → E × F} :
Integrable f μ ↔ Integrable (fun (x : α) => (f x).1) μ ∧ Integrable (fun (x : α) => (f x).2) μ
source
theorem MeasureTheory.lintegral_enorm_le_liminf_of_tendsto {G : ℕ → ℝ → ℝ} {f : ℝ → ℝ} {μ : Measure ℝ} (hGf : ∀ᵐ (x : ℝ) ∂μ, Filter.Tendsto (fun (n : ℕ) => G n x) Filter.atTop (nhds (f x))) (hG : ∀ (n : ℕ), AEMeasurable (fun (x : ℝ) => ‖G n x‖ₑ) μ) :
∫⁻ (x : ℝ), ‖f x‖ₑ ∂μ ≤ Filter.liminf (fun (n : ℕ) => ∫⁻ (x : ℝ), ‖G n x‖ₑ ∂μ) Filter.atTop

If `G n` tends to `f` a.e. and each `‖G n ·‖ₑ` is `AEMeasurable`, then the lower Lebesgue integral of `‖f ·‖ₑ` is at most the liminf of the lower Lebesgue integral of `‖G n ·‖ₑ`.

source
theorem MeasureTheory.integrable_of_tendsto {G : ℕ → ℝ → ℝ} {f : ℝ → ℝ} {μ : Measure ℝ} (hGf : ∀ᵐ (x : ℝ) ∂μ, Filter.Tendsto (fun (n : ℕ) => G n x) Filter.atTop (nhds (f x))) (hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) μ) (hG' : Filter.liminf (fun (n : ℕ) => ∫⁻ (x : ℝ), ‖G n x‖ₑ ∂μ) Filter.atTop ≠ ⊤) :
Integrable f μ

If `G n` tends to `f` a.e., each `G n` is `AEStronglyMeasurable` and the liminf of the lower Lebesgue integral of `‖G n ·‖ₑ` is finite, then `f` is Lebesgue integrable.