Step
*
of Lemma
Legendre-rpolynomial
∀n:ℕ. ∃a:ℕn + 1 ⟶ ℝ. ((∀x:ℝ. (Legendre(n;x) = (Σi≤n. a_i * x^i))) ∧ ((a n) = (r(doublefact((2 * n) - 1))/r((n)!))))
BY
{ (CompleteInductionOnNat
THEN (CaseNat 0 `n'
THENL [(Reduce 0
THEN (D 0 With ⌜λi.r1⌝ THEN Auto)
THEN Reduce 0
THEN (RWO "rpolynomial_unroll" 0 ORELSE nRNorm 0)
THEN Reduce 0
THEN Auto)
; (CaseNat 1 `n'
THENL [(Reduce 0
THEN (D 0 With ⌜λi.if (i =z 1) then r1 else r0 fi ⌝ THEN Auto)
THEN Reduce 0
THEN (RWO "rpolynomial_unroll" 0 ORELSE ((Subst' (1)! ~ 1 0 THENA Auto) THEN nRNorm 0))
THEN Reduce 0
THEN Auto
THEN (RWO "rpolynomial_unroll" 0 THEN Reduce 0)
THEN Auto
THEN RWO "rnexp1" 0
THEN Auto)
; ((InstHyp [⌜n - 2⌝] 2⋅ THENA Auto)
THEN ExRepD
THEN (D 2 With ⌜n - 1⌝ THENA Auto)
THEN D -1
THEN RenameVar `b' (-2)
THEN ExRepD
THEN Unfold `Legendre` 0
THEN (Subst' (n =z 0) ~ ff 0 THENA Auto)
THEN (Subst' (n =z 1) ~ ff 0 THENA Auto)
THEN Reduce 0
THEN D 0 With ⌜λi.if (i =z 0) then (1 - n * a i)/n
if i <z n - 1 then ((2 * n) - 1 * b (i - 1))/n - (n - 1 * a i)/n
else ((2 * n) - 1 * b (i - 1))/n
fi ⌝
THEN Reduce 0
THEN Auto)]
)]
)
) }
1
1. n : ℕ
2. ¬(n = 0 ∈ ℤ)
3. ¬(n = 1 ∈ ℤ)
4. a : ℕ(n - 2) + 1 ⟶ ℝ
5. ∀x:ℝ. (Legendre(n - 2;x) = (Σi≤n - 2. a_i * x^i))
6. (a (n - 2)) = (r(doublefact((2 * (n - 2)) - 1))/r((n - 2)!))
7. b : ℕ(n - 1) + 1 ⟶ ℝ
8. ∀x:ℝ. (Legendre(n - 1;x) = (Σi≤n - 1. b_i * x^i))
9. (b (n - 1)) = (r(doublefact((2 * (n - 1)) - 1))/r((n - 1)!))
10. x : ℝ
⊢ ((2 * n) - 1 * x * Legendre(n - 1;x) - n - 1 * Legendre(n - 2;x))/n
= (Σi≤n. λi.if (i =z 0) then (1 - n * a i)/n
if i <z n - 1 then ((2 * n) - 1 * b (i - 1))/n - (n - 1 * a i)/n
else ((2 * n) - 1 * b (i - 1))/n
fi _i * x^i)
2
1. n : ℕ
2. ¬(n = 0 ∈ ℤ)
3. ¬(n = 1 ∈ ℤ)
4. a : ℕ(n - 2) + 1 ⟶ ℝ
5. ∀x:ℝ. (Legendre(n - 2;x) = (Σi≤n - 2. a_i * x^i))
6. (a (n - 2)) = (r(doublefact((2 * (n - 2)) - 1))/r((n - 2)!))
7. b : ℕ(n - 1) + 1 ⟶ ℝ
8. ∀x:ℝ. (Legendre(n - 1;x) = (Σi≤n - 1. b_i * x^i))
9. (b (n - 1)) = (r(doublefact((2 * (n - 1)) - 1))/r((n - 1)!))
10. ∀x:ℝ
(((2 * n) - 1 * x * Legendre(n - 1;x) - n - 1 * Legendre(n - 2;x))/n
= (Σi≤n. λi.if (i =z 0) then (1 - n * a i)/n
if i <z n - 1 then ((2 * n) - 1 * b (i - 1))/n - (n - 1 * a i)/n
else ((2 * n) - 1 * b (i - 1))/n
fi _i * x^i))
⊢ if (n =z 0) then (1 - n * a n)/n
if n <z n - 1 then ((2 * n) - 1 * b (n - 1))/n - (n - 1 * a n)/n
else ((2 * n) - 1 * b (n - 1))/n
fi
= (r(doublefact((2 * n) - 1))/r((n)!))
Latex:
Latex:
\mforall{}n:\mBbbN{}
\mexists{}a:\mBbbN{}n + 1 {}\mrightarrow{} \mBbbR{}
((\mforall{}x:\mBbbR{}. (Legendre(n;x) = (\mSigma{}i\mleq{}n. a\_i * x\^{}i))) \mwedge{} ((a n) = (r(doublefact((2 * n) - 1))/r((n)!))))
By
Latex:
(CompleteInductionOnNat
THEN (CaseNat 0 `n'
THENL [(Reduce 0
THEN (D 0 With \mkleeneopen{}\mlambda{}i.r1\mkleeneclose{} THEN Auto)
THEN Reduce 0
THEN (RWO "rpolynomial\_unroll" 0 ORELSE nRNorm 0)
THEN Reduce 0
THEN Auto)
; (CaseNat 1 `n'
THENL [(Reduce 0
THEN (D 0 With \mkleeneopen{}\mlambda{}i.if (i =\msubz{} 1) then r1 else r0 fi \mkleeneclose{} THEN Auto)
THEN Reduce 0
THEN (RWO "rpolynomial\_unroll" 0
ORELSE ((Subst' (1)! \msim{} 1 0 THENA Auto) THEN nRNorm 0)
)
THEN Reduce 0
THEN Auto
THEN (RWO "rpolynomial\_unroll" 0 THEN Reduce 0)
THEN Auto
THEN RWO "rnexp1" 0
THEN Auto)
; ((InstHyp [\mkleeneopen{}n - 2\mkleeneclose{}] 2\mcdot{} THENA Auto)
THEN ExRepD
THEN (D 2 With \mkleeneopen{}n - 1\mkleeneclose{} THENA Auto)
THEN D -1
THEN RenameVar `b' (-2)
THEN ExRepD
THEN Unfold `Legendre` 0
THEN (Subst' (n =\msubz{} 0) \msim{} ff 0 THENA Auto)
THEN (Subst' (n =\msubz{} 1) \msim{} ff 0 THENA Auto)
THEN Reduce 0
THEN D 0 With \mkleeneopen{}\mlambda{}i.if (i =\msubz{} 0) then (1 - n * a i)/n
if i <z n - 1
then ((2 * n) - 1 * b (i - 1))/n - (n - 1 * a i)/n
else ((2 * n) - 1 * b (i - 1))/n
fi \mkleeneclose{}
THEN Reduce 0
THEN Auto)]
)]
)
)
Home
Index