mathlib documentation

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

In the second part, the space of equivalence classes of integrable functions under the relation of being almost everywhere equal is defined as a subspace of the space L⁰. See the file src/measure_theory/ae_eq_fun.lean for information on L⁰ space.

Notation

Main definitions

Main statements

, as a subspace, inherits most of the structures of L⁰.

Implementation notes

Maybe integrable f should be mean (∫⁻ a, edist (f a) 0) < ⊤, so that integrable and ae_eq_fun.integrable are more aligned. But in the end one can use the lemma lintegral_nnnorm_eq_lintegral_edist : (∫⁻ a, nnnorm (f a)) = (∫⁻ a, edist (f a) 0) to switch the two forms.

To prove something for an arbitrary integrable + measurable 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} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] (f : α → β) :
∫⁻ (a : α), (nnnorm (f a)) μ = ∫⁻ (a : α), edist (f a) 0 μ

theorem measure_theory.lintegral_norm_eq_lintegral_edist {α : Type u_1} {β : Type u_2} [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} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [topological_space.second_countable_topology β] [measurable_space β] [opens_measurable_space β] {f g h : α → β} :
measurable fmeasurable gmeasurable 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} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] :
∫⁻ (a : α), (nnnorm 0) μ = 0

theorem measure_theory.lintegral_nnnorm_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [normed_group γ] [measurable_space β] [opens_measurable_space β] [measurable_space γ] [opens_measurable_space γ] {f : α → β} {g : α → γ} :
measurable fmeasurable g∫⁻ (a : α), (nnnorm (f a)) + (nnnorm (g a)) μ = ∫⁻ (a : α), (nnnorm (f a)) μ + ∫⁻ (a : α), (nnnorm (g a)) μ

theorem measure_theory.lintegral_nnnorm_neg {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] {f : α → β} :
∫⁻ (a : α), (nnnorm ((-f) a)) μ = ∫⁻ (a : α), (nnnorm (f a)) μ

The predicate has_finite_integral

def measure_theory.has_finite_integral {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_group β] :
(α → β)(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_edist {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] (f : α → β) :

theorem measure_theory.has_finite_integral.mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} :

theorem measure_theory.has_finite_integral.mono' {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] {f : α → β} {g : α → } :
measure_theory.has_finite_integral g μ(∀ᵐ (a : α) ∂μ, f a g a)measure_theory.has_finite_integral f μ

theorem measure_theory.has_finite_integral.congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} :

theorem measure_theory.has_finite_integral_congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [normed_group γ] {f : α → β} {g : α → γ} :

theorem measure_theory.has_finite_integral.congr {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] {f g : α → β} :

theorem measure_theory.has_finite_integral_const_iff {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] {c : β} :

theorem measure_theory.has_finite_integral_of_bounded {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measure_theory.finite_measure μ] {f : α → β} {C : } :
(∀ᵐ (a : α) ∂μ, f a C)measure_theory.has_finite_integral f μ

@[simp]
theorem measure_theory.has_finite_integral_zero_measure {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_group β] (f : α → β) :

@[simp]
theorem measure_theory.has_finite_integral_zero (α : Type u_1) (β : Type u_2) [measurable_space α] (μ : measure_theory.measure α) [normed_group β] :

theorem measure_theory.has_finite_integral.norm {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] {f : α → β} :

theorem measure_theory.all_ae_of_real_F_le_bound {α : Type u_1} {β : Type u_2} [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} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] {F : α → β} {f : α → β} :
(∀ᵐ (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} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] {F : α → β} {f : α → β} {bound : α → } :
(∀ (n : ), ∀ᵐ (a : α) ∂μ, F n a bound a)(∀ᵐ (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} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] {F : α → β} {f : α → β} {bound : α → } :
measure_theory.has_finite_integral bound μ(∀ (n : ), ∀ᵐ (a : α) ∂μ, F n a bound a)(∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ), F n a) filter.at_top (𝓝 (f a)))measure_theory.has_finite_integral f μ

theorem measure_theory.tendsto_lintegral_norm_of_dominated_convergence {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [borel_space β] [topological_space.second_countable_topology β] {F : α → β} {f : α → β} {bound : α → } :
(∀ (n : ), measurable (F n))measurable fmeasure_theory.has_finite_integral bound μ(∀ (n : ), ∀ᵐ (a : α) ∂μ, F n a bound a)(∀ᵐ (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} [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} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 β] {c : 𝕜} (hc : c 0) (f : α → β) :

The predicate integrable

def measure_theory.integrable {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_group β] [measurable_space β] :
(α → β)(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.measurable {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] {f : α → β} :

theorem measure_theory.integrable.mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [normed_group γ] [measurable_space β] [measurable_space γ] {f : α → β} {g : α → γ} :
measure_theory.integrable g μmeasurable f(∀ᵐ (a : α) ∂μ, f a g a)measure_theory.integrable f μ

theorem measure_theory.integrable.mono' {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] {f : α → β} {g : α → } :
measure_theory.integrable g μmeasurable f(∀ᵐ (a : α) ∂μ, f a g a)measure_theory.integrable f μ

theorem measure_theory.integrable.congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [normed_group γ] [measurable_space β] [measurable_space γ] {f : α → β} {g : α → γ} :
measure_theory.integrable f μmeasurable g(∀ᵐ (a : α) ∂μ, f a = g a)measure_theory.integrable g μ

theorem measure_theory.integrable_congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [normed_group γ] [measurable_space β] [measurable_space γ] {f : α → β} {g : α → γ} :
measurable fmeasurable g(∀ᵐ (a : α) ∂μ, f a = g a)(measure_theory.integrable f μ measure_theory.integrable g μ)

theorem measure_theory.integrable.congr {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] {f g : α → β} :

theorem measure_theory.integrable_congr {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] {f g : α → β} :

theorem measure_theory.integrable_const_iff {α : Type u_1} {β : Type u_2} [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} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [measure_theory.finite_measure μ] (c : β) :
measure_theory.integrable (λ (x : α), c) μ

theorem measure_theory.integrable.mono_measure {α : Type u_1} {β : Type u_2} [measurable_space α] {μ ν : measure_theory.measure α} [normed_group β] [measurable_space β] {f : α → β} :

theorem measure_theory.integrable.add_measure {α : Type u_1} {β : Type u_2} [measurable_space α] {μ ν : measure_theory.measure α} [normed_group β] [measurable_space β] {f : α → β} :

theorem measure_theory.integrable.left_of_add_measure {α : Type u_1} {β : Type u_2} [measurable_space α] {μ ν : measure_theory.measure α} [normed_group β] [measurable_space β] {f : α → β} :

theorem measure_theory.integrable.right_of_add_measure {α : Type u_1} {β : Type u_2} [measurable_space α] {μ ν : measure_theory.measure α} [normed_group β] [measurable_space β] {f : α → β} :

@[simp]

theorem measure_theory.integrable.smul_measure {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] {f : α → β} (h : measure_theory.integrable f μ) {c : ennreal} :

theorem measure_theory.integrable_map_measure {α : Type u_1} {β : Type u_2} {δ : Type u_4} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [measurable_space δ] [opens_measurable_space β] {f : α → δ} {g : δ → β} :

@[simp]
theorem measure_theory.integrable_zero (α : Type u_1) (β : Type u_2) [measurable_space α] (μ : measure_theory.measure α) [normed_group β] [measurable_space β] :
measure_theory.integrable (λ (_x : α), 0) μ

theorem measure_theory.integrable_finset_sum {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] {ι : Type u_3} [borel_space β] [topological_space.second_countable_topology β] (s : finset ι) {f : ι → α → β} :
(∀ (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} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [borel_space β] {f : α → β} :

@[simp]
theorem measure_theory.integrable_neg_iff {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [borel_space β] {f : α → β} :

theorem measure_theory.integrable.norm {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [opens_measurable_space β] {f : α → β} :

theorem measure_theory.integrable_norm_iff {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [opens_measurable_space β] {f : α → β} :

theorem measure_theory.integrable.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [normed_group γ] [measurable_space β] [measurable_space γ] [opens_measurable_space β] [opens_measurable_space γ] {f : α → β} {g : α → γ} :

Lemmas used for defining the positive part of a function

theorem measure_theory.integrable.max_zero {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {f : α → } :
measure_theory.integrable f μmeasure_theory.integrable (λ (a : α), max (f a) 0) μ

theorem measure_theory.integrable.min_zero {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {f : α → } :
measure_theory.integrable f μmeasure_theory.integrable (λ (a : α), min (f a) 0) μ

theorem measure_theory.integrable.smul {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 β] [borel_space β] (c : 𝕜) {f : α → β} :

theorem measure_theory.integrable_smul_iff {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 β] [borel_space β] {c : 𝕜} (hc : c 0) (f : α → β) :

theorem measure_theory.integrable.const_mul {α : Type u_1} [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} [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} [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} :
c 0(measure_theory.integrable (λ (x : α), f x c) μ measure_theory.integrable f μ)

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

A class of almost everywhere equal functions is integrable if it has a finite distance to the origin. It means the same thing as the predicate integrable over functions.

Equations
theorem measure_theory.ae_eq_fun.integrable.smul {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [borel_space β] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 β] {c : 𝕜} {f : α →ₘ[μ] β} :

The space of functions

The space of equivalence classes of integrable (and measurable) functions, where two integrable functions are equivalent if they agree almost everywhere, i.e., they differ on a set of measure 0.

Equations
@[instance]

Equations
theorem measure_theory.l1.eq {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [opens_measurable_space β] {f g : α →₁[μ] β} :
f = gf = g

@[instance]

space forms a emetric_space, with the emetric being inherited from almost everywhere functions, i.e., edist f g = ∫⁻ a, edist (f a) (g a).

Equations
@[instance]

space forms a metric_space, with the metric being inherited from almost everywhere functions, i.e., edist f g = ennreal.to_real (∫⁻ a, edist (f a) (g a)).

Equations
@[simp]
theorem measure_theory.l1.coe_add {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [borel_space β] (f g : α →₁[μ] β) :
(f + g) = f + g

@[simp]

@[simp]
theorem measure_theory.l1.coe_sub {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [borel_space β] (f g : α →₁[μ] β) :
(f - g) = f - g

@[simp]
theorem measure_theory.l1.edist_eq {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [borel_space β] (f g : α →₁[μ] β) :

@[instance]

The norm on space is defined to be ∥f∥ = ∫⁻ a, edist (f a) 0.

Equations
@[instance]

Equations
@[instance]
def measure_theory.l1.has_scalar {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [borel_space β] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 β] :
has_scalar 𝕜 →₁[μ] β)

Equations
@[simp]
theorem measure_theory.l1.coe_smul {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [borel_space β] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 β] (c : 𝕜) (f : α →₁[μ] β) :
(c f) = c f

def measure_theory.l1.of_fun {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [borel_space β] (f : α → β) :

Construct the equivalence class [f] of a measurable and integrable function f.

Equations
theorem measure_theory.l1.of_fun_smul {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [borel_space β] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 β] (f : α → β) (hf : measure_theory.integrable f μ) (k : 𝕜) :

theorem measure_theory.l1.dist_to_fun {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [borel_space β] (f g : α →₁[μ] β) :
dist f g = (∫⁻ (x : α), edist (f x) (g x) μ).to_real

theorem measure_theory.l1.smul_to_fun {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [borel_space β] {𝕜 : Type u_5} [normed_field 𝕜] [normed_space 𝕜 β] (c : 𝕜) (f : α →₁[μ] β) :
(c f) =ᵐ[μ] c f

theorem measure_theory.l1.norm_sub_eq_lintegral {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [borel_space β] (f g : α →₁[μ] β) :
f - g = (∫⁻ (x : α), (nnnorm (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_eq_lintegral 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).

def measure_theory.l1.pos_part {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} :
→₁[μ] )→₁[μ] )

Positive part of a function in space.

Equations
def measure_theory.l1.neg_part {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} :
→₁[μ] )→₁[μ] )

Negative part of a function in space.

Equations
theorem measure_theory.l1.pos_part_to_fun {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} (f : α →₁[μ] ) :
(f.pos_part) =ᵐ[μ] λ (a : α), max (f a) 0

theorem measure_theory.l1.neg_part_to_fun_eq_max {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} (f : α →₁[μ] ) :
∀ᵐ (a : α) ∂μ, (f.neg_part) a = max (-f a) 0

theorem measure_theory.l1.neg_part_to_fun_eq_min {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} (f : α →₁[μ] ) :
∀ᵐ (a : α) ∂μ, (f.neg_part) a = -min (f a) 0

theorem measure_theory.l1.norm_le_norm_of_ae_le {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [normed_group β] [measurable_space β] [topological_space.second_countable_topology β] [borel_space β] {f g : α →₁[μ] β} :
(∀ᵐ (a : α) ∂μ, f a g a)f g

theorem measurable.integrable_zero {α : Type u_1} {β : Type u_2} [measurable_space α] [normed_group β] [measurable_space β] {f : α → β} :