English
Assume n and that no k < n equals -a, -b, or -c after casting. Then the ratio of consecutive ordinary hypergeometric coefficients satisfies a multiplicative formula:
Русский
Пусть выполнено, что для всех k < n не выполняются равенства k ≠ -a, -b, -c после приведения. Тогда отношение норм коэффициентов обыкновенной гипергеометрической последовательности при n и n+1 равно произведению нормовых факторов:
LaTeX
$$$$ \frac{\|\mathrm{ordinaryHypergeometricCoefficient} \\{a,b,c\} (n)\|}{\|\mathrm{ordinaryHypergeometricCoefficient} \\{a,b,c\} (n+1)\|} \\= \|a+n\|^{-1} \|b+n\|^{-1} \|c+n\| \|1+n\|. $$$$
Lean4
theorem ordinaryHypergeometricSeries_norm_div_succ_norm (n : ℕ) (habc : ∀ kn < n, (↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c)) :
‖ordinaryHypergeometricCoefficient a b c n‖ / ‖ordinaryHypergeometricCoefficient a b c n.succ‖ =
‖a + n‖⁻¹ * ‖b + n‖⁻¹ * ‖c + n‖ * ‖1 + (n : 𝕂)‖ :=
by
simp only [mul_inv_rev, factorial_succ, cast_mul, cast_add, cast_one, ascPochhammer_succ_eval, norm_mul, norm_inv]
calc
_ =
‖Polynomial.eval a (ascPochhammer 𝕂 n)‖ * ‖Polynomial.eval a (ascPochhammer 𝕂 n)‖⁻¹ *
‖Polynomial.eval b (ascPochhammer 𝕂 n)‖ *
‖Polynomial.eval b (ascPochhammer 𝕂 n)‖⁻¹ *
‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹⁻¹ *
‖Polynomial.eval c (ascPochhammer 𝕂 n)‖⁻¹ *
‖(n ! : 𝕂)‖⁻¹⁻¹ *
‖(n ! : 𝕂)‖⁻¹ *
‖a + n‖⁻¹ *
‖b + n‖⁻¹ *
‖c + n‖⁻¹⁻¹ *
‖1 + (n : 𝕂)‖⁻¹⁻¹ :=
by ring_nf
_ = _ := by
simp only [inv_inv]
repeat rw [DivisionRing.mul_inv_cancel, one_mul]
all_goals rw [norm_ne_zero_iff]
any_goals
apply (ascPochhammer_eval_eq_zero_iff n _).not.2
push_neg
exact fun kn hkn ↦ by simp [habc kn hkn]
exact cast_ne_zero.2 (factorial_ne_zero n)
