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

@[deprecated MeasureTheory.lintegral_enorm_eq_lintegral_edist (since := "2025-01-20")]

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

Alias of MeasureTheory.lintegral_enorm_eq_lintegral_edist.

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_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] : ∫⁻ (x : α), ‖0‖ₑ ∂μ = 0

theorem MeasureTheory.lintegral_enorm_add_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {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_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] (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‖ₑ ∂μ

@[deprecated MeasureTheory.lintegral_enorm_zero (since := "2025-01-21")]

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

Alias of MeasureTheory.lintegral_enorm_zero.

@[deprecated MeasureTheory.lintegral_enorm_add_left (since := "2025-01-21")]

theorem MeasureTheory.lintegral_nnnorm_add_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] {f : α → β} (hf : AEStronglyMeasurable f μ) (g : α → γ) : ∫⁻ (a : α), ‖f a‖ₑ + ‖g a‖ₑ ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖g a‖ₑ ∂μ

Alias of MeasureTheory.lintegral_enorm_add_left.

@[deprecated MeasureTheory.lintegral_enorm_add_right (since := "2025-01-21")]

theorem MeasureTheory.lintegral_nnnorm_add_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] [NormedAddCommGroup γ] (f : α → β) {g : α → γ} (hg : AEStronglyMeasurable g μ) : ∫⁻ (a : α), ‖f a‖ₑ + ‖g a‖ₑ ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖g a‖ₑ ∂μ

Alias of MeasureTheory.lintegral_enorm_add_right.

@[deprecated MeasureTheory.lintegral_enorm_neg (since := "2025-01-21")]

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

Alias of MeasureTheory.lintegral_enorm_neg.

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_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} : HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤

@[deprecated MeasureTheory.hasFiniteIntegral_iff_enorm (since := "2025-01-20")]

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

Alias of MeasureTheory.hasFiniteIntegral_iff_enorm.

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 ≤ᶠ[ae μ] 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 {α : 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' {α : 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' {α : 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' {α : 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_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f g : α → β} (hf : HasFiniteIntegral f μ) (h : f =ᶠ[ae μ] g) : HasFiniteIntegral g μ

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

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 {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {c : β} (hc : c ≠ 0) : HasFiniteIntegral (fun (x : α) => c) μ ↔ IsFiniteMeasure μ

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 {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] (a b : ℝ) {X : α → ℝ} (h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Set.Icc a b) : HasFiniteIntegral X μ

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 μ

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_2} {m : MeasurableSpace α} {μ ν : Measure α} [NormedAddCommGroup β] {f : α → β} (h : HasFiniteIntegral f ν) (hμ : μ ≤ ν) : HasFiniteIntegral f μ

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

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

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

@[simp]

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

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

@[simp]

theorem MeasureTheory.hasFiniteIntegral_zero_measure {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {m : MeasurableSpace α} (f : α → β) : HasFiniteIntegral f 0

@[simp]

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

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.norm {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : α → β} (hfi : HasFiniteIntegral f μ) : HasFiniteIntegral (fun (a : α) => ‖f a‖) μ

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_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_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.all_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.all_ae_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.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 : α) => f a ⊔ 0) μ

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

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

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

theorem MeasureTheory.HasFiniteIntegral.const_mul {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {𝕜 : Type u_5} [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_5} [NormedRing 𝕜] {f : α → 𝕜} (h : HasFiniteIntegral f μ) (c : 𝕜) : HasFiniteIntegral (fun (x : α) => f x * c) μ

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} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_6} [NormedAddCommGroup E] {f : α → E} (h : HasFiniteIntegral f μ) {s : Set α} : HasFiniteIntegral f (μ.restrict s)