Integrable functions and L¹ space #
In the first part of this file, the predicate integrable is defined and basic properties of
integrable functions are proved.
Such a predicate is already available under the name mem_ℒp 1. We give a direct definition which
is easier to use, and show that it is equivalent to mem_ℒp 1
In the second part, we establish an API between integrable and the space L¹ of equivalence
classes of integrable functions, already defined as a special case of L^p spaces for p = 1.
Notation #
-
α →₁[μ] βis the type 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.
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}
[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 : ae_measurable f μ)
(hg : ae_measurable g μ)
(hh : ae_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 : ae_measurable f μ)
(hg : ae_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 : ℝ≥0∞}
(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 : ℕ), 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 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 : α → β} :
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.ae_measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
{f : α → β}
(hf : measure_theory.integrable f μ) :
ae_measurable 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 : ae_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 : ae_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 : ae_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 : ae_measurable f μ)
(hg : ae_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 μ)
(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 : α → β}
(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 : ℝ≥0∞}
(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 : δ → β}
(hg : ae_measurable g (⇑(measure_theory.measure.map f) μ))
(hf : measurable f) :
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 : ae_measurable f μ) :
measure_theory.integrable (λ (a : α), ∥f a∥) μ ↔ measure_theory.integrable f μ
theorem
measure_theory.integrable_of_norm_sub_le
{α : Type u_1}
{β : Type u_2}
[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}
[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}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
{f : α → β} :
measure_theory.mem_ℒp f 1 μ ↔ measure_theory.integrable f μ
theorem
measure_theory.mem_ℒp.integrable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[borel_space β]
{q : ℝ≥0∞}
(hq1 : 1 ≤ q)
{f : α → β}
[measure_theory.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}
[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) :
measure_theory.integrable (g ∘ f) μ ↔ measure_theory.integrable f μ
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 𝕜 β]
[measurable_space 𝕜]
[opens_measurable_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 𝕜 β]
[measurable_space 𝕜]
[opens_measurable_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) μ
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}
(hc : c ≠ 0) :
measure_theory.integrable (λ (x : α), f x • c) μ ↔ measure_theory.integrable f μ
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 β]
(f : α →ₘ[μ] β) :
Prop
A class of almost everywhere equal functions is integrable if its function representative
is integrable.
Equations
theorem
measure_theory.ae_eq_fun.integrable_mk
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
{f : α → β}
(hf : ae_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 β]
{f : α →ₘ[μ] β} :
theorem
measure_theory.ae_eq_fun.integrable_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β] :
theorem
measure_theory.ae_eq_fun.integrable.neg
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[borel_space β]
{f : α →ₘ[μ] β} :
f.integrable → (-f).integrable
theorem
measure_theory.ae_eq_fun.integrable_iff_mem_L1
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[borel_space β]
[topological_space.second_countable_topology β]
{f : α →ₘ[μ] β} :
f.integrable ↔ f ∈ measure_theory.Lp β 1 μ
theorem
measure_theory.ae_eq_fun.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 : α →ₘ[μ] β} :
f.integrable → g.integrable → (f + g).integrable
theorem
measure_theory.ae_eq_fun.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 : f.integrable)
(hg : g.integrable) :
(f - g).integrable
theorem
measure_theory.ae_eq_fun.integrable.smul
{α : Type u_1}
{β : Type u_2}
[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 : α →ₘ[μ] β} :
f.integrable → (c • f).integrable
theorem
measure_theory.L1.integrable_coe_fn
{α : 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.Lp β 1 μ)) :
theorem
measure_theory.L1.has_finite_integral_coe_fn
{α : 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.Lp β 1 μ)) :
theorem
measure_theory.L1.measurable_coe_fn
{α : 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.Lp β 1 μ)) :
theorem
measure_theory.L1.ae_measurable_coe_fn
{α : 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.Lp β 1 μ)) :
ae_measurable ⇑f μ
theorem
measure_theory.L1.edist_def
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f g : ↥(measure_theory.Lp β 1 μ)) :
theorem
measure_theory.L1.dist_def
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f g : ↥(measure_theory.Lp β 1 μ)) :
theorem
measure_theory.L1.norm_def
{α : 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.Lp β 1 μ)) :
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 : ↥(measure_theory.Lp β 1 μ)) :
Computing the norm of a difference between two L¹-functions. Note that this is not a
special case of norm_def since (f - g) x and f x - g x are not equal
(but only a.e.-equal).
theorem
measure_theory.L1.of_real_norm_eq_lintegral
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f : ↥(measure_theory.Lp β 1 μ)) :
theorem
measure_theory.L1.of_real_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 : ↥(measure_theory.Lp β 1 μ)) :
Computing the norm of a difference between two L¹-functions. Note that this is not a
special case of of_real_norm_eq_lintegral since (f - g) x and f x - g x are not equal
(but only a.e.-equal).
def
measure_theory.integrable.to_L1
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f : α → β)
(hf : measure_theory.integrable f μ) :
↥(measure_theory.Lp β 1 μ)
Construct the equivalence class [f] of an integrable function f, as a member of the
space L1 β 1 μ.
Equations
@[simp]
theorem
measure_theory.integrable.to_L1_coe_fn
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(f : ↥(measure_theory.Lp β 1 μ))
(hf : measure_theory.integrable ⇑f μ) :
theorem
measure_theory.integrable.coe_fn_to_L1
{α : 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.integrable.to_L1 f hf) =ᵐ[μ] f
@[simp]
theorem
measure_theory.integrable.to_L1_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group β]
[measurable_space β]
[topological_space.second_countable_topology β]
[borel_space β]
(h : measure_theory.integrable 0 μ) :
@[simp]
theorem
measure_theory.integrable.to_L1_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 μ) :
@[simp]
theorem
measure_theory.integrable.to_L1_eq_to_L1_iff
{α : 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.integrable.to_L1 f hf = measure_theory.integrable.to_L1 g hg ↔ f =ᵐ[μ] g
theorem
measure_theory.integrable.to_L1_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 μ) :
theorem
measure_theory.integrable.to_L1_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 μ) :
theorem
measure_theory.integrable.to_L1_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 μ) :
theorem
measure_theory.integrable.norm_to_L1
{α : 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.integrable.norm_to_L1_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 μ) :
@[simp]
theorem
measure_theory.integrable.edist_to_L1_to_L1
{α : 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 μ) :
edist (measure_theory.integrable.to_L1 f hf) (measure_theory.integrable.to_L1 g hg) = ∫⁻ (a : α), edist (f a) (g a) ∂μ
@[simp]
theorem
measure_theory.integrable.edist_to_L1_zero
{α : 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.integrable.to_L1_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 𝕜 β]
[measurable_space 𝕜]
[opens_measurable_space 𝕜]
(f : α → β)
(hf : measure_theory.integrable f μ)
(k : 𝕜) :
measure_theory.integrable.to_L1 (λ (a : α), k • f a) _ = k • measure_theory.integrable.to_L1 f hf
theorem
integrable_zero_measure
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[normed_group β]
[measurable_space β]
{f : α → β} :
theorem
measure_theory.integrable.apply_continuous_linear_map
{α : Type u_1}
[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) μ