Integrable functions #
In 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.
Main definition #
- Let
f : α → βbe a function, whereαis aMeasureSpaceandβaNormedAddCommGroupwhich also aMeasurableSpace. Thenfis calledIntegrableiffisMeasurableandHasFiniteIntegral fholds.
Implementation notes #
To prove something for an arbitrary integrable function, a useful theorem is
Integrable.induction in the file SetIntegral.
Tags #
integrable
The predicate Integrable #
def
MeasureTheory.Integrable
{ε : Type u_5}
[ENorm ε]
[TopologicalSpace ε]
{α : Type u_6}
{x✝ : MeasurableSpace α}
(f : α → ε)
(μ : Measure α := by volume_tac)
:
Integrable f μ means that f is measurable and that the integral ∫⁻ a, ‖f a‖ ∂μ is finite.
Integrable f means Integrable f volume.
Equations
Instances For
Notation for Integrable with respect to a non-standard σ-algebra.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.memℒp_one_iff_integrable
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
:
Memℒp f 1 μ ↔ Integrable f μ
theorem
MeasureTheory.Integrable.aestronglyMeasurable
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : Integrable f μ)
:
theorem
MeasureTheory.Integrable.aemeasurable
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
[MeasurableSpace β]
[BorelSpace β]
{f : α → β}
(hf : Integrable f μ)
:
AEMeasurable f μ
theorem
MeasureTheory.Integrable.hasFiniteIntegral
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : Integrable f μ)
:
theorem
MeasureTheory.Integrable.mono
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
[NormedAddCommGroup γ]
{f : α → β}
{g : α → γ}
(hg : Integrable g μ)
(hf : AEStronglyMeasurable f μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖)
:
Integrable f μ
theorem
MeasureTheory.Integrable.mono'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → ℝ}
(hg : Integrable g μ)
(hf : AEStronglyMeasurable f μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a)
:
Integrable f μ
theorem
MeasureTheory.Integrable.congr'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
[NormedAddCommGroup γ]
{f : α → β}
{g : α → γ}
(hf : Integrable f μ)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖)
:
Integrable g μ
theorem
MeasureTheory.integrable_congr'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
[NormedAddCommGroup γ]
{f : α → β}
{g : α → γ}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖)
:
Integrable f μ ↔ Integrable g μ
theorem
MeasureTheory.Integrable.congr
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f g : α → β}
(hf : Integrable f μ)
(h : f =ᶠ[ae μ] g)
:
Integrable g μ
theorem
MeasureTheory.integrable_congr
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f g : α → β}
(h : f =ᶠ[ae μ] g)
:
Integrable f μ ↔ Integrable g μ
theorem
MeasureTheory.integrable_const_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{c : β}
:
Integrable (fun (x : α) => c) μ ↔ c = 0 ∨ IsFiniteMeasure μ
theorem
MeasureTheory.integrable_const_iff_isFiniteMeasure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{c : β}
(hc : c ≠ 0)
:
Integrable (fun (x : α) => c) μ ↔ IsFiniteMeasure μ
theorem
MeasureTheory.Integrable.of_mem_Icc
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
[IsFiniteMeasure μ]
(a b : ℝ)
{X : α → ℝ}
(hX : AEMeasurable X μ)
(h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Set.Icc a b)
:
Integrable X μ
@[simp]
theorem
MeasureTheory.integrable_const
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
[IsFiniteMeasure μ]
(c : β)
:
Integrable (fun (x : α) => c) μ
@[simp]
theorem
MeasureTheory.Integrable.of_finite
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
[Finite α]
[MeasurableSingletonClass α]
[IsFiniteMeasure μ]
{f : α → β}
:
Integrable f μ
@[deprecated MeasureTheory.Integrable.of_finite (since := "2024-10-05")]
theorem
MeasureTheory.Integrable.of_isEmpty
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
[IsEmpty α]
{f : α → β}
:
Integrable f μ
This lemma is a special case of Integrable.of_finite.
theorem
MeasureTheory.Memℒp.integrable_norm_rpow
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
{p : ENNReal}
(hf : Memℒp f p μ)
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
Integrable (fun (x : α) => ‖f x‖ ^ p.toReal) μ
theorem
MeasureTheory.Memℒp.integrable_norm_rpow'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
[IsFiniteMeasure μ]
{f : α → β}
{p : ENNReal}
(hf : Memℒp f p μ)
:
Integrable (fun (x : α) => ‖f x‖ ^ p.toReal) μ
theorem
MeasureTheory.Memℒp.integrable_norm_pow
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
{p : ℕ}
(hf : Memℒp f (↑p) μ)
(hp : p ≠ 0)
:
Integrable (fun (x : α) => ‖f x‖ ^ p) μ
theorem
MeasureTheory.Memℒp.integrable_norm_pow'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
[IsFiniteMeasure μ]
{f : α → β}
{p : ℕ}
(hf : Memℒp f (↑p) μ)
:
Integrable (fun (x : α) => ‖f x‖ ^ p) μ
theorem
MeasureTheory.integrable_norm_rpow_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
{p : ENNReal}
(hf : AEStronglyMeasurable f μ)
(p_zero : p ≠ 0)
(p_top : p ≠ ⊤)
:
theorem
MeasureTheory.Integrable.mono_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ ν : Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : Integrable f ν)
(hμ : μ ≤ ν)
:
Integrable f μ
theorem
MeasureTheory.Integrable.of_measure_le_smul
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{μ' : Measure α}
(c : ENNReal)
(hc : c ≠ ⊤)
(hμ'_le : μ' ≤ c • μ)
{f : α → β}
(hf : Integrable f μ)
:
Integrable f μ'
theorem
MeasureTheory.Integrable.add_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ ν : Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hμ : Integrable f μ)
(hν : Integrable f ν)
:
Integrable f (μ + ν)
theorem
MeasureTheory.Integrable.left_of_add_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ ν : Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : Integrable f (μ + ν))
:
Integrable f μ
theorem
MeasureTheory.Integrable.right_of_add_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ ν : Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : Integrable f (μ + ν))
:
Integrable f ν
@[simp]
theorem
MeasureTheory.integrable_add_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ ν : Measure α}
[NormedAddCommGroup β]
{f : α → β}
:
Integrable f (μ + ν) ↔ Integrable f μ ∧ Integrable f ν
@[simp]
theorem
MeasureTheory.integrable_zero_measure
{α : Type u_1}
{β : Type u_2}
[NormedAddCommGroup β]
{x✝ : MeasurableSpace α}
{f : α → β}
:
Integrable f 0
theorem
MeasureTheory.integrable_finset_sum_measure
{α : Type u_1}
{β : Type u_2}
[NormedAddCommGroup β]
{ι : Type u_6}
{m : MeasurableSpace α}
{f : α → β}
{μ : ι → Measure α}
{s : Finset ι}
:
Integrable f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)
theorem
MeasureTheory.Integrable.smul_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : Integrable f μ)
{c : ENNReal}
(hc : c ≠ ⊤)
:
Integrable f (c • μ)
theorem
MeasureTheory.Integrable.smul_measure_nnreal
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : Integrable f μ)
{c : NNReal}
:
Integrable f (c • μ)
theorem
MeasureTheory.integrable_smul_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
{c : ENNReal}
(h₁ : c ≠ 0)
(h₂ : c ≠ ⊤)
:
Integrable f (c • μ) ↔ Integrable f μ
theorem
MeasureTheory.integrable_inv_smul_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
{c : ENNReal}
(h₁ : c ≠ 0)
(h₂ : c ≠ ⊤)
:
Integrable f (c⁻¹ • μ) ↔ Integrable f μ
theorem
MeasureTheory.Integrable.to_average
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : Integrable f μ)
:
Integrable f ((μ Set.univ)⁻¹ • μ)
theorem
MeasureTheory.integrable_average
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
[IsFiniteMeasure μ]
{f : α → β}
:
Integrable f ((μ Set.univ)⁻¹ • μ) ↔ Integrable f μ
theorem
MeasureTheory.integrable_map_measure
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MeasurableSpace δ]
[NormedAddCommGroup β]
{f : α → δ}
{g : δ → β}
(hg : AEStronglyMeasurable g (Measure.map f μ))
(hf : AEMeasurable f μ)
:
Integrable g (Measure.map f μ) ↔ Integrable (g ∘ f) μ
theorem
MeasureTheory.Integrable.comp_aemeasurable
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MeasurableSpace δ]
[NormedAddCommGroup β]
{f : α → δ}
{g : δ → β}
(hg : Integrable g (Measure.map f μ))
(hf : AEMeasurable f μ)
:
Integrable (g ∘ f) μ
theorem
MeasureTheory.Integrable.comp_measurable
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MeasurableSpace δ]
[NormedAddCommGroup β]
{f : α → δ}
{g : δ → β}
(hg : Integrable g (Measure.map f μ))
(hf : Measurable f)
:
Integrable (g ∘ f) μ
theorem
MeasurableEmbedding.integrable_map_iff
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasurableSpace δ]
[NormedAddCommGroup β]
{f : α → δ}
(hf : MeasurableEmbedding f)
{g : δ → β}
:
MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Integrable (g ∘ f) μ
theorem
MeasureTheory.integrable_map_equiv
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MeasurableSpace δ]
[NormedAddCommGroup β]
(f : α ≃ᵐ δ)
(g : δ → β)
:
Integrable g (Measure.map (⇑f) μ) ↔ Integrable (g ∘ ⇑f) μ
theorem
MeasureTheory.MeasurePreserving.integrable_comp
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MeasurableSpace δ]
[NormedAddCommGroup β]
{ν : Measure δ}
{g : δ → β}
{f : α → δ}
(hf : MeasurePreserving f μ ν)
(hg : AEStronglyMeasurable g ν)
:
Integrable (g ∘ f) μ ↔ Integrable g ν
theorem
MeasureTheory.MeasurePreserving.integrable_comp_emb
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[MeasurableSpace δ]
[NormedAddCommGroup β]
{f : α → δ}
{ν : Measure δ}
(h₁ : MeasurePreserving f μ ν)
(h₂ : MeasurableEmbedding f)
{g : δ → β}
:
Integrable (g ∘ f) μ ↔ Integrable g ν
theorem
MeasureTheory.lintegral_edist_lt_top
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f g : α → β}
(hf : Integrable f μ)
(hg : Integrable g μ)
:
@[simp]
theorem
MeasureTheory.integrable_zero
(α : Type u_1)
(β : Type u_2)
{m : MeasurableSpace α}
(μ : Measure α)
[NormedAddCommGroup β]
:
Integrable (fun (x : α) => 0) μ
theorem
MeasureTheory.Integrable.add'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f g : α → β}
(hf : Integrable f μ)
(hg : Integrable g μ)
:
HasFiniteIntegral (f + g) μ
theorem
MeasureTheory.Integrable.add
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f g : α → β}
(hf : Integrable f μ)
(hg : Integrable g μ)
:
Integrable (f + g) μ
theorem
MeasureTheory.Integrable.add''
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f g : α → β}
(hf : Integrable f μ)
(hg : Integrable g μ)
:
Integrable (fun (x : α) => f x + g x) μ
theorem
MeasureTheory.integrable_finset_sum'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{ι : Type u_6}
(s : Finset ι)
{f : ι → α → β}
(hf : ∀ i ∈ s, Integrable (f i) μ)
:
Integrable (∑ i ∈ s, f i) μ
theorem
MeasureTheory.integrable_finset_sum
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{ι : Type u_6}
(s : Finset ι)
{f : ι → α → β}
(hf : ∀ i ∈ s, Integrable (f i) μ)
:
Integrable (fun (a : α) => ∑ i ∈ s, f i a) μ
theorem
MeasureTheory.Integrable.neg
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : Integrable f μ)
:
Integrable (-f) μ
If f is integrable, then so is -f.
See Integrable.neg' for the same statement, but formulated with x ↦ - f x instead of -f.
theorem
MeasureTheory.Integrable.neg'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : Integrable f μ)
:
Integrable (fun (x : α) => -f x) μ
If f is integrable, then so is fun x ↦ - f x.
See Integrable.neg for the same statement, but formulated with -f instead of fun x ↦ - f x.
@[simp]
theorem
MeasureTheory.integrable_neg_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
:
Integrable (-f) μ ↔ Integrable f μ
@[simp]
theorem
MeasureTheory.integrable_add_iff_integrable_right
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f g : α → β}
(hf : Integrable f μ)
:
Integrable (f + g) μ ↔ Integrable g μ
if f is integrable, then f + g is integrable iff g is.
See integrable_add_iff_integrable_right' for the same statement with fun x ↦ f x + g x instead
of f + g.
@[simp]
theorem
MeasureTheory.integrable_add_iff_integrable_right'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f g : α → β}
(hf : Integrable f μ)
:
Integrable (fun (x : α) => f x + g x) μ ↔ Integrable g μ
if f is integrable, then fun x ↦ f x + g x is integrable iff g is.
See integrable_add_iff_integrable_right for the same statement with f + g instead
of fun x ↦ f x + g x.
@[simp]
theorem
MeasureTheory.integrable_add_iff_integrable_left
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f g : α → β}
(hf : Integrable f μ)
:
Integrable (g + f) μ ↔ Integrable g μ
if f is integrable, then g + f is integrable iff g is.
See integrable_add_iff_integrable_left' for the same statement with fun x ↦ g x + f x instead
of g + f.
@[simp]
theorem
MeasureTheory.integrable_add_iff_integrable_left'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f g : α → β}
(hf : Integrable f μ)
:
Integrable (fun (x : α) => g x + f x) μ ↔ Integrable g μ
if f is integrable, then fun x ↦ g x + f x is integrable iff g is.
See integrable_add_iff_integrable_left' for the same statement with g + f instead
of fun x ↦ g x + f x.
theorem
MeasureTheory.integrable_left_of_integrable_add_of_nonneg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f g : α → ℝ}
(h_meas : AEStronglyMeasurable f μ)
(hf : 0 ≤ᶠ[ae μ] f)
(hg : 0 ≤ᶠ[ae μ] g)
(h_int : Integrable (f + g) μ)
:
Integrable f μ
theorem
MeasureTheory.integrable_right_of_integrable_add_of_nonneg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f g : α → ℝ}
(h_meas : AEStronglyMeasurable f μ)
(hf : 0 ≤ᶠ[ae μ] f)
(hg : 0 ≤ᶠ[ae μ] g)
(h_int : Integrable (f + g) μ)
:
Integrable g μ
theorem
MeasureTheory.integrable_add_iff_of_nonneg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f g : α → ℝ}
(h_meas : AEStronglyMeasurable f μ)
(hf : 0 ≤ᶠ[ae μ] f)
(hg : 0 ≤ᶠ[ae μ] g)
:
Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ
theorem
MeasureTheory.integrable_add_iff_of_nonpos
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f g : α → ℝ}
(h_meas : AEStronglyMeasurable f μ)
(hf : f ≤ᶠ[ae μ] 0)
(hg : g ≤ᶠ[ae μ] 0)
:
Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ
theorem
MeasureTheory.integrable_add_const_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
[IsFiniteMeasure μ]
{f : α → β}
{c : β}
:
Integrable (fun (x : α) => f x + c) μ ↔ Integrable f μ
theorem
MeasureTheory.integrable_const_add_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
[IsFiniteMeasure μ]
{f : α → β}
{c : β}
:
Integrable (fun (x : α) => c + f x) μ ↔ Integrable f μ
theorem
MeasureTheory.Integrable.sub
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f g : α → β}
(hf : Integrable f μ)
(hg : Integrable g μ)
:
Integrable (f - g) μ
theorem
MeasureTheory.Integrable.sub'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f g : α → β}
(hf : Integrable f μ)
(hg : Integrable g μ)
:
Integrable (fun (a : α) => f a - g a) μ
theorem
MeasureTheory.Integrable.norm
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : Integrable f μ)
:
Integrable (fun (a : α) => ‖f a‖) μ
theorem
MeasureTheory.Integrable.inf
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{β : Type u_6}
[NormedLatticeAddCommGroup β]
{f g : α → β}
(hf : Integrable f μ)
(hg : Integrable g μ)
:
Integrable (f ⊓ g) μ
theorem
MeasureTheory.Integrable.sup
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{β : Type u_6}
[NormedLatticeAddCommGroup β]
{f g : α → β}
(hf : Integrable f μ)
(hg : Integrable g μ)
:
Integrable (f ⊔ g) μ
theorem
MeasureTheory.Integrable.abs
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{β : Type u_6}
[NormedLatticeAddCommGroup β]
{f : α → β}
(hf : Integrable f μ)
:
Integrable (fun (a : α) => |f a|) μ
theorem
MeasureTheory.Integrable.bdd_mul
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{F : Type u_6}
[NormedDivisionRing F]
{f g : α → F}
(hint : Integrable g μ)
(hm : AEStronglyMeasurable f μ)
(hfbdd : ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C)
:
Integrable (fun (x : α) => f x * g x) μ
theorem
MeasureTheory.Integrable.essSup_smul
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_6}
[NormedField 𝕜]
[NormedSpace 𝕜 β]
{f : α → β}
(hf : Integrable f μ)
{g : α → 𝕜}
(g_aestronglyMeasurable : AEStronglyMeasurable g μ)
(ess_sup_g : essSup (fun (x : α) => ‖g x‖ₑ) μ ≠ ⊤)
:
Integrable (fun (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
MeasureTheory.Integrable.smul_essSup
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[Module 𝕜 β]
[BoundedSMul 𝕜 β]
{f : α → 𝕜}
(hf : Integrable f μ)
{g : α → β}
(g_aestronglyMeasurable : AEStronglyMeasurable g μ)
(ess_sup_g : essSup (fun (x : α) => ‖g x‖ₑ) μ ≠ ⊤)
:
Integrable (fun (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
MeasureTheory.integrable_norm_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : AEStronglyMeasurable f μ)
:
Integrable (fun (a : α) => ‖f a‖) μ ↔ Integrable f μ
theorem
MeasureTheory.integrable_of_norm_sub_le
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f₀ f₁ : α → β}
{g : α → ℝ}
(hf₁_m : AEStronglyMeasurable f₁ μ)
(hf₀_i : Integrable f₀ μ)
(hg_i : Integrable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a)
:
Integrable f₁ μ
theorem
MeasureTheory.integrable_of_le_of_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f g₁ g₂ : α → ℝ}
(hf : AEStronglyMeasurable f μ)
(h_le₁ : g₁ ≤ᶠ[ae μ] f)
(h_le₂ : f ≤ᶠ[ae μ] g₂)
(h_int₁ : Integrable g₁ μ)
(h_int₂ : Integrable g₂ μ)
:
Integrable f μ
theorem
MeasureTheory.Integrable.prod_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
[NormedAddCommGroup γ]
{f : α → β}
{g : α → γ}
(hf : Integrable f μ)
(hg : Integrable g μ)
:
Integrable (fun (x : α) => (f x, g x)) μ
theorem
MeasureTheory.Memℒp.integrable
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{q : ENNReal}
(hq1 : 1 ≤ q)
{f : α → β}
[IsFiniteMeasure μ]
(hfq : Memℒp f q μ)
:
Integrable f μ
theorem
MeasureTheory.Integrable.measure_norm_ge_lt_top
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : 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
MeasureTheory.Integrable.measure_norm_gt_lt_top
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : 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
MeasureTheory.Integrable.measure_ge_lt_top
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
(hf : Integrable f μ)
{ε : ℝ}
(ε_pos : 0 < ε)
:
If f is ℝ-valued and integrable, then for any c > 0 the set {x | f x ≥ c} has finite
measure.
theorem
MeasureTheory.Integrable.measure_le_lt_top
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
(hf : Integrable f μ)
{c : ℝ}
(c_neg : c < 0)
:
If f is ℝ-valued and integrable, then for any c < 0 the set {x | f x ≤ c} has finite
measure.
theorem
MeasureTheory.Integrable.measure_gt_lt_top
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
(hf : Integrable f μ)
{ε : ℝ}
(ε_pos : 0 < ε)
:
If f is ℝ-valued and integrable, then for any c > 0 the set {x | f x > c} has finite
measure.
theorem
MeasureTheory.Integrable.measure_lt_lt_top
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
(hf : Integrable f μ)
{c : ℝ}
(c_neg : c < 0)
:
If f is ℝ-valued and integrable, then for any c < 0 the set {x | f x < c} has finite
measure.
theorem
MeasureTheory.LipschitzWith.integrable_comp_iff_of_antilipschitz
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
[NormedAddCommGroup γ]
{K K' : NNReal}
{f : α → β}
{g : β → γ}
(hg : LipschitzWith K g)
(hg' : AntilipschitzWith K' g)
(g0 : g 0 = 0)
:
Integrable (g ∘ f) μ ↔ Integrable f μ
theorem
MeasureTheory.Integrable.real_toNNReal
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
(hf : Integrable f μ)
:
Integrable (fun (x : α) => ↑(f x).toNNReal) μ
theorem
MeasureTheory.ofReal_toReal_ae_eq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ENNReal}
(hf : ∀ᵐ (x : α) ∂μ, f x < ⊤)
:
(fun (x : α) => ENNReal.ofReal (f x).toReal) =ᶠ[ae μ] f
theorem
MeasureTheory.integrable_count_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup β]
[MeasurableSingletonClass α]
{f : α → β}
:
Integrable f Measure.count ↔ Summable fun (x : α) => ‖f x‖
A function is integrable for the counting measure iff its norm is summable.
theorem
MeasureTheory.integrable_withDensity_iff_integrable_coe_smul
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → NNReal}
(hf : Measurable f)
{g : α → E}
:
Integrable g (μ.withDensity fun (x : α) => ↑(f x)) ↔ Integrable (fun (x : α) => ↑(f x) • g x) μ
theorem
MeasureTheory.integrable_withDensity_iff_integrable_smul
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → NNReal}
(hf : Measurable f)
{g : α → E}
:
Integrable g (μ.withDensity fun (x : α) => ↑(f x)) ↔ Integrable (fun (x : α) => f x • g x) μ
theorem
MeasureTheory.integrable_withDensity_iff_integrable_smul'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → ENNReal}
(hf : Measurable f)
(hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤)
{g : α → E}
:
Integrable g (μ.withDensity f) ↔ Integrable (fun (x : α) => (f x).toReal • g x) μ
theorem
MeasureTheory.integrable_withDensity_iff_integrable_coe_smul₀
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → NNReal}
(hf : AEMeasurable f μ)
{g : α → E}
:
Integrable g (μ.withDensity fun (x : α) => ↑(f x)) ↔ Integrable (fun (x : α) => ↑(f x) • g x) μ
theorem
MeasureTheory.integrable_withDensity_iff_integrable_smul₀
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → NNReal}
(hf : AEMeasurable f μ)
{g : α → E}
:
Integrable g (μ.withDensity fun (x : α) => ↑(f x)) ↔ Integrable (fun (x : α) => f x • g x) μ
theorem
MeasureTheory.integrable_withDensity_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ENNReal}
(hf : Measurable f)
(hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤)
{g : α → ℝ}
:
Integrable g (μ.withDensity f) ↔ Integrable (fun (x : α) => g x * (f x).toReal) μ
theorem
MeasureTheory.memℒ1_smul_of_L1_withDensity
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → NNReal}
(f_meas : Measurable f)
(u : ↥(Lp E 1 (μ.withDensity fun (x : α) => ↑(f x))))
:
noncomputable def
MeasureTheory.withDensitySMulLI
{α : Type u_1}
{m : MeasurableSpace α}
(μ : Measure α)
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → NNReal}
(f_meas : Measurable f)
:
The map u ↦ f • u is an isometry between the L^1 spaces for μ.withDensity f and μ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
MeasureTheory.withDensitySMulLI_apply
{α : Type u_1}
{m : MeasurableSpace α}
(μ : Measure α)
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → NNReal}
(f_meas : Measurable f)
(u : ↥(Lp E 1 (μ.withDensity fun (x : α) => ↑(f x))))
:
(withDensitySMulLI μ f_meas) u = Memℒp.toLp (fun (x : α) => f x • ↑↑u x) ⋯
theorem
MeasureTheory.mem_ℒ1_toReal_of_lintegral_ne_top
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ENNReal}
(hfm : AEMeasurable f μ)
(hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤)
:
Memℒp (fun (x : α) => (f x).toReal) 1 μ
theorem
MeasureTheory.integrable_toReal_of_lintegral_ne_top
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ENNReal}
(hfm : AEMeasurable f μ)
(hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤)
:
Integrable (fun (x : α) => (f x).toReal) μ
theorem
MeasureTheory.integrable_toReal_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ENNReal}
(hf : AEMeasurable f μ)
(hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤)
:
theorem
MeasureTheory.lintegral_ofReal_ne_top_iff_integrable
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
(hfm : AEStronglyMeasurable f μ)
(hf : 0 ≤ᶠ[ae μ] f)
:
∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ ≠ ⊤ ↔ Integrable f μ
Lemmas used for defining the positive part of an L¹ function #
theorem
MeasureTheory.Integrable.pos_part
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
(hf : Integrable f μ)
:
Integrable (fun (a : α) => f a ⊔ 0) μ
theorem
MeasureTheory.Integrable.neg_part
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ℝ}
(hf : Integrable f μ)
:
Integrable (fun (a : α) => -f a ⊔ 0) μ
theorem
MeasureTheory.Integrable.smul
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_6}
[NormedAddCommGroup 𝕜]
[SMulZeroClass 𝕜 β]
[BoundedSMul 𝕜 β]
(c : 𝕜)
{f : α → β}
(hf : Integrable f μ)
:
Integrable (c • f) μ
theorem
IsUnit.integrable_smul_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[Module 𝕜 β]
[BoundedSMul 𝕜 β]
{c : 𝕜}
(hc : IsUnit c)
(f : α → β)
:
MeasureTheory.Integrable (c • f) μ ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.integrable_smul_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_6}
[NormedDivisionRing 𝕜]
[Module 𝕜 β]
[BoundedSMul 𝕜 β]
{c : 𝕜}
(hc : c ≠ 0)
(f : α → β)
:
Integrable (c • f) μ ↔ Integrable f μ
theorem
MeasureTheory.Integrable.smul_of_top_right
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[Module 𝕜 β]
[BoundedSMul 𝕜 β]
{f : α → β}
{φ : α → 𝕜}
(hf : Integrable f μ)
(hφ : Memℒp φ ⊤ μ)
:
Integrable (φ • f) μ
theorem
MeasureTheory.Integrable.smul_of_top_left
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[Module 𝕜 β]
[BoundedSMul 𝕜 β]
{f : α → β}
{φ : α → 𝕜}
(hφ : Integrable φ μ)
(hf : Memℒp f ⊤ μ)
:
Integrable (φ • f) μ
theorem
MeasureTheory.Integrable.smul_const
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_6}
[NormedRing 𝕜]
[Module 𝕜 β]
[BoundedSMul 𝕜 β]
{f : α → 𝕜}
(hf : Integrable f μ)
(c : β)
:
Integrable (fun (x : α) => f x • c) μ
theorem
MeasureTheory.integrable_smul_const
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_6}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_7}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{f : α → 𝕜}
{c : E}
(hc : c ≠ 0)
:
Integrable (fun (x : α) => f x • c) μ ↔ Integrable f μ
theorem
MeasureTheory.Integrable.const_mul
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_6}
[NormedRing 𝕜]
{f : α → 𝕜}
(h : Integrable f μ)
(c : 𝕜)
:
Integrable (fun (x : α) => c * f x) μ
theorem
MeasureTheory.Integrable.const_mul'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_6}
[NormedRing 𝕜]
{f : α → 𝕜}
(h : Integrable f μ)
(c : 𝕜)
:
Integrable ((fun (x : α) => c) * f) μ
theorem
MeasureTheory.Integrable.mul_const
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_6}
[NormedRing 𝕜]
{f : α → 𝕜}
(h : Integrable f μ)
(c : 𝕜)
:
Integrable (fun (x : α) => f x * c) μ
theorem
MeasureTheory.Integrable.mul_const'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_6}
[NormedRing 𝕜]
{f : α → 𝕜}
(h : Integrable f μ)
(c : 𝕜)
:
Integrable (f * fun (x : α) => c) μ
theorem
MeasureTheory.integrable_const_mul_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_6}
[NormedRing 𝕜]
{c : 𝕜}
(hc : IsUnit c)
(f : α → 𝕜)
:
Integrable (fun (x : α) => c * f x) μ ↔ Integrable f μ
theorem
MeasureTheory.integrable_mul_const_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_6}
[NormedRing 𝕜]
{c : 𝕜}
(hc : IsUnit c)
(f : α → 𝕜)
:
Integrable (fun (x : α) => f x * c) μ ↔ Integrable f μ
theorem
MeasureTheory.Integrable.bdd_mul'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_6}
[NormedRing 𝕜]
{f g : α → 𝕜}
{c : ℝ}
(hg : Integrable g μ)
(hf : AEStronglyMeasurable f μ)
(hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c)
:
Integrable (fun (x : α) => f x * g x) μ
theorem
MeasureTheory.Integrable.mul_of_top_right
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_6}
[NormedRing 𝕜]
{f φ : α → 𝕜}
(hf : Integrable f μ)
(hφ : Memℒp φ ⊤ μ)
:
Integrable (φ * f) μ
theorem
MeasureTheory.Integrable.mul_of_top_left
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_6}
[NormedRing 𝕜]
{f φ : α → 𝕜}
(hφ : Integrable φ μ)
(hf : Memℒp f ⊤ μ)
:
Integrable (φ * f) μ
theorem
MeasureTheory.Integrable.div_const
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_6}
[NormedDivisionRing 𝕜]
{f : α → 𝕜}
(h : Integrable f μ)
(c : 𝕜)
:
Integrable (fun (x : α) => f x / c) μ
theorem
MeasureTheory.Integrable.ofReal
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_6}
[RCLike 𝕜]
{f : α → ℝ}
(hf : Integrable f μ)
:
Integrable (fun (x : α) => ↑(f x)) μ
theorem
MeasureTheory.Integrable.re_im_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_6}
[RCLike 𝕜]
{f : α → 𝕜}
:
Integrable (fun (x : α) => RCLike.re (f x)) μ ∧ Integrable (fun (x : α) => RCLike.im (f x)) μ ↔ Integrable f μ
theorem
MeasureTheory.Integrable.re
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_6}
[RCLike 𝕜]
{f : α → 𝕜}
(hf : Integrable f μ)
:
Integrable (fun (x : α) => RCLike.re (f x)) μ
theorem
MeasureTheory.Integrable.im
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{𝕜 : Type u_6}
[RCLike 𝕜]
{f : α → 𝕜}
(hf : Integrable f μ)
:
Integrable (fun (x : α) => RCLike.im (f x)) μ
theorem
MeasureTheory.Integrable.trim
{α : Type u_1}
{m : MeasurableSpace α}
{H : Type u_6}
[NormedAddCommGroup H]
{m0 : MeasurableSpace α}
{μ' : Measure α}
{f : α → H}
(hm : m ≤ m0)
(hf_int : Integrable f μ')
(hf : StronglyMeasurable f)
:
Integrable f (μ'.trim hm)
theorem
MeasureTheory.integrable_of_integrable_trim
{α : Type u_1}
{m : MeasurableSpace α}
{H : Type u_6}
[NormedAddCommGroup H]
{m0 : MeasurableSpace α}
{μ' : Measure α}
{f : α → H}
(hm : m ≤ m0)
(hf_int : Integrable f (μ'.trim hm))
:
Integrable f μ'
theorem
MeasureTheory.integrable_of_forall_fin_meas_le'
{α : Type u_1}
{m : MeasurableSpace α}
{E : Type u_6}
{m0 : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : Measure α}
(hm : m ≤ m0)
[SigmaFinite (μ.trim hm)]
(C : ENNReal)
(hC : C < ⊤)
{f : α → E}
(hf_meas : AEStronglyMeasurable f μ)
(hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ ≤ C)
:
Integrable f μ
theorem
MeasureTheory.integrable_of_forall_fin_meas_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_6}
[NormedAddCommGroup E]
[SigmaFinite μ]
(C : ENNReal)
(hC : C < ⊤)
{f : α → E}
(hf_meas : AEStronglyMeasurable f μ)
(hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ ≤ C)
:
Integrable f μ
theorem
MeasureTheory.Integrable.restrict
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_6}
[NormedAddCommGroup E]
{f : α → E}
(hf : Integrable f μ)
{s : Set α}
:
Integrable f (μ.restrict s)
One should usually use MeasureTheory.Integrable.IntegrableOn instead.
theorem
ContinuousLinearMap.integrable_comp
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_6}
[NormedAddCommGroup E]
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
{H : Type u_8}
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{φ : α → H}
(L : H →L[𝕜] E)
(φ_int : MeasureTheory.Integrable φ μ)
:
MeasureTheory.Integrable (fun (a : α) => L (φ a)) μ
@[simp]
theorem
ContinuousLinearEquiv.integrable_comp_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_6}
[NormedAddCommGroup E]
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
{H : Type u_8}
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{φ : α → H}
(L : H ≃L[𝕜] E)
:
MeasureTheory.Integrable (fun (a : α) => L (φ a)) μ ↔ MeasureTheory.Integrable φ μ
@[simp]
theorem
LinearIsometryEquiv.integrable_comp_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_6}
[NormedAddCommGroup E]
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
{H : Type u_8}
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{φ : α → H}
(L : H ≃ₗᵢ[𝕜] E)
:
MeasureTheory.Integrable (fun (a : α) => L (φ a)) μ ↔ MeasureTheory.Integrable φ μ
theorem
MeasureTheory.Integrable.apply_continuousLinearMap
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_6}
[NormedAddCommGroup E]
{𝕜 : Type u_7}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
{H : Type u_8}
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{φ : α → H →L[𝕜] E}
(φ_int : Integrable φ μ)
(v : H)
:
Integrable (fun (a : α) => (φ a) v) μ
theorem
MeasureTheory.Integrable.fst
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_6}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : α → E × F}
(hf : Integrable f μ)
:
Integrable (fun (x : α) => (f x).1) μ
theorem
MeasureTheory.Integrable.snd
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_6}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : α → E × F}
(hf : Integrable f μ)
:
Integrable (fun (x : α) => (f x).2) μ
theorem
MeasureTheory.integrable_prod
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{E : Type u_6}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : α → E × F}
:
Integrable f μ ↔ Integrable (fun (x : α) => (f x).1) μ ∧ Integrable (fun (x : α) => (f x).2) μ