Step
*
3
1
2
1
1
2
1
1
1
1
1
1
1
4
1
1
of Lemma
Legendre-orthogonal
1. n : ℕ
2. ∀n:ℕn
∀[k:ℕ]
r(-1)_∫-r1 x^k * Legendre(n;x) dx = if (k =z n) then (r(2 * (n)!)/r(doublefact((2 * n) + 1))) else r0 fi
supposing k ≤ n
3. ¬(n = 0 ∈ ℤ)
4. ¬(n = 1 ∈ ℤ)
5. k : ℕ
6. ∀k:ℕk
r(-1)_∫-r1 x^k * Legendre(n;x) dx = if (k =z n) then (r(2 * (n)!)/r(doublefact((2 * n) + 1))) else r0 fi
supposing k ≤ n
7. ¬(k = 0 ∈ ℤ)
8. k ≤ n
9. g : (-∞, ∞) ⟶ℝ
10. ∀x,y:ℝ. ((x = y) ⇒ ((g x) = (g y)))
11. d(Legendre(n;x))/dx = λx.g[x] on (-∞, ∞)
12. ∀x:ℝ. ((x * Legendre(n;x)) = (Legendre(n - 1;x) + ((x^2 - r1/r(n)) * (g x))))
13. ∀x:ℝ. ((x^k * Legendre(n;x)) = ((x^k - 1 * Legendre(n - 1;x)) + ((x^k + 1 - x^k - 1/r(n)) * (g x))))
14. r(-1)_∫-r1 x^k * Legendre(n;x) dx
= (if (k =z n) then (r(2 * (n - 1)!)/r(doublefact((2 * n) - 1))) else r0 fi
+ r(-1)_∫-r1 (x^k + 1 - x^k - 1/r(n)) * (g x) dx)
15. r(-1)_∫-r1 x^k - 1 * Legendre(n - 1;x) dx
= if (k =z n) then (r(2 * (n - 1)!)/r(doublefact((2 * n) - 1))) else r0 fi
16. r(-1)_∫-r1 (x^k + 1 - x^k - 1/r(n)) * (g x) dx ∈ ℝ
17. r(-1)_∫-r1 (t^k + 1 - t^k - 1/r(n)) * (g t) dt
= (((r1^k + 1 - r1^k - 1/r(n)) * Legendre(n;r1)) - (r(-1)^k + 1 - r(-1)^k - 1/r(n)) * Legendre(n;r(-1))
- r(-1)_∫-r1 ((r(k + 1) * t^(k + 1) - 1) - if (k =z 1) then r0 else r(k - 1) * t^k - 2 fi /r(n)) * Legendre(n;t) dt)
18. (r1^k + 1 - r1^k - 1) = r0
19. (r(-1)^k + 1 - r(-1)^k - 1) = r0
⊢ r(-1)_∫-r1 x^k * Legendre(n;x) dx = if (k =z n) then (r(2 * (n)!)/r(doublefact((2 * n) + 1))) else r0 fi
BY
{ (Assert r(-1)_∫-r1 ((r(k + 1) * t^(k + 1) - 1) - if (k =z 1) then r0 else r(k - 1) * t^k - 2 fi /r(n))
* Legendre(n;t) dt ∈ ℝ BY
AutoSplit) }
1
1. n : ℕ
2. ∀n:ℕn
∀[k:ℕ]
r(-1)_∫-r1 x^k * Legendre(n;x) dx = if (k =z n) then (r(2 * (n)!)/r(doublefact((2 * n) + 1))) else r0 fi
supposing k ≤ n
3. ¬(n = 0 ∈ ℤ)
4. ¬(n = 1 ∈ ℤ)
5. k : ℕ
6. ∀k:ℕk
r(-1)_∫-r1 x^k * Legendre(n;x) dx = if (k =z n) then (r(2 * (n)!)/r(doublefact((2 * n) + 1))) else r0 fi
supposing k ≤ n
7. ¬(k = 0 ∈ ℤ)
8. k ≤ n
9. g : (-∞, ∞) ⟶ℝ
10. ∀x,y:ℝ. ((x = y) ⇒ ((g x) = (g y)))
11. d(Legendre(n;x))/dx = λx.g[x] on (-∞, ∞)
12. ∀x:ℝ. ((x * Legendre(n;x)) = (Legendre(n - 1;x) + ((x^2 - r1/r(n)) * (g x))))
13. ∀x:ℝ. ((x^k * Legendre(n;x)) = ((x^k - 1 * Legendre(n - 1;x)) + ((x^k + 1 - x^k - 1/r(n)) * (g x))))
14. r(-1)_∫-r1 x^k * Legendre(n;x) dx
= (if (k =z n) then (r(2 * (n - 1)!)/r(doublefact((2 * n) - 1))) else r0 fi
+ r(-1)_∫-r1 (x^k + 1 - x^k - 1/r(n)) * (g x) dx)
15. r(-1)_∫-r1 x^k - 1 * Legendre(n - 1;x) dx
= if (k =z n) then (r(2 * (n - 1)!)/r(doublefact((2 * n) - 1))) else r0 fi
16. r(-1)_∫-r1 (x^k + 1 - x^k - 1/r(n)) * (g x) dx ∈ ℝ
17. r(-1)_∫-r1 (t^k + 1 - t^k - 1/r(n)) * (g t) dt
= (((r1^k + 1 - r1^k - 1/r(n)) * Legendre(n;r1)) - (r(-1)^k + 1 - r(-1)^k - 1/r(n)) * Legendre(n;r(-1))
- r(-1)_∫-r1 ((r(k + 1) * t^(k + 1) - 1) - if (k =z 1) then r0 else r(k - 1) * t^k - 2 fi /r(n)) * Legendre(n;t) dt)
18. (r1^k + 1 - r1^k - 1) = r0
19. (r(-1)^k + 1 - r(-1)^k - 1) = r0
20. r(-1)_∫-r1 ((r(k + 1) * t^(k + 1) - 1) - if (k =z 1) then r0 else r(k - 1) * t^k - 2 fi /r(n)) * Legendre(n;t) dt
∈ ℝ
⊢ r(-1)_∫-r1 x^k * Legendre(n;x) dx = if (k =z n) then (r(2 * (n)!)/r(doublefact((2 * n) + 1))) else r0 fi
Latex:
Latex:
1. n : \mBbbN{}
2. \mforall{}n:\mBbbN{}n
\mforall{}[k:\mBbbN{}]
r(-1)\_\mint{}\msupminus{}r1 x\^{}k * Legendre(n;x) dx
= if (k =\msubz{} n) then (r(2 * (n)!)/r(doublefact((2 * n) + 1))) else r0 fi
supposing k \mleq{} n
3. \mneg{}(n = 0)
4. \mneg{}(n = 1)
5. k : \mBbbN{}
6. \mforall{}k:\mBbbN{}k
r(-1)\_\mint{}\msupminus{}r1 x\^{}k * Legendre(n;x) dx
= if (k =\msubz{} n) then (r(2 * (n)!)/r(doublefact((2 * n) + 1))) else r0 fi
supposing k \mleq{} n
7. \mneg{}(k = 0)
8. k \mleq{} n
9. g : (-\minfty{}, \minfty{}) {}\mrightarrow{}\mBbbR{}
10. \mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} ((g x) = (g y)))
11. d(Legendre(n;x))/dx = \mlambda{}x.g[x] on (-\minfty{}, \minfty{})
12. \mforall{}x:\mBbbR{}. ((x * Legendre(n;x)) = (Legendre(n - 1;x) + ((x\^{}2 - r1/r(n)) * (g x))))
13. \mforall{}x:\mBbbR{}
((x\^{}k * Legendre(n;x)) = ((x\^{}k - 1 * Legendre(n - 1;x)) + ((x\^{}k + 1 - x\^{}k - 1/r(n)) * (g x))))
14. r(-1)\_\mint{}\msupminus{}r1 x\^{}k * Legendre(n;x) dx
= (if (k =\msubz{} n) then (r(2 * (n - 1)!)/r(doublefact((2 * n) - 1))) else r0 fi
+ r(-1)\_\mint{}\msupminus{}r1 (x\^{}k + 1 - x\^{}k - 1/r(n)) * (g x) dx)
15. r(-1)\_\mint{}\msupminus{}r1 x\^{}k - 1 * Legendre(n - 1;x) dx
= if (k =\msubz{} n) then (r(2 * (n - 1)!)/r(doublefact((2 * n) - 1))) else r0 fi
16. r(-1)\_\mint{}\msupminus{}r1 (x\^{}k + 1 - x\^{}k - 1/r(n)) * (g x) dx \mmember{} \mBbbR{}
17. r(-1)\_\mint{}\msupminus{}r1 (t\^{}k + 1 - t\^{}k - 1/r(n)) * (g t) dt
= (((r1\^{}k + 1 - r1\^{}k - 1/r(n)) * Legendre(n;r1)) - (r(-1)\^{}k + 1 - r(-1)\^{}k - 1/r(n))
* Legendre(n;r(-1)) - r(-1)\_\mint{}\msupminus{}r1 ((r(k + 1) * t\^{}(k + 1) - 1) - if (k =\msubz{} 1)
then r0
else r(k - 1) * t\^{}k - 2
fi /r(n))
* Legendre(n;t) dt)
18. (r1\^{}k + 1 - r1\^{}k - 1) = r0
19. (r(-1)\^{}k + 1 - r(-1)\^{}k - 1) = r0
\mvdash{} r(-1)\_\mint{}\msupminus{}r1 x\^{}k * Legendre(n;x) dx
= if (k =\msubz{} n) then (r(2 * (n)!)/r(doublefact((2 * n) + 1))) else r0 fi
By
Latex:
(Assert r(-1)\_\mint{}\msupminus{}r1 ((r(k + 1) * t\^{}(k + 1) - 1) - if (k =\msubz{} 1)
then r0
else r(k - 1) * t\^{}k - 2
fi /r(n))
* Legendre(n;t) dt \mmember{} \mBbbR{} BY
AutoSplit)
Home
Index