Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
⊢ HasFiniteIntegral ↑f
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
⊢ Integrable ↑f
refine' ⟨f.continuous.measurable.aestronglyMeasurable, _⟩
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
aux : NNReal.toReal ∘ ↑(BoundedContinuousFunction.nnnorm f) = fun x => ‖↑f x‖
⊢ HasFiniteIntegral ↑f
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
⊢ HasFiniteIntegral ↑f
have aux : ((↑) : ℝ≥0 → ℝ) ∘ ⇑f.nnnorm = fun x => ‖f x‖ := by
  ext ω
  simp only [Function.comp_apply, BoundedContinuousFunction.nnnorm_coeFn_eq, coe_nnnorm]
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
aux : NNReal.toReal ∘ ↑(BoundedContinuousFunction.nnnorm f) = fun x => ‖↑f x‖
⊢ (∫⁻ (a : Ω), ENNReal.ofReal ‖↑f a‖ ∂μ) < ⊤
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
aux : NNReal.toReal ∘ ↑(BoundedContinuousFunction.nnnorm f) = fun x => ‖↑f x‖
⊢ HasFiniteIntegral ↑f
apply (hasFiniteIntegral_iff_norm f).mpr
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
aux : NNReal.toReal ∘ ↑(BoundedContinuousFunction.nnnorm f) = fun x => ‖↑f x‖
⊢ ENNReal.ofReal (∫ (x : Ω), ‖↑f x‖ ∂μ) < ⊤

case hfi
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
aux : NNReal.toReal ∘ ↑(BoundedContinuousFunction.nnnorm f) = fun x => ‖↑f x‖
⊢ Integrable fun a => ‖↑f a‖

case f_nn
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
aux : NNReal.toReal ∘ ↑(BoundedContinuousFunction.nnnorm f) = fun x => ‖↑f x‖
⊢ 0 ≤ᵐ[μ] fun a => ‖↑f a‖
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
aux : NNReal.toReal ∘ ↑(BoundedContinuousFunction.nnnorm f) = fun x => ‖↑f x‖
⊢ (∫⁻ (a : Ω), ENNReal.ofReal ‖↑f a‖ ∂μ) < ⊤
rw [← ofReal_integral_eq_lintegral_ofReal]
case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
ω : Ω
⊢ (NNReal.toReal ∘ ↑(BoundedContinuousFunction.nnnorm f)) ω = ‖↑f ω‖
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
⊢ NNReal.toReal ∘ ↑(BoundedContinuousFunction.nnnorm f) = fun x => ‖↑f x‖
ext ω
no goals
case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
ω : Ω
⊢ (NNReal.toReal ∘ ↑(BoundedContinuousFunction.nnnorm f)) ω = ‖↑f ω‖
simp only [Function.comp_apply, BoundedContinuousFunction.nnnorm_coeFn_eq, coe_nnnorm]
no goals
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
aux : NNReal.toReal ∘ ↑(BoundedContinuousFunction.nnnorm f) = fun x => ‖↑f x‖
⊢ ENNReal.ofReal (∫ (x : Ω), ‖↑f x‖ ∂μ) < ⊤
exact ENNReal.ofReal_lt_top
no goals
case hfi
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
aux : NNReal.toReal ∘ ↑(BoundedContinuousFunction.nnnorm f) = fun x => ‖↑f x‖
⊢ Integrable fun a => ‖↑f a‖
exact aux ▸ integrable_of_boundedContinuous_to_nnreal μ f.nnnorm
no goals
case f_nn
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω →ᵇ ℝ
aux : NNReal.toReal ∘ ↑(BoundedContinuousFunction.nnnorm f) = fun x => ‖↑f x‖
⊢ 0 ≤ᵐ[μ] fun a => ‖↑f a‖
exact eventually_of_forall fun ω => norm_nonneg (f ω)