α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.704421
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
g : α → γ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖
hg : (∫⁻ (a : α), ENNReal.ofReal ‖g a‖ ∂μ) < ⊤
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ) < ⊤
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.704421
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
g : α → γ
hg : HasFiniteIntegral g
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖
⊢ HasFiniteIntegral f
simp only [hasFiniteIntegral_iff_norm] at *
no goals
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.704421
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
g : α → γ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖
hg : (∫⁻ (a : α), ENNReal.ofReal ‖g a‖ ∂μ) < ⊤
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ) < ⊤
calc
  (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) ≤ ∫⁻ a : α, ENNReal.ofReal ‖g a‖ ∂μ :=
    lintegral_mono_ae (h.mono fun a h => ofReal_le_ofReal h)
  _ < ∞ := hg