# mathlibdocumentation

measure_theory.function.l1_space

# Integrable functions and `L¹` 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 `L¹` of equivalence classes of integrable functions, already defined as a special case of `L^p` spaces for `p = 1`.

## Notation #

• `α →₁[μ] β` is the type of `L¹` space, where `α` is a `measure_space` and `β` is a `normed_group` with a `second_countable_topology`. `f : α →ₘ β` is a "function" in `L¹`. In comments, `[f]` is also used to denote an `L¹` function.

`₁` can be typed as `\1`.

## Main definitions #

• Let `f : α → β` be a function, where `α` is a `measure_space` and `β` a `normed_group`. Then `has_finite_integral f` means `(∫⁻ a, ∥f a∥₊) < ∞`.

• If `β` is moreover a `measurable_space` then `f` is called `integrable` if `f` is `measurable` and `has_finite_integral f` holds.

## Implementation notes #

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

## Tags #

integrable, function space, l1

### Some results about the Lebesgue integral involving a normed group #

theorem measure_theory.lintegral_nnnorm_eq_lintegral_edist {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : α → β) :
∫⁻ (a : α), f a∥₊ μ = ∫⁻ (a : α), has_edist.edist (f a) 0 μ
theorem measure_theory.lintegral_norm_eq_lintegral_edist {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : α → β) :
∫⁻ (a : α), μ = ∫⁻ (a : α), has_edist.edist (f a) 0 μ
theorem measure_theory.lintegral_edist_triangle {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f g h : α → β}  :
∫⁻ (a : α), has_edist.edist (f a) (g a) μ ∫⁻ (a : α), has_edist.edist (f a) (h a) μ + ∫⁻ (a : α), has_edist.edist (g a) (h a) μ
theorem measure_theory.lintegral_nnnorm_zero {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] :
∫⁻ (a : α), 0∥₊ μ = 0
theorem measure_theory.lintegral_nnnorm_add_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} (g : α → γ) :
∫⁻ (a : α), f a∥₊ + g a∥₊ μ = ∫⁻ (a : α), f a∥₊ μ + ∫⁻ (a : α), g a∥₊ μ
theorem measure_theory.lintegral_nnnorm_add_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] (f : α → β) {g : α → γ}  :
∫⁻ (a : α), f a∥₊ + g a∥₊ μ = ∫⁻ (a : α), f a∥₊ μ + ∫⁻ (a : α), g a∥₊ μ
theorem measure_theory.lintegral_nnnorm_neg {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} :
∫⁻ (a : α), (-f) a∥₊ μ = ∫⁻ (a : α), f a∥₊ μ

### The predicate `has_finite_integral`#

def measure_theory.has_finite_integral {α : Type u_1} {β : Type u_2} [normed_group β] {m : measurable_space α} (f : α → β) (μ : . "volume_tac") :
Prop

`has_finite_integral f μ` means that the integral `∫⁻ a, ∥f a∥ ∂μ` is finite. `has_finite_integral f` means `has_finite_integral f volume`.

Equations
theorem measure_theory.has_finite_integral_iff_norm {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : α → β) :
∫⁻ (a : α), μ <
theorem measure_theory.has_finite_integral_iff_edist {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : α → β) :
∫⁻ (a : α), has_edist.edist (f a) 0 μ <
theorem measure_theory.has_finite_integral_iff_of_real {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (h : 0 ≤ᵐ[μ] f) :
∫⁻ (a : α), ennreal.of_real (f a) μ <
theorem measure_theory.has_finite_integral_iff_of_nnreal {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → nnreal} :
measure_theory.has_finite_integral (λ (x : α), (f x)) μ ∫⁻ (a : α), (f a) μ <
theorem measure_theory.has_finite_integral.mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} (hg : μ) (h : ∀ᵐ (a : α) ∂μ, f a g a) :
theorem measure_theory.has_finite_integral.mono' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} {g : α → } (hg : μ) (h : ∀ᵐ (a : α) ∂μ, f a g a) :
theorem measure_theory.has_finite_integral.congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} (hf : μ) (h : ∀ᵐ (a : α) ∂μ, f a = g a) :
theorem measure_theory.has_finite_integral_congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} (h : ∀ᵐ (a : α) ∂μ, f a = g a) :
theorem measure_theory.has_finite_integral.congr {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f g : α → β} (hf : μ) (h : f =ᵐ[μ] g) :
theorem measure_theory.has_finite_integral_congr {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f g : α → β} (h : f =ᵐ[μ] g) :
theorem measure_theory.has_finite_integral_const_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {c : β} :
measure_theory.has_finite_integral (λ (x : α), c) μ c = 0
theorem measure_theory.has_finite_integral_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (c : β) :
theorem measure_theory.has_finite_integral_of_bounded {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} {C : } (hC : ∀ᵐ (a : α) ∂μ, f a C) :
theorem measure_theory.has_finite_integral.mono_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (hμ : μ ν) :
theorem measure_theory.has_finite_integral.add_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (hμ : μ) (hν : ν) :
theorem measure_theory.has_finite_integral.left_of_add_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (h : + ν)) :
theorem measure_theory.has_finite_integral.right_of_add_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (h : + ν)) :
@[simp]
theorem measure_theory.has_finite_integral_add_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} :
theorem measure_theory.has_finite_integral.smul_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} {c : ennreal} (hc : c ) :
@[simp]
theorem measure_theory.has_finite_integral_zero_measure {α : Type u_1} {β : Type u_2} [normed_group β] {m : measurable_space α} (f : α → β) :
@[simp]
theorem measure_theory.has_finite_integral_zero (α : Type u_1) (β : Type u_2) {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] :
theorem measure_theory.has_finite_integral.neg {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (hfi : μ) :
@[simp]
theorem measure_theory.has_finite_integral_neg_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} :
theorem measure_theory.has_finite_integral.norm {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (hfi : μ) :
theorem measure_theory.has_finite_integral_norm_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : α → β) :
theorem measure_theory.has_finite_integral_to_real_of_lintegral_ne_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} (hf : ∫⁻ (x : α), f x μ ) :
theorem measure_theory.all_ae_of_real_F_le_bound {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {F : α → β} {bound : α → } (h : ∀ (n : ), ∀ᵐ (a : α) ∂μ, F n a bound a) (n : ) :
∀ᵐ (a : α) ∂μ, ennreal.of_real F n a ennreal.of_real (bound a)
theorem measure_theory.all_ae_tendsto_of_real_norm {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {F : α → β} {f : α → β} (h : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ), F n a) filter.at_top (nhds (f a))) :
∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ), ennreal.of_real F n a) filter.at_top (nhds (ennreal.of_real f a))
theorem measure_theory.all_ae_of_real_f_le_bound {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {F : α → β} {f : α → β} {bound : α → } (h_bound : ∀ (n : ), ∀ᵐ (a : α) ∂μ, F n a bound a) (h_lim : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ), F n a) filter.at_top (nhds (f a))) :
∀ᵐ (a : α) ∂μ, ennreal.of_real (bound a)
theorem measure_theory.has_finite_integral_of_dominated_convergence {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {F : α → β} {f : α → β} {bound : α → } (bound_has_finite_integral : μ) (h_bound : ∀ (n : ), ∀ᵐ (a : α) ∂μ, F n a bound a) (h_lim : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ), F n a) filter.at_top (nhds (f a))) :
theorem measure_theory.tendsto_lintegral_norm_of_dominated_convergence {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {F : α → β} {f : α → β} {bound : α → } (F_measurable : ∀ (n : ), ) (bound_has_finite_integral : μ) (h_bound : ∀ (n : ), ∀ᵐ (a : α) ∂μ, F n a bound a) (h_lim : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ), F n a) filter.at_top (nhds (f a))) :
filter.tendsto (λ (n : ), ∫⁻ (a : α), ennreal.of_real F n a - f a μ) filter.at_top (nhds 0)

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

theorem measure_theory.has_finite_integral.max_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : μ) :
theorem measure_theory.has_finite_integral.min_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : μ) :
theorem measure_theory.has_finite_integral.smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {𝕜 : Type u_5} [normed_field 𝕜] [ β] (c : 𝕜) {f : α → β} :
theorem measure_theory.has_finite_integral_smul_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {𝕜 : Type u_5} [normed_field 𝕜] [ β] {c : 𝕜} (hc : c 0) (f : α → β) :
theorem measure_theory.has_finite_integral.const_mul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (c : ) :
measure_theory.has_finite_integral (λ (x : α), c * f x) μ
theorem measure_theory.has_finite_integral.mul_const {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (c : ) :
measure_theory.has_finite_integral (λ (x : α), f x * c) μ

### The predicate `integrable`#

def measure_theory.integrable {β : Type u_2} [normed_group β] {α : Type u_1} {m : measurable_space α} (f : α → β) (μ : . "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
theorem measure_theory.mem_ℒp_one_iff_integrable {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} :
theorem measure_theory.integrable.ae_strongly_measurable {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (hf : μ) :
theorem measure_theory.integrable.ae_measurable {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [borel_space β] {f : α → β} (hf : μ) :
theorem measure_theory.integrable.has_finite_integral {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (hf : μ) :
theorem measure_theory.integrable.mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} (hg : μ) (h : ∀ᵐ (a : α) ∂μ, f a g a) :
theorem measure_theory.integrable.mono' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} {g : α → } (hg : μ) (h : ∀ᵐ (a : α) ∂μ, f a g a) :
theorem measure_theory.integrable.congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} (hf : μ) (h : ∀ᵐ (a : α) ∂μ, f a = g a) :
theorem measure_theory.integrable_congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} (h : ∀ᵐ (a : α) ∂μ, f a = g a) :
theorem measure_theory.integrable.congr {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f g : α → β} (hf : μ) (h : f =ᵐ[μ] g) :
theorem measure_theory.integrable_congr {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f g : α → β} (h : f =ᵐ[μ] g) :
theorem measure_theory.integrable_const_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {c : β} :
measure_theory.integrable (λ (x : α), c) μ c = 0
theorem measure_theory.integrable_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (c : β) :
measure_theory.integrable (λ (x : α), c) μ
theorem measure_theory.mem_ℒp.integrable_norm_rpow {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} {p : ennreal} (hf : μ) (hp_ne_zero : p 0) (hp_ne_top : p ) :
measure_theory.integrable (λ (x : α), f x ^ p.to_real) μ
theorem measure_theory.mem_ℒp.integrable_norm_rpow' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} {p : ennreal} (hf : μ) :
measure_theory.integrable (λ (x : α), f x ^ p.to_real) μ
theorem measure_theory.integrable.mono_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (h : ν) (hμ : μ ν) :
theorem measure_theory.integrable.of_measure_le_smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {μ' : measure_theory.measure α} (c : ennreal) (hc : c ) (hμ'_le : μ' c μ) {f : α → β} (hf : μ) :
theorem measure_theory.integrable.add_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (hμ : μ) (hν : ν) :
+ ν)
theorem measure_theory.integrable.left_of_add_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (h : + ν)) :
theorem measure_theory.integrable.right_of_add_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (h : + ν)) :
@[simp]
theorem measure_theory.integrable_add_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} :
@[simp]
theorem measure_theory.integrable_zero_measure {α : Type u_1} {β : Type u_2} [normed_group β] {m : measurable_space α} {f : α → β} :
theorem measure_theory.integrable_finset_sum_measure {α : Type u_1} {β : Type u_2} [normed_group β] {ι : Type u_3} {m : measurable_space α} {f : α → β} {μ : ι → } {s : finset ι} :
(s.sum (λ (i : ι), μ i)) ∀ (i : ι), i s (μ i)
theorem measure_theory.integrable.smul_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (h : μ) {c : ennreal} (hc : c ) :
(c μ)
theorem measure_theory.integrable_smul_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} {c : ennreal} (h₁ : c 0) (h₂ : c ) :
(c μ)
theorem measure_theory.integrable.to_average {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (h : μ) :
theorem measure_theory.integrable_average {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} :
theorem measure_theory.integrable_map_measure {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → δ} {g : δ → β} (hf : μ) :
theorem measure_theory.integrable.comp_ae_measurable {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → δ} {g : δ → β} (hg : ) (hf : μ) :
μ
theorem measure_theory.integrable.comp_measurable {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → δ} {g : δ → β} (hg : ) (hf : measurable f) :
μ
theorem measurable_embedding.integrable_map_iff {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → δ} (hf : measurable_embedding f) {g : δ → β} :
theorem measure_theory.integrable_map_equiv {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : α ≃ᵐ δ) (g : δ → β) :
theorem measure_theory.measure_preserving.integrable_comp {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {ν : measure_theory.measure δ} {g : δ → β} {f : α → δ} (hf : ν)  :
μ
theorem measure_theory.measure_preserving.integrable_comp_emb {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → δ} {ν : . "volume_tac"} (h₁ : ν) (h₂ : measurable_embedding f) {g : δ → β} :
μ
theorem measure_theory.lintegral_edist_lt_top {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f g : α → β} (hf : μ) (hg : μ) :
∫⁻ (a : α), has_edist.edist (f a) (g a) μ <
@[simp]
theorem measure_theory.integrable_zero (α : Type u_1) (β : Type u_2) {m : measurable_space α} (μ : measure_theory.measure α) [normed_group β] :
measure_theory.integrable (λ (_x : α), 0) μ
theorem measure_theory.integrable.add' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f g : α → β} (hf : μ) (hg : μ) :
theorem measure_theory.integrable.add {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f g : α → β} (hf : μ) (hg : μ) :
μ
theorem measure_theory.integrable_finset_sum' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {ι : Type u_3} (s : finset ι) {f : ι → α → β} (hf : ∀ (i : ι), i s μ) :
measure_theory.integrable (s.sum (λ (i : ι), f i)) μ
theorem measure_theory.integrable_finset_sum {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {ι : Type u_3} (s : finset ι) {f : ι → α → β} (hf : ∀ (i : ι), i s μ) :
measure_theory.integrable (λ (a : α), s.sum (λ (i : ι), f i a)) μ
theorem measure_theory.integrable.neg {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (hf : μ) :
@[simp]
theorem measure_theory.integrable_neg_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} :
theorem measure_theory.integrable.sub {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f g : α → β} (hf : μ) (hg : μ) :
μ
theorem measure_theory.integrable.norm {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (hf : μ) :
measure_theory.integrable (λ (a : α), f a) μ
theorem measure_theory.integrable.inf {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} {f g : α → β} (hf : μ) (hg : μ) :
μ
theorem measure_theory.integrable.sup {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} {f g : α → β} (hf : μ) (hg : μ) :
μ
theorem measure_theory.integrable.abs {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} {f : α → β} (hf : μ) :
measure_theory.integrable (λ (a : α), |f a|) μ
theorem measure_theory.integrable.bdd_mul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {F : Type u_2} {f g : α → F} (hint : μ) (hfbdd : ∃ (C : ), ∀ (x : α), f x C) :
measure_theory.integrable (λ (x : α), f x * g x) μ
theorem measure_theory.integrable_norm_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β}  :
measure_theory.integrable (λ (a : α), f a) μ
theorem measure_theory.integrable_of_norm_sub_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f₀ f₁ : α → β} {g : α → } (hf₁_m : μ) (hf₀_i : μ) (hg_i : μ) (h : ∀ᵐ (a : α) ∂μ, f₀ a - f₁ a g a) :
theorem measure_theory.integrable.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} (hf : μ) (hg : μ) :
measure_theory.integrable (λ (x : α), (f x, g x)) μ
theorem measure_theory.mem_ℒp.integrable {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {q : ennreal} (hq1 : 1 q) {f : α → β} (hfq : μ) :
theorem measure_theory.lipschitz_with.integrable_comp_iff_of_antilipschitz {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {K K' : nnreal} {f : α → β} {g : β → γ} (hg : g) (hg' : g) (g0 : g 0 = 0) :
μ
theorem measure_theory.integrable.real_to_nnreal {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : μ) :
measure_theory.integrable (λ (x : α), ((f x).to_nnreal)) μ
theorem measure_theory.of_real_to_real_ae_eq {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} (hf : ∀ᵐ (x : α) ∂μ, f x < ) :
(λ (x : α), ennreal.of_real (f x).to_real) =ᵐ[μ] f
theorem measure_theory.coe_to_nnreal_ae_eq {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} (hf : ∀ᵐ (x : α) ∂μ, f x < ) :
(λ (x : α), ((f x).to_nnreal)) =ᵐ[μ] f
theorem measure_theory.integrable_with_density_iff_integrable_coe_smul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_5} [normed_group E] [ E] {f : α → nnreal} (hf : measurable f) {g : α → E} :
(μ.with_density (λ (x : α), (f x))) measure_theory.integrable (λ (x : α), (f x) g x) μ
theorem measure_theory.integrable_with_density_iff_integrable_smul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_5} [normed_group E] [ E] {f : α → nnreal} (hf : measurable f) {g : α → E} :
(μ.with_density (λ (x : α), (f x))) measure_theory.integrable (λ (x : α), f x g x) μ
theorem measure_theory.integrable_with_density_iff_integrable_smul' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_5} [normed_group E] [ E] {f : α → ennreal} (hf : measurable f) (hflt : ∀ᵐ (x : α) ∂μ, f x < ) {g : α → E} :
measure_theory.integrable (λ (x : α), (f x).to_real g x) μ
theorem measure_theory.integrable_with_density_iff_integrable_coe_smul₀ {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_5} [normed_group E] [ E] {f : α → nnreal} (hf : μ) {g : α → E} :
(μ.with_density (λ (x : α), (f x))) measure_theory.integrable (λ (x : α), (f x) g x) μ
theorem measure_theory.integrable_with_density_iff_integrable_smul₀ {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_5} [normed_group E] [ E] {f : α → nnreal} (hf : μ) {g : α → E} :
(μ.with_density (λ (x : α), (f x))) measure_theory.integrable (λ (x : α), f x g x) μ
theorem measure_theory.integrable_with_density_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} (hf : measurable f) (hflt : ∀ᵐ (x : α) ∂μ, f x < ) {g : α → } :
measure_theory.integrable (λ (x : α), g x * (f x).to_real) μ
theorem measure_theory.mem_ℒ1_smul_of_L1_with_density {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_5} [normed_group E] [ E] {f : α → nnreal} (f_meas : measurable f) (u : (μ.with_density (λ (x : α), (f x))))) :
measure_theory.mem_ℒp (λ (x : α), f x u x) 1 μ
noncomputable def measure_theory.with_density_smul_li {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) {E : Type u_5} [normed_group E] [ E] {f : α → nnreal} (f_meas : measurable f) :
(μ.with_density (λ (x : α), (f x)))) →ₗᵢ[] μ)

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

Equations
@[simp]
theorem measure_theory.with_density_smul_li_apply {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) {E : Type u_5} [normed_group E] [ E] {f : α → nnreal} (f_meas : measurable f) (u : (μ.with_density (λ (x : α), (f x))))) :
f_meas) u = measure_theory.mem_ℒp.to_Lp (λ (x : α), f x u x) _
theorem measure_theory.mem_ℒ1_to_real_of_lintegral_ne_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} (hfm : μ) (hfi : ∫⁻ (x : α), f x μ ) :
measure_theory.mem_ℒp (λ (x : α), (f x).to_real) 1 μ
theorem measure_theory.integrable_to_real_of_lintegral_ne_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} (hfm : μ) (hfi : ∫⁻ (x : α), f x μ ) :
measure_theory.integrable (λ (x : α), (f x).to_real) μ

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

theorem measure_theory.integrable.pos_part {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : μ) :
theorem measure_theory.integrable.neg_part {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : μ) :
theorem measure_theory.integrable.smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {𝕜 : Type u_5} [normed_field 𝕜] [ β] (c : 𝕜) {f : α → β} (hf : μ) :
μ
theorem measure_theory.integrable_smul_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {𝕜 : Type u_5} [normed_field 𝕜] [ β] {c : 𝕜} (hc : c 0) (f : α → β) :
μ
theorem measure_theory.integrable.const_mul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (h : μ) (c : ) :
measure_theory.integrable (λ (x : α), c * f x) μ
theorem measure_theory.integrable.const_mul' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (h : μ) (c : ) :
measure_theory.integrable ((λ (x : α), c) * f) μ
theorem measure_theory.integrable.mul_const {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (h : μ) (c : ) :
measure_theory.integrable (λ (x : α), f x * c) μ
theorem measure_theory.integrable.mul_const' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (h : μ) (c : ) :
measure_theory.integrable (f * λ (x : α), c) μ
theorem measure_theory.integrable.div_const {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (h : μ) (c : ) :
measure_theory.integrable (λ (x : α), f x / c) μ
theorem measure_theory.integrable_smul_const {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} {E : Type u_6} [normed_group E] [ E] {f : α → 𝕜} {c : E} (hc : c 0) :
measure_theory.integrable (λ (x : α), f x c) μ
theorem measure_theory.integrable.of_real {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [is_R_or_C 𝕜] {f : α → } (hf : μ) :
measure_theory.integrable (λ (x : α), (f x)) μ
theorem measure_theory.integrable.re_im_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [is_R_or_C 𝕜] {f : α → 𝕜} :
theorem measure_theory.integrable.re {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [is_R_or_C 𝕜] {f : α → 𝕜} (hf : μ) :
theorem measure_theory.integrable.im {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [is_R_or_C 𝕜] {f : α → 𝕜} (hf : μ) :
theorem measure_theory.integrable.const_inner {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} {E : Type u_6} [is_R_or_C 𝕜] [ E] {f : α → E} (c : E) (hf : μ) :
measure_theory.integrable (λ (x : α), (f x)) μ
theorem measure_theory.integrable.inner_const {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} {E : Type u_6} [is_R_or_C 𝕜] [ E] {f : α → E} (hf : μ) (c : E) :
measure_theory.integrable (λ (x : α), has_inner.inner (f x) c) μ
theorem measure_theory.integrable.trim {α : Type u_1} {m : measurable_space α} {H : Type u_5} [normed_group H] {m0 : measurable_space α} {μ' : measure_theory.measure α} {f : α → H} (hm : m m0) (hf_int : μ')  :
(μ'.trim hm)
theorem measure_theory.integrable_of_integrable_trim {α : Type u_1} {m : measurable_space α} {H : Type u_5} [normed_group H] {m0 : measurable_space α} {μ' : measure_theory.measure α} {f : α → H} (hm : m m0) (hf_int : (μ'.trim hm)) :
theorem measure_theory.integrable_of_forall_fin_meas_le' {α : Type u_1} {m : measurable_space α} {E : Type u_5} {m0 : measurable_space α} [normed_group E] {μ : measure_theory.measure α} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (C : ennreal) (hC : C < ) {f : α → E} (hf_meas : μ) (hf : ∀ (s : set α), μ s ∫⁻ (x : α) in s, f x∥₊ μ C) :
theorem measure_theory.integrable_of_forall_fin_meas_le {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_5} [normed_group E] (C : ennreal) (hC : C < ) {f : α → E} (hf_meas : μ) (hf : ∀ (s : set α), μ s ∫⁻ (x : α) in s, f x∥₊ μ C) :

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

def measure_theory.ae_eq_fun.integrable {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : α →ₘ[μ] β) :
Prop

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

Equations
theorem measure_theory.ae_eq_fun.integrable_mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β}  :
theorem measure_theory.ae_eq_fun.integrable_coe_fn {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α →ₘ[μ] β} :
theorem measure_theory.ae_eq_fun.integrable_zero {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] :
theorem measure_theory.ae_eq_fun.integrable.neg {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α →ₘ[μ] β} :
theorem measure_theory.ae_eq_fun.integrable_iff_mem_L1 {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α →ₘ[μ] β} :
theorem measure_theory.ae_eq_fun.integrable.add {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f g : α →ₘ[μ] β} :
f.integrableg.integrable(f + g).integrable
theorem measure_theory.ae_eq_fun.integrable.sub {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f g : α →ₘ[μ] β} (hf : f.integrable) (hg : g.integrable) :
theorem measure_theory.ae_eq_fun.integrable.smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {𝕜 : Type u_5} [normed_field 𝕜] [ β] {c : 𝕜} {f : α →ₘ[μ] β} :
theorem measure_theory.L1.integrable_coe_fn {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : μ)) :
theorem measure_theory.L1.has_finite_integral_coe_fn {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : μ)) :
theorem measure_theory.L1.strongly_measurable_coe_fn {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : μ)) :
theorem measure_theory.L1.measurable_coe_fn {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f : μ)) :
theorem measure_theory.L1.ae_strongly_measurable_coe_fn {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : μ)) :
theorem measure_theory.L1.ae_measurable_coe_fn {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f : μ)) :
theorem measure_theory.L1.edist_def {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f g : μ)) :
= ∫⁻ (a : α), has_edist.edist (f a) (g a) μ
theorem measure_theory.L1.dist_def {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f g : μ)) :
= (∫⁻ (a : α), has_edist.edist (f a) (g a) μ).to_real
theorem measure_theory.L1.norm_def {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : μ)) :
theorem measure_theory.L1.norm_sub_eq_lintegral {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f g : μ)) :
f - g = (∫⁻ (x : α), f x - g x∥₊ μ).to_real

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 measure_theory.L1.of_real_norm_eq_lintegral {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : μ)) :
= ∫⁻ (x : α), f x∥₊ μ
theorem measure_theory.L1.of_real_norm_sub_eq_lintegral {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (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 `of_real_norm_eq_lintegral` since `(f - g) x` and `f x - g x` are not equal (but only a.e.-equal).

noncomputable def measure_theory.integrable.to_L1 {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : α → β) (hf : μ) :
μ)

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

Equations
@[simp]
theorem measure_theory.integrable.to_L1_coe_fn {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : μ)) (hf : μ) :
theorem measure_theory.integrable.coe_fn_to_L1 {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (hf : μ) :
=ᵐ[μ] f
@[simp]
theorem measure_theory.integrable.to_L1_zero {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (h : μ) :
@[simp]
theorem measure_theory.integrable.to_L1_eq_mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : α → β) (hf : μ) :
@[simp]
theorem measure_theory.integrable.to_L1_eq_to_L1_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f g : α → β) (hf : μ) (hg : μ) :
f =ᵐ[μ] g
theorem measure_theory.integrable.to_L1_add {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f g : α → β) (hf : μ) (hg : μ) :
theorem measure_theory.integrable.to_L1_neg {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : α → β) (hf : μ) :
theorem measure_theory.integrable.to_L1_sub {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f g : α → β) (hf : μ) (hg : μ) :
theorem measure_theory.integrable.norm_to_L1 {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : α → β) (hf : μ) :
= (∫⁻ (a : α), has_edist.edist (f a) 0 μ).to_real
theorem measure_theory.integrable.norm_to_L1_eq_lintegral_norm {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : α → β) (hf : μ) :
= (∫⁻ (a : α), μ).to_real
@[simp]
theorem measure_theory.integrable.edist_to_L1_to_L1 {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f g : α → β) (hf : μ) (hg : μ) :
= ∫⁻ (a : α), has_edist.edist (f a) (g a) μ
@[simp]
theorem measure_theory.integrable.edist_to_L1_zero {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : α → β) (hf : μ) :
= ∫⁻ (a : α), has_edist.edist (f a) 0 μ
theorem measure_theory.integrable.to_L1_smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {𝕜 : Type u_5} [normed_field 𝕜] [ β] (f : α → β) (hf : μ) (k : 𝕜) :
measure_theory.integrable.to_L1 (λ (a : α), k f a) _ =
theorem measure_theory.integrable.to_L1_smul' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {𝕜 : Type u_5} [normed_field 𝕜] [ β] (f : α → β) (hf : μ) (k : 𝕜) :
_ =
theorem measure_theory.integrable.apply_continuous_linear_map {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_5} [normed_group E] {𝕜 : Type u_6} [ E] {H : Type u_7} [normed_group H] [ H] {φ : α → (H →L[𝕜] E)} (φ_int : μ) (v : H) :
measure_theory.integrable (λ (a : α), (φ a) v) μ
theorem continuous_linear_map.integrable_comp {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_5} [normed_group E] {𝕜 : Type u_6} [ E] {H : Type u_7} [normed_group H] [ H] {φ : α → H} (L : H →L[𝕜] E) (φ_int : μ) :
measure_theory.integrable (λ (a : α), L (φ a)) μ