shiftedLegendre_eval_symm — Mathlib

English

For any n, over a ring R, aeval x (shiftedLegendre n) equals (-1)^n times aeval (1 - x) (shiftedLegendre n).

Русский

Для любого n над кольцом R выполнено: aeval_x(shiftedLegendre(n)) = (-1)^n aeval_{1-x}(shiftedLegendre(n)).

LaTeX

$$$\\forall n \\;\\forall R [\\text{Ring } R] \\; (x)\\; aeval\\ x\\ (\\mathrm{shiftedLegendre}(n)) = (-1)^n \\cdot aeval\\ (1 - x) (\\mathrm{shiftedLegendre}(n))$$$

Lean4

/-- The values of the Legendre polynomial at `x` and `1 - x` differ by a factor `(-1)ⁿ`. -/
theorem shiftedLegendre_eval_symm (n : ℕ) {R : Type*} [Ring R] (x : R) :
    aeval x (shiftedLegendre n) = (-1) ^ n * aeval (1 - x) (shiftedLegendre n) :=
  by
  have := congr(aeval x $(neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq n))
  simpa [aeval_comp] using this.symm

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