proposition: Theorem Zumkeller_monot_rem (x0 : R) (n : nat) : dom x0 -> Rcst_sign dom (Dn n.+1) -> Rmonot (fun t => dom t /\ (t <= x0)%R) (Rdelta n x0) /\ Rmonot (fun t => dom t /\ (x0 <= t)%R) (Rdelta n x0).
proof: Proof. move=> Hx0. case: n =>[|nm1] ; last set n := nm1.+1. move=> Hsign; split; apply (@Rderive_cst_sign _ _ (Dn 1)) =>//. - apply: connected_and => //. exact: connected_le. - move=> x [Hx1 Hx2]. rewrite -[Dn 1 x]Rminus_0_r. apply: is_derive_minus. apply: Derive_correct. exact: (Hder_n 1). auto_derive. exact: PolR.ex_derive_horner. rewrite Rmult_1_l (Derive_ext _ (fun r => PolR.nth (P x0 0) 0)). by rewrite Derive_const. by move=> r; rewrite PolR.hornerE Poly_size big_nat1 pow_O Rmult_1_r. - case: Hsign => Hsign; [left|right]; move: Hsign; rewrite /Rpos_over /Rneg_over. + move=> Htop x [Hx1 Hx2]; exact: Htop. + move=> Htop x [Hx1 Hx2]; exact: Htop. - apply: connected_and => //. exact: connected_ge. - move=> x [Hx1 Hx2]. rewrite -[Dn 1 x]Rminus_0_r. apply: is_derive_minus. apply: Derive_correct. exact: (Hder_n 1). auto_derive. exact: PolR.ex_derive_horner. rewrite Rmult_1_l (Derive_ext _ (fun r => PolR.nth (P x0 0) 0)). by rewrite Derive_const. by move=> r; rewrite PolR.hornerE Poly_size big_nat1 pow_O Rmult_1_r. case: Hsign => Hsign; [left|right]; move: Hsign; rewrite /Rpos_over /Rneg_over. + move=> Htop x [Hx1 Hx2]; exact: Htop. + move=> Htop x [Hx1 Hx2]; exact: Htop. have TL := @ITaylor_Lagrange (fun x => Xreal (Derive f0 x)) dom Hdom n.-1 _ x0 _ Hx0. case=>[Hpos|Hneg]. split. apply: (@Rderive_cst_sign _ _ (Rdelta' n x0)) =>//. * apply: connected_and => //. exact: connected_le. * apply: Rderive_delta => //. exact: Rle_refl. { have [Heven|Hodd] := (Z.Even_or_Odd (Z_of_nat nm1.+1)). - left. move=> x [Hx1 Hx2]. have [||c [H1 [H2 H3]]] := TL _ x =>//. move=> k t Ht. case: k => [//|k]; rewrite -ex_derive_nSS. exact: (Hder_n k.+2). rewrite /Rdelta' PolR.horner_derivE Poly_size. rewrite bigXadd'_P //; last exact/Hder_n. set b := \big[Rplus/R0]_(_ <= i < _) _. set b2 := \big[Rplus/R0]_(_ <= i < _) _ in H2. have->: b = b2 by apply: eq_bigr => i _; rewrite -Derive_nS. rewrite /b /b2 H2 -Derive_nS. exact: (@lower_even_Rpos_over c x0 nm1). - right. move=> x [Hx1 Hx2]. have [||c [H1 [H2 H3]]] := TL _ x =>//. move=> k t Ht. case: k => [//|k]; rewrite -ex_derive_nSS. exact: (Hder_n k.+2). rewrite /Rdelta' PolR.horner_derivE Poly_size. rewrite bigXadd'_P //; last exact/Hder_n. set b := \big[Rplus/R0]_(_ <= i < _) _. set b2 := \big[Rplus/R0]_(_ <= i < _) _ in H2. have->: b = b2 by apply: eq_bigr => i _; rewrite -Derive_nS. rewrite /b /b2 H2 -Derive_nS. exact: (@lower_odd_Rpos_over c x0 nm1). } apply: (@Rderive_cst_sign _ _ (Rdelta' n x0)) =>//. * apply: connected_and => //. exact: connected_ge. * apply: Rderive_delta => //. exact: Rle_refl. left. move=> x [Hx1 Hx2]. have [||c [H1 [H2 H3]]] := TL _ x =>//. move=> k t Ht. case: k => [//|k]; rewrite -ex_derive_nSS. exact: (Hder_n k.+2). rewrite /Rdelta' PolR.horner_derivE Poly_size. rewrite bigXadd'_P //; last exact/Hder_n. set b := \big[Rplus/R0]_(_ <= i < _) _. set b2 := \big[Rplus/R0]_(_ <= i < _) _ in H2. have->: b = b2 by apply: eq_bigr => i _; rewrite -Derive_nS. rewrite /b /b2 H2 -Derive_nS. exact: (@upper_Rpos_over c x0 nm1). split. apply: (@Rderive_cst_sign _ _ (Rdelta' n x0)) =>//. * apply: connected_and => //. exact: connected_le. * apply: Rderive_delta => //. exact: Rle_refl. { have [Heven|Hodd] := (Z.Even_or_Odd (Z_of_nat nm1.+1)). - right. move=> x [Hx1 Hx2]. have [||c [H1 [H2 H3]]] := TL _ x =>//. move=> k t Ht. case: k => [//|k]; rewrite -ex_derive_nSS. exact: (Hder_n k.+2). rewrite /Rdelta' PolR.horner_derivE Poly_size. rewrite bigXadd'_P //; last exact/Hder_n. set b := \big[Rplus/R0]_(_ <= i < _) _. set b2 := \big[Rplus/R0]_(_ <= i < _) _ in H2. have->: b = b2 by apply: eq_bigr => i _; rewrite -Derive_nS. rewrite /b /b2 H2 -Derive_nS. exact: (@lower_even_Rneg_over c x0 nm1). - left. move=> x [Hx1 Hx2]. have [||c [H1 [H2 H3]]] := TL _ x =>//. move=> k t Ht. case: k => [//|k]; rewrite -ex_derive_nSS. exact: (Hder_n k.+2). rewrite /Rdelta' PolR.horner_derivE Poly_size. rewrite bigXadd'_P //; last exact/Hder_n. set b := \big[Rplus/R0]_(_ <= i < _) _. set b2 := \big[Rplus/R0]_(_ <= i < _) _ in H2. have->: b = b2 by apply: eq_bigr => i _; rewrite -Derive_nS. rewrite /b /b2 H2 -Derive_nS. exact: (@lower_odd_Rneg_over c x0 nm1). } apply: (@Rderive_cst_sign _ _ (Rdelta' n x0)) =>//. * apply: connected_and => //. exact: connected_ge. * apply: Rderive_delta => //. exact: Rle_refl. right. move=> x [Hx1 Hx2]. have [||c [H1 [H2 H3]]] := TL _ x =>//. move=> k t Ht. case: k => [//|k]; rewrite -ex_derive_nSS. exact: (Hder_n k.+2). rewrite /Rdelta' PolR.horner_derivE Poly_size. rewrite bigXadd'_P //; last exact/Hder_n. set b := \big[Rplus/R0]_(_ <= i < _) _. set b2 := \big[Rplus/R0]_(_ <= i < _) _ in H2. have->: b = b2 by apply: eq_bigr => i _; rewrite -Derive_nS. rewrite /b /b2 H2 -Derive_nS. exact: (@upper_Rneg_over c x0 nm1). Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound