proposition: Lemma Derive_n_comp_scal (f : R -> R) (a : R) (n : nat) (x : R) : locally (a * x) (fun x => forall k, (k <= n)%nat -> ex_derive_n f k x) -> Derive_n (fun y => f (a * y)) n x = (a ^ n * Derive_n f n (a * x)).
proof: Proof. case: (Req_dec a 0) => [ -> _ | Ha] /=. rewrite Rmult_0_l. elim: n x => [ | n IH] x /= ; rewrite ?Rmult_0_l. ring. rewrite (Derive_ext _ _ _ IH). by apply Derive_const. move => Hf. apply (locally_singleton _ (fun x => Derive_n (fun y : R => f (a * y)) n x = a ^ n * Derive_n f n (a * x))). elim: n Hf => [ | n IH] Hf. apply filter_forall => /= y ; ring. case: IH => [ | r IH]. case: Hf => r0 Hf. exists r0 => y Hy k Hk ; by intuition. case: Hf => r0 Hf. have Hr1 : 0 < Rmin (r0 / (Rabs a)) r. apply Rmin_case. apply Rdiv_lt_0_compat. by apply r0. by apply Rabs_pos_lt. by apply r. set r1 := mkposreal _ Hr1. exists r1 => y Hy /=. rewrite (Derive_ext_loc _ (fun y => a ^ n * Derive_n f n (a * y))). rewrite Derive_scal. rewrite (Rmult_comm a (a^n)) Rmult_assoc. apply f_equal. rewrite Derive_comp. rewrite (Derive_ext (Rmult a) (fun x => a * x)) => //. rewrite Derive_scal Derive_id ; ring. apply Hf with (k := S n). rewrite /ball /= /AbsRing_ball /= /abs /minus /plus /opp /=. rewrite -/(Rminus _ _) -Rmult_minus_distr_l Rabs_mult. apply Rlt_le_trans with (Rabs a * r1). apply Rmult_lt_compat_l. by apply Rabs_pos_lt. by apply Hy. rewrite Rmult_comm ; apply Rle_div_r. by apply Rabs_pos_lt. rewrite /r1 ; by apply Rmin_l. by apply Nat.lt_succ_diag_r. apply ex_derive_scal. by apply ex_derive_id. rewrite /ball /= /AbsRing_ball /= in Hy. apply Rabs_lt_between' in Hy. case: Hy => Hy1 Hy2. apply Rlt_Rminus in Hy1. apply Rlt_Rminus in Hy2. have Hy : 0 < Rmin (y - (x - r1)) (x + r1 - y). by apply Rmin_case. exists (mkposreal (Rmin (y - (x - r1)) (x + r1 - y)) Hy). set r2 := Rmin (y - (x - r1)) (x + r1 - y). move => t Ht. apply IH. apply Rabs_lt_between'. rewrite /ball /= /AbsRing_ball /= in Ht. apply Rabs_lt_between' in Ht. simpl in Ht. split. apply Rle_lt_trans with (2 := proj1 Ht). rewrite /r2 ; apply Rle_trans with (y-(y-(x-r1))). ring_simplify ; apply Rplus_le_compat_l, Ropp_le_contravar. rewrite /r1 ; apply Rmin_r. apply Rplus_le_compat_l, Ropp_le_contravar, Rmin_l. apply Rlt_le_trans with (1 := proj2 Ht). rewrite /r2 ; apply Rle_trans with (y+((x+r1)-y)). apply Rplus_le_compat_l, Rmin_r. ring_simplify ; apply Rplus_le_compat_l. rewrite /r1 ; apply Rmin_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv