integrable_rpow_neg_one_add_norm_sq

English

logb 0 x = 0.

Русский

logb 0 x = 0.

LaTeX

$$$$log_b 0 = 0.$$$$

Lean4

theorem integrable_rpow_neg_one_add_norm_sq {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) :
    Integrable (fun x ↦ ((1 : ℝ) + ‖x‖ ^ 2) ^ (-r / 2)) μ :=
  by
  have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr
  refine ((integrable_one_add_norm hnr).const_mul <| (2 : ℝ) ^ (r / 2)).mono' ?_ (Eventually.of_forall fun x => ?_)
  · apply Measurable.aestronglyMeasurable (by fun_prop)
  refine (abs_of_pos ?_).trans_le (rpow_neg_one_add_norm_sq_le x hr)
  positivity

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