mathlib documentation

measure_theory.function.l1_space

Integrable functions and space #

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

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

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

Notation #

Main definitions #

Implementation notes #

To prove something for an arbitrary integrable function, a useful theorem is integrable.induction in the file 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 : α), 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 : α), ennreal.of_real f a μ = ∫⁻ (a : α), edist (f a) 0 μ
theorem measure_theory.lintegral_edist_triangle {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [topological_space.second_countable_topology β] [measurable_space β] [opens_measurable_space β] {f g h : α → β} (hf : ae_measurable f μ) (hg : ae_measurable g μ) (hh : ae_measurable h μ) :
∫⁻ (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} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] :
∫⁻ (a : α), 0∥₊ μ = 0
theorem measure_theory.lintegral_nnnorm_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] [measurable_space β] [opens_measurable_space β] [measurable_space γ] [opens_measurable_space γ] {f : α → β} {g : α → γ} (hf : ae_measurable f μ) (hg : ae_measurable 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 : α → β) (μ : measure_theory.measure α . "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 : α → β) :
theorem measure_theory.has_finite_integral_iff_edist {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] (f : α → β) :
theorem measure_theory.has_finite_integral_iff_of_nnreal {α : Type u_1} {m : measurable_space α} {μ : 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} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} (hg : measure_theory.has_finite_integral g μ) (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 : measure_theory.has_finite_integral g μ) (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 : measure_theory.has_finite_integral f μ) (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 : measure_theory.has_finite_integral f μ) (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 : β} :
theorem measure_theory.has_finite_integral_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measure_theory.is_finite_measure μ] (c : β) :
theorem measure_theory.has_finite_integral_of_bounded {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measure_theory.is_finite_measure μ] {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 : measure_theory.has_finite_integral f ν) (hμ : μ ν) :
theorem measure_theory.has_finite_integral.smul_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (h : measure_theory.has_finite_integral f μ) {c : ℝ≥0∞} (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 : measure_theory.has_finite_integral f μ) :
theorem measure_theory.has_finite_integral.norm {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] {f : α → β} (hfi : measure_theory.has_finite_integral f μ) :
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 : α → ℝ≥0∞} (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 (𝓝 (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} {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 (𝓝 (f a))) :
∀ᵐ (a : α) ∂μ, ennreal.of_real f 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 : measure_theory.has_finite_integral bound μ) (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} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [borel_space β] [topological_space.second_countable_topology β] {F : α → β} {f : α → β} {bound : α → } (F_measurable : ∀ (n : ), ae_measurable (F n) μ) (f_measurable : ae_measurable f μ) (bound_has_finite_integral : measure_theory.has_finite_integral bound μ) (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 function

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 𝕜] [normed_space 𝕜 β] (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 𝕜] [normed_space 𝕜 β] {c : 𝕜} (hc : c 0) (f : α → β) :
theorem measure_theory.has_finite_integral.const_mul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (h : measure_theory.has_finite_integral 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 : α → } (h : measure_theory.has_finite_integral f μ) (c : ) :
measure_theory.has_finite_integral (λ (x : α), (f x) * c) μ

The predicate integrable #

def measure_theory.integrable {β : Type u_2} [normed_group β] [measurable_space β] {α : Type u_1} {m : measurable_space α} (f : α → β) (μ : measure_theory.measure α . "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} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] {f : α → β} (hf : measure_theory.integrable f μ) :
theorem measure_theory.integrable.mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [normed_group γ] [measurable_space β] [measurable_space γ] {f : α → β} {g : α → γ} (hg : measure_theory.integrable g μ) (hf : ae_measurable f μ) (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 β] [measurable_space β] {f : α → β} {g : α → } (hg : measure_theory.integrable g μ) (hf : ae_measurable f μ) (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 γ] [measurable_space β] [measurable_space γ] {f : α → β} {g : α → γ} (hf : measure_theory.integrable f μ) (hg : ae_measurable g μ) (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 γ] [measurable_space β] [measurable_space γ] {f : α → β} {g : α → γ} (hf : ae_measurable f μ) (hg : ae_measurable 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 β] [measurable_space β] {f g : α → β} (hf : measure_theory.integrable f μ) (h : f =ᵐ[μ] g) :
theorem measure_theory.integrable_congr {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] {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 β] [measurable_space β] {c : β} :
measure_theory.integrable (λ (x : α), c) μ c = 0 μ set.univ <
theorem measure_theory.integrable_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [measure_theory.is_finite_measure μ] (c : β) :
measure_theory.integrable (λ (x : α), c) μ
theorem measure_theory.integrable.mono_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [normed_group β] [measurable_space β] {f : α → β} (h : measure_theory.integrable f ν) (hμ : μ ν) :
theorem measure_theory.integrable.add_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [normed_group β] [measurable_space β] {f : α → β} (hμ : measure_theory.integrable f μ) (hν : measure_theory.integrable f ν) :
theorem measure_theory.integrable.left_of_add_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [normed_group β] [measurable_space β] {f : α → β} (h : measure_theory.integrable f + ν)) :
theorem measure_theory.integrable.right_of_add_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ ν : measure_theory.measure α} [normed_group β] [measurable_space β] {f : α → β} (h : measure_theory.integrable f + ν)) :
@[simp]
theorem measure_theory.integrable.smul_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] {f : α → β} (h : measure_theory.integrable f μ) {c : ℝ≥0∞} (hc : c ) :
theorem measure_theory.integrable_map_measure {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [measurable_space δ] [opens_measurable_space β] {f : α → δ} {g : δ → β} (hg : ae_measurable g ((measure_theory.measure.map f) μ)) (hf : measurable f) :
theorem measure_theory.integrable_map_equiv {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [measurable_space δ] (f : α ≃ᵐ δ) (g : δ → β) :
theorem measure_theory.lintegral_edist_lt_top {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [opens_measurable_space β] {f g : α → β} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) :
∫⁻ (a : α), 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 β] [measurable_space β] :
measure_theory.integrable (λ (_x : α), 0) μ
theorem measure_theory.integrable.add' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [opens_measurable_space β] {f g : α → β} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) :
theorem measure_theory.integrable_finset_sum {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] {ι : Type u_3} [borel_space β] [topological_space.second_countable_topology β] (s : finset ι) {f : ι → α → β} (hf : ∀ (i : ι), measure_theory.integrable (f i) μ) :
measure_theory.integrable (λ (a : α), ∑ (i : ι) in s, f i a) μ
theorem measure_theory.integrable.neg {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [borel_space β] {f : α → β} (hf : measure_theory.integrable f μ) :
@[simp]
theorem measure_theory.integrable_neg_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [borel_space β] {f : α → β} :
theorem measure_theory.integrable.sub' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [opens_measurable_space β] {f g : α → β} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) :
theorem measure_theory.integrable.norm {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [opens_measurable_space β] {f : α → β} (hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (a : α), f a) μ
theorem measure_theory.integrable_norm_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [opens_measurable_space β] {f : α → β} (hf : ae_measurable f μ) :
theorem measure_theory.integrable_of_norm_sub_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [opens_measurable_space β] {f₀ f₁ : α → β} {g : α → } (hf₁_m : ae_measurable f₁ μ) (hf₀_i : measure_theory.integrable f₀ μ) (hg_i : measure_theory.integrable g μ) (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 γ] [measurable_space β] [measurable_space γ] [opens_measurable_space β] [opens_measurable_space γ] {f : α → β} {g : α → γ} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) :
measure_theory.integrable (λ (x : α), (f x, g x)) μ
theorem measure_theory.mem_ℒp_one_iff_integrable {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] {f : α → β} :
theorem measure_theory.mem_ℒp.integrable {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [borel_space β] {q : ℝ≥0∞} (hq1 : 1 q) {f : α → β} [measure_theory.is_finite_measure μ] (hfq : measure_theory.mem_ℒp f q μ) :
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 γ] [measurable_space β] [measurable_space γ] [complete_space β] [borel_space β] [borel_space γ] {K K' : ℝ≥0} {f : α → β} {g : β → γ} (hg : lipschitz_with K g) (hg' : antilipschitz_with K' 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 f μ) :
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 : α → ℝ≥0∞} (hf : ∀ᵐ (x : α) ∂μ, f x < ) :
(λ (x : α), ennreal.of_real (f x).to_real) =ᵐ[μ] f
theorem measure_theory.integrable_with_density_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (hf : measurable f) (hflt : ∀ᵐ (x : α) ∂μ, f x < ) {g : α → } (hg : measurable g) :
theorem measure_theory.mem_ℒ1_to_real_of_lintegral_ne_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ℝ≥0∞} (hfm : ae_measurable f μ) (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 : α → ℝ≥0∞} (hfm : ae_measurable f μ) (hfi : ∫⁻ (x : α), f x μ ) :
measure_theory.integrable (λ (x : α), (f x).to_real) μ

Lemmas used for defining the positive part of a function #

theorem measure_theory.integrable.max_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (a : α), max (f a) 0) μ
theorem measure_theory.integrable.min_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (a : α), min (f a) 0) μ
theorem measure_theory.integrable.smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 β] [measurable_space 𝕜] [opens_measurable_space 𝕜] [borel_space β] (c : 𝕜) {f : α → β} (hf : measure_theory.integrable f μ) :
theorem measure_theory.integrable_smul_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 β] [measurable_space 𝕜] [opens_measurable_space 𝕜] [borel_space β] {c : 𝕜} (hc : c 0) (f : α → β) :
theorem measure_theory.integrable.const_mul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (h : measure_theory.integrable f μ) (c : ) :
measure_theory.integrable (λ (x : α), c * f x) μ
theorem measure_theory.integrable.mul_const {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → } (h : measure_theory.integrable f μ) (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} [nondiscrete_normed_field 𝕜] [complete_space 𝕜] [measurable_space 𝕜] [borel_space 𝕜] {E : Type u_6} [normed_group E] [normed_space 𝕜 E] [measurable_space E] [borel_space E] {f : α → 𝕜} {c : E} (hc : c 0) :
theorem measure_theory.integrable.re {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [is_R_or_C 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] {f : α → 𝕜} (hf : measure_theory.integrable f μ) :
theorem measure_theory.integrable.im {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [is_R_or_C 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] {f : α → 𝕜} (hf : measure_theory.integrable f μ) :
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 𝕜] [measurable_space 𝕜] [borel_space 𝕜] [inner_product_space 𝕜 E] [measurable_space E] [opens_measurable_space E] [topological_space.second_countable_topology E] {f : α → E} (c : E) (hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (x : α), inner c (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 𝕜] [measurable_space 𝕜] [borel_space 𝕜] [inner_product_space 𝕜 E] [measurable_space E] [opens_measurable_space E] [topological_space.second_countable_topology E] {f : α → E} (hf : measure_theory.integrable f μ) (c : E) :
measure_theory.integrable (λ (x : α), inner (f x) c) μ
theorem measure_theory.integrable.trim {α : Type u_1} {m : measurable_space α} {H : Type u_5} [normed_group H] [measurable_space H] [opens_measurable_space H] {m0 : measurable_space α} {μ' : measure_theory.measure α} {f : α → H} (hm : m m0) (hf_int : measure_theory.integrable f μ') (hf : measurable f) :
theorem measure_theory.integrable_of_integrable_trim {α : Type u_1} {m : measurable_space α} {H : Type u_5} [normed_group H] [measurable_space H] [opens_measurable_space H] {m0 : measurable_space α} {μ' : measure_theory.measure α} {f : α → H} (hm : m m0) (hf_int : measure_theory.integrable f (μ'.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] [measurable_space E] [opens_measurable_space E] {μ : measure_theory.measure α} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (C : ℝ≥0∞) (hC : C < ) {f : α → E} (hf_meas : ae_measurable f μ) (hf : ∀ (s : set α), measurable_set sμ 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] [measurable_space E] [opens_measurable_space E] [measure_theory.sigma_finite μ] (C : ℝ≥0∞) (hC : C < ) {f : α → E} (hf_meas : ae_measurable f μ) (hf : ∀ (s : set α), measurable_set sμ 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 β] [measurable_space β] (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_zero {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] :
theorem measure_theory.ae_eq_fun.integrable.neg {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [borel_space β] {f : α →ₘ[μ] β} :
theorem measure_theory.ae_eq_fun.integrable.sub {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [borel_space β] [topological_space.second_countable_topology β] {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 β] [measurable_space β] [borel_space β] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 β] [measurable_space 𝕜] [opens_measurable_space 𝕜] {c : 𝕜} {f : α →ₘ[μ] β} :
theorem measure_theory.L1.edist_def {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [borel_space β] (f g : (measure_theory.Lp β 1 μ)) :
edist f g = ∫⁻ (a : α), 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 β] [measurable_space β] [topological_space.second_countable_topology β] [borel_space β] (f g : (measure_theory.Lp β 1 μ)) :
dist f g = (∫⁻ (a : α), edist (f a) (g a) μ).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).

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).

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

Equations
theorem measure_theory.integrable.to_L1_smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [borel_space β] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 β] [measurable_space 𝕜] [opens_measurable_space 𝕜] (f : α → β) (hf : measure_theory.integrable f μ) (k : 𝕜) :
theorem integrable_zero_measure {α : Type u_1} {β : Type u_2} [normed_group β] {m : measurable_space α} [measurable_space β] {f : α → β} :
theorem measure_theory.integrable.apply_continuous_linear_map {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_5} [normed_group E] [measurable_space E] [borel_space E] [normed_space E] {H : Type u_6} [normed_group H] [normed_space H] {φ : α → (H →L[] E)} (φ_int : measure_theory.integrable φ μ) (v : H) :
measure_theory.integrable (λ (a : α), (φ a) v) μ
theorem continuous_linear_map.integrable_comp {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_7} [is_R_or_C 𝕜] {G : Type u_8} [normed_group G] [normed_space 𝕜 G] [measurable_space G] [borel_space G] {F : Type u_9} [normed_group F] [normed_space 𝕜 F] [measurable_space F] [opens_measurable_space F] {φ : α → F} (L : F →L[𝕜] G) (φ_int : measure_theory.integrable φ μ) :
measure_theory.integrable (λ (a : α), L (φ a)) μ