GammaIntegral_conj — Mathlib

English

Conjugation commutes with the Gamma integral: ΓIntegral(conj s) = conj(ΓIntegral s).

Русский

Сопряжение числа сохраняется под гамма-интегралом: ΓIntegral(conj s) = conj(ΓIntegral s).

LaTeX

$$$$ \GammaIntegral(\overline{s}) = \overline{\GammaIntegral(s)}. $$$$

Lean4

theorem GammaIntegral_conj (s : ℂ) : GammaIntegral (conj s) = conj (GammaIntegral s) :=
  by
  rw [GammaIntegral, GammaIntegral, ← integral_conj]
  refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_
  dsimp only
  rw [RingHom.map_mul, conj_ofReal, cpow_def_of_ne_zero (ofReal_ne_zero.mpr (ne_of_gt hx)),
    cpow_def_of_ne_zero (ofReal_ne_zero.mpr (ne_of_gt hx)), ← exp_conj, RingHom.map_mul, ← ofReal_log (le_of_lt hx),
    conj_ofReal, RingHom.map_sub, RingHom.map_one]

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