Integrable functions and L¹ space #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In the first part of this file, the predicate integrable is defined and basic properties of
integrable functions are proved.
Such a predicate is already available under the name mem_ℒp 1. We give a direct definition which
is easier to use, and show that it is equivalent to mem_ℒp 1
In the second part, we establish an API between integrable and the space 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_add_comm_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_add_comm_group. Thenhas_finite_integral fmeans(∫⁻ a, ‖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}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : α → β) :
theorem
measure_theory.lintegral_norm_eq_lintegral_edist
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : α → β) :
theorem
measure_theory.lintegral_edist_triangle
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f g h : α → β}
(hf : measure_theory.ae_strongly_measurable f μ)
(hh : measure_theory.ae_strongly_measurable h μ) :
∫⁻ (a : α), has_edist.edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), has_edist.edist (f a) (h a) ∂μ + ∫⁻ (a : α), has_edist.edist (g a) (h a) ∂μ
theorem
measure_theory.lintegral_nnnorm_zero
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β] :
theorem
measure_theory.lintegral_nnnorm_add_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[normed_add_comm_group γ]
{f : α → β}
(hf : measure_theory.ae_strongly_measurable f μ)
(g : α → γ) :
theorem
measure_theory.lintegral_nnnorm_add_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[normed_add_comm_group γ]
(f : α → β)
{g : α → γ}
(hg : measure_theory.ae_strongly_measurable g μ) :
The predicate has_finite_integral #
def
measure_theory.has_finite_integral
{α : Type u_1}
{β : Type u_2}
[normed_add_comm_group β]
{m : measurable_space α}
(f : α → β)
(μ : measure_theory.measure α . "volume_tac") :
Prop
has_finite_integral f μ means that the integral ∫⁻ a, ‖f a‖ ∂μ is finite.
has_finite_integral f means has_finite_integral f volume.
theorem
measure_theory.has_finite_integral_iff_norm
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_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}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : α → β) :
measure_theory.has_finite_integral f μ ↔ ∫⁻ (a : α), has_edist.edist (f a) 0 ∂μ < ⊤
theorem
measure_theory.has_finite_integral_iff_of_real
{α : Type u_1}
{m : 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_iff_of_nnreal
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → nnreal} :
theorem
measure_theory.has_finite_integral.mono
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[normed_add_comm_group γ]
{f : α → β}
{g : α → γ}
(hg : measure_theory.has_finite_integral g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖) :
theorem
measure_theory.has_finite_integral.mono'
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
{g : α → ℝ}
(hg : measure_theory.has_finite_integral g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a) :
theorem
measure_theory.has_finite_integral.congr'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[normed_add_comm_group γ]
{f : α → β}
{g : α → γ}
(hf : measure_theory.has_finite_integral f μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) :
theorem
measure_theory.has_finite_integral_congr'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[normed_add_comm_group γ]
{f : α → β}
{g : α → γ}
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) :
theorem
measure_theory.has_finite_integral.congr
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f g : α → β}
(hf : measure_theory.has_finite_integral f μ)
(h : f =ᵐ[μ] g) :
theorem
measure_theory.has_finite_integral_congr
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f g : α → β}
(h : f =ᵐ[μ] g) :
theorem
measure_theory.has_finite_integral_const_iff
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{c : β} :
theorem
measure_theory.has_finite_integral_const
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[measure_theory.is_finite_measure μ]
(c : β) :
measure_theory.has_finite_integral (λ (x : α), c) μ
theorem
measure_theory.has_finite_integral_of_bounded
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[measure_theory.is_finite_measure μ]
{f : α → β}
{C : ℝ}
(hC : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ C) :
theorem
measure_theory.has_finite_integral.mono_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(h : measure_theory.has_finite_integral f ν)
(hμ : μ ≤ ν) :
theorem
measure_theory.has_finite_integral.add_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[normed_add_comm_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}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[normed_add_comm_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}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(h : measure_theory.has_finite_integral f (μ + ν)) :
@[simp]
theorem
measure_theory.has_finite_integral_add_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β} :
theorem
measure_theory.has_finite_integral.smul_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_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}
[normed_add_comm_group β]
{m : measurable_space α}
(f : α → β) :
@[simp]
theorem
measure_theory.has_finite_integral_zero
(α : Type u_1)
(β : Type u_2)
{m : measurable_space α}
(μ : measure_theory.measure α)
[normed_add_comm_group β] :
measure_theory.has_finite_integral (λ (a : α), 0) μ
theorem
measure_theory.has_finite_integral.neg
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(hfi : measure_theory.has_finite_integral f μ) :
@[simp]
theorem
measure_theory.has_finite_integral_neg_iff
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β} :
theorem
measure_theory.has_finite_integral.norm
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_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}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : α → β) :
measure_theory.has_finite_integral (λ (a : α), ‖f a‖) μ ↔ measure_theory.has_finite_integral f μ
theorem
measure_theory.has_finite_integral_to_real_of_lintegral_ne_top
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ennreal}
(hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤) :
measure_theory.has_finite_integral (λ (x : α), (f x).to_real) μ
theorem
measure_theory.is_finite_measure_with_density_of_real
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ}
(hfi : measure_theory.has_finite_integral f μ) :
measure_theory.is_finite_measure (μ.with_density (λ (x : α), ennreal.of_real (f x)))
theorem
measure_theory.all_ae_of_real_F_le_bound
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{F : ℕ → α → β}
{bound : α → ℝ}
(h : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a)
(n : ℕ) :
∀ᵐ (a : α) ∂μ, ennreal.of_real ‖F n a‖ ≤ ennreal.of_real (bound a)
theorem
measure_theory.all_ae_tendsto_of_real_norm
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{F : ℕ → α → β}
{f : α → β}
(h : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ℕ), F n a) filter.at_top (nhds (f a))) :
∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ℕ), ennreal.of_real ‖F n a‖) filter.at_top (nhds (ennreal.of_real ‖f a‖))
theorem
measure_theory.all_ae_of_real_f_le_bound
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{F : ℕ → α → β}
{f : α → β}
{bound : α → ℝ}
(h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a)
(h_lim : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ℕ), F n a) filter.at_top (nhds (f a))) :
∀ᵐ (a : α) ∂μ, ennreal.of_real ‖f a‖ ≤ ennreal.of_real (bound a)
theorem
measure_theory.has_finite_integral_of_dominated_convergence
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{F : ℕ → α → β}
{f : α → β}
{bound : α → ℝ}
(bound_has_finite_integral : measure_theory.has_finite_integral bound μ)
(h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a)
(h_lim : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ℕ), F n a) filter.at_top (nhds (f a))) :
theorem
measure_theory.tendsto_lintegral_norm_of_dominated_convergence
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{F : ℕ → α → β}
{f : α → β}
{bound : α → ℝ}
(F_measurable : ∀ (n : ℕ), measure_theory.ae_strongly_measurable (F n) μ)
(bound_has_finite_integral : measure_theory.has_finite_integral bound μ)
(h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a)
(h_lim : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (n : ℕ), F n a) filter.at_top (nhds (f a))) :
filter.tendsto (λ (n : ℕ), ∫⁻ (a : α), ennreal.of_real ‖F n a - f a‖ ∂μ) filter.at_top (nhds 0)
Lemmas used for defining the positive part of a L¹ function
theorem
measure_theory.has_finite_integral.max_zero
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ}
(hf : measure_theory.has_finite_integral f μ) :
measure_theory.has_finite_integral (λ (a : α), linear_order.max (f a) 0) μ
theorem
measure_theory.has_finite_integral.min_zero
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ}
(hf : measure_theory.has_finite_integral f μ) :
measure_theory.has_finite_integral (λ (a : α), linear_order.min (f a) 0) μ
theorem
measure_theory.has_finite_integral.smul
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{𝕜 : Type u_5}
[normed_add_comm_group 𝕜]
[smul_zero_class 𝕜 β]
[has_bounded_smul 𝕜 β]
(c : 𝕜)
{f : α → β} :
theorem
measure_theory.has_finite_integral_smul_iff
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{𝕜 : Type u_5}
[normed_ring 𝕜]
[mul_action_with_zero 𝕜 β]
[has_bounded_smul 𝕜 β]
{c : 𝕜}
(hc : is_unit c)
(f : α → β) :
theorem
measure_theory.has_finite_integral.const_mul
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[normed_ring 𝕜]
{f : α → 𝕜}
(h : measure_theory.has_finite_integral f μ)
(c : 𝕜) :
measure_theory.has_finite_integral (λ (x : α), c * f x) μ
theorem
measure_theory.has_finite_integral.mul_const
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[normed_ring 𝕜]
{f : α → 𝕜}
(h : measure_theory.has_finite_integral f μ)
(c : 𝕜) :
measure_theory.has_finite_integral (λ (x : α), f x * c) μ
The predicate integrable #
def
measure_theory.integrable
{β : Type u_2}
[normed_add_comm_group β]
{α : Type u_1}
{m : measurable_space α}
(f : α → β)
(μ : measure_theory.measure α . "volume_tac") :
Prop
integrable f μ means that f is measurable and that the integral ∫⁻ a, ‖f a‖ ∂μ is finite.
integrable f means integrable f volume.
Equations
theorem
measure_theory.mem_ℒp_one_iff_integrable
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β} :
measure_theory.mem_ℒp f 1 μ ↔ measure_theory.integrable f μ
theorem
measure_theory.integrable.ae_strongly_measurable
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.integrable.ae_measurable
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[measurable_space β]
[borel_space β]
{f : α → β}
(hf : measure_theory.integrable f μ) :
ae_measurable f μ
theorem
measure_theory.integrable.has_finite_integral
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.integrable.mono
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[normed_add_comm_group γ]
{f : α → β}
{g : α → γ}
(hg : measure_theory.integrable g μ)
(hf : measure_theory.ae_strongly_measurable f μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖) :
theorem
measure_theory.integrable.mono'
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
{g : α → ℝ}
(hg : measure_theory.integrable g μ)
(hf : measure_theory.ae_strongly_measurable f μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a) :
theorem
measure_theory.integrable.congr'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[normed_add_comm_group γ]
{f : α → β}
{g : α → γ}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.ae_strongly_measurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) :
theorem
measure_theory.integrable_congr'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[normed_add_comm_group γ]
{f : α → β}
{g : α → γ}
(hf : measure_theory.ae_strongly_measurable f μ)
(hg : measure_theory.ae_strongly_measurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) :
theorem
measure_theory.integrable.congr
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f g : α → β}
(hf : measure_theory.integrable f μ)
(h : f =ᵐ[μ] g) :
theorem
measure_theory.integrable_congr
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f g : α → β}
(h : f =ᵐ[μ] g) :
theorem
measure_theory.integrable_const_iff
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{c : β} :
@[simp]
theorem
measure_theory.integrable_const
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[measure_theory.is_finite_measure μ]
(c : β) :
measure_theory.integrable (λ (x : α), c) μ
theorem
measure_theory.mem_ℒp.integrable_norm_rpow
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
{p : ennreal}
(hf : measure_theory.mem_ℒp f p μ)
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤) :
measure_theory.integrable (λ (x : α), ‖f x‖ ^ p.to_real) μ
theorem
measure_theory.mem_ℒp.integrable_norm_rpow'
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[measure_theory.is_finite_measure μ]
{f : α → β}
{p : ennreal}
(hf : measure_theory.mem_ℒp f p μ) :
measure_theory.integrable (λ (x : α), ‖f x‖ ^ p.to_real) μ
theorem
measure_theory.integrable.mono_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(h : measure_theory.integrable f ν)
(hμ : μ ≤ ν) :
theorem
measure_theory.integrable.of_measure_le_smul
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{μ' : measure_theory.measure α}
(c : ennreal)
(hc : c ≠ ⊤)
(hμ'_le : μ' ≤ c • μ)
{f : α → β}
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.integrable.add_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[normed_add_comm_group β]
{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}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(h : measure_theory.integrable f (μ + ν)) :
theorem
measure_theory.integrable.right_of_add_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(h : measure_theory.integrable f (μ + ν)) :
@[simp]
theorem
measure_theory.integrable_add_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β} :
measure_theory.integrable f (μ + ν) ↔ measure_theory.integrable f μ ∧ measure_theory.integrable f ν
@[simp]
theorem
measure_theory.integrable_zero_measure
{α : Type u_1}
{β : Type u_2}
[normed_add_comm_group β]
{m : measurable_space α}
{f : α → β} :
theorem
measure_theory.integrable_finset_sum_measure
{α : Type u_1}
{β : Type u_2}
[normed_add_comm_group β]
{ι : Type u_3}
{m : measurable_space α}
{f : α → β}
{μ : ι → measure_theory.measure α}
{s : finset ι} :
measure_theory.integrable f (s.sum (λ (i : ι), μ i)) ↔ ∀ (i : ι), i ∈ s → measure_theory.integrable f (μ i)
theorem
measure_theory.integrable.smul_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(h : measure_theory.integrable f μ)
{c : ennreal}
(hc : c ≠ ⊤) :
measure_theory.integrable f (c • μ)
theorem
measure_theory.integrable_smul_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
{c : ennreal}
(h₁ : c ≠ 0)
(h₂ : c ≠ ⊤) :
measure_theory.integrable f (c • μ) ↔ measure_theory.integrable f μ
theorem
measure_theory.integrable_inv_smul_measure
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
{c : ennreal}
(h₁ : c ≠ 0)
(h₂ : c ≠ ⊤) :
measure_theory.integrable f (c⁻¹ • μ) ↔ measure_theory.integrable f μ
theorem
measure_theory.integrable.to_average
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(h : measure_theory.integrable f μ) :
measure_theory.integrable f ((⇑μ set.univ)⁻¹ • μ)
theorem
measure_theory.integrable_average
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[measure_theory.is_finite_measure μ]
{f : α → β} :
measure_theory.integrable f ((⇑μ set.univ)⁻¹ • μ) ↔ measure_theory.integrable f μ
theorem
measure_theory.integrable_map_measure
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measurable_space δ]
[normed_add_comm_group β]
{f : α → δ}
{g : δ → β}
(hg : measure_theory.ae_strongly_measurable g (measure_theory.measure.map f μ))
(hf : ae_measurable f μ) :
measure_theory.integrable g (measure_theory.measure.map f μ) ↔ measure_theory.integrable (g ∘ f) μ
theorem
measure_theory.integrable.comp_ae_measurable
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measurable_space δ]
[normed_add_comm_group β]
{f : α → δ}
{g : δ → β}
(hg : measure_theory.integrable g (measure_theory.measure.map f μ))
(hf : ae_measurable f μ) :
measure_theory.integrable (g ∘ f) μ
theorem
measure_theory.integrable.comp_measurable
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measurable_space δ]
[normed_add_comm_group β]
{f : α → δ}
{g : δ → β}
(hg : measure_theory.integrable g (measure_theory.measure.map f μ))
(hf : measurable f) :
measure_theory.integrable (g ∘ f) μ
theorem
measurable_embedding.integrable_map_iff
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measurable_space δ]
[normed_add_comm_group β]
{f : α → δ}
(hf : measurable_embedding f)
{g : δ → β} :
measure_theory.integrable g (measure_theory.measure.map f μ) ↔ measure_theory.integrable (g ∘ f) μ
theorem
measure_theory.integrable_map_equiv
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measurable_space δ]
[normed_add_comm_group β]
(f : α ≃ᵐ δ)
(g : δ → β) :
measure_theory.integrable g (measure_theory.measure.map ⇑f μ) ↔ measure_theory.integrable (g ∘ ⇑f) μ
theorem
measure_theory.measure_preserving.integrable_comp
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measurable_space δ]
[normed_add_comm_group β]
{ν : measure_theory.measure δ}
{g : δ → β}
{f : α → δ}
(hf : measure_theory.measure_preserving f μ ν)
(hg : measure_theory.ae_strongly_measurable g ν) :
measure_theory.integrable (g ∘ f) μ ↔ measure_theory.integrable g ν
theorem
measure_theory.measure_preserving.integrable_comp_emb
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measurable_space δ]
[normed_add_comm_group β]
{f : α → δ}
{ν : measure_theory.measure δ . "volume_tac"}
(h₁ : measure_theory.measure_preserving f μ ν)
(h₂ : measurable_embedding f)
{g : δ → β} :
measure_theory.integrable (g ∘ f) μ ↔ measure_theory.integrable g ν
theorem
measure_theory.lintegral_edist_lt_top
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f g : α → β}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
@[simp]
theorem
measure_theory.integrable_zero
(α : Type u_1)
(β : Type u_2)
{m : measurable_space α}
(μ : measure_theory.measure α)
[normed_add_comm_group β] :
measure_theory.integrable (λ (_x : α), 0) μ
theorem
measure_theory.integrable.add'
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f g : α → β}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.has_finite_integral (f + g) μ
theorem
measure_theory.integrable.add
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f g : α → β}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.integrable (f + g) μ
theorem
measure_theory.integrable_finset_sum'
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{ι : Type u_3}
(s : finset ι)
{f : ι → α → β}
(hf : ∀ (i : ι), i ∈ s → measure_theory.integrable (f i) μ) :
measure_theory.integrable (s.sum (λ (i : ι), f i)) μ
theorem
measure_theory.integrable_finset_sum
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{ι : Type u_3}
(s : finset ι)
{f : ι → α → β}
(hf : ∀ (i : ι), i ∈ s → measure_theory.integrable (f i) μ) :
measure_theory.integrable (λ (a : α), s.sum (λ (i : ι), f i a)) μ
theorem
measure_theory.integrable.neg
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(hf : measure_theory.integrable f μ) :
@[simp]
theorem
measure_theory.integrable_neg_iff
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β} :
theorem
measure_theory.integrable.sub
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f g : α → β}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.integrable (f - g) μ
theorem
measure_theory.integrable.norm
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (a : α), ‖f a‖) μ
theorem
measure_theory.integrable.inf
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_2}
[normed_lattice_add_comm_group β]
{f g : α → β}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.integrable (f ⊓ g) μ
theorem
measure_theory.integrable.sup
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_2}
[normed_lattice_add_comm_group β]
{f g : α → β}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.integrable (f ⊔ g) μ
theorem
measure_theory.integrable.abs
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{β : Type u_2}
[normed_lattice_add_comm_group β]
{f : α → β}
(hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (a : α), |f a|) μ
theorem
measure_theory.integrable.bdd_mul
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{F : Type u_2}
[normed_division_ring F]
{f g : α → F}
(hint : measure_theory.integrable g μ)
(hm : measure_theory.ae_strongly_measurable f μ)
(hfbdd : ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C) :
measure_theory.integrable (λ (x : α), f x * g x) μ
theorem
measure_theory.integrable.ess_sup_smul
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{𝕜 : Type u_3}
[normed_field 𝕜]
[normed_space 𝕜 β]
{f : α → β}
(hf : measure_theory.integrable f μ)
{g : α → 𝕜}
(g_ae_strongly_measurable : measure_theory.ae_strongly_measurable g μ)
(ess_sup_g : ess_sup (λ (x : α), ↑‖g x‖₊) μ ≠ ⊤) :
measure_theory.integrable (λ (x : α), g x • f x) μ
Hölder's inequality for integrable functions: the scalar multiplication of an integrable vector-valued function by a scalar function with finite essential supremum is integrable.
theorem
measure_theory.integrable.smul_ess_sup
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{𝕜 : Type u_3}
[normed_ring 𝕜]
[module 𝕜 β]
[has_bounded_smul 𝕜 β]
{f : α → 𝕜}
(hf : measure_theory.integrable f μ)
{g : α → β}
(g_ae_strongly_measurable : measure_theory.ae_strongly_measurable g μ)
(ess_sup_g : ess_sup (λ (x : α), ↑‖g x‖₊) μ ≠ ⊤) :
measure_theory.integrable (λ (x : α), f x • g x) μ
Hölder's inequality for integrable functions: the scalar multiplication of an integrable scalar-valued function by a vector-value function with finite essential supremum is integrable.
theorem
measure_theory.integrable_norm_iff
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(hf : measure_theory.ae_strongly_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}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f₀ f₁ : α → β}
{g : α → ℝ}
(hf₁_m : measure_theory.ae_strongly_measurable f₁ μ)
(hf₀_i : measure_theory.integrable f₀ μ)
(hg_i : measure_theory.integrable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a) :
theorem
measure_theory.integrable.prod_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[normed_add_comm_group γ]
{f : α → β}
{g : α → γ}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.integrable (λ (x : α), (f x, g x)) μ
theorem
measure_theory.mem_ℒp.integrable
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{q : ennreal}
(hq1 : 1 ≤ q)
{f : α → β}
[measure_theory.is_finite_measure μ]
(hfq : measure_theory.mem_ℒp f q μ) :
theorem
measure_theory.integrable.measure_ge_lt_top
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(hf : measure_theory.integrable f μ)
{ε : ℝ}
(hε : 0 < ε) :
A non-quantitative version of Markov inequality for integrable functions: the measure of points
where ‖f x‖ ≥ ε is finite for all positive ε.
theorem
measure_theory.lipschitz_with.integrable_comp_iff_of_antilipschitz
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[normed_add_comm_group γ]
{K K' : nnreal}
{f : α → β}
{g : β → γ}
(hg : lipschitz_with K g)
(hg' : antilipschitz_with K' g)
(g0 : g 0 = 0) :
measure_theory.integrable (g ∘ f) μ ↔ measure_theory.integrable f μ
theorem
measure_theory.integrable.real_to_nnreal
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ}
(hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (x : α), ↑((f x).to_nnreal)) μ
theorem
measure_theory.of_real_to_real_ae_eq
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ennreal}
(hf : ∀ᵐ (x : α) ∂μ, f x < ⊤) :
(λ (x : α), ennreal.of_real (f x).to_real) =ᵐ[μ] f
theorem
measure_theory.integrable_with_density_iff_integrable_coe_smul
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_5}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : α → nnreal}
(hf : measurable f)
{g : α → E} :
measure_theory.integrable g (μ.with_density (λ (x : α), ↑(f x))) ↔ measure_theory.integrable (λ (x : α), ↑(f x) • g x) μ
theorem
measure_theory.integrable_with_density_iff_integrable_smul
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_5}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : α → nnreal}
(hf : measurable f)
{g : α → E} :
measure_theory.integrable g (μ.with_density (λ (x : α), ↑(f x))) ↔ measure_theory.integrable (λ (x : α), f x • g x) μ
theorem
measure_theory.integrable_with_density_iff_integrable_smul'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_5}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : α → ennreal}
(hf : measurable f)
(hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤)
{g : α → E} :
measure_theory.integrable g (μ.with_density f) ↔ measure_theory.integrable (λ (x : α), (f x).to_real • g x) μ
theorem
measure_theory.integrable_with_density_iff_integrable_coe_smul₀
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_5}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : α → nnreal}
(hf : ae_measurable f μ)
{g : α → E} :
measure_theory.integrable g (μ.with_density (λ (x : α), ↑(f x))) ↔ measure_theory.integrable (λ (x : α), ↑(f x) • g x) μ
theorem
measure_theory.integrable_with_density_iff_integrable_smul₀
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_5}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : α → nnreal}
(hf : ae_measurable f μ)
{g : α → E} :
measure_theory.integrable g (μ.with_density (λ (x : α), ↑(f x))) ↔ measure_theory.integrable (λ (x : α), f x • g x) μ
theorem
measure_theory.integrable_with_density_iff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ennreal}
(hf : measurable f)
(hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤)
{g : α → ℝ} :
measure_theory.integrable g (μ.with_density f) ↔ measure_theory.integrable (λ (x : α), g x * (f x).to_real) μ
theorem
measure_theory.mem_ℒ1_smul_of_L1_with_density
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_5}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : α → nnreal}
(f_meas : measurable f)
(u : ↥(measure_theory.Lp E 1 (μ.with_density (λ (x : α), ↑(f x))))) :
measure_theory.mem_ℒp (λ (x : α), f x • ⇑u x) 1 μ
noncomputable
def
measure_theory.with_density_smul_li
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α)
{E : Type u_5}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : α → nnreal}
(f_meas : measurable f) :
↥(measure_theory.Lp E 1 (μ.with_density (λ (x : α), ↑(f x)))) →ₗᵢ[ℝ] ↥(measure_theory.Lp E 1 μ)
The map u ↦ f • u is an isometry between the L^1 spaces for μ.with_density f and μ.
Equations
- measure_theory.with_density_smul_li μ f_meas = {to_linear_map := {to_fun := λ (u : ↥(measure_theory.Lp E 1 (μ.with_density (λ (x : α), ↑(f x))))), measure_theory.mem_ℒp.to_Lp (λ (x : α), f x • ⇑u x) _, map_add' := _, map_smul' := _}, norm_map' := _}
@[simp]
theorem
measure_theory.with_density_smul_li_apply
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α)
{E : Type u_5}
[normed_add_comm_group E]
[normed_space ℝ E]
{f : α → nnreal}
(f_meas : measurable f)
(u : ↥(measure_theory.Lp E 1 (μ.with_density (λ (x : α), ↑(f x))))) :
⇑(measure_theory.with_density_smul_li μ f_meas) u = measure_theory.mem_ℒp.to_Lp (λ (x : α), f x • ⇑u x) _
theorem
measure_theory.mem_ℒ1_to_real_of_lintegral_ne_top
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ennreal}
(hfm : ae_measurable f μ)
(hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) :
measure_theory.mem_ℒp (λ (x : α), (f x).to_real) 1 μ
theorem
measure_theory.integrable_to_real_of_lintegral_ne_top
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ennreal}
(hfm : ae_measurable f μ)
(hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) :
measure_theory.integrable (λ (x : α), (f x).to_real) μ
Lemmas used for defining the positive part of a L¹ function #
theorem
measure_theory.integrable.pos_part
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ}
(hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (a : α), linear_order.max (f a) 0) μ
theorem
measure_theory.integrable.neg_part
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ}
(hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (a : α), linear_order.max (-f a) 0) μ
theorem
measure_theory.integrable.smul
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{𝕜 : Type u_5}
[normed_add_comm_group 𝕜]
[smul_zero_class 𝕜 β]
[has_bounded_smul 𝕜 β]
(c : 𝕜)
{f : α → β}
(hf : measure_theory.integrable f μ) :
measure_theory.integrable (c • f) μ
theorem
measure_theory.is_unit.integrable_smul_iff
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{𝕜 : Type u_5}
[normed_ring 𝕜]
[module 𝕜 β]
[has_bounded_smul 𝕜 β]
{c : 𝕜}
(hc : is_unit c)
(f : α → β) :
measure_theory.integrable (c • f) μ ↔ measure_theory.integrable f μ
theorem
measure_theory.integrable_smul_iff
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{𝕜 : Type u_5}
[normed_division_ring 𝕜]
[module 𝕜 β]
[has_bounded_smul 𝕜 β]
{c : 𝕜}
(hc : c ≠ 0)
(f : α → β) :
measure_theory.integrable (c • f) μ ↔ measure_theory.integrable f μ
theorem
measure_theory.integrable.smul_of_top_right
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{𝕜 : Type u_5}
[normed_ring 𝕜]
[module 𝕜 β]
[has_bounded_smul 𝕜 β]
{f : α → β}
{φ : α → 𝕜}
(hf : measure_theory.integrable f μ)
(hφ : measure_theory.mem_ℒp φ ⊤ μ) :
measure_theory.integrable (φ • f) μ
theorem
measure_theory.integrable.smul_of_top_left
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{𝕜 : Type u_5}
[normed_ring 𝕜]
[module 𝕜 β]
[has_bounded_smul 𝕜 β]
{f : α → β}
{φ : α → 𝕜}
(hφ : measure_theory.integrable φ μ)
(hf : measure_theory.mem_ℒp f ⊤ μ) :
measure_theory.integrable (φ • f) μ
theorem
measure_theory.integrable.smul_const
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{𝕜 : Type u_5}
[normed_ring 𝕜]
[module 𝕜 β]
[has_bounded_smul 𝕜 β]
{f : α → 𝕜}
(hf : measure_theory.integrable f μ)
(c : β) :
measure_theory.integrable (λ (x : α), f x • c) μ
theorem
measure_theory.integrable_smul_const
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[nontrivially_normed_field 𝕜]
[complete_space 𝕜]
{E : Type u_6}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{f : α → 𝕜}
{c : E}
(hc : c ≠ 0) :
measure_theory.integrable (λ (x : α), f x • c) μ ↔ measure_theory.integrable f μ
theorem
measure_theory.integrable.const_mul
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[normed_ring 𝕜]
{f : α → 𝕜}
(h : measure_theory.integrable f μ)
(c : 𝕜) :
measure_theory.integrable (λ (x : α), c * f x) μ
theorem
measure_theory.integrable.const_mul'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[normed_ring 𝕜]
{f : α → 𝕜}
(h : measure_theory.integrable f μ)
(c : 𝕜) :
measure_theory.integrable ((λ (x : α), c) * f) μ
theorem
measure_theory.integrable.mul_const
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[normed_ring 𝕜]
{f : α → 𝕜}
(h : measure_theory.integrable f μ)
(c : 𝕜) :
measure_theory.integrable (λ (x : α), f x * c) μ
theorem
measure_theory.integrable.mul_const'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[normed_ring 𝕜]
{f : α → 𝕜}
(h : measure_theory.integrable f μ)
(c : 𝕜) :
measure_theory.integrable (f * λ (x : α), c) μ
theorem
measure_theory.integrable_const_mul_iff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[normed_ring 𝕜]
{c : 𝕜}
(hc : is_unit c)
(f : α → 𝕜) :
measure_theory.integrable (λ (x : α), c * f x) μ ↔ measure_theory.integrable f μ
theorem
measure_theory.integrable_mul_const_iff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[normed_ring 𝕜]
{c : 𝕜}
(hc : is_unit c)
(f : α → 𝕜) :
measure_theory.integrable (λ (x : α), f x * c) μ ↔ measure_theory.integrable f μ
theorem
measure_theory.integrable.bdd_mul'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[normed_ring 𝕜]
{f g : α → 𝕜}
{c : ℝ}
(hg : measure_theory.integrable g μ)
(hf : measure_theory.ae_strongly_measurable f μ)
(hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c) :
measure_theory.integrable (λ (x : α), f x * g x) μ
theorem
measure_theory.integrable.div_const
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[normed_division_ring 𝕜]
{f : α → 𝕜}
(h : measure_theory.integrable f μ)
(c : 𝕜) :
measure_theory.integrable (λ (x : α), f x / c) μ
theorem
measure_theory.integrable.of_real
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[is_R_or_C 𝕜]
{f : α → ℝ}
(hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (x : α), ↑(f x)) μ
theorem
measure_theory.integrable.re_im_iff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[is_R_or_C 𝕜]
{f : α → 𝕜} :
measure_theory.integrable (λ (x : α), ⇑is_R_or_C.re (f x)) μ ∧ measure_theory.integrable (λ (x : α), ⇑is_R_or_C.im (f x)) μ ↔ measure_theory.integrable f μ
theorem
measure_theory.integrable.re
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[is_R_or_C 𝕜]
{f : α → 𝕜}
(hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (x : α), ⇑is_R_or_C.re (f x)) μ
theorem
measure_theory.integrable.im
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_5}
[is_R_or_C 𝕜]
{f : α → 𝕜}
(hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (x : α), ⇑is_R_or_C.im (f x)) μ
theorem
measure_theory.integrable.trim
{α : Type u_1}
{m : measurable_space α}
{H : Type u_5}
[normed_add_comm_group H]
{m0 : measurable_space α}
{μ' : measure_theory.measure α}
{f : α → H}
(hm : m ≤ m0)
(hf_int : measure_theory.integrable f μ')
(hf : measure_theory.strongly_measurable f) :
measure_theory.integrable f (μ'.trim hm)
theorem
measure_theory.integrable_of_integrable_trim
{α : Type u_1}
{m : measurable_space α}
{H : Type u_5}
[normed_add_comm_group H]
{m0 : measurable_space α}
{μ' : measure_theory.measure α}
{f : α → H}
(hm : m ≤ m0)
(hf_int : measure_theory.integrable f (μ'.trim hm)) :
theorem
measure_theory.integrable_of_forall_fin_meas_le'
{α : Type u_1}
{m : measurable_space α}
{E : Type u_5}
{m0 : measurable_space α}
[normed_add_comm_group E]
{μ : measure_theory.measure α}
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
(C : ennreal)
(hC : C < ⊤)
{f : α → E}
(hf_meas : measure_theory.ae_strongly_measurable f μ)
(hf : ∀ (s : set α), measurable_set s → ⇑μ s ≠ ⊤ → ∫⁻ (x : α) in s, ↑‖f x‖₊ ∂μ ≤ C) :
theorem
measure_theory.integrable_of_forall_fin_meas_le
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_5}
[normed_add_comm_group E]
[measure_theory.sigma_finite μ]
(C : ennreal)
(hC : C < ⊤)
{f : α → E}
(hf_meas : measure_theory.ae_strongly_measurable f μ)
(hf : ∀ (s : set α), measurable_set s → ⇑μ s ≠ ⊤ → ∫⁻ (x : α) in s, ↑‖f x‖₊ ∂μ ≤ C) :
The predicate integrable on measurable functions modulo a.e.-equality #
def
measure_theory.ae_eq_fun.integrable
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : α →ₘ[μ] β) :
Prop
A class of almost everywhere equal functions is integrable if its function representative
is integrable.
Equations
theorem
measure_theory.ae_eq_fun.integrable_mk
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(hf : measure_theory.ae_strongly_measurable f μ) :
theorem
measure_theory.ae_eq_fun.integrable_coe_fn
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α →ₘ[μ] β} :
theorem
measure_theory.ae_eq_fun.integrable_zero
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β] :
theorem
measure_theory.ae_eq_fun.integrable.neg
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α →ₘ[μ] β} :
f.integrable → (-f).integrable
theorem
measure_theory.ae_eq_fun.integrable_iff_mem_L1
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α →ₘ[μ] β} :
f.integrable ↔ f ∈ measure_theory.Lp β 1 μ
theorem
measure_theory.ae_eq_fun.integrable.add
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f g : α →ₘ[μ] β} :
f.integrable → g.integrable → (f + g).integrable
theorem
measure_theory.ae_eq_fun.integrable.sub
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f g : α →ₘ[μ] β}
(hf : f.integrable)
(hg : g.integrable) :
(f - g).integrable
theorem
measure_theory.ae_eq_fun.integrable.smul
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{𝕜 : Type u_5}
[normed_ring 𝕜]
[module 𝕜 β]
[has_bounded_smul 𝕜 β]
{c : 𝕜}
{f : α →ₘ[μ] β} :
f.integrable → (c • f).integrable
theorem
measure_theory.L1.integrable_coe_fn
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : ↥(measure_theory.Lp β 1 μ)) :
theorem
measure_theory.L1.has_finite_integral_coe_fn
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : ↥(measure_theory.Lp β 1 μ)) :
theorem
measure_theory.L1.strongly_measurable_coe_fn
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : ↥(measure_theory.Lp β 1 μ)) :
theorem
measure_theory.L1.measurable_coe_fn
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[measurable_space β]
[borel_space β]
(f : ↥(measure_theory.Lp β 1 μ)) :
theorem
measure_theory.L1.ae_strongly_measurable_coe_fn
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : ↥(measure_theory.Lp β 1 μ)) :
theorem
measure_theory.L1.ae_measurable_coe_fn
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
[measurable_space β]
[borel_space β]
(f : ↥(measure_theory.Lp β 1 μ)) :
ae_measurable ⇑f μ
theorem
measure_theory.L1.edist_def
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f g : ↥(measure_theory.Lp β 1 μ)) :
has_edist.edist f g = ∫⁻ (a : α), has_edist.edist (⇑f a) (⇑g a) ∂μ
theorem
measure_theory.L1.dist_def
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f g : ↥(measure_theory.Lp β 1 μ)) :
has_dist.dist f g = (∫⁻ (a : α), has_edist.edist (⇑f a) (⇑g a) ∂μ).to_real
theorem
measure_theory.L1.norm_def
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : ↥(measure_theory.Lp β 1 μ)) :
theorem
measure_theory.L1.norm_sub_eq_lintegral
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f g : ↥(measure_theory.Lp β 1 μ)) :
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}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : ↥(measure_theory.Lp β 1 μ)) :
theorem
measure_theory.L1.of_real_norm_sub_eq_lintegral
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f g : ↥(measure_theory.Lp β 1 μ)) :
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}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(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}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : ↥(measure_theory.Lp β 1 μ))
(hf : measure_theory.integrable ⇑f μ) :
theorem
measure_theory.integrable.coe_fn_to_L1
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{f : α → β}
(hf : measure_theory.integrable f μ) :
⇑(measure_theory.integrable.to_L1 f hf) =ᵐ[μ] f
@[simp]
theorem
measure_theory.integrable.to_L1_zero
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(h : measure_theory.integrable 0 μ) :
@[simp]
theorem
measure_theory.integrable.to_L1_eq_mk
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : α → β)
(hf : measure_theory.integrable f μ) :
@[simp]
theorem
measure_theory.integrable.to_L1_eq_to_L1_iff
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f g : α → β)
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
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}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(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}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : α → β)
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.integrable.to_L1_sub
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f g : α → β)
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
theorem
measure_theory.integrable.norm_to_L1
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : α → β)
(hf : measure_theory.integrable f μ) :
‖measure_theory.integrable.to_L1 f hf‖ = (∫⁻ (a : α), has_edist.edist (f a) 0 ∂μ).to_real
theorem
measure_theory.integrable.norm_to_L1_eq_lintegral_norm
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : α → β)
(hf : measure_theory.integrable f μ) :
@[simp]
theorem
measure_theory.integrable.edist_to_L1_to_L1
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f g : α → β)
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
has_edist.edist (measure_theory.integrable.to_L1 f hf) (measure_theory.integrable.to_L1 g hg) = ∫⁻ (a : α), has_edist.edist (f a) (g a) ∂μ
@[simp]
theorem
measure_theory.integrable.edist_to_L1_zero
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
(f : α → β)
(hf : measure_theory.integrable f μ) :
has_edist.edist (measure_theory.integrable.to_L1 f hf) 0 = ∫⁻ (a : α), has_edist.edist (f a) 0 ∂μ
theorem
measure_theory.integrable.to_L1_smul
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{𝕜 : Type u_5}
[normed_ring 𝕜]
[module 𝕜 β]
[has_bounded_smul 𝕜 β]
(f : α → β)
(hf : measure_theory.integrable f μ)
(k : 𝕜) :
measure_theory.integrable.to_L1 (λ (a : α), k • f a) _ = k • measure_theory.integrable.to_L1 f hf
theorem
measure_theory.integrable.to_L1_smul'
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group β]
{𝕜 : Type u_5}
[normed_ring 𝕜]
[module 𝕜 β]
[has_bounded_smul 𝕜 β]
(f : α → β)
(hf : measure_theory.integrable f μ)
(k : 𝕜) :
measure_theory.integrable.to_L1 (k • f) _ = k • measure_theory.integrable.to_L1 f hf
theorem
measure_theory.integrable.apply_continuous_linear_map
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_5}
[normed_add_comm_group E]
{𝕜 : Type u_6}
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
{H : Type u_7}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{φ : α → (H →L[𝕜] E)}
(φ_int : measure_theory.integrable φ μ)
(v : H) :
measure_theory.integrable (λ (a : α), ⇑(φ a) v) μ
theorem
continuous_linear_map.integrable_comp
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_5}
[normed_add_comm_group E]
{𝕜 : Type u_6}
[nontrivially_normed_field 𝕜]
[normed_space 𝕜 E]
{H : Type u_7}
[normed_add_comm_group H]
[normed_space 𝕜 H]
{φ : α → H}
(L : H →L[𝕜] E)
(φ_int : measure_theory.integrable φ μ) :
measure_theory.integrable (λ (a : α), ⇑L (φ a)) μ