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.
In the second part, the space L¹ 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
α →₁ βis the type ofL¹space, whereαis ameasure_spaceandβis anormed_groupwith asecond_countable_topology.f : α →ₘ βis a "function" inL¹. In comments,[f]is also used to denote anL¹function.₁can be typed as\1.
Main definitions
Let
f : α → βbe a function, whereαis ameasure_spaceandβanormed_group. Thenhas_finite_integral fmeans(∫⁻ a, nnnorm (f a)) < ⊤.If
βis moreover ameasurable_spacethenfis calledintegrableiffismeasurableandhas_finite_integral fholds.The space
L¹is defined as a subspace ofL⁰: Anae_eq_fun[f] : α →ₘ βis in the spaceL¹ifedist [f] 0 < ⊤, which means(∫⁻ a, edist (f a) 0) < ⊤if we expand the definition ofedistinL⁰.
Main statements
L¹, 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 : α → β) :
theorem
measure_theory.lintegral_norm_eq_lintegral_edist
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
(f : α → β) :
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 : α → β}
(hf : measurable f)
(hg : measurable g)
(hh : measurable h) :
theorem
measure_theory.lintegral_nnnorm_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β] :
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 : α → γ}
(hf : measurable f)
(hg : measurable g) :
theorem
measure_theory.lintegral_nnnorm_neg
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
{f : α → β} :
The predicate has_finite_integral
def
measure_theory.has_finite_integral
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[normed_group β]
(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.
theorem
measure_theory.has_finite_integral_iff_norm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
(f : α → β) :
measure_theory.has_finite_integral f μ ↔ ∫⁻ (a : α), ennreal.of_real ∥f a∥ ∂μ < ⊤
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_iff_of_real
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α → ℝ}
(h : 0 ≤ᵐ[μ] f) :
measure_theory.has_finite_integral f μ ↔ ∫⁻ (a : α), ennreal.of_real (f a) ∂μ < ⊤
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 : α → γ}
(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}
[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}
[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}
[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}
[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}
[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}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
{c : β} :
theorem
measure_theory.has_finite_integral_const
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measure_theory.finite_measure μ]
(c : β) :
measure_theory.has_finite_integral (λ (x : α), 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 : ℝ}
(hC : ∀ᵐ (a : α) ∂μ, ∥f a∥ ≤ C) :
theorem
measure_theory.has_finite_integral.mono_measure
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ ν : measure_theory.measure α}
[normed_group β]
{f : α → β}
(h : measure_theory.has_finite_integral f ν)
(hμ : μ ≤ ν) :
theorem
measure_theory.has_finite_integral.add_measure
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ ν : measure_theory.measure α}
[normed_group β]
{f : α → β}
(hμ : measure_theory.has_finite_integral f μ)
(hν : measure_theory.has_finite_integral f ν) :
measure_theory.has_finite_integral f (μ + ν)
theorem
measure_theory.has_finite_integral.left_of_add_measure
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ ν : measure_theory.measure α}
[normed_group β]
{f : α → β}
(h : measure_theory.has_finite_integral f (μ + ν)) :
theorem
measure_theory.has_finite_integral.right_of_add_measure
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ ν : measure_theory.measure α}
[normed_group β]
{f : α → β}
(h : measure_theory.has_finite_integral f (μ + ν)) :
@[simp]
theorem
measure_theory.has_finite_integral_add_measure
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ ν : measure_theory.measure α}
[normed_group β]
{f : α → β} :
theorem
measure_theory.has_finite_integral.smul_measure
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
{f : α → β}
(h : measure_theory.has_finite_integral f μ)
{c : ennreal}
(hc : c < ⊤) :
measure_theory.has_finite_integral f (c • μ)
@[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 β] :
measure_theory.has_finite_integral (λ (a : α), 0) μ
theorem
measure_theory.has_finite_integral.neg
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
{f : α → β}
(hfi : measure_theory.has_finite_integral f μ) :
@[simp]
theorem
measure_theory.has_finite_integral_neg_iff
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
{f : α → β} :
theorem
measure_theory.has_finite_integral.norm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
{f : α → β}
(hfi : measure_theory.has_finite_integral f μ) :
measure_theory.has_finite_integral (λ (a : α), ∥f a∥) μ
theorem
measure_theory.has_finite_integral_norm_iff
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
(f : α → β) :
measure_theory.has_finite_integral (λ (a : α), ∥f a∥) μ ↔ measure_theory.has_finite_integral 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 : α → β}
(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}
[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}
[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}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[borel_space β]
[topological_space.second_countable_topology β]
{F : ℕ → α → β}
{f : α → β}
{bound : α → ℝ}
(F_measurable : ∀ (n : ℕ), measurable (F n))
(f_measurable : 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 L¹ function
theorem
measure_theory.has_finite_integral.max_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α → ℝ}
(hf : measure_theory.has_finite_integral f μ) :
measure_theory.has_finite_integral (λ (a : α), max (f a) 0) μ
theorem
measure_theory.has_finite_integral.min_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : α → ℝ}
(hf : measure_theory.has_finite_integral f μ) :
measure_theory.has_finite_integral (λ (a : α), min (f a) 0) μ
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 : α → β}
(a : measure_theory.has_finite_integral f μ) :
measure_theory.has_finite_integral (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 : α → β) :
theorem
measure_theory.has_finite_integral.const_mul
{α : Type u_1}
[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}
[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_1}
{β : Type u_2}
[measurable_space α]
[normed_group β]
[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.measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
{f : α → β}
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.integrable.has_finite_integral
{α : Type u_1}
{β : Type u_2}
[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}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[normed_group γ]
[measurable_space β]
[measurable_space γ]
{f : α → β}
{g : α → γ}
(hg : measure_theory.integrable g μ)
(hf : measurable f)
(h : ∀ᵐ (a : α) ∂μ, ∥f a∥ ≤ ∥g a∥) :
theorem
measure_theory.integrable.mono'
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
{f : α → β}
{g : α → ℝ}
(hg : measure_theory.integrable g μ)
(hf : measurable f)
(h : ∀ᵐ (a : α) ∂μ, ∥f a∥ ≤ g a) :
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 : α → γ}
(hf : measure_theory.integrable f μ)
(hg : measurable g)
(h : ∀ᵐ (a : α) ∂μ, ∥f a∥ = ∥g a∥) :
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 : α → γ}
(hf : measurable f)
(hg : measurable g)
(h : ∀ᵐ (a : α) ∂μ, ∥f a∥ = ∥g a∥) :
theorem
measure_theory.integrable.congr
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
{f g : α → β}
(hf : measure_theory.integrable f μ)
(hg : measurable g)
(h : f =ᵐ[μ] g) :
theorem
measure_theory.integrable_congr
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
{f g : α → β}
(hf : measurable f)
(hg : measurable g)
(h : f =ᵐ[μ] g) :
theorem
measure_theory.integrable_const_iff
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
{c : β} :
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 : α → β}
(h : measure_theory.integrable f ν)
(hμ : μ ≤ ν) :
theorem
measure_theory.integrable.add_measure
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ ν : measure_theory.measure α}
[normed_group β]
[measurable_space β]
{f : α → β}
(hμ : measure_theory.integrable f μ)
(hν : measure_theory.integrable f ν) :
measure_theory.integrable 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 : α → β}
(h : measure_theory.integrable 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 : α → β}
(h : measure_theory.integrable f (μ + ν)) :
@[simp]
theorem
measure_theory.integrable_add_measure
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ ν : measure_theory.measure α}
[normed_group β]
[measurable_space β]
{f : α → β} :
measure_theory.integrable f (μ + ν) ↔ measure_theory.integrable f μ ∧ measure_theory.integrable f ν
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}
(hc : c < ⊤) :
measure_theory.integrable f (c • μ)
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 : δ → β}
(hf : measurable f)
(hg : measurable g) :
measure_theory.integrable g (⇑(measure_theory.measure.map f) μ) ↔ measure_theory.integrable (g ∘ f) μ
theorem
measure_theory.lintegral_edist_lt_top
{α : 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 : α → β}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable 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.add'
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[opens_measurable_space β]
{f g : α → β}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.has_finite_integral (f + g) μ
theorem
measure_theory.integrable.add
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[borel_space β]
[topological_space.second_countable_topology β]
{f g : α → β}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.integrable (f + g) μ
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 : ι → α → β}
(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}
[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}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[borel_space β]
{f : α → β} :
theorem
measure_theory.integrable.sub'
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[opens_measurable_space β]
{f g : α → β}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.has_finite_integral (f - g) μ
theorem
measure_theory.integrable.sub
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[borel_space β]
[topological_space.second_countable_topology β]
{f g : α → β}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.integrable (f - g) μ
theorem
measure_theory.integrable.norm
{α : Type u_1}
{β : Type u_2}
[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}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[opens_measurable_space β]
{f : α → β}
(hf : measurable f) :
measure_theory.integrable (λ (a : α), ∥f a∥) μ ↔ measure_theory.integrable 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 : α → γ}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.integrable (λ (x : α), (f x, g x)) μ
Lemmas used for defining the positive part of a L¹ function
theorem
measure_theory.integrable.max_zero
{α : Type u_1}
[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}
[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}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
{𝕜 : Type u_5}
[normed_field 𝕜]
[normed_space 𝕜 β]
[borel_space β]
(c : 𝕜)
{f : α → β}
(hf : measure_theory.integrable f μ) :
measure_theory.integrable (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 : α → β) :
measure_theory.integrable (c • f) μ ↔ measure_theory.integrable 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) μ
The predicate integrable on measurable functions modulo a.e.-equality
def
measure_theory.ae_eq_fun.integrable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[opens_measurable_space β]
(f : α →ₘ[μ] β) :
Prop
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
- f.integrable = (f ∈ emetric.ball 0 ⊤)
theorem
measure_theory.ae_eq_fun.integrable_mk
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[opens_measurable_space β]
{f : α → β}
(hf : measurable f) :
theorem
measure_theory.ae_eq_fun.integrable_coe_fn
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[opens_measurable_space β]
{f : α →ₘ[μ] β} :
theorem
measure_theory.ae_eq_fun.integrable_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[opens_measurable_space β] :
theorem
measure_theory.ae_eq_fun.integrable.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 : α →ₘ[μ] β}
(a : f.integrable)
(a_1 : g.integrable) :
(f + g).integrable
theorem
measure_theory.ae_eq_fun.integrable.neg
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
{f : α →ₘ[μ] β}
(a : f.integrable) :
(-f).integrable
theorem
measure_theory.ae_eq_fun.integrable.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 : α →ₘ[μ] β}
(hf : f.integrable)
(hg : g.integrable) :
(f - g).integrable
theorem
measure_theory.ae_eq_fun.is_add_subgroup
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β] :
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 : α →ₘ[μ] β}
(a : f.integrable) :
(c • f).integrable
The L¹ space of functions
def
measure_theory.l1
(α : Type u_1)
(β : Type u_2)
[measurable_space α]
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[opens_measurable_space β]
(μ : measure_theory.measure α) :
Type (max u_1 u_2)
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
- (α →₁[μ] β) = {f // f.integrable}
@[instance]
def
measure_theory.l1.has_coe
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[opens_measurable_space β] :
Equations
@[instance]
def
measure_theory.l1.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[opens_measurable_space β] :
has_coe_to_fun (α →₁[μ] β)
@[simp]
theorem
measure_theory.l1.coe_coe
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[opens_measurable_space β]
(f : α →₁[μ] β) :
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 : α →₁[μ] β}
(a : ↑f = ↑g) :
f = g
theorem
measure_theory.l1.eq_iff
{α : 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 : α →₁[μ] β} :
@[instance]
def
measure_theory.l1.emetric_space
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[opens_measurable_space β] :
emetric_space (α →₁[μ] β)
L¹ 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).
@[instance]
def
measure_theory.l1.metric_space
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[opens_measurable_space β] :
metric_space (α →₁[μ] β)
L¹ 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
@[instance]
def
measure_theory.l1.add_comm_group
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β] :
add_comm_group (α →₁[μ] β)
@[instance]
def
measure_theory.l1.inhabited
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β] :
Equations
@[simp]
theorem
measure_theory.l1.coe_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β] :
@[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 : α →₁[μ] β) :
@[simp]
theorem
measure_theory.l1.coe_neg
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f : α →₁[μ] β) :
@[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 : α →₁[μ] β) :
@[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 : α →₁[μ] β) :
theorem
measure_theory.l1.dist_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]
def
measure_theory.l1.has_norm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β] :
The norm on L¹ space is defined to be ∥f∥ = ∫⁻ a, edist (f a) 0.
theorem
measure_theory.l1.norm_eq
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f : α →₁[μ] β) :
@[instance]
def
measure_theory.l1.normed_group
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β] :
normed_group (α →₁[μ] β)
Equations
- measure_theory.l1.normed_group = normed_group.of_add_dist measure_theory.l1.normed_group._proof_4 measure_theory.l1.normed_group._proof_5
@[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 𝕜 (α →₁[μ] β)
@[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 : α →₁[μ] β) :
@[instance]
def
measure_theory.l1.semimodule
{α : 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 𝕜 β] :
semimodule 𝕜 (α →₁[μ] β)
Equations
- measure_theory.l1.semimodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := measure_theory.l1.has_scalar _inst_10, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[instance]
def
measure_theory.l1.normed_space
{α : 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 𝕜 β] :
normed_space 𝕜 (α →₁[μ] β)
Equations
- measure_theory.l1.normed_space = {to_semimodule := measure_theory.l1.semimodule _inst_10, norm_smul_le := _}
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 : α → β)
(hf : measure_theory.integrable f μ) :
Construct the equivalence class [f] of a measurable and integrable function f.
Equations
- measure_theory.l1.of_fun f hf = ⟨measure_theory.ae_eq_fun.mk f _, _⟩
@[simp]
theorem
measure_theory.l1.of_fun_eq_mk
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f : α → β)
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.l1.of_fun_eq_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 g : α → β)
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.l1.of_fun f hf = measure_theory.l1.of_fun g hg ↔ f =ᵐ[μ] g
theorem
measure_theory.l1.of_fun_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β] :
measure_theory.l1.of_fun (λ (_x : α), 0) _ = 0
theorem
measure_theory.l1.of_fun_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 : α → β)
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.l1.of_fun (f + g) _ = measure_theory.l1.of_fun f hf + measure_theory.l1.of_fun g hg
theorem
measure_theory.l1.of_fun_neg
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f : α → β)
(hf : measure_theory.integrable f μ) :
measure_theory.l1.of_fun (-f) _ = -measure_theory.l1.of_fun f hf
theorem
measure_theory.l1.of_fun_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 : α → β)
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.l1.of_fun (f - g) _ = measure_theory.l1.of_fun f hf - measure_theory.l1.of_fun g hg
theorem
measure_theory.l1.norm_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 : α → β)
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.l1.norm_of_fun_eq_lintegral_norm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f : α → β)
(hf : measure_theory.integrable f μ) :
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 : 𝕜) :
measure_theory.l1.of_fun (λ (a : α), k • f a) _ = k • measure_theory.l1.of_fun f hf
theorem
measure_theory.l1.measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f : α →₁[μ] β) :
theorem
measure_theory.l1.measurable_norm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f : α →₁[μ] β) :
measurable (λ (a : α), ∥⇑f a∥)
theorem
measure_theory.l1.integrable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f : α →₁[μ] β) :
theorem
measure_theory.l1.has_finite_integral
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f : α →₁[μ] β) :
theorem
measure_theory.l1.integrable_norm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f : α →₁[μ] β) :
measure_theory.integrable (λ (a : α), ∥⇑f a∥) μ
theorem
measure_theory.l1.of_fun_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 : α →₁[μ] β) :
measure_theory.l1.of_fun ⇑f _ = f
theorem
measure_theory.l1.mk_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 : α →₁[μ] β) :
theorem
measure_theory.l1.to_fun_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 : α → β)
(hf : measure_theory.integrable f μ) :
⇑(measure_theory.l1.of_fun f hf) =ᵐ[μ] f
theorem
measure_theory.l1.zero_to_fun
(α : Type u_1)
(β : Type u_2)
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β] :
theorem
measure_theory.l1.add_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 : α →₁[μ] β) :
theorem
measure_theory.l1.neg_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 : α →₁[μ] β) :
theorem
measure_theory.l1.sub_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 : α →₁[μ] β) :
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 : α →₁[μ] β) :
theorem
measure_theory.l1.norm_eq_nnnorm_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 : α →₁[μ] β) :
theorem
measure_theory.l1.norm_eq_norm_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 : α →₁[μ] β) :
theorem
measure_theory.l1.lintegral_edist_to_fun_lt_top
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f g : α →₁[μ] β) :
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 : α →₁[μ] β) :
def
measure_theory.l1.pos_part
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α →₁[μ] ℝ) :
Positive part of a function in L¹ space.
def
measure_theory.l1.neg_part
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α →₁[μ] ℝ) :
Negative part of a function in L¹ space.
theorem
measure_theory.l1.coe_pos_part
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α →₁[μ] ℝ) :
theorem
measure_theory.l1.pos_part_to_fun
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α →₁[μ] ℝ) :
theorem
measure_theory.l1.neg_part_to_fun_eq_max
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α →₁[μ] ℝ) :
theorem
measure_theory.l1.neg_part_to_fun_eq_min
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α →₁[μ] ℝ) :
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 : α →₁[μ] β}
(h : ∀ᵐ (a : α) ∂μ, ∥⇑f a∥ ≤ ∥⇑g a∥) :
theorem
measure_theory.l1.continuous_pos_part
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
continuous (λ (f : α →₁[μ] ℝ), f.pos_part)
theorem
measure_theory.l1.continuous_neg_part
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
continuous (λ (f : α →₁[μ] ℝ), f.neg_part)
theorem
measurable.integrable_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[normed_group β]
[measurable_space β]
{f : α → β}
(hf : measurable f) :