hasFiniteIntegral_toReal_of_lintegral_ne_top

English

If ∫⁻ x f x ∂μ ≠ ∞ for f: α → ℝ≥0∞, then HasFiniteIntegral (fun x ↦ (f x).toReal) μ.

Русский

Если линетиал ∫⁻ f ≠ ∞ для f: α → ℝ≥0∞, тогда HasFiniteIntegral (f(x).toReal) μ.

LaTeX

$$$\int⁻ x, f x ∂μ \neq ∞ \Rightarrow HasFiniteIntegral (x \mapsto (f x).toReal) μ$$$

Lean4

theorem hasFiniteIntegral_toReal_of_lintegral_ne_top {f : α → ℝ≥0∞} (hf : ∫⁻ x, f x ∂μ ≠ ∞) :
    HasFiniteIntegral (fun x ↦ (f x).toReal) μ :=
  by
  have h x : ‖(f x).toReal‖ₑ = .ofReal (f x).toReal := by rw [Real.enorm_of_nonneg ENNReal.toReal_nonneg]
  simp_rw [hasFiniteIntegral_iff_enorm, h]
  refine lt_of_le_of_lt (lintegral_mono fun x => ?_) (lt_top_iff_ne_top.2 hf)
  by_cases hfx : f x = ∞
  · simp [hfx]
  · lift f x to ℝ≥0 using hfx with fx h
    simp

Похожие утверждения