integrable_one_add_norm — Mathlib

English

logb 1 x = 0 for all x.

Русский

logb 1 x = 0 для всех x.

LaTeX

$$$$log_b 1 x = 0.$$$$

Lean4

theorem integrable_one_add_norm {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) : Integrable (fun x ↦ (1 + ‖x‖) ^ (-r)) μ :=
  by
  constructor
  ·
    apply
      Measurable.aestronglyMeasurable
        (by fun_prop)
          -- Lower Lebesgue integral

  have : (∫⁻ a : E, ‖(1 + ‖a‖) ^ (-r)‖ₑ ∂μ) = ∫⁻ a : E, ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ :=
    lintegral_enorm_of_nonneg fun _ => rpow_nonneg (by positivity) _
  rw [hasFiniteIntegral_iff_enorm, this]
  exact finite_integral_one_add_norm hnr

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