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 of L¹ space, where α is a MeasureSpace and β is a NormedAddCommGroup with a SecondCountableTopology. f : α →ₘ β is a "function" in L¹. In comments, [f] is also used to denote an L¹ function.

  ₁ can be typed as \1.

Main definitions

• Let f : α → β be a function, where α is a MeasureSpace and β a NormedAddCommGroup. Then HasFiniteIntegral f means (∫⁻ a, ‖f a‖₊) < ∞.

• If β is moreover a MeasurableSpace then f is called Integrable if f is Measurable and HasFiniteIntegral f holds.

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 : α → β) : ∫⁻ (a : α), ↑‖f a‖₊ ∂μ = ∫⁻ (a : α), edist (f a) 0 ∂μ

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 μ) : ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) ∂μ + ∫⁻ (a : α), edist (g a) (h a) ∂μ

theorem MeasureTheory.lintegral_nnnorm_zero {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] : ∫⁻ (x : α), ↑‖0‖₊ ∂μ = 0

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 : α → γ) : ∫⁻ (a : α), ↑‖f a‖₊ + ↑‖g a‖₊ ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ∂μ + ∫⁻ (a : α), ↑‖g a‖₊ ∂μ

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 μ) : ∫⁻ (a : α), ↑‖f a‖₊ + ↑‖g a‖₊ ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ∂μ + ∫⁻ (a : α), ↑‖g a‖₊ ∂μ

theorem MeasureTheory.lintegral_nnnorm_neg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α → β} : ∫⁻ (a : α), ↑‖(-f) a‖₊ ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ∂μ

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.

Equations

• MeasureTheory.HasFiniteIntegral f μ = (∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤)

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 ≤ᶠ[MeasureTheory.Measure.ae μ] 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‖) : MeasureTheory.HasFiniteIntegral f μ

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) : MeasureTheory.HasFiniteIntegral f μ

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‖) : MeasureTheory.HasFiniteIntegral g μ

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‖) : MeasureTheory.HasFiniteIntegral f μ ↔ MeasureTheory.HasFiniteIntegral g μ

theorem MeasureTheory.HasFiniteIntegral.congr {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α → β} {g : α → β} (hf : MeasureTheory.HasFiniteIntegral f μ) (h : f =ᶠ[MeasureTheory.Measure.ae μ] g) : MeasureTheory.HasFiniteIntegral g μ

theorem MeasureTheory.hasFiniteIntegral_congr {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α → β} {g : α → β} (h : f =ᶠ[MeasureTheory.Measure.ae μ] g) : MeasureTheory.HasFiniteIntegral f μ ↔ MeasureTheory.HasFiniteIntegral g μ

theorem MeasureTheory.hasFiniteIntegral_const_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {c : β} : MeasureTheory.HasFiniteIntegral (fun (x : α) => c) μ ↔ c = 0 ∨ ↑↑μ Set.univ < ⊤

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) : MeasureTheory.HasFiniteIntegral f μ

theorem MeasureTheory.HasFiniteIntegral.of_finite {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] [Finite α] [MeasureTheory.IsFiniteMeasure μ] {f : α → β} : MeasureTheory.HasFiniteIntegral 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 : α → β} : MeasureTheory.HasFiniteIntegral f μ

Alias of MeasureTheory.HasFiniteIntegral.of_finite.

theorem MeasureTheory.HasFiniteIntegral.mono_measure {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α → β} (h : MeasureTheory.HasFiniteIntegral f ν) (hμ : μ ≤ ν) : MeasureTheory.HasFiniteIntegral f μ

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 (μ + ν)) : 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 (μ + ν)) : MeasureTheory.HasFiniteIntegral f ν

@[simp]

theorem MeasureTheory.hasFiniteIntegral_add_measure {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α → β} : MeasureTheory.HasFiniteIntegral f (μ + ν) ↔ MeasureTheory.HasFiniteIntegral f μ ∧ MeasureTheory.HasFiniteIntegral 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 : α → β) : MeasureTheory.HasFiniteIntegral f 0

@[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 μ) : MeasureTheory.HasFiniteIntegral (-f) μ

@[simp]

theorem MeasureTheory.hasFiniteIntegral_neg_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α → β} : MeasureTheory.HasFiniteIntegral (-f) μ ↔ MeasureTheory.HasFiniteIntegral 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))) : MeasureTheory.HasFiniteIntegral f μ

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 : α → β) : MeasureTheory.HasFiniteIntegral (c • f) μ ↔ MeasureTheory.HasFiniteIntegral 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

• MeasureTheory.Integrable f μ = (MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.HasFiniteIntegral f μ)

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 μ) : MeasureTheory.AEStronglyMeasurable 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 μ) : MeasureTheory.HasFiniteIntegral 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‖) : MeasureTheory.Integrable f μ

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) : MeasureTheory.Integrable f μ

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‖) : MeasureTheory.Integrable g μ

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‖) : MeasureTheory.Integrable f μ ↔ MeasureTheory.Integrable g μ

theorem MeasureTheory.Integrable.congr {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α → β} {g : α → β} (hf : MeasureTheory.Integrable f μ) (h : f =ᶠ[MeasureTheory.Measure.ae μ] g) : MeasureTheory.Integrable g μ

theorem MeasureTheory.integrable_congr {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α → β} {g : α → β} (h : f =ᶠ[MeasureTheory.Measure.ae μ] g) : MeasureTheory.Integrable f μ ↔ MeasureTheory.Integrable g μ

theorem MeasureTheory.integrable_const_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {c : β} : MeasureTheory.Integrable (fun (x : α) => c) μ ↔ c = 0 ∨ ↑↑μ Set.univ < ⊤

@[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μ : μ ≤ ν) : MeasureTheory.Integrable f μ

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 μ) : 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 (μ + ν)) : 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 (μ + ν)) : 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 (Finset.sum s fun (i : ι) => μ 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 μ) : ∫⁻ (a : α), edist (f a) (g a) ∂μ < ⊤

@[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 (Finset.sum s fun (i : ι) => 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 : α) => Finset.sum s fun (i : ι) => f i a) μ

theorem MeasureTheory.Integrable.neg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α → β} (hf : MeasureTheory.Integrable f μ) : MeasureTheory.Integrable (-f) μ

@[simp]

theorem MeasureTheory.integrable_neg_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α → β} : MeasureTheory.Integrable (-f) μ ↔ MeasureTheory.Integrable 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 μ

@[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) : MeasureTheory.Integrable f₁ μ

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 μ) : MeasureTheory.Integrable f μ

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 < ε) : ↑↑μ {x : α | ε ≤ ‖f x‖} < ⊤

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 < ε) : ↑↑μ {x : α | ε < ‖f x‖} < ⊤

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 < ε) : ↑↑μ {a : α | ε ≤ f a} < ⊤

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) : ↑↑μ {a : α | f a ≤ c} < ⊤

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 < ε) : ↑↑μ {a : α | ε < f a} < ⊤

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) : ↑↑μ {a : α | f a < c} < ⊤

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 : α) => ↑(Real.toNNReal (f x))) μ

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) =ᶠ[MeasureTheory.Measure.ae μ] f

theorem MeasureTheory.coe_toNNReal_ae_eq {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : ∀ᵐ (x : α) ∂μ, f x < ⊤) : (fun (x : α) => ↑(f x).toNNReal) =ᶠ[MeasureTheory.Measure.ae μ] f

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.

@[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)) : MeasureTheory.Integrable f μ'

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) : MeasureTheory.Integrable f μ

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) : MeasureTheory.Integrable f μ

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 : α →ₘ[μ] β) : Prop

A class of almost everywhere equal functions is Integrable if its function representative is integrable.

Equations

• MeasureTheory.AEEqFun.Integrable f = MeasureTheory.Integrable (↑f) μ

theorem MeasureTheory.AEEqFun.integrable_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEEqFun.Integrable (MeasureTheory.AEEqFun.mk f hf) ↔ MeasureTheory.Integrable f μ

theorem MeasureTheory.AEEqFun.integrable_coeFn {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α →ₘ[μ] β} : MeasureTheory.Integrable (↑f) μ ↔ MeasureTheory.AEEqFun.Integrable f

theorem MeasureTheory.AEEqFun.integrable_zero {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] : MeasureTheory.AEEqFun.Integrable 0

theorem MeasureTheory.AEEqFun.Integrable.neg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α →ₘ[μ] β} : MeasureTheory.AEEqFun.Integrable f → MeasureTheory.AEEqFun.Integrable (-f)

theorem MeasureTheory.AEEqFun.integrable_iff_mem_L1 {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α →ₘ[μ] β} : MeasureTheory.AEEqFun.Integrable f ↔ f ∈ MeasureTheory.Lp β 1 μ

theorem MeasureTheory.AEEqFun.Integrable.add {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α →ₘ[μ] β} {g : α →ₘ[μ] β} : MeasureTheory.AEEqFun.Integrable f → MeasureTheory.AEEqFun.Integrable g → MeasureTheory.AEEqFun.Integrable (f + g)

theorem MeasureTheory.AEEqFun.Integrable.sub {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {f : α →ₘ[μ] β} {g : α →ₘ[μ] β} (hf : MeasureTheory.AEEqFun.Integrable f) (hg : MeasureTheory.AEEqFun.Integrable g) : MeasureTheory.AEEqFun.Integrable (f - g)

theorem MeasureTheory.AEEqFun.Integrable.smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 β] [BoundedSMul 𝕜 β] {c : 𝕜} {f : α →ₘ[μ] β} : MeasureTheory.AEEqFun.Integrable f → MeasureTheory.AEEqFun.Integrable (c • f)

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 μ)) : MeasureTheory.StronglyMeasurable ↑↑f

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 μ)) : MeasureTheory.AEStronglyMeasurable (↑↑f) μ

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 μ)) : edist f g = ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ

theorem MeasureTheory.L1.dist_def {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : ↥(MeasureTheory.Lp β 1 μ)) (g : ↥(MeasureTheory.Lp β 1 μ)) : dist f g = (∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ).toReal

theorem MeasureTheory.L1.norm_def {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (f : ↥(MeasureTheory.Lp β 1 μ)) : ‖f‖ = (∫⁻ (a : α), ↑‖↑↑f a‖₊ ∂μ).toReal

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 μ)) : ‖f - g‖ = (∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ).toReal

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 μ)) : ENNReal.ofReal ‖f‖ = ∫⁻ (x : α), ↑‖↑↑f x‖₊ ∂μ

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 μ)) : ENNReal.ofReal ‖f - g‖ = ∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ

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

• MeasureTheory.Integrable.toL1 f hf = MeasureTheory.Memℒp.toLp f ⋯

@[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) =ᶠ[MeasureTheory.Measure.ae μ] f

@[simp]

theorem MeasureTheory.Integrable.toL1_zero {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] (h : MeasureTheory.Integrable 0 μ) : MeasureTheory.Integrable.toL1 0 h = 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 =ᶠ[MeasureTheory.Measure.ae μ] 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 μ) : MeasureTheory.Integrable.toL1 (-f) ⋯ = -MeasureTheory.Integrable.toL1 f hf

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 μ) : ↑‖MeasureTheory.Integrable.toL1 f hf‖₊ = ∫⁻ (a : α), ↑‖f a‖₊ ∂μ

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) μ