proposition: Lemma bnd_imp_Taylor_bnd : forall (f : nat -> PartIR) (F : PartIR), (forall n x Hx Hx', AbsIR (f n x Hx) [<=] AbsIR (F x Hx')) -> Continuous realline F -> (forall n, included (fun _ => True) (Dom (f n))) -> Taylor_bnd f.
proof: Proof. intros f F H H0 H1. apply Taylor_bnd_trans with (fun n : nat => F); auto. red in |- *; intros. unfold Fscalmult in |- *. apply conv_fun_seq'_wdr'_IR with (contF := Continuous_mult _ _ _ (Continuous_const _ [0]) H0). FEQ. apply fun_Lim_seq_mult'_IR with (f := fun n : nat => [-C-] (r[^]n[/] _[//]nring_fac_ap_zero _ n)) (contf := fun n : nat => Continuous_const realline (r[^]n[/] _[//]nring_fac_ap_zero _ n)) (g := fun n : nat => F) (contg := fun n : nat => H0) (contF := Continuous_const realline [0]) (contG := H0). apply convergence_lemma. apply fun_Lim_seq_const_IR. Qed.
imports: CoRN.transc.PowerSeries CoRN.ftc.Taylor