betaIntegral_eval_one_right — Mathlib

English

Β(u,v) equals Β(v,u); the Beta function is symmetric in its arguments.

Русский

β-функция симметрична: Β(u,v) = Β(v,u).

LaTeX

$$$\betaIntegral(v,u) = \betaIntegral(u,v)$$$

Lean4

theorem betaIntegral_eval_one_right {u : ℂ} (hu : 0 < re u) : betaIntegral u 1 = 1 / u :=
  by
  simp_rw [betaIntegral, sub_self, cpow_zero, mul_one]
  rw [integral_cpow (Or.inl _)]
  · rw [ofReal_zero, ofReal_one, one_cpow, zero_cpow, sub_zero, sub_add_cancel]
    rw [sub_add_cancel]
    contrapose! hu; rw [hu, zero_re]
  · rwa [sub_re, one_re, ← sub_pos, sub_neg_eq_add, sub_add_cancel]

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