mathlib3 documentation

measure_theory.function.l1_space

Integrable functions and space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_add_comm_group β] (f : α β) :
∫⁻ (a : α), 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_add_comm_group β] {f g h : α β} (hf : measure_theory.ae_strongly_measurable f μ) (hh : measure_theory.ae_strongly_measurable 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_add_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] [normed_add_comm_group γ] {f : α β} (hf : measure_theory.ae_strongly_measurable 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_add_comm_group β] [normed_add_comm_group γ] (f : α β) {g : α γ} (hg : measure_theory.ae_strongly_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_add_comm_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_add_comm_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.all_ae_of_real_F_le_bound {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {F : α β} {bound : α } (h : (n : ), ∀ᵐ (a : α) μ, F n a bound a) (n : ) :
theorem measure_theory.all_ae_tendsto_of_real_norm {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {F : α β} {f : α β} (h : ∀ᵐ (a : α) μ, filter.tendsto (λ (n : ), F n a) filter.at_top (nhds (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_add_comm_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))) :
theorem measure_theory.has_finite_integral_of_dominated_convergence {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_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 (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_add_comm_group β] {F : α β} {f : α β} {bound : α } (F_measurable : (n : ), measure_theory.ae_strongly_measurable (F n) μ) (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 (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 function

theorem measure_theory.has_finite_integral.const_mul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] {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 α} {𝕜 : Type u_5} [normed_ring 𝕜] {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_add_comm_group β] {α : 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.mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] [normed_add_comm_group γ] {f : α β} {g : α γ} (hg : measure_theory.integrable g μ) (hf : measure_theory.ae_strongly_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_add_comm_group β] {f : α β} {g : α } (hg : measure_theory.integrable g μ) (hf : measure_theory.ae_strongly_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_add_comm_group β] [normed_add_comm_group γ] {f : α β} {g : α γ} (hf : measure_theory.integrable f μ) (hg : measure_theory.ae_strongly_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_add_comm_group β] {f g : α β} (hf : measure_theory.integrable f μ) (h : f =ᵐ[μ] g) :
theorem measure_theory.integrable_const_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {c : β} :
measure_theory.integrable (λ (x : α), c) μ c = 0 μ set.univ <
@[simp]
theorem measure_theory.mem_ℒp.integrable_norm_rpow {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {f : α β} {p : ennreal} (hf : measure_theory.mem_ℒp f p μ) (hp_ne_zero : p 0) (hp_ne_top : p ) :
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_add_comm_group β] {f : α β} (h : measure_theory.integrable f ν) (hμ : μ ν) :
theorem measure_theory.integrable.of_measure_le_smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {μ' : measure_theory.measure α} (c : ennreal) (hc : c ) (hμ'_le : μ' c μ) {f : α β} (hf : measure_theory.integrable f μ) :
@[simp]
theorem measure_theory.integrable_finset_sum_measure {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {ι : Type u_3} {m : measurable_space α} {f : α β} {μ : ι measure_theory.measure α} {s : finset ι} :
measure_theory.integrable f (s.sum (λ (i : ι), μ i)) (i : ι), i s measure_theory.integrable f (μ i)
theorem measure_theory.integrable_smul_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {f : α β} {c : ennreal} (h₁ : c 0) (h₂ : c ) :
theorem measure_theory.integrable_inv_smul_measure {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {f : α β} {c : ennreal} (h₁ : c 0) (h₂ : c ) :
theorem measure_theory.lintegral_edist_lt_top {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {f g : α β} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) :
∫⁻ (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_add_comm_group β] :
measure_theory.integrable (λ (_x : α), 0) μ
theorem measure_theory.integrable_finset_sum' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {ι : Type u_3} (s : finset ι) {f : ι α β} (hf : (i : ι), i s measure_theory.integrable (f i) μ) :
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_add_comm_group β] {ι : Type u_3} (s : finset ι) {f : ι α β} (hf : (i : ι), i s measure_theory.integrable (f i) μ) :
measure_theory.integrable (λ (a : α), s.sum (λ (i : ι), f i a)) μ
theorem measure_theory.integrable.norm {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {f : α β} (hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (a : α), f a) μ
theorem measure_theory.integrable.abs {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {β : Type u_2} [normed_lattice_add_comm_group β] {f : α β} (hf : measure_theory.integrable f μ) :
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} [normed_division_ring F] {f g : α F} (hint : measure_theory.integrable g μ) (hm : measure_theory.ae_strongly_measurable f μ) (hfbdd : (C : ), (x : α), f x C) :
measure_theory.integrable (λ (x : α), f x * g x) μ
theorem measure_theory.integrable.ess_sup_smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {𝕜 : Type u_3} [normed_field 𝕜] [normed_space 𝕜 β] {f : α β} (hf : measure_theory.integrable f μ) {g : α 𝕜} (g_ae_strongly_measurable : measure_theory.ae_strongly_measurable g μ) (ess_sup_g : ess_sup (λ (x : α), g x‖₊) μ ) :
measure_theory.integrable (λ (x : α), g x f x) μ

Hölder's inequality for integrable functions: the scalar multiplication of an integrable vector-valued function by a scalar function with finite essential supremum is integrable.

theorem measure_theory.integrable.smul_ess_sup {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {𝕜 : Type u_3} [normed_ring 𝕜] [module 𝕜 β] [has_bounded_smul 𝕜 β] {f : α 𝕜} (hf : measure_theory.integrable f μ) {g : α β} (g_ae_strongly_measurable : measure_theory.ae_strongly_measurable g μ) (ess_sup_g : ess_sup (λ (x : α), g x‖₊) μ ) :
measure_theory.integrable (λ (x : α), f x g x) μ

Hölder's inequality for integrable functions: the scalar multiplication of an integrable scalar-valued function by a vector-value function with finite essential supremum is integrable.

theorem measure_theory.integrable_of_norm_sub_le {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {f₀ f₁ : α β} {g : α } (hf₁_m : measure_theory.ae_strongly_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_add_comm_group β] [normed_add_comm_group γ] {f : α β} {g : α γ} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) :
measure_theory.integrable (λ (x : α), (f x, g x)) μ
theorem measure_theory.integrable.measure_ge_lt_top {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {f : α β} (hf : measure_theory.integrable f μ) {ε : } (hε : 0 < ε) :
μ {x : α | ε f x} <

A non-quantitative version of Markov inequality for integrable functions: the measure of points where ‖f x‖ ≥ ε is finite for all positive ε.

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_add_comm_group β] [normed_add_comm_group γ] {K K' : nnreal} {f : α β} {g : β γ} (hg : lipschitz_with K g) (hg' : antilipschitz_with K' g) (g0 : g 0 = 0) :
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_smul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_5} [normed_add_comm_group E] [normed_space E] {f : α nnreal} (hf : measurable f) {g : α E} :
measure_theory.integrable g (μ.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_add_comm_group E] [normed_space E] {f : α ennreal} (hf : measurable f) (hflt : ∀ᵐ (x : α) μ, f x < ) {g : α E} :
theorem measure_theory.integrable_with_density_iff_integrable_smul₀ {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_5} [normed_add_comm_group E] [normed_space E] {f : α nnreal} (hf : ae_measurable f μ) {g : α E} :
measure_theory.integrable g (μ.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 : α } :
theorem measure_theory.mem_ℒ1_smul_of_L1_with_density {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_5} [normed_add_comm_group E] [normed_space E] {f : α nnreal} (f_meas : measurable f) (u : (measure_theory.Lp E 1 (μ.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_add_comm_group E] [normed_space E] {f : α nnreal} (f_meas : measurable f) :

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_add_comm_group E] [normed_space E] {f : α nnreal} (f_meas : measurable f) (u : (measure_theory.Lp E 1 (μ.with_density (λ (x : α), (f x))))) :
theorem measure_theory.mem_ℒ1_to_real_of_lintegral_ne_top {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (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 : α ennreal} (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.smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {𝕜 : Type u_5} [normed_add_comm_group 𝕜] [smul_zero_class 𝕜 β] [has_bounded_smul 𝕜 β] (c : 𝕜) {f : α β} (hf : measure_theory.integrable f μ) :
theorem measure_theory.is_unit.integrable_smul_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {𝕜 : Type u_5} [normed_ring 𝕜] [module 𝕜 β] [has_bounded_smul 𝕜 β] {c : 𝕜} (hc : is_unit c) (f : α β) :
theorem measure_theory.integrable_smul_iff {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {𝕜 : Type u_5} [normed_division_ring 𝕜] [module 𝕜 β] [has_bounded_smul 𝕜 β] {c : 𝕜} (hc : c 0) (f : α β) :
theorem measure_theory.integrable.smul_of_top_right {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {𝕜 : Type u_5} [normed_ring 𝕜] [module 𝕜 β] [has_bounded_smul 𝕜 β] {f : α β} {φ : α 𝕜} (hf : measure_theory.integrable f μ) (hφ : measure_theory.mem_ℒp φ μ) :
theorem measure_theory.integrable.smul_of_top_left {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {𝕜 : Type u_5} [normed_ring 𝕜] [module 𝕜 β] [has_bounded_smul 𝕜 β] {f : α β} {φ : α 𝕜} (hφ : measure_theory.integrable φ μ) (hf : measure_theory.mem_ℒp f μ) :
theorem measure_theory.integrable.smul_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {𝕜 : Type u_5} [normed_ring 𝕜] [module 𝕜 β] [has_bounded_smul 𝕜 β] {f : α 𝕜} (hf : 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} [nontrivially_normed_field 𝕜] [complete_space 𝕜] {E : Type u_6} [normed_add_comm_group E] [normed_space 𝕜 E] {f : α 𝕜} {c : E} (hc : c 0) :
theorem measure_theory.integrable.const_mul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] {f : α 𝕜} (h : measure_theory.integrable f μ) (c : 𝕜) :
measure_theory.integrable (λ (x : α), c * f x) μ
theorem measure_theory.integrable.const_mul' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] {f : α 𝕜} (h : measure_theory.integrable f μ) (c : 𝕜) :
measure_theory.integrable ((λ (x : α), c) * f) μ
theorem measure_theory.integrable.mul_const {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] {f : α 𝕜} (h : measure_theory.integrable f μ) (c : 𝕜) :
measure_theory.integrable (λ (x : α), f x * c) μ
theorem measure_theory.integrable.mul_const' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] {f : α 𝕜} (h : measure_theory.integrable f μ) (c : 𝕜) :
measure_theory.integrable (f * λ (x : α), c) μ
theorem measure_theory.integrable_const_mul_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] {c : 𝕜} (hc : is_unit c) (f : α 𝕜) :
theorem measure_theory.integrable_mul_const_iff {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] {c : 𝕜} (hc : is_unit c) (f : α 𝕜) :
theorem measure_theory.integrable.bdd_mul' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_ring 𝕜] {f g : α 𝕜} {c : } (hg : measure_theory.integrable g μ) (hf : measure_theory.ae_strongly_measurable f μ) (hf_bound : ∀ᵐ (x : α) μ, f x c) :
measure_theory.integrable (λ (x : α), f x * g x) μ
theorem measure_theory.integrable.div_const {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {𝕜 : Type u_5} [normed_division_ring 𝕜] {f : α 𝕜} (h : measure_theory.integrable f μ) (c : 𝕜) :
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 f μ) :
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 : 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 𝕜] {f : α 𝕜} (hf : measure_theory.integrable f μ) :
theorem measure_theory.integrable_of_integrable_trim {α : Type u_1} {m : measurable_space α} {H : Type u_5} [normed_add_comm_group 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_add_comm_group E] {μ : measure_theory.measure α} (hm : m m0) [measure_theory.sigma_finite (μ.trim hm)] (C : ennreal) (hC : C < ) {f : α E} (hf_meas : measure_theory.ae_strongly_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_add_comm_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.sub {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_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_add_comm_group β] {𝕜 : Type u_5} [normed_ring 𝕜] [module 𝕜 β] [has_bounded_smul 𝕜 β] {c : 𝕜} {f : α →ₘ[μ] β} :
theorem measure_theory.L1.edist_def {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] (f g : (measure_theory.Lp β 1 μ)) :
theorem measure_theory.L1.dist_def {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] (f g : (measure_theory.Lp β 1 μ)) :
theorem measure_theory.L1.norm_sub_eq_lintegral {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] (f g : (measure_theory.Lp β 1 μ)) :
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).

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_add_comm_group β] {𝕜 : Type u_5} [normed_ring 𝕜] [module 𝕜 β] [has_bounded_smul 𝕜 β] (f : α β) (hf : measure_theory.integrable f μ) (k : 𝕜) :
theorem measure_theory.integrable.to_L1_smul' {α : Type u_1} {β : Type u_2} {m : measurable_space α} {μ : measure_theory.measure α} [normed_add_comm_group β] {𝕜 : Type u_5} [normed_ring 𝕜] [module 𝕜 β] [has_bounded_smul 𝕜 β] (f : α β) (hf : measure_theory.integrable f μ) (k : 𝕜) :
theorem measure_theory.integrable.apply_continuous_linear_map {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_5} [normed_add_comm_group E] {𝕜 : Type u_6} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] {H : Type u_7} [normed_add_comm_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 α} {E : Type u_5} [normed_add_comm_group E] {𝕜 : Type u_6} [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] {H : Type u_7} [normed_add_comm_group H] [normed_space 𝕜 H] {φ : α H} (L : H →L[𝕜] E) (φ_int : measure_theory.integrable φ μ) :
measure_theory.integrable (λ (a : α), L (φ a)) μ