power_series_deriv: THEORY %---------------------------------------------------------------------------- % % Term by term differentiation of power series % % Author: Ricky W. Butler 10/2/00 % % %---------------------------------------------------------------------------- BEGIN IMPORTING power_series x,r,y: VAR real c: VAR posreal x1,z: VAR nonzero_real n: VAR nat a: VAR sequence[real] S: VAR set[real] k,ii: VAR nat t: VAR real epsilon: VAR posreal deriv_prep: AXIOM EXISTS (N: posnat): FORALL (k: nat): k >= N AND abs(k*t^(k-1)) <= (abs(t) + epsilon)^k deriv_powerseries_conv: THEOREM (FORALL x: convergent(powerseries(a,x))) IMPLIES (FORALL x: convergent((series(LAMBDA (k: nat): IF k = 0 THEN 0 ELSE k*a(k)*x^(k-1) ENDIF)))) analysis: LIBRARY = "../analysis" IMPORTING analysis@derivatives deriv_lim_funs: AXIOM % Proof relies on fundamental theorem of calculus FORALL (ff: [nat -> [real -> real]]): (FORALL x: convergent(LAMBDA n: ff(n)(x))) AND (FORALL n: derivable(ff(n))) AND (FORALL x:convergent(LAMBDA n: deriv[real](ff(n))(x))) AND (FORALL n: continuous(deriv(ff(n)))) IMPLIES derivable[real](LAMBDA x: limit(LAMBDA n: ff(n)(x))) AND deriv(LAMBDA x: limit(LAMBDA n: ff(n)(x))) = (LAMBDA x: limit(LAMBDA n: deriv(ff(n))(x))) % ----------------------- convergence everywhere ------------------------- h: VAR nzreal H: VAR [nzreal -> real] f,g: VAR [real -> real] derivseq(a): sequence[real] = (LAMBDA (k: nat): (k+1)*a(k+1)) deriv_powerseq(a,x): sequence[real] = (LAMBDA (k: nat): IF k = 0 THEN 0 ELSE k*a(k)*x^(k-1) ENDIF) derivseq_conv: LEMMA (FORALL x: convergent(powerseries(a, x))) IMPLIES convergent(series(powerseq(derivseq(a),x))) deriv_series_shift: LEMMA (FORALL x: convergent(powerseries(a,x))) % IMPLIES limit(series(deriv_powerseq(a,x))) = limit(series(powerseq(derivseq(a),x))) deriv_powerseq_lem: LEMMA derivable(LAMBDA x: powerseq(a, x)(n)) AND deriv(LAMBDA x: powerseq(a, x)(n)) = (LAMBDA x: deriv_powerseq(a,x)(n)) sigma_power_derivable: LEMMA derivable(LAMBDA x: sigma(0,n,powerseq(a,x))) deriv_sigma_power: LEMMA deriv(LAMBDA x: sigma(0, n, powerseq(a, x))) = (LAMBDA x: sigma(0, n, deriv_powerseq(a,x))) deriv_sigma_power_conv: LEMMA (FORALL x: convergent(powerseries(a, x))) IMPLIES convergent(LAMBDA (n: nat): deriv(LAMBDA x: sigma(0, n, powerseq(a, x)))(x)) deriv_conv_prep: LEMMA (FORALL x: convergent(powerseries(a, x))) IMPLIES convergent(LAMBDA (n: nat): sigma(0, n, deriv_powerseq(a,x))) x_to_n_continuous: LEMMA continuous(LAMBDA x: x^n) deriv_powerseq_cont: LEMMA continuous(LAMBDA x: sigma(0,n,deriv_powerseq(a,x))) % ------------------------- main results ------------------------- powerseries_derivable: THEOREM (FORALL x: convergent(powerseries(a, x))) IMPLIES derivable(LAMBDA (xx: real): limit(powerseries(a, xx))) deriv_inf_series: THEOREM (FORALL x: convergent(powerseries(a,x))) IMPLIES ( LET f = (LAMBDA x: limit(powerseries(a,x))) IN LET g = (LAMBDA x: limit(series(deriv_powerseq(a,x)))) IN g = deriv(f) ) deriv_inf_series_shift: THEOREM (FORALL x: convergent(powerseries(a,x))) IMPLIES deriv(LAMBDA x: limit(powerseries(a,x))) = (LAMBDA x: limit(powerseries(derivseq(a),x))) deriv_powerseries_derivable: THEOREM (FORALL x: convergent(powerseries(a,x))) IMPLIES derivable(deriv(LAMBDA x: limit(powerseries(a,x)))) IMPORTING nth_derivatives powerseries_derivable_n_times: LEMMA (FORALL x: convergent(powerseries(a,x))) IMPLIES derivable_n_times((LAMBDA x: limit(powerseries(a,x))),n) END power_series_deriv