# mathlibdocumentation

measure_theory.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, nnnorm (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} {μ : measure_theory.measure α} [normed_group β] (f : α → β) :
∫⁻ (a : α), f a∥₊ μ = ∫⁻ (a : α), edist (f a) 0 μ
theorem measure_theory.lintegral_norm_eq_lintegral_edist {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] (f : α → β) :
∫⁻ (a : α), μ = ∫⁻ (a : α), edist (f a) 0 μ
theorem measure_theory.lintegral_edist_triangle {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f g h : α → β} (hf : μ) (hg : μ) (hh : μ) :
∫⁻ (a : α), edist (f a) (g a) μ ∫⁻ (a : α), edist (f a) (h a) μ + ∫⁻ (a : α), edist (g a) (h a) μ
theorem measure_theory.lintegral_nnnorm_zero {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] :
∫⁻ (a : α), 0∥₊ μ = 0
theorem measure_theory.lintegral_nnnorm_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} (hf : μ) (hg : μ) :
∫⁻ (a : α), f a∥₊ + g a∥₊ μ = ∫⁻ (a : α), f a∥₊ μ + ∫⁻ (a : α), g a∥₊ μ
theorem measure_theory.lintegral_nnnorm_neg {α : Type u_1} {β : Type u_2} {μ : 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 β] (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} {μ : measure_theory.measure α} [normed_group β] (f : α → β) :
∫⁻ (a : α), μ <
theorem measure_theory.has_finite_integral_iff_edist {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] (f : α → β) :
∫⁻ (a : α), edist (f a) 0 μ <
theorem measure_theory.has_finite_integral_iff_of_real {α : Type u_1} {μ : 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} {μ : measure_theory.measure α} {f : α → ℝ≥0} :
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} {μ : 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} {μ : 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} {μ : 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} {μ : 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} {μ : measure_theory.measure α} [normed_group β] {f g : α → β} (hf : μ) (h : f =ᵐ[μ] g) :
theorem measure_theory.has_finite_integral_congr {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f g : α → β} (h : f =ᵐ[μ] g) :
theorem measure_theory.has_finite_integral_const_iff {α : Type u_1} {β : Type u_2} {μ : 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} {μ : measure_theory.measure α} [normed_group β] (c : β) :
theorem measure_theory.has_finite_integral_of_bounded {α : Type u_1} {β : Type u_2} {μ : 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} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (hμ : μ ν) :
theorem measure_theory.has_finite_integral.add_measure {α : Type u_1} {β : Type u_2} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (hμ : μ) (hν : ν) :
theorem measure_theory.has_finite_integral.left_of_add_measure {α : Type u_1} {β : Type u_2} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (h : + ν)) :
theorem measure_theory.has_finite_integral.right_of_add_measure {α : Type u_1} {β : Type u_2} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (h : + ν)) :
@[simp]
theorem measure_theory.has_finite_integral_add_measure {α : Type u_1} {β : Type u_2} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} :
theorem measure_theory.has_finite_integral.smul_measure {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f : α → β} {c : ℝ≥0∞} (hc : c < ) :
@[simp]
theorem measure_theory.has_finite_integral_zero_measure {α : Type u_1} {β : Type u_2} [normed_group β] (f : α → β) :
@[simp]
theorem measure_theory.has_finite_integral_zero (α : Type u_1) (β : Type u_2) (μ : measure_theory.measure α) [normed_group β] :
theorem measure_theory.has_finite_integral.neg {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (hfi : μ) :
@[simp]
theorem measure_theory.has_finite_integral_neg_iff {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f : α → β} :
theorem measure_theory.has_finite_integral.norm {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (hfi : μ) :
theorem measure_theory.has_finite_integral_norm_iff {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] (f : α → β) :
theorem measure_theory.all_ae_of_real_F_le_bound {α : Type u_1} {β : Type u_2} {μ : 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} {μ : measure_theory.measure α} [normed_group β] {F : α → β} {f : α → β} (h : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ), F n a) filter.at_top (𝓝 (f a))) :
∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ), ennreal.of_real F n a) filter.at_top (𝓝 (ennreal.of_real f a))
theorem measure_theory.all_ae_of_real_f_le_bound {α : Type u_1} {β : Type u_2} {μ : 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 (𝓝 (f a))) :
∀ᵐ (a : α) ∂μ, ennreal.of_real (bound a)
theorem measure_theory.has_finite_integral_of_dominated_convergence {α : Type u_1} {β : Type u_2} {μ : 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 (𝓝 (f a))) :
theorem measure_theory.tendsto_lintegral_norm_of_dominated_convergence {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] {F : α → β} {f : α → β} {bound : α → } (F_measurable : ∀ (n : ), ae_measurable (F n) μ) (f_measurable : μ) (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 (𝓝 (f a))) :
filter.tendsto (λ (n : ), ∫⁻ (a : α), ennreal.of_real F n a - f a μ) filter.at_top (𝓝 0)

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

theorem measure_theory.has_finite_integral.max_zero {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (hf : μ) :
measure_theory.has_finite_integral (λ (a : α), max (f a) 0) μ
theorem measure_theory.has_finite_integral.min_zero {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (hf : μ) :
measure_theory.has_finite_integral (λ (a : α), min (f a) 0) μ
theorem measure_theory.has_finite_integral.smul {α : Type u_1} {β : Type u_2} {μ : 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} {μ : 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} {μ : 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} {μ : measure_theory.measure α} {f : α → } (c : ) :
measure_theory.has_finite_integral (λ (x : α), (f x) * c) μ

### The predicate integrable#

def measure_theory.integrable {α : Type u_1} {β : Type u_2} [normed_group β] (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.integrable.ae_measurable {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (hf : μ) :
theorem measure_theory.integrable.has_finite_integral {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (hf : μ) :
theorem measure_theory.integrable.mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} (hg : μ) (hf : μ) (h : ∀ᵐ (a : α) ∂μ, f a g a) :
theorem measure_theory.integrable.mono' {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f : α → β} {g : α → } (hg : μ) (hf : μ) (h : ∀ᵐ (a : α) ∂μ, f a g a) :
theorem measure_theory.integrable.congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} (hf : μ) (hg : μ) (h : ∀ᵐ (a : α) ∂μ, f a = g a) :
theorem measure_theory.integrable_congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} (hf : μ) (hg : μ) (h : ∀ᵐ (a : α) ∂μ, f a = g a) :
theorem measure_theory.integrable.congr {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f g : α → β} (hf : μ) (h : f =ᵐ[μ] g) :
theorem measure_theory.integrable_congr {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f g : α → β} (h : f =ᵐ[μ] g) :
theorem measure_theory.integrable_const_iff {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {c : β} :
measure_theory.integrable (λ (x : α), c) μ c = 0
theorem measure_theory.integrable_const {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] (c : β) :
measure_theory.integrable (λ (x : α), c) μ
theorem measure_theory.integrable.mono_measure {α : Type u_1} {β : Type u_2} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (h : ν) (hμ : μ ν) :
theorem measure_theory.integrable.add_measure {α : Type u_1} {β : Type u_2} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (hμ : μ) (hν : ν) :
+ ν)
theorem measure_theory.integrable.left_of_add_measure {α : Type u_1} {β : Type u_2} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (h : + ν)) :
theorem measure_theory.integrable.right_of_add_measure {α : Type u_1} {β : Type u_2} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} (h : + ν)) :
@[simp]
theorem measure_theory.integrable_add_measure {α : Type u_1} {β : Type u_2} {μ ν : measure_theory.measure α} [normed_group β] {f : α → β} :
theorem measure_theory.integrable.smul_measure {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (h : μ) {c : ℝ≥0∞} (hc : c < ) :
(c μ)
theorem measure_theory.integrable_map_measure {α : Type u_1} {β : Type u_2} {δ : Type u_4} {μ : measure_theory.measure α} [normed_group β] {f : α → δ} {g : δ → β} (hg : μ)) (hf : measurable f) :
μ
theorem measure_theory.lintegral_edist_lt_top {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f g : α → β} (hf : μ) (hg : μ) :
∫⁻ (a : α), edist (f a) (g a) μ <
@[simp]
theorem measure_theory.integrable_zero (α : Type u_1) (β : Type u_2) (μ : measure_theory.measure α) [normed_group β]  :
measure_theory.integrable (λ (_x : α), 0) μ
theorem measure_theory.integrable.add' {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f g : α → β} (hf : μ) (hg : μ) :
theorem measure_theory.integrable.add {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] {f g : α → β} (hf : μ) (hg : μ) :
μ
theorem measure_theory.integrable_finset_sum {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {ι : Type u_3} [borel_space β] (s : finset ι) {f : ι → α → β} (hf : ∀ (i : ι), μ) :
measure_theory.integrable (λ (a : α), ∑ (i : ι) in s, f i a) μ
theorem measure_theory.integrable.neg {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] {f : α → β} (hf : μ) :
@[simp]
theorem measure_theory.integrable_neg_iff {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] {f : α → β} :
theorem measure_theory.integrable.sub' {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f g : α → β} (hf : μ) (hg : μ) :
theorem measure_theory.integrable.sub {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] {f g : α → β} (hf : μ) (hg : μ) :
μ
theorem measure_theory.integrable.norm {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (hf : μ) :
measure_theory.integrable (λ (a : α), f a) μ
theorem measure_theory.integrable_norm_iff {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (hf : μ) :
measure_theory.integrable (λ (a : α), f a) μ
theorem measure_theory.integrable_of_norm_sub_le {α : Type u_1} {β : Type u_2} {μ : 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} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} (hf : μ) (hg : μ) :
measure_theory.integrable (λ (x : α), (f x, g x)) μ
theorem measure_theory.mem_ℒp_one_iff_integrable {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f : α → β} :
theorem measure_theory.mem_ℒp.integrable {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] {q : ℝ≥0∞} (hq1 : 1 q) {f : α → β} (hfq : μ) :
theorem measure_theory.lipschitz_with.integrable_comp_iff_of_antilipschitz {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] [borel_space β] [borel_space γ] {K K' : ℝ≥0} {f : α → β} {g : β → γ} (hg : g) (hg' : g) (g0 : g 0 = 0) :
μ
theorem measure_theory.integrable.real_to_nnreal {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (hf : μ) :
measure_theory.integrable (λ (x : α), ((f x).to_nnreal)) μ

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

theorem measure_theory.integrable.max_zero {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (hf : μ) :
measure_theory.integrable (λ (a : α), max (f a) 0) μ
theorem measure_theory.integrable.min_zero {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (hf : μ) :
measure_theory.integrable (λ (a : α), min (f a) 0) μ
theorem measure_theory.integrable.smul {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {𝕜 : Type u_5} [normed_field 𝕜] [ β] [borel_space β] (c : 𝕜) {f : α → β} (hf : μ) :
μ
theorem measure_theory.integrable_smul_iff {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {𝕜 : Type u_5} [normed_field 𝕜] [ β] [borel_space β] {c : 𝕜} (hc : c 0) (f : α → β) :
μ
theorem measure_theory.integrable.const_mul {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (h : μ) (c : ) :
measure_theory.integrable (λ (x : α), c * f x) μ
theorem measure_theory.integrable.mul_const {α : Type u_1} {μ : measure_theory.measure α} {f : α → } (h : μ) (c : ) :
measure_theory.integrable (λ (x : α), (f x) * c) μ
theorem measure_theory.integrable_smul_const {α : Type u_1} {μ : measure_theory.measure α} {𝕜 : Type u_5} [borel_space 𝕜] {E : Type u_6} [normed_group E] [ E] [borel_space E] {f : α → 𝕜} {c : E} (hc : c 0) :
measure_theory.integrable (λ (x : α), f x c) μ
theorem measure_theory.integrable.trim {H : Type u_5} {α' : Type u_6} [normed_group H] {m m0 : measurable_space α'} {μ' : measure_theory.measure α'} (hm : m m0) {f : α' → H} (hf_int : μ') (hf : measurable f) :
(μ'.trim hm)
theorem measure_theory.integrable_of_integrable_trim {H : Type u_5} {α' : Type u_6} [normed_group H] {m m0 : measurable_space α'} {μ' : measure_theory.measure α'} (hm : m m0) {f : α' → H} (hf_int : (μ'.trim hm)) :
theorem measure_theory.integrable_of_forall_fin_meas_le' {α' : Type u_5} {E : Type u_6} {m m0 : measurable_space α'} [normed_group E] {μ : measure_theory.measure α'} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (C : ℝ≥0∞) (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} {μ : measure_theory.measure α} {E : Type u_6} [normed_group E] (C : ℝ≥0∞) (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} {μ : 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} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (hf : μ) :
theorem measure_theory.ae_eq_fun.integrable_coe_fn {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] {f : α →ₘ[μ] β} :
theorem measure_theory.ae_eq_fun.integrable_zero {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β]  :
theorem measure_theory.ae_eq_fun.integrable.neg {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] {f : α →ₘ[μ] β} :
theorem measure_theory.ae_eq_fun.integrable_iff_mem_L1 {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] {f : α →ₘ[μ] β} :
theorem measure_theory.ae_eq_fun.integrable.add {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] {f g : α →ₘ[μ] β} :
f.integrableg.integrable(f + g).integrable
theorem measure_theory.ae_eq_fun.integrable.sub {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] {f g : α →ₘ[μ] β} (hf : f.integrable) (hg : g.integrable) :
theorem measure_theory.ae_eq_fun.integrable.smul {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] {𝕜 : Type u_5} [normed_field 𝕜] [ β] {c : 𝕜} {f : α →ₘ[μ] β} :
theorem measure_theory.L1.integrable_coe_fn {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f : μ)) :
theorem measure_theory.L1.has_finite_integral_coe_fn {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f : μ)) :
theorem measure_theory.L1.measurable_coe_fn {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f : μ)) :
theorem measure_theory.L1.ae_measurable_coe_fn {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f : μ)) :
theorem measure_theory.L1.edist_def {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f g : μ)) :
g = ∫⁻ (a : α), edist (f a) (g a) μ
theorem measure_theory.L1.dist_def {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f g : μ)) :
dist f g = (∫⁻ (a : α), edist (f a) (g a) μ).to_real
theorem measure_theory.L1.norm_def {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f : μ)) :
theorem measure_theory.L1.norm_sub_eq_lintegral {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (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} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f : μ)) :
= ∫⁻ (x : α), f x∥₊ μ
theorem measure_theory.L1.of_real_norm_sub_eq_lintegral {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (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).

def measure_theory.integrable.to_L1 {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (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} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f : μ)) (hf : μ) :
theorem measure_theory.integrable.coe_fn_to_L1 {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] {f : α → β} (hf : μ) :
=ᵐ[μ] f
@[simp]
theorem measure_theory.integrable.to_L1_zero {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (h : μ) :
@[simp]
theorem measure_theory.integrable.to_L1_eq_mk {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f : α → β) (hf : μ) :
@[simp]
theorem measure_theory.integrable.to_L1_eq_to_L1_iff {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f g : α → β) (hf : μ) (hg : μ) :
f =ᵐ[μ] g
theorem measure_theory.integrable.to_L1_add {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f g : α → β) (hf : μ) (hg : μ) :
theorem measure_theory.integrable.to_L1_neg {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f : α → β) (hf : μ) :
theorem measure_theory.integrable.to_L1_sub {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f g : α → β) (hf : μ) (hg : μ) :
theorem measure_theory.integrable.norm_to_L1 {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f : α → β) (hf : μ) :
= (∫⁻ (a : α), edist (f a) 0 μ).to_real
theorem measure_theory.integrable.norm_to_L1_eq_lintegral_norm {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f : α → β) (hf : μ) :
= (∫⁻ (a : α), μ).to_real
@[simp]
theorem measure_theory.integrable.edist_to_L1_to_L1 {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f g : α → β) (hf : μ) (hg : μ) :
= ∫⁻ (a : α), edist (f a) (g a) μ
@[simp]
theorem measure_theory.integrable.edist_to_L1_zero {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] (f : α → β) (hf : μ) :
0 = ∫⁻ (a : α), edist (f a) 0 μ
theorem measure_theory.integrable.to_L1_smul {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [normed_group β] [borel_space β] {𝕜 : Type u_5} [normed_field 𝕜] [ β] (f : α → β) (hf : μ) (k : 𝕜) :
measure_theory.integrable.to_L1 (λ (a : α), k f a) _ =
theorem integrable_zero_measure {α : Type u_1} {β : Type u_2} [normed_group β] {f : α → β} :
theorem measure_theory.integrable.apply_continuous_linear_map {α : Type u_1} {μ : measure_theory.measure α} {E : Type u_5} [normed_group E] [borel_space E] [ E] {H : Type u_6} [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} {μ : measure_theory.measure α} {𝕜 : Type u_7} [is_R_or_C 𝕜] {G : Type u_8} [normed_group G] [ G] [borel_space G] {F : Type u_9} [normed_group F] [ F] {φ : α → F} (L : F →L[𝕜] G) (φ_int : μ) :
measure_theory.integrable (λ (a : α), L (φ a)) μ