---

Step * of Lemma Legendre-rpolynomial-same-degree

∀[n:ℕ]. ∀[a:ℕn + 1 ⟶ ℝ]. ∀[f:[r(-1), r1] ⟶ℝ].
  r(-1)_∫-r1 f[x] * Legendre(n;x) dx = ((r(2 * (n)!)/r(doublefact((2 * n) + 1))) * (a n)) 
  supposing ∀x:{x:ℝ| x ∈ [r(-1), r1]} . ((f x) = (Σi≤n. a_i * x^i))
BY
{ (Unfold `so_apply` 0
   THEN Intros
   THEN Assert ⌜λx.((f x) * Legendre(n;x)) ∈ {f:[rmin(r(-1);r1), rmax(r(-1);r1)] ⟶ℝ| 
                                              ifun(f;[rmin(r(-1);r1), rmax(r(-1);r1)])} ⌝⋅) }

1
.....assertion..... 
1. [n] : ℕ
2. [a] : ℕn + 1 ⟶ ℝ
3. [f] : [r(-1), r1] ⟶ℝ
4. [%] : ∀x:{x:ℝ| x ∈ [r(-1), r1]} . ((f x) = (Σi≤n. a_i * x^i))
⊢ λx.((f x) * Legendre(n;x)) ∈ {f:[rmin(r(-1);r1), rmax(r(-1);r1)] ⟶ℝ| ifun(f;[rmin(r(-1);r1), rmax(r(-1);r1)])} 

2
1. [n] : ℕ
2. [a] : ℕn + 1 ⟶ ℝ
3. [f] : [r(-1), r1] ⟶ℝ
4. [%] : ∀x:{x:ℝ| x ∈ [r(-1), r1]} . ((f x) = (Σi≤n. a_i * x^i))
5. λx.((f x) * Legendre(n;x)) ∈ {f:[rmin(r(-1);r1), rmax(r(-1);r1)] ⟶ℝ| ifun(f;[rmin(r(-1);r1), rmax(r(-1);r1)])} 
⊢ r(-1)_∫-r1 (f x) * Legendre(n;x) dx = ((r(2 * (n)!)/r(doublefact((2 * n) + 1))) * (a n))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[f:[r(-1),  r1]  {}\mrightarrow{}\mBbbR{}].
    r(-1)\_\mint{}\msupminus{}r1  f[x]  *  Legendre(n;x)  dx  =  ((r(2  *  (n)!)/r(doublefact((2  *  n)  +  1)))  *  (a  n)) 
    supposing  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [r(-1),  r1]\}  .  ((f  x)  =  (\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i))


By

---

Latex:
(Unfold  `so\_apply`  0
  THEN  Intros
  THEN  Assert  \mkleeneopen{}\mlambda{}x.((f  x)  *  Legendre(n;x))  \mmember{}  \{f:[rmin(r(-1);r1),  rmax(r(-1);r1)]  {}\mrightarrow{}\mBbbR{}| 
                                                                                        ifun(f;[rmin(r(-1);r1),  rmax(r(-1);r1)])\}  \mkleeneclose{}\mcdot{})

---

Home Index