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 aMeasureSpaceandβis aNormedAddCommGroupwith aSecondCountableTopology.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 aMeasureSpaceandβaNormedAddCommGroup. ThenHasFiniteIntegral fmeans(∫⁻ a, ‖f a‖₊) < ∞.If
βis moreover aMeasurableSpacethenfis calledIntegrableiffisMeasurableandHasFiniteIntegral fholds.
Implementation notes #
To prove something for an arbitrary integrable function, a useful theorem is
Integrable.induction in the file SetIntegral.
Tags #
integrable, function space, l1
Some results about the Lebesgue integral involving a normed group #
theorem
MeasureTheory.lintegral_nnnorm_eq_lintegral_edist
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α → β)
:
theorem
MeasureTheory.lintegral_norm_eq_lintegral_edist
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α → β)
:
∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∫⁻ (a : α), edist (f a) 0 ∂μ
theorem
MeasureTheory.lintegral_edist_triangle
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → β}
{h : α → β}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hh : MeasureTheory.AEStronglyMeasurable h μ)
:
theorem
MeasureTheory.lintegral_nnnorm_zero
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
:
theorem
MeasureTheory.lintegral_nnnorm_add_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[NormedAddCommGroup γ]
{f : α → β}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(g : α → γ)
:
theorem
MeasureTheory.lintegral_nnnorm_add_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[NormedAddCommGroup γ]
(f : α → β)
{g : α → γ}
(hg : MeasureTheory.AEStronglyMeasurable g μ)
:
theorem
MeasureTheory.lintegral_nnnorm_neg
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
:
The predicate HasFiniteIntegral #
def
MeasureTheory.HasFiniteIntegral
{α : Type u_1}
{β : Type u_2}
[NormedAddCommGroup β]
:
{x : MeasurableSpace α} → (α → β) → autoParam (MeasureTheory.Measure α) _auto✝ → Prop
HasFiniteIntegral f μ means that the integral ∫⁻ a, ‖f a‖ ∂μ is finite.
HasFiniteIntegral f means HasFiniteIntegral f volume.
Instances For
theorem
MeasureTheory.hasFiniteIntegral_def
{α : Type u_1}
{β : Type u_2}
[NormedAddCommGroup β]
:
∀ {x : MeasurableSpace α} (f : α → β) (μ : MeasureTheory.Measure α),
MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
theorem
MeasureTheory.hasFiniteIntegral_iff_norm
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α → β)
:
MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ⊤
theorem
MeasureTheory.hasFiniteIntegral_iff_edist
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α → β)
:
MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), edist (f a) 0 ∂μ < ⊤
theorem
MeasureTheory.hasFiniteIntegral_iff_ofReal
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(h : 0 ≤ᵐ[μ] f)
:
MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ⊤
theorem
MeasureTheory.hasFiniteIntegral_iff_ofNNReal
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → NNReal}
:
MeasureTheory.HasFiniteIntegral (fun (x : α) => ↑(f x)) μ ↔ ∫⁻ (a : α), ↑(f a) ∂μ < ⊤
theorem
MeasureTheory.HasFiniteIntegral.mono
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[NormedAddCommGroup γ]
{f : α → β}
{g : α → γ}
(hg : MeasureTheory.HasFiniteIntegral g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖)
:
theorem
MeasureTheory.HasFiniteIntegral.mono'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → ℝ}
(hg : MeasureTheory.HasFiniteIntegral g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a)
:
theorem
MeasureTheory.HasFiniteIntegral.congr'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[NormedAddCommGroup γ]
{f : α → β}
{g : α → γ}
(hf : MeasureTheory.HasFiniteIntegral f μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖)
:
theorem
MeasureTheory.hasFiniteIntegral_congr'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[NormedAddCommGroup γ]
{f : α → β}
{g : α → γ}
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖)
:
theorem
MeasureTheory.HasFiniteIntegral.congr
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → β}
(hf : MeasureTheory.HasFiniteIntegral f μ)
(h : f =ᵐ[μ] g)
:
theorem
MeasureTheory.hasFiniteIntegral_congr
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → β}
(h : f =ᵐ[μ] g)
:
theorem
MeasureTheory.hasFiniteIntegral_const_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{c : β}
:
theorem
MeasureTheory.hasFiniteIntegral_const
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[MeasureTheory.IsFiniteMeasure μ]
(c : β)
:
MeasureTheory.HasFiniteIntegral (fun (x : α) => c) μ
theorem
MeasureTheory.hasFiniteIntegral_of_bounded
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[MeasureTheory.IsFiniteMeasure μ]
{f : α → β}
{C : ℝ}
(hC : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ C)
:
theorem
MeasureTheory.HasFiniteIntegral.of_finite
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[Finite α]
[MeasureTheory.IsFiniteMeasure μ]
{f : α → β}
:
@[deprecated MeasureTheory.HasFiniteIntegral.of_finite]
theorem
MeasureTheory.hasFiniteIntegral_of_fintype
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[Finite α]
[MeasureTheory.IsFiniteMeasure μ]
{f : α → β}
:
theorem
MeasureTheory.HasFiniteIntegral.mono_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : MeasureTheory.HasFiniteIntegral f ν)
(hμ : μ ≤ ν)
:
theorem
MeasureTheory.HasFiniteIntegral.add_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hμ : MeasureTheory.HasFiniteIntegral f μ)
(hν : MeasureTheory.HasFiniteIntegral f ν)
:
MeasureTheory.HasFiniteIntegral f (μ + ν)
theorem
MeasureTheory.HasFiniteIntegral.left_of_add_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : MeasureTheory.HasFiniteIntegral f (μ + ν))
:
theorem
MeasureTheory.HasFiniteIntegral.right_of_add_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : MeasureTheory.HasFiniteIntegral f (μ + ν))
:
@[simp]
theorem
MeasureTheory.hasFiniteIntegral_add_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
:
theorem
MeasureTheory.HasFiniteIntegral.smul_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : MeasureTheory.HasFiniteIntegral f μ)
{c : ENNReal}
(hc : c ≠ ⊤)
:
MeasureTheory.HasFiniteIntegral f (c • μ)
@[simp]
theorem
MeasureTheory.hasFiniteIntegral_zero_measure
{α : Type u_1}
{β : Type u_2}
[NormedAddCommGroup β]
{m : MeasurableSpace α}
(f : α → β)
:
@[simp]
theorem
MeasureTheory.hasFiniteIntegral_zero
(α : Type u_1)
(β : Type u_2)
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup β]
:
MeasureTheory.HasFiniteIntegral (fun (x : α) => 0) μ
theorem
MeasureTheory.HasFiniteIntegral.neg
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hfi : MeasureTheory.HasFiniteIntegral f μ)
:
@[simp]
theorem
MeasureTheory.hasFiniteIntegral_neg_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
:
theorem
MeasureTheory.HasFiniteIntegral.norm
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hfi : MeasureTheory.HasFiniteIntegral f μ)
:
MeasureTheory.HasFiniteIntegral (fun (a : α) => ‖f a‖) μ
theorem
MeasureTheory.hasFiniteIntegral_norm_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α → β)
:
MeasureTheory.HasFiniteIntegral (fun (a : α) => ‖f a‖) μ ↔ MeasureTheory.HasFiniteIntegral f μ
theorem
MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
(hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤)
:
MeasureTheory.HasFiniteIntegral (fun (x : α) => (f x).toReal) μ
theorem
MeasureTheory.isFiniteMeasure_withDensity_ofReal
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hfi : MeasureTheory.HasFiniteIntegral f μ)
:
MeasureTheory.IsFiniteMeasure (μ.withDensity fun (x : α) => ENNReal.ofReal (f x))
theorem
MeasureTheory.all_ae_ofReal_F_le_bound
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{F : ℕ → α → β}
{bound : α → ℝ}
(h : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a)
(n : ℕ)
:
∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
theorem
MeasureTheory.all_ae_tendsto_ofReal_norm
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{F : ℕ → α → β}
{f : α → β}
(h : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a)))
:
∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => ENNReal.ofReal ‖F n a‖) Filter.atTop (nhds (ENNReal.ofReal ‖f a‖))
theorem
MeasureTheory.all_ae_ofReal_f_le_bound
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{F : ℕ → α → β}
{f : α → β}
{bound : α → ℝ}
(h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a)
(h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a)))
:
∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
theorem
MeasureTheory.hasFiniteIntegral_of_dominated_convergence
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{F : ℕ → α → β}
{f : α → β}
{bound : α → ℝ}
(bound_hasFiniteIntegral : MeasureTheory.HasFiniteIntegral bound μ)
(h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a)
(h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a)))
:
theorem
MeasureTheory.tendsto_lintegral_norm_of_dominated_convergence
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{F : ℕ → α → β}
{f : α → β}
{bound : α → ℝ}
(F_measurable : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) μ)
(bound_hasFiniteIntegral : MeasureTheory.HasFiniteIntegral bound μ)
(h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a)
(h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n a) Filter.atTop (nhds (f a)))
:
Filter.Tendsto (fun (n : ℕ) => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) Filter.atTop (nhds 0)
Lemmas used for defining the positive part of an L¹ function
theorem
MeasureTheory.HasFiniteIntegral.max_zero
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hf : MeasureTheory.HasFiniteIntegral f μ)
:
MeasureTheory.HasFiniteIntegral (fun (a : α) => max (f a) 0) μ
theorem
MeasureTheory.HasFiniteIntegral.min_zero
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hf : MeasureTheory.HasFiniteIntegral f μ)
:
MeasureTheory.HasFiniteIntegral (fun (a : α) => min (f a) 0) μ
theorem
MeasureTheory.HasFiniteIntegral.smul
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_5}
[NormedAddCommGroup 𝕜]
[SMulZeroClass 𝕜 β]
[BoundedSMul 𝕜 β]
(c : 𝕜)
{f : α → β}
:
MeasureTheory.HasFiniteIntegral f μ → MeasureTheory.HasFiniteIntegral (c • f) μ
theorem
MeasureTheory.hasFiniteIntegral_smul_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[MulActionWithZero 𝕜 β]
[BoundedSMul 𝕜 β]
{c : 𝕜}
(hc : IsUnit c)
(f : α → β)
:
theorem
MeasureTheory.HasFiniteIntegral.const_mul
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[NormedRing 𝕜]
{f : α → 𝕜}
(h : MeasureTheory.HasFiniteIntegral f μ)
(c : 𝕜)
:
MeasureTheory.HasFiniteIntegral (fun (x : α) => c * f x) μ
theorem
MeasureTheory.HasFiniteIntegral.mul_const
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[NormedRing 𝕜]
{f : α → 𝕜}
(h : MeasureTheory.HasFiniteIntegral f μ)
(c : 𝕜)
:
MeasureTheory.HasFiniteIntegral (fun (x : α) => f x * c) μ
The predicate Integrable #
def
MeasureTheory.Integrable
{β : Type u_2}
[NormedAddCommGroup β]
{α : Type u_5}
:
{x : MeasurableSpace α} → (α → β) → autoParam (MeasureTheory.Measure α) _auto✝ → Prop
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
theorem
MeasureTheory.memℒp_one_iff_integrable
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
:
MeasureTheory.Memℒp f 1 μ ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.Integrable.aestronglyMeasurable
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.Integrable f μ)
:
theorem
MeasureTheory.Integrable.aemeasurable
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[MeasurableSpace β]
[BorelSpace β]
{f : α → β}
(hf : MeasureTheory.Integrable f μ)
:
AEMeasurable f μ
theorem
MeasureTheory.Integrable.hasFiniteIntegral
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.Integrable f μ)
:
theorem
MeasureTheory.Integrable.mono
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[NormedAddCommGroup γ]
{f : α → β}
{g : α → γ}
(hg : MeasureTheory.Integrable g μ)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖)
:
theorem
MeasureTheory.Integrable.mono'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → ℝ}
(hg : MeasureTheory.Integrable g μ)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a)
:
theorem
MeasureTheory.Integrable.congr'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[NormedAddCommGroup γ]
{f : α → β}
{g : α → γ}
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖)
:
theorem
MeasureTheory.integrable_congr'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[NormedAddCommGroup γ]
{f : α → β}
{g : α → γ}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖)
:
theorem
MeasureTheory.Integrable.congr
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → β}
(hf : MeasureTheory.Integrable f μ)
(h : f =ᵐ[μ] g)
:
theorem
MeasureTheory.integrable_congr
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → β}
(h : f =ᵐ[μ] g)
:
theorem
MeasureTheory.integrable_const_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{c : β}
:
@[simp]
theorem
MeasureTheory.integrable_const
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[MeasureTheory.IsFiniteMeasure μ]
(c : β)
:
MeasureTheory.Integrable (fun (x : α) => c) μ
@[simp]
theorem
MeasureTheory.Integrable.of_finite
{α : Type u_1}
{β : Type u_2}
[NormedAddCommGroup β]
[Finite α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(f : α → β)
:
MeasureTheory.Integrable (fun (a : α) => f a) μ
@[deprecated MeasureTheory.Integrable.of_finite]
theorem
MeasureTheory.integrable_of_fintype
{α : Type u_1}
{β : Type u_2}
[NormedAddCommGroup β]
[Finite α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(f : α → β)
:
MeasureTheory.Integrable (fun (a : α) => f a) μ
Alias of MeasureTheory.Integrable.of_finite.
theorem
MeasureTheory.Memℒp.integrable_norm_rpow
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{p : ENNReal}
(hf : MeasureTheory.Memℒp f p μ)
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
:
MeasureTheory.Integrable (fun (x : α) => ‖f x‖ ^ p.toReal) μ
theorem
MeasureTheory.Memℒp.integrable_norm_rpow'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[MeasureTheory.IsFiniteMeasure μ]
{f : α → β}
{p : ENNReal}
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Integrable (fun (x : α) => ‖f x‖ ^ p.toReal) μ
theorem
MeasureTheory.Integrable.mono_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : MeasureTheory.Integrable f ν)
(hμ : μ ≤ ν)
:
theorem
MeasureTheory.Integrable.of_measure_le_smul
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{μ' : MeasureTheory.Measure α}
(c : ENNReal)
(hc : c ≠ ⊤)
(hμ'_le : μ' ≤ c • μ)
{f : α → β}
(hf : MeasureTheory.Integrable f μ)
:
theorem
MeasureTheory.Integrable.add_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hμ : MeasureTheory.Integrable f μ)
(hν : MeasureTheory.Integrable f ν)
:
MeasureTheory.Integrable f (μ + ν)
theorem
MeasureTheory.Integrable.left_of_add_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : MeasureTheory.Integrable f (μ + ν))
:
theorem
MeasureTheory.Integrable.right_of_add_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : MeasureTheory.Integrable f (μ + ν))
:
@[simp]
theorem
MeasureTheory.integrable_add_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
:
MeasureTheory.Integrable f (μ + ν) ↔ MeasureTheory.Integrable f μ ∧ MeasureTheory.Integrable f ν
@[simp]
theorem
MeasureTheory.integrable_zero_measure
{α : Type u_1}
{β : Type u_2}
[NormedAddCommGroup β]
:
∀ {x : MeasurableSpace α} {f : α → β}, MeasureTheory.Integrable f 0
theorem
MeasureTheory.integrable_finset_sum_measure
{α : Type u_1}
{β : Type u_2}
[NormedAddCommGroup β]
{ι : Type u_5}
{m : MeasurableSpace α}
{f : α → β}
{μ : ι → MeasureTheory.Measure α}
{s : Finset ι}
:
MeasureTheory.Integrable f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, MeasureTheory.Integrable f (μ i)
theorem
MeasureTheory.Integrable.smul_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : MeasureTheory.Integrable f μ)
{c : ENNReal}
(hc : c ≠ ⊤)
:
MeasureTheory.Integrable f (c • μ)
theorem
MeasureTheory.Integrable.smul_measure_nnreal
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : MeasureTheory.Integrable f μ)
{c : NNReal}
:
MeasureTheory.Integrable f (c • μ)
theorem
MeasureTheory.integrable_smul_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{c : ENNReal}
(h₁ : c ≠ 0)
(h₂ : c ≠ ⊤)
:
MeasureTheory.Integrable f (c • μ) ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.integrable_inv_smul_measure
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{c : ENNReal}
(h₁ : c ≠ 0)
(h₂ : c ≠ ⊤)
:
MeasureTheory.Integrable f (c⁻¹ • μ) ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.Integrable.to_average
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(h : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable f ((μ Set.univ)⁻¹ • μ)
theorem
MeasureTheory.integrable_average
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[MeasureTheory.IsFiniteMeasure μ]
{f : α → β}
:
MeasureTheory.Integrable f ((μ Set.univ)⁻¹ • μ) ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.integrable_map_measure
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasurableSpace δ]
[NormedAddCommGroup β]
{f : α → δ}
{g : δ → β}
(hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ))
(hf : AEMeasurable f μ)
:
MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Integrable (g ∘ f) μ
theorem
MeasureTheory.Integrable.comp_aemeasurable
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasurableSpace δ]
[NormedAddCommGroup β]
{f : α → δ}
{g : δ → β}
(hg : MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ))
(hf : AEMeasurable f μ)
:
MeasureTheory.Integrable (g ∘ f) μ
theorem
MeasureTheory.Integrable.comp_measurable
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasurableSpace δ]
[NormedAddCommGroup β]
{f : α → δ}
{g : δ → β}
(hg : MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ))
(hf : Measurable f)
:
MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[MeasurableSpace δ]
[NormedAddCommGroup β]
(f : α ≃ᵐ δ)
(g : δ → β)
:
MeasureTheory.Integrable g (MeasureTheory.Measure.map (⇑f) μ) ↔ MeasureTheory.Integrable (g ∘ ⇑f) μ
theorem
MeasureTheory.MeasurePreserving.integrable_comp
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasurableSpace δ]
[NormedAddCommGroup β]
{ν : MeasureTheory.Measure δ}
{g : δ → β}
{f : α → δ}
(hf : MeasureTheory.MeasurePreserving f μ ν)
(hg : MeasureTheory.AEStronglyMeasurable g ν)
:
MeasureTheory.Integrable (g ∘ f) μ ↔ MeasureTheory.Integrable g ν
theorem
MeasureTheory.MeasurePreserving.integrable_comp_emb
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasurableSpace δ]
[NormedAddCommGroup β]
{f : α → δ}
{ν : MeasureTheory.Measure δ}
(h₁ : MeasureTheory.MeasurePreserving f μ ν)
(h₂ : MeasurableEmbedding f)
{g : δ → β}
:
MeasureTheory.Integrable (g ∘ f) μ ↔ MeasureTheory.Integrable g ν
theorem
MeasureTheory.lintegral_edist_lt_top
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → β}
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
@[simp]
theorem
MeasureTheory.integrable_zero
(α : Type u_1)
(β : Type u_2)
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[NormedAddCommGroup β]
:
MeasureTheory.Integrable (fun (x : α) => 0) μ
theorem
MeasureTheory.Integrable.add'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → β}
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.HasFiniteIntegral (f + g) μ
theorem
MeasureTheory.Integrable.add
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → β}
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.Integrable (f + g) μ
theorem
MeasureTheory.integrable_finset_sum'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{ι : Type u_5}
(s : Finset ι)
{f : ι → α → β}
(hf : ∀ i ∈ s, MeasureTheory.Integrable (f i) μ)
:
MeasureTheory.Integrable (∑ i ∈ s, f i) μ
theorem
MeasureTheory.integrable_finset_sum
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{ι : Type u_5}
(s : Finset ι)
{f : ι → α → β}
(hf : ∀ i ∈ s, MeasureTheory.Integrable (f i) μ)
:
MeasureTheory.Integrable (fun (a : α) => ∑ i ∈ s, f i a) μ
theorem
MeasureTheory.Integrable.neg
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.Integrable f μ)
:
@[simp]
theorem
MeasureTheory.integrable_neg_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
:
@[simp]
theorem
MeasureTheory.integrable_add_iff_integrable_right
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → β}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (f + g) μ ↔ MeasureTheory.Integrable g μ
@[simp]
theorem
MeasureTheory.integrable_add_iff_integrable_left
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → β}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (g + f) μ ↔ MeasureTheory.Integrable g μ
theorem
MeasureTheory.integrable_left_of_integrable_add_of_nonneg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
{g : α → ℝ}
(h_meas : MeasureTheory.AEStronglyMeasurable f μ)
(hf : 0 ≤ᵐ[μ] f)
(hg : 0 ≤ᵐ[μ] g)
(h_int : MeasureTheory.Integrable (f + g) μ)
:
theorem
MeasureTheory.integrable_right_of_integrable_add_of_nonneg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
{g : α → ℝ}
(h_meas : MeasureTheory.AEStronglyMeasurable f μ)
(hf : 0 ≤ᵐ[μ] f)
(hg : 0 ≤ᵐ[μ] g)
(h_int : MeasureTheory.Integrable (f + g) μ)
:
theorem
MeasureTheory.integrable_add_iff_of_nonneg
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
{g : α → ℝ}
(h_meas : MeasureTheory.AEStronglyMeasurable f μ)
(hf : 0 ≤ᵐ[μ] f)
(hg : 0 ≤ᵐ[μ] g)
:
MeasureTheory.Integrable (f + g) μ ↔ MeasureTheory.Integrable f μ ∧ MeasureTheory.Integrable g μ
theorem
MeasureTheory.integrable_add_iff_of_nonpos
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
{g : α → ℝ}
(h_meas : MeasureTheory.AEStronglyMeasurable f μ)
(hf : f ≤ᵐ[μ] 0)
(hg : g ≤ᵐ[μ] 0)
:
MeasureTheory.Integrable (f + g) μ ↔ MeasureTheory.Integrable f μ ∧ MeasureTheory.Integrable g μ
@[simp]
theorem
MeasureTheory.integrable_add_const_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[MeasureTheory.IsFiniteMeasure μ]
{f : α → β}
{c : β}
:
MeasureTheory.Integrable (fun (x : α) => f x + c) μ ↔ MeasureTheory.Integrable f μ
@[simp]
theorem
MeasureTheory.integrable_const_add_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[MeasureTheory.IsFiniteMeasure μ]
{f : α → β}
{c : β}
:
MeasureTheory.Integrable (fun (x : α) => c + f x) μ ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.Integrable.sub
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
{g : α → β}
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.Integrable (f - g) μ
theorem
MeasureTheory.Integrable.norm
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (a : α) => ‖f a‖) μ
theorem
MeasureTheory.Integrable.inf
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_5}
[NormedLatticeAddCommGroup β]
{f : α → β}
{g : α → β}
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.Integrable (f ⊓ g) μ
theorem
MeasureTheory.Integrable.sup
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_5}
[NormedLatticeAddCommGroup β]
{f : α → β}
{g : α → β}
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.Integrable (f ⊔ g) μ
theorem
MeasureTheory.Integrable.abs
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_5}
[NormedLatticeAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (a : α) => |f a|) μ
theorem
MeasureTheory.Integrable.bdd_mul
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{F : Type u_5}
[NormedDivisionRing F]
{f : α → F}
{g : α → F}
(hint : MeasureTheory.Integrable g μ)
(hm : MeasureTheory.AEStronglyMeasurable f μ)
(hfbdd : ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C)
:
MeasureTheory.Integrable (fun (x : α) => f x * g x) μ
theorem
MeasureTheory.Integrable.essSup_smul
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_5}
[NormedField 𝕜]
[NormedSpace 𝕜 β]
{f : α → β}
(hf : MeasureTheory.Integrable f μ)
{g : α → 𝕜}
(g_aestronglyMeasurable : MeasureTheory.AEStronglyMeasurable g μ)
(ess_sup_g : essSup (fun (x : α) => ↑‖g x‖₊) μ ≠ ⊤)
:
MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[Module 𝕜 β]
[BoundedSMul 𝕜 β]
{f : α → 𝕜}
(hf : MeasureTheory.Integrable f μ)
{g : α → β}
(g_aestronglyMeasurable : MeasureTheory.AEStronglyMeasurable g μ)
(ess_sup_g : essSup (fun (x : α) => ↑‖g x‖₊) μ ≠ ⊤)
:
MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.Integrable (fun (a : α) => ‖f a‖) μ ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.integrable_of_norm_sub_le
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f₀ : α → β}
{f₁ : α → β}
{g : α → ℝ}
(hf₁_m : MeasureTheory.AEStronglyMeasurable f₁ μ)
(hf₀_i : MeasureTheory.Integrable f₀ μ)
(hg_i : MeasureTheory.Integrable g μ)
(h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a)
:
theorem
MeasureTheory.Integrable.prod_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[NormedAddCommGroup γ]
{f : α → β}
{g : α → γ}
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.Integrable (fun (x : α) => (f x, g x)) μ
theorem
MeasureTheory.Memℒp.integrable
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{q : ENNReal}
(hq1 : 1 ≤ q)
{f : α → β}
[MeasureTheory.IsFiniteMeasure μ]
(hfq : MeasureTheory.Memℒp f q μ)
:
theorem
MeasureTheory.Integrable.measure_norm_ge_lt_top
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hf : MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hf : MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hf : MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hf : MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[NormedAddCommGroup γ]
{K : NNReal}
{K' : NNReal}
{f : α → β}
{g : β → γ}
(hg : LipschitzWith K g)
(hg' : AntilipschitzWith K' g)
(g0 : g 0 = 0)
:
MeasureTheory.Integrable (g ∘ f) μ ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.Integrable.real_toNNReal
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (x : α) => ↑(f x).toNNReal) μ
theorem
MeasureTheory.ofReal_toReal_ae_eq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
(hf : ∀ᵐ (x : α) ∂μ, f x < ⊤)
:
(fun (x : α) => ENNReal.ofReal (f x).toReal) =ᵐ[μ] f
theorem
MeasureTheory.coe_toNNReal_ae_eq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
(hf : ∀ᵐ (x : α) ∂μ, f x < ⊤)
:
theorem
MeasureTheory.hasFiniteIntegral_count_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup β]
[MeasurableSingletonClass α]
{f : α → β}
:
MeasureTheory.HasFiniteIntegral f MeasureTheory.Measure.count ↔ Summable fun (x : α) => ‖f x‖
A function has finite integral for the counting measure iff its norm is summable.
theorem
MeasureTheory.integrable_count_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup β]
[MeasurableSingletonClass α]
{f : α → β}
:
MeasureTheory.Integrable f MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → NNReal}
(hf : Measurable f)
{g : α → E}
:
MeasureTheory.Integrable g (μ.withDensity fun (x : α) => ↑(f x)) ↔ MeasureTheory.Integrable (fun (x : α) => ↑(f x) • g x) μ
theorem
MeasureTheory.integrable_withDensity_iff_integrable_smul
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → NNReal}
(hf : Measurable f)
{g : α → E}
:
MeasureTheory.Integrable g (μ.withDensity fun (x : α) => ↑(f x)) ↔ MeasureTheory.Integrable (fun (x : α) => f x • g x) μ
theorem
MeasureTheory.integrable_withDensity_iff_integrable_smul'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → ENNReal}
(hf : Measurable f)
(hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤)
{g : α → E}
:
MeasureTheory.Integrable g (μ.withDensity f) ↔ MeasureTheory.Integrable (fun (x : α) => (f x).toReal • g x) μ
theorem
MeasureTheory.integrable_withDensity_iff_integrable_coe_smul₀
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → NNReal}
(hf : AEMeasurable f μ)
{g : α → E}
:
MeasureTheory.Integrable g (μ.withDensity fun (x : α) => ↑(f x)) ↔ MeasureTheory.Integrable (fun (x : α) => ↑(f x) • g x) μ
theorem
MeasureTheory.integrable_withDensity_iff_integrable_smul₀
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → NNReal}
(hf : AEMeasurable f μ)
{g : α → E}
:
MeasureTheory.Integrable g (μ.withDensity fun (x : α) => ↑(f x)) ↔ MeasureTheory.Integrable (fun (x : α) => f x • g x) μ
theorem
MeasureTheory.integrable_withDensity_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
(hf : Measurable f)
(hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤)
{g : α → ℝ}
:
MeasureTheory.Integrable g (μ.withDensity f) ↔ MeasureTheory.Integrable (fun (x : α) => g x * (f x).toReal) μ
theorem
MeasureTheory.memℒ1_smul_of_L1_withDensity
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → NNReal}
(f_meas : Measurable f)
(u : ↥(MeasureTheory.Lp E 1 (μ.withDensity fun (x : α) => ↑(f x))))
:
MeasureTheory.Memℒp (fun (x : α) => f x • ↑↑u x) 1 μ
noncomputable def
MeasureTheory.withDensitySMulLI
{α : Type u_1}
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → NNReal}
(f_meas : Measurable f)
:
↥(MeasureTheory.Lp E 1 (μ.withDensity fun (x : α) => ↑(f x))) →ₗᵢ[ℝ] ↥(MeasureTheory.Lp E 1 μ)
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 α}
(μ : MeasureTheory.Measure α)
{E : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : α → NNReal}
(f_meas : Measurable f)
(u : ↥(MeasureTheory.Lp E 1 (μ.withDensity fun (x : α) => ↑(f x))))
:
(MeasureTheory.withDensitySMulLI μ f_meas) u = MeasureTheory.Memℒp.toLp (fun (x : α) => f x • ↑↑u x) ⋯
theorem
MeasureTheory.mem_ℒ1_toReal_of_lintegral_ne_top
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
(hfm : AEMeasurable f μ)
(hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤)
:
MeasureTheory.Memℒp (fun (x : α) => (f x).toReal) 1 μ
theorem
MeasureTheory.integrable_toReal_of_lintegral_ne_top
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
(hfm : AEMeasurable f μ)
(hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤)
:
MeasureTheory.Integrable (fun (x : α) => (f x).toReal) μ
Lemmas used for defining the positive part of an L¹ function #
theorem
MeasureTheory.Integrable.pos_part
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (a : α) => max (f a) 0) μ
theorem
MeasureTheory.Integrable.neg_part
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (a : α) => max (-f a) 0) μ
theorem
MeasureTheory.Integrable.smul
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_5}
[NormedAddCommGroup 𝕜]
[SMulZeroClass 𝕜 β]
[BoundedSMul 𝕜 β]
(c : 𝕜)
{f : α → β}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (c • f) μ
theorem
IsUnit.integrable_smul_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_5}
[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 α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_5}
[NormedDivisionRing 𝕜]
[Module 𝕜 β]
[BoundedSMul 𝕜 β]
{c : 𝕜}
(hc : c ≠ 0)
(f : α → β)
:
MeasureTheory.Integrable (c • f) μ ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.Integrable.smul_of_top_right
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[Module 𝕜 β]
[BoundedSMul 𝕜 β]
{f : α → β}
{φ : α → 𝕜}
(hf : MeasureTheory.Integrable f μ)
(hφ : MeasureTheory.Memℒp φ ⊤ μ)
:
MeasureTheory.Integrable (φ • f) μ
theorem
MeasureTheory.Integrable.smul_of_top_left
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[Module 𝕜 β]
[BoundedSMul 𝕜 β]
{f : α → β}
{φ : α → 𝕜}
(hφ : MeasureTheory.Integrable φ μ)
(hf : MeasureTheory.Memℒp f ⊤ μ)
:
MeasureTheory.Integrable (φ • f) μ
theorem
MeasureTheory.Integrable.smul_const
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[Module 𝕜 β]
[BoundedSMul 𝕜 β]
{f : α → 𝕜}
(hf : MeasureTheory.Integrable f μ)
(c : β)
:
MeasureTheory.Integrable (fun (x : α) => f x • c) μ
theorem
MeasureTheory.integrable_smul_const
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{f : α → 𝕜}
{c : E}
(hc : c ≠ 0)
:
MeasureTheory.Integrable (fun (x : α) => f x • c) μ ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.Integrable.const_mul
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[NormedRing 𝕜]
{f : α → 𝕜}
(h : MeasureTheory.Integrable f μ)
(c : 𝕜)
:
MeasureTheory.Integrable (fun (x : α) => c * f x) μ
theorem
MeasureTheory.Integrable.const_mul'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[NormedRing 𝕜]
{f : α → 𝕜}
(h : MeasureTheory.Integrable f μ)
(c : 𝕜)
:
MeasureTheory.Integrable ((fun (x : α) => c) * f) μ
theorem
MeasureTheory.Integrable.mul_const
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[NormedRing 𝕜]
{f : α → 𝕜}
(h : MeasureTheory.Integrable f μ)
(c : 𝕜)
:
MeasureTheory.Integrable (fun (x : α) => f x * c) μ
theorem
MeasureTheory.Integrable.mul_const'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[NormedRing 𝕜]
{f : α → 𝕜}
(h : MeasureTheory.Integrable f μ)
(c : 𝕜)
:
MeasureTheory.Integrable (f * fun (x : α) => c) μ
theorem
MeasureTheory.integrable_const_mul_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[NormedRing 𝕜]
{c : 𝕜}
(hc : IsUnit c)
(f : α → 𝕜)
:
MeasureTheory.Integrable (fun (x : α) => c * f x) μ ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.integrable_mul_const_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[NormedRing 𝕜]
{c : 𝕜}
(hc : IsUnit c)
(f : α → 𝕜)
:
MeasureTheory.Integrable (fun (x : α) => f x * c) μ ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.Integrable.bdd_mul'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[NormedRing 𝕜]
{f : α → 𝕜}
{g : α → 𝕜}
{c : ℝ}
(hg : MeasureTheory.Integrable g μ)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c)
:
MeasureTheory.Integrable (fun (x : α) => f x * g x) μ
theorem
MeasureTheory.Integrable.div_const
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[NormedDivisionRing 𝕜]
{f : α → 𝕜}
(h : MeasureTheory.Integrable f μ)
(c : 𝕜)
:
MeasureTheory.Integrable (fun (x : α) => f x / c) μ
theorem
MeasureTheory.Integrable.ofReal
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[RCLike 𝕜]
{f : α → ℝ}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (x : α) => ↑(f x)) μ
theorem
MeasureTheory.Integrable.re_im_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[RCLike 𝕜]
{f : α → 𝕜}
:
MeasureTheory.Integrable (fun (x : α) => RCLike.re (f x)) μ ∧ MeasureTheory.Integrable (fun (x : α) => RCLike.im (f x)) μ ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.Integrable.re
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[RCLike 𝕜]
{f : α → 𝕜}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (x : α) => RCLike.re (f x)) μ
theorem
MeasureTheory.Integrable.im
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{𝕜 : Type u_5}
[RCLike 𝕜]
{f : α → 𝕜}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (x : α) => RCLike.im (f x)) μ
theorem
MeasureTheory.Integrable.trim
{α : Type u_1}
{m : MeasurableSpace α}
{H : Type u_5}
[NormedAddCommGroup H]
{m0 : MeasurableSpace α}
{μ' : MeasureTheory.Measure α}
{f : α → H}
(hm : m ≤ m0)
(hf_int : MeasureTheory.Integrable f μ')
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.Integrable f (μ'.trim hm)
theorem
MeasureTheory.integrable_of_integrable_trim
{α : Type u_1}
{m : MeasurableSpace α}
{H : Type u_5}
[NormedAddCommGroup H]
{m0 : MeasurableSpace α}
{μ' : MeasureTheory.Measure α}
{f : α → H}
(hm : m ≤ m0)
(hf_int : MeasureTheory.Integrable f (μ'.trim hm))
:
theorem
MeasureTheory.integrable_of_forall_fin_meas_le'
{α : Type u_1}
{m : MeasurableSpace α}
{E : Type u_5}
{m0 : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
[MeasureTheory.SigmaFinite (μ.trim hm)]
(C : ENNReal)
(hC : C < ⊤)
{f : α → E}
(hf_meas : MeasureTheory.AEStronglyMeasurable f μ)
(hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, ↑‖f x‖₊ ∂μ ≤ C)
:
theorem
MeasureTheory.integrable_of_forall_fin_meas_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
[MeasureTheory.SigmaFinite μ]
(C : ENNReal)
(hC : C < ⊤)
{f : α → E}
(hf_meas : MeasureTheory.AEStronglyMeasurable f μ)
(hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, ↑‖f x‖₊ ∂μ ≤ C)
:
The predicate Integrable on measurable functions modulo a.e.-equality #
def
MeasureTheory.AEEqFun.Integrable
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α →ₘ[μ] β)
:
A class of almost everywhere equal functions is Integrable if its function representative
is integrable.
Equations
- f.Integrable = MeasureTheory.Integrable (↑f) μ
Instances For
theorem
MeasureTheory.AEEqFun.integrable_mk
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
(MeasureTheory.AEEqFun.mk f hf).Integrable ↔ MeasureTheory.Integrable f μ
theorem
MeasureTheory.AEEqFun.integrable_coeFn
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α →ₘ[μ] β}
:
MeasureTheory.Integrable (↑f) μ ↔ f.Integrable
theorem
MeasureTheory.AEEqFun.integrable_zero
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
:
theorem
MeasureTheory.AEEqFun.Integrable.neg
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α →ₘ[μ] β}
:
f.Integrable → (-f).Integrable
theorem
MeasureTheory.AEEqFun.integrable_iff_mem_L1
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α →ₘ[μ] β}
:
f.Integrable ↔ f ∈ MeasureTheory.Lp β 1 μ
theorem
MeasureTheory.AEEqFun.Integrable.add
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α →ₘ[μ] β}
{g : α →ₘ[μ] β}
:
f.Integrable → g.Integrable → (f + g).Integrable
theorem
MeasureTheory.AEEqFun.Integrable.sub
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α →ₘ[μ] β}
{g : α →ₘ[μ] β}
(hf : f.Integrable)
(hg : g.Integrable)
:
(f - g).Integrable
theorem
MeasureTheory.AEEqFun.Integrable.smul
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[Module 𝕜 β]
[BoundedSMul 𝕜 β]
{c : 𝕜}
{f : α →ₘ[μ] β}
:
f.Integrable → (c • f).Integrable
theorem
MeasureTheory.L1.integrable_coeFn
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : ↥(MeasureTheory.Lp β 1 μ))
:
MeasureTheory.Integrable (↑↑f) μ
theorem
MeasureTheory.L1.hasFiniteIntegral_coeFn
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : ↥(MeasureTheory.Lp β 1 μ))
:
MeasureTheory.HasFiniteIntegral (↑↑f) μ
theorem
MeasureTheory.L1.stronglyMeasurable_coeFn
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : ↥(MeasureTheory.Lp β 1 μ))
:
theorem
MeasureTheory.L1.measurable_coeFn
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[MeasurableSpace β]
[BorelSpace β]
(f : ↥(MeasureTheory.Lp β 1 μ))
:
Measurable ↑↑f
theorem
MeasureTheory.L1.aestronglyMeasurable_coeFn
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : ↥(MeasureTheory.Lp β 1 μ))
:
theorem
MeasureTheory.L1.aemeasurable_coeFn
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
[MeasurableSpace β]
[BorelSpace β]
(f : ↥(MeasureTheory.Lp β 1 μ))
:
AEMeasurable (↑↑f) μ
theorem
MeasureTheory.L1.edist_def
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : ↥(MeasureTheory.Lp β 1 μ))
(g : ↥(MeasureTheory.Lp β 1 μ))
:
theorem
MeasureTheory.L1.dist_def
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : ↥(MeasureTheory.Lp β 1 μ))
(g : ↥(MeasureTheory.Lp β 1 μ))
:
theorem
MeasureTheory.L1.norm_def
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : ↥(MeasureTheory.Lp β 1 μ))
:
theorem
MeasureTheory.L1.norm_sub_eq_lintegral
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : ↥(MeasureTheory.Lp β 1 μ))
(g : ↥(MeasureTheory.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
MeasureTheory.L1.ofReal_norm_eq_lintegral
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : ↥(MeasureTheory.Lp β 1 μ))
:
theorem
MeasureTheory.L1.ofReal_norm_sub_eq_lintegral
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : ↥(MeasureTheory.Lp β 1 μ))
(g : ↥(MeasureTheory.Lp β 1 μ))
:
Computing the norm of a difference between two L¹-functions. Note that this is not a
special case of ofReal_norm_eq_lintegral since (f - g) x and f x - g x are not equal
(but only a.e.-equal).
def
MeasureTheory.Integrable.toL1
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α → β)
(hf : MeasureTheory.Integrable f μ)
:
↥(MeasureTheory.Lp β 1 μ)
Construct the equivalence class [f] of an integrable function f, as a member of the
space L1 β 1 μ.
Equations
Instances For
@[simp]
theorem
MeasureTheory.Integrable.toL1_coeFn
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : ↥(MeasureTheory.Lp β 1 μ))
(hf : MeasureTheory.Integrable (↑↑f) μ)
:
MeasureTheory.Integrable.toL1 (↑↑f) hf = f
theorem
MeasureTheory.Integrable.coeFn_toL1
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.Integrable f μ)
:
↑↑(MeasureTheory.Integrable.toL1 f hf) =ᵐ[μ] f
@[simp]
theorem
MeasureTheory.Integrable.toL1_zero
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(h : MeasureTheory.Integrable 0 μ)
:
@[simp]
theorem
MeasureTheory.Integrable.toL1_eq_mk
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α → β)
(hf : MeasureTheory.Integrable f μ)
:
↑(MeasureTheory.Integrable.toL1 f hf) = MeasureTheory.AEEqFun.mk f ⋯
@[simp]
theorem
MeasureTheory.Integrable.toL1_eq_toL1_iff
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α → β)
(g : α → β)
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.Integrable.toL1 f hf = MeasureTheory.Integrable.toL1 g hg ↔ f =ᵐ[μ] g
theorem
MeasureTheory.Integrable.toL1_add
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α → β)
(g : α → β)
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.Integrable.toL1 (f + g) ⋯ = MeasureTheory.Integrable.toL1 f hf + MeasureTheory.Integrable.toL1 g hg
theorem
MeasureTheory.Integrable.toL1_neg
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α → β)
(hf : MeasureTheory.Integrable f μ)
:
theorem
MeasureTheory.Integrable.toL1_sub
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α → β)
(g : α → β)
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
MeasureTheory.Integrable.toL1 (f - g) ⋯ = MeasureTheory.Integrable.toL1 f hf - MeasureTheory.Integrable.toL1 g hg
theorem
MeasureTheory.Integrable.norm_toL1
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α → β)
(hf : MeasureTheory.Integrable f μ)
:
‖MeasureTheory.Integrable.toL1 f hf‖ = (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal
theorem
MeasureTheory.Integrable.nnnorm_toL1
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{f : α → β}
(hf : MeasureTheory.Integrable f μ)
:
theorem
MeasureTheory.Integrable.norm_toL1_eq_lintegral_norm
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α → β)
(hf : MeasureTheory.Integrable f μ)
:
‖MeasureTheory.Integrable.toL1 f hf‖ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
@[simp]
theorem
MeasureTheory.Integrable.edist_toL1_toL1
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α → β)
(g : α → β)
(hf : MeasureTheory.Integrable f μ)
(hg : MeasureTheory.Integrable g μ)
:
edist (MeasureTheory.Integrable.toL1 f hf) (MeasureTheory.Integrable.toL1 g hg) = ∫⁻ (a : α), edist (f a) (g a) ∂μ
@[simp]
theorem
MeasureTheory.Integrable.edist_toL1_zero
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
(f : α → β)
(hf : MeasureTheory.Integrable f μ)
:
edist (MeasureTheory.Integrable.toL1 f hf) 0 = ∫⁻ (a : α), edist (f a) 0 ∂μ
theorem
MeasureTheory.Integrable.toL1_smul
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[Module 𝕜 β]
[BoundedSMul 𝕜 β]
(f : α → β)
(hf : MeasureTheory.Integrable f μ)
(k : 𝕜)
:
MeasureTheory.Integrable.toL1 (fun (a : α) => k • f a) ⋯ = k • MeasureTheory.Integrable.toL1 f hf
theorem
MeasureTheory.Integrable.toL1_smul'
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{𝕜 : Type u_5}
[NormedRing 𝕜]
[Module 𝕜 β]
[BoundedSMul 𝕜 β]
(f : α → β)
(hf : MeasureTheory.Integrable f μ)
(k : 𝕜)
:
MeasureTheory.Integrable.toL1 (k • f) ⋯ = k • MeasureTheory.Integrable.toL1 f hf
theorem
MeasureTheory.HasFiniteIntegral.restrict
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
{f : α → E}
(h : MeasureTheory.HasFiniteIntegral f μ)
{s : Set α}
:
MeasureTheory.HasFiniteIntegral f (μ.restrict s)
theorem
MeasureTheory.Integrable.restrict
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
{f : α → E}
(f_intble : MeasureTheory.Integrable f μ)
{s : Set α}
:
MeasureTheory.Integrable f (μ.restrict s)
theorem
ContinuousLinearMap.integrable_comp
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
{𝕜 : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
{H : Type u_7}
[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_5}
[NormedAddCommGroup E]
{𝕜 : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
{H : Type u_7}
[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_5}
[NormedAddCommGroup E]
{𝕜 : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
{H : Type u_7}
[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 α}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
[NormedAddCommGroup E]
{𝕜 : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
{H : Type u_7}
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{φ : α → H →L[𝕜] E}
(φ_int : MeasureTheory.Integrable φ μ)
(v : H)
:
MeasureTheory.Integrable (fun (a : α) => (φ a) v) μ
theorem
MeasureTheory.Integrable.fst
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
{F : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : α → E × F}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (x : α) => (f x).1) μ
theorem
MeasureTheory.Integrable.snd
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
{F : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : α → E × F}
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (x : α) => (f x).2) μ
theorem
MeasureTheory.integrable_prod
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_5}
{F : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{f : α → E × F}
:
MeasureTheory.Integrable f μ ↔ MeasureTheory.Integrable (fun (x : α) => (f x).1) μ ∧ MeasureTheory.Integrable (fun (x : α) => (f x).2) μ