integrable_pow_mul_norm_one_add_mul_inv

English

If ||z||<1, then the function t ↦ t^n * ||(1+t z)^{-1}|| is interval-integrable on [0,1].

Русский

Если ∥z∥<1, то функция t ↦ t^n · ∥(1+t z)^{-1}∥ интегрируема на отрезке [0,1].

LaTeX

$$$\\displaystyle \\text{IntervalIntegrable}\\left( t \\mapsto t^{n} \\cdot \\| (1 + t z)^{-1} \\| \\right) \\text{ на } [0,1]$$$

Lean4

theorem integrable_pow_mul_norm_one_add_mul_inv (n : ℕ) {z : ℂ} (hz : ‖z‖ < 1) :
    IntervalIntegrable (fun t : ℝ ↦ t ^ n * ‖(1 + t * z)⁻¹‖) MeasureTheory.volume 0 1 :=
  by
  have := continuousOn_one_add_mul_inv <| mem_slitPlane_of_norm_lt_one hz
  rw [← Set.uIcc_of_le zero_le_one] at this
  exact ContinuousOn.intervalIntegrable (by fun_prop)

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