Function with finite integral

In this file we define the predicate HasFiniteIntegral, which is then used to define the predicate Integrable in the corresponding file.

Main definition

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

Tags

finite integral

Some results about the Lebesgue integral involving a normed group

theorem MeasureTheory.lintegral_enorm_eq_lintegral_edist {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : 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 α} {μ : 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 α} {μ : Measure α} [NormedAddCommGroup β] {f g h : α → β} (hf : AEStronglyMeasurable f μ) (hh : AEStronglyMeasurable h μ) : ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) ∂μ + ∫⁻ (a : α), edist (g a) (h a) ∂μ

theorem MeasureTheory.lintegral_enorm_zero {α : Type u_1} {ε'' : Type u_6} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] : ∫⁻ (x : α), ‖0‖ₑ ∂μ = 0

theorem MeasureTheory.lintegral_enorm_add_left {α : Type u_1} {ε' : Type u_5} {ε'' : Type u_6} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε'] [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] {f : α → ε''} (hf : AEStronglyMeasurable f μ) (g : α → ε') : ∫⁻ (a : α), ‖f a‖ₑ + ‖g a‖ₑ ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖g a‖ₑ ∂μ

theorem MeasureTheory.lintegral_enorm_add_right {α : Type u_1} {ε' : Type u_5} {ε'' : Type u_6} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε'] [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] (f : α → ε') {g : α → ε''} (hg : AEStronglyMeasurable g μ) : ∫⁻ (a : α), ‖f a‖ₑ + ‖g a‖ₑ ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖g a‖ₑ ∂μ

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

The predicate HasFiniteIntegral

def MeasureTheory.HasFiniteIntegral {α : Type u_1} {ε : Type u_4} [ENorm ε] {x✝ : MeasurableSpace α} (f : α → ε) (μ : Measure α := by volume_tac) : 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_4} [ENorm ε] {x✝ : MeasurableSpace α} (f : α → ε) (μ : Measure α) : HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤

theorem MeasureTheory.hasFiniteIntegral_iff_enorm {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} : HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤

theorem MeasureTheory.hasFiniteIntegral_iff_norm {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : α → β) : HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ⊤

theorem MeasureTheory.hasFiniteIntegral_iff_edist {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : α → β) : HasFiniteIntegral f μ ↔ ∫⁻ (a : α), edist (f a) 0 ∂μ < ⊤

theorem MeasureTheory.hasFiniteIntegral_iff_ofReal {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (h : 0 ≤ᵐ[μ] f) : HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ⊤

theorem MeasureTheory.hasFiniteIntegral_iff_ofNNReal {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → NNReal} : HasFiniteIntegral (fun (x : α) => ↑(f x)) μ ↔ ∫⁻ (a : α), ↑(f a) ∂μ < ⊤

theorem MeasureTheory.HasFiniteIntegral.mono_enorm {α : Type u_1} {ε : Type u_4} {ε' : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] [ENorm ε'] {f : α → ε} {g : α → ε'} (hg : HasFiniteIntegral g μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ ‖g a‖ₑ) : HasFiniteIntegral f μ

theorem MeasureTheory.HasFiniteIntegral.mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : α → β} {g : α → γ} (hg : HasFiniteIntegral g μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖) : HasFiniteIntegral f μ

theorem MeasureTheory.HasFiniteIntegral.mono_nonneg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [Lattice β] [HasSolidNorm β] [AddLeftMono β] {f g : α → β} (hg : HasFiniteIntegral g μ) (hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a) (h : ∀ᵐ (a : α) ∂μ, f a ≤ g a) : HasFiniteIntegral f μ

theorem MeasureTheory.HasFiniteIntegral.mono'_enorm {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} {g : α → ENNReal} (hg : HasFiniteIntegral g μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ g a) : HasFiniteIntegral f μ

theorem MeasureTheory.HasFiniteIntegral.mono' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} {g : α → ℝ} (hg : HasFiniteIntegral g μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a) : HasFiniteIntegral f μ

theorem MeasureTheory.HasFiniteIntegral.congr'_enorm {α : Type u_1} {ε : Type u_4} {ε' : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] [ENorm ε'] {f : α → ε} {g : α → ε'} (hf : HasFiniteIntegral f μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) : HasFiniteIntegral g μ

theorem MeasureTheory.HasFiniteIntegral.congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : α → β} {g : α → γ} (hf : HasFiniteIntegral f μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) : HasFiniteIntegral g μ

theorem MeasureTheory.hasFiniteIntegral_congr'_enorm {α : Type u_1} {ε : Type u_4} {ε' : Type u_5} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] [ENorm ε'] {f : α → ε} {g : α → ε'} (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) : HasFiniteIntegral f μ ↔ HasFiniteIntegral g μ

theorem MeasureTheory.hasFiniteIntegral_congr' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : α → β} {g : α → γ} (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) : HasFiniteIntegral f μ ↔ HasFiniteIntegral g μ

theorem MeasureTheory.HasFiniteIntegral.congr {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f g : α → ε} (hf : HasFiniteIntegral f μ) (h : f =ᵐ[μ] g) : HasFiniteIntegral g μ

theorem MeasureTheory.hasFiniteIntegral_congr {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f g : α → ε} (h : f =ᵐ[μ] g) : HasFiniteIntegral f μ ↔ HasFiniteIntegral g μ

theorem MeasureTheory.hasFiniteIntegral_const_iff_enorm {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {c : ε} (hc : ‖c‖ₑ ≠ ⊤) : HasFiniteIntegral (fun (x : α) => c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ

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

theorem MeasureTheory.hasFiniteIntegral_const_iff_isFiniteMeasure_enorm {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {c : ε} (hc : ‖c‖ₑ ≠ 0) (hc' : ‖c‖ₑ ≠ ⊤) : HasFiniteIntegral (fun (x : α) => c) μ ↔ IsFiniteMeasure μ

theorem MeasureTheory.hasFiniteIntegral_const_iff_isFiniteMeasure {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {c : β} (hc : c ≠ 0) : HasFiniteIntegral (fun (x : α) => c) μ ↔ IsFiniteMeasure μ

theorem MeasureTheory.hasFiniteIntegral_const_enorm {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] [IsFiniteMeasure μ] {c : ε} (hc : ‖c‖ₑ ≠ ⊤) : HasFiniteIntegral (fun (x : α) => c) μ

theorem MeasureTheory.hasFiniteIntegral_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [IsFiniteMeasure μ] (c : β) : HasFiniteIntegral (fun (x : α) => c) μ

theorem MeasureTheory.HasFiniteIntegral.of_mem_Icc_of_ne_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) {X : α → ENNReal} (h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Set.Icc a b) : HasFiniteIntegral X μ

theorem MeasureTheory.HasFiniteIntegral.of_mem_Icc {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] (a b : ℝ) {X : α → ℝ} (h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Set.Icc a b) : HasFiniteIntegral X μ

theorem MeasureTheory.HasFiniteIntegral.of_bounded_enorm {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] [IsFiniteMeasure μ] {f : α → ε} {C : ENNReal} (hC' : ‖C‖ₑ ≠ ⊤ := by finiteness) (hC : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ C) : HasFiniteIntegral f μ

theorem MeasureTheory.HasFiniteIntegral.of_bounded {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [IsFiniteMeasure μ] {f : α → β} {C : ℝ} (hC : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ C) : HasFiniteIntegral f μ

@[simp]

theorem MeasureTheory.HasFiniteIntegral.of_finite {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [Finite α] [IsFiniteMeasure μ] {f : α → β} : HasFiniteIntegral f μ

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

theorem MeasureTheory.HasFiniteIntegral.add_measure {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ ν : Measure α} [ENorm ε] {f : α → ε} (hμ : HasFiniteIntegral f μ) (hν : HasFiniteIntegral f ν) : HasFiniteIntegral f (μ + ν)

theorem MeasureTheory.HasFiniteIntegral.left_of_add_measure {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ ν : Measure α} [ENorm ε] {f : α → ε} (h : HasFiniteIntegral f (μ + ν)) : HasFiniteIntegral f μ

theorem MeasureTheory.HasFiniteIntegral.right_of_add_measure {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ ν : Measure α} [ENorm ε] {f : α → ε} (h : HasFiniteIntegral f (μ + ν)) : HasFiniteIntegral f ν

@[simp]

theorem MeasureTheory.hasFiniteIntegral_add_measure {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ ν : Measure α} [ENorm ε] {f : α → ε} : HasFiniteIntegral f (μ + ν) ↔ HasFiniteIntegral f μ ∧ HasFiniteIntegral f ν

theorem MeasureTheory.HasFiniteIntegral.smul_measure {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} (h : HasFiniteIntegral f μ) {c : ENNReal} (hc : c ≠ ⊤) : HasFiniteIntegral f (c • μ)

@[simp]

theorem MeasureTheory.hasFiniteIntegral_zero_measure {α : Type u_1} {ε : Type u_4} [ENorm ε] {m : MeasurableSpace α} (f : α → ε) : HasFiniteIntegral f 0

@[simp]

theorem MeasureTheory.hasFiniteIntegral_zero (α : Type u_1) {m : MeasurableSpace α} (μ : Measure α) {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] : HasFiniteIntegral 0 μ

@[simp]

theorem MeasureTheory.hasFiniteIntegral_fun_zero (α : Type u_1) {m : MeasurableSpace α} (μ : Measure α) {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] : HasFiniteIntegral (fun (x : α) => 0) μ

Eta-expanded form of MeasureTheory.hasFiniteIntegral_zero

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

@[simp]

theorem MeasureTheory.hasFiniteIntegral_neg_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} : HasFiniteIntegral (-f) μ ↔ HasFiniteIntegral f μ

theorem MeasureTheory.HasFiniteIntegral.enorm {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} (hfi : HasFiniteIntegral f μ) : HasFiniteIntegral (fun (x : α) => ‖f x‖ₑ) μ

theorem MeasureTheory.HasFiniteIntegral.norm {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} (hfi : HasFiniteIntegral f μ) : HasFiniteIntegral (fun (a : α) => ‖f a‖) μ

theorem MeasureTheory.hasFiniteIntegral_enorm_iff {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] (f : α → ε) : HasFiniteIntegral (fun (x : α) => ‖f x‖ₑ) μ ↔ HasFiniteIntegral f μ

theorem MeasureTheory.hasFiniteIntegral_norm_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] (f : α → β) : HasFiniteIntegral (fun (a : α) => ‖f a‖) μ ↔ HasFiniteIntegral f μ

theorem MeasureTheory.HasFiniteIntegral.of_subsingleton {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [Subsingleton α] [IsFiniteMeasure μ] {f : α → β} : HasFiniteIntegral f μ

theorem MeasureTheory.HasFiniteIntegral.of_isEmpty {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [IsEmpty α] {f : α → β} : HasFiniteIntegral f μ

@[simp]

theorem MeasureTheory.HasFiniteIntegral.of_subsingleton_codomain {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] [Subsingleton ε] {f : α → ε} : HasFiniteIntegral f μ

theorem MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤) : HasFiniteIntegral (fun (x : α) => (f x).toReal) μ

theorem MeasureTheory.hasFiniteIntegral_toReal_iff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : HasFiniteIntegral (fun (x : α) => (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ⊤

theorem MeasureTheory.isFiniteMeasure_withDensity_ofReal {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hfi : HasFiniteIntegral f μ) : IsFiniteMeasure (μ.withDensity fun (x : α) => ENNReal.ofReal (f x))

theorem MeasureTheory.all_ae_norm_ofReal_F_le_bound {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : 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.ae_tendsto_enorm {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {F' : ℕ → α → ε} {f' : α → ε} (h : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => F' n a) Filter.atTop (nhds (f' a))) : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => ‖F' n a‖ₑ) Filter.atTop (nhds ‖f' a‖ₑ)

theorem MeasureTheory.ae_tendsto_ofReal_norm {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : 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.ae_norm_ofReal_f_le_bound {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : 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.ae_enorm_le_bound {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {F' : ℕ → α → ε} {f' : α → ε} {bound' : α → ENNReal} (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 : α) ∂μ, ‖f' a‖ₑ ≤ bound' a

theorem MeasureTheory.hasFiniteIntegral_of_dominated_convergence_enorm {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {F' : ℕ → α → ε} {f' : α → ε} {bound' : α → ENNReal} (bound_hasFiniteIntegral : 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))) : HasFiniteIntegral f' μ

theorem MeasureTheory.hasFiniteIntegral_of_dominated_convergence {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {F : ℕ → α → β} {f : α → β} {bound : α → ℝ} (bound_hasFiniteIntegral : 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))) : HasFiniteIntegral f μ

theorem MeasureTheory.tendsto_lintegral_norm_of_dominated_convergence {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {F : ℕ → α → β} {f : α → β} {bound : α → ℝ} (F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ) (bound_hasFiniteIntegral : 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 α} {μ : Measure α} {f : α → ℝ} (hf : HasFiniteIntegral f μ) : HasFiniteIntegral (fun (a : α) => max (f a) 0) μ

theorem MeasureTheory.HasFiniteIntegral.min_zero {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hf : HasFiniteIntegral f μ) : HasFiniteIntegral (fun (a : α) => min (f a) 0) μ

theorem MeasureTheory.HasFiniteIntegral.smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {𝕜 : Type u_7} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 β] [IsBoundedSMul 𝕜 β] (c : 𝕜) {f : α → β} (hf : HasFiniteIntegral f μ) : HasFiniteIntegral (c • f) μ

theorem MeasureTheory.HasFiniteIntegral.smul_enorm {α : Type u_1} {ε'' : Type u_6} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] {𝕜 : Type u_7} [NormedAddGroup 𝕜] [SMul 𝕜 ε''] [ENormSMulClass 𝕜 ε''] (c : 𝕜) {f : α → ε''} (hf : HasFiniteIntegral f μ) : HasFiniteIntegral (c • f) μ

theorem MeasureTheory.hasFiniteIntegral_smul_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {𝕜 : Type u_7} [NormedRing 𝕜] [MulActionWithZero 𝕜 β] [IsBoundedSMul 𝕜 β] {c : 𝕜} (hc : IsUnit c) (f : α → β) : HasFiniteIntegral (c • f) μ ↔ HasFiniteIntegral f μ

theorem MeasureTheory.HasFiniteIntegral.const_mul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_7} [NormedRing 𝕜] {f : α → 𝕜} (h : HasFiniteIntegral f μ) (c : 𝕜) : HasFiniteIntegral (fun (x : α) => c * f x) μ

theorem MeasureTheory.HasFiniteIntegral.mul_const {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_7} [NormedRing 𝕜] {f : α → 𝕜} (h : HasFiniteIntegral f μ) (c : 𝕜) : HasFiniteIntegral (fun (x : α) => f x * c) μ

theorem MeasureTheory.hasFiniteIntegral_count_iff_enorm {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} [ENorm ε] [MeasurableSingletonClass α] {f : α → ε} : HasFiniteIntegral f Measure.count ↔ ∑' (x : α), ‖f x‖ₑ < ⊤

A function has finite integral for the counting measure iff its enorm has finite tsum.

theorem MeasureTheory.hasFiniteIntegral_count_iff {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup β] [MeasurableSingletonClass α] {f : α → β} : HasFiniteIntegral f Measure.count ↔ Summable fun (x : α) => ‖f x‖

A function has finite integral for the counting measure iff its norm is summable.

theorem MeasureTheory.HasFiniteIntegral.restrict {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} (h : HasFiniteIntegral f μ) {s : Set α} : HasFiniteIntegral f (μ.restrict s)