α : Type u_1
β : Type ?u.994446
γ : Type ?u.994449
δ : Type ?u.994452
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
⊢ HasFiniteIntegral fun x => ↑(Real.toNNReal (f x))
α : Type u_1
β : Type ?u.994446
γ : Type ?u.994449
δ : Type ?u.994452
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
⊢ Integrable fun x => ↑(Real.toNNReal (f x))
refine'
  ⟨hf.aestronglyMeasurable.aemeasurable.real_toNNReal.coe_nnreal_real.aestronglyMeasurable, _⟩
α : Type u_1
β : Type ?u.994446
γ : Type ?u.994449
δ : Type ?u.994452
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖↑(Real.toNNReal (f a))‖ ∂μ) < ⊤
α : Type u_1
β : Type ?u.994446
γ : Type ?u.994449
δ : Type ?u.994452
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
⊢ HasFiniteIntegral fun x => ↑(Real.toNNReal (f x))
rw [hasFiniteIntegral_iff_norm]
α : Type u_1
β : Type ?u.994446
γ : Type ?u.994449
δ : Type ?u.994452
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖↑(Real.toNNReal (f a))‖ ∂μ) ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
α : Type u_1
β : Type ?u.994446
γ : Type ?u.994449
δ : Type ?u.994452
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖↑(Real.toNNReal (f a))‖ ∂μ) < ⊤
refine' lt_of_le_of_lt _ ((hasFiniteIntegral_iff_norm _).1 hf.hasFiniteIntegral)
case hfg
α : Type u_1
β : Type ?u.994446
γ : Type ?u.994449
δ : Type ?u.994452
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
⊢ (fun a => ENNReal.ofReal ‖↑(Real.toNNReal (f a))‖) ≤ fun a => ENNReal.ofReal ‖f a‖
α : Type u_1
β : Type ?u.994446
γ : Type ?u.994449
δ : Type ?u.994452
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖↑(Real.toNNReal (f a))‖ ∂μ) ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
apply lintegral_mono
case hfg
α : Type u_1
β : Type ?u.994446
γ : Type ?u.994449
δ : Type ?u.994452
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
x : α
⊢ (fun a => ENNReal.ofReal ‖↑(Real.toNNReal (f a))‖) x ≤ (fun a => ENNReal.ofReal ‖f a‖) x
case hfg
α : Type u_1
β : Type ?u.994446
γ : Type ?u.994449
δ : Type ?u.994452
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
⊢ (fun a => ENNReal.ofReal ‖↑(Real.toNNReal (f a))‖) ≤ fun a => ENNReal.ofReal ‖f a‖
intro x
no goals
case hfg
α : Type u_1
β : Type ?u.994446
γ : Type ?u.994449
δ : Type ?u.994452
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ
hf : Integrable f
x : α
⊢ (fun a => ENNReal.ofReal ‖↑(Real.toNNReal (f a))‖) x ≤ (fun a => ENNReal.ofReal ‖f a‖) x
simp [ENNReal.ofReal_le_ofReal, abs_le, le_abs_self]