proposition: Lemma ex_antiderive_segm (U : C -> Prop) (z0 : C) (f : C -> C) : open U -> is_starred U z0 -> continuous_on U f -> (forall z1 z2 : C, U z1 -> U z2 -> (forall z, complex_segment z1 z2 z -> U z) -> C_RInt_segm f z0 z1 + C_RInt_segm f z1 z2 + C_RInt_segm f z2 z0 = 0) -> forall z, U z -> is_derive (C_RInt_segm f z0) z (f z).
proof: Proof. intros oU sU Cf Hf. assert (forall z, U z -> locally z (ex_C_RInt_segm f z)). intros z Hz. move: (locally_C_segm _ _ (oU z Hz)). apply filter_imp => y Hy. apply ex_C_RInt_segm_continuous. intros z1 Hz1. apply continuous_continuous_on with U => //. by apply oU, Hy. intros z Hz. split. by apply @is_linear_scal_l. simpl => x Hx eps. change norm with Cmod ; change minus with Cminus. replace x with z. 2: by apply @is_filter_lim_locally_unique in Hx. clear x Hx. eapply filter_imp. intros x Hx. rewrite {2}/Cminus C_RInt_segm_swap Cplus_comm. replace (C_RInt_segm f z z0 + C_RInt_segm f z0 x) with ((C_RInt_segm f z0 x + C_RInt_segm f x z + C_RInt_segm f z z0) + - (C_RInt_segm f x z)) by ring. rewrite Hf => //. rewrite C_RInt_segm_swap. move: (@plus_zero_l _ (C_RInt_segm f z x)). change plus with Cplus ; change zero with (RtoC 0). move => ->. eapply (proj1 Hx). eapply (proj1 (proj2 Hx)). apply (proj2 (proj2 Hx)). repeat apply filter_and. 2: by apply locally_C, (oU z). eapply filter_imp. intros x Hx. change scal with Cmult ; rewrite -C_RInt_segm_const. rewrite -C_RInt_segm_minus. 2: eapply (proj1 Hx). rewrite -(Cmod_opp (_-_)). move: (opp_minus (G := C_AbelianGroup)). change opp with Copp ; change minus with Cminus. move => ->. apply is_C_RInt_segm_norm with (fun z1 : C => f z1 - f z). apply C_RInt_segm_correct. apply ex_C_RInt_segm_minus. by apply Hx. by apply ex_C_RInt_segm_const. apply (proj2 Hx). apply ex_C_RInt_segm_const. apply filter_and. by apply locally_C, H. apply locally_C. assert (He : 0 < eps / (norm_factor (V := C_NormedModule))). apply Rdiv_lt_0_compat. by apply eps. by apply norm_factor_gt_0. set (e := mkposreal _ He). destruct (proj1 (filterlim_locally _ _) (continuous_continuous_on _ _ z (oU z Hz) Cf) e) as [d Hd]. exists d => /= y Hy x Hx. replace (pos eps) with ((norm_factor (V := C_NormedModule)) * e)%R. apply Rlt_le, (norm_compat2 (V := C_NormedModule)). apply Hd. case: Hx => {x} x [Hx ->]. split. rewrite /ball /= /AbsRing_ball. change minus with Rminus ; change abs with Rabs. change scal with Rmult ; replace ((1 - x) * fst z + x * fst y - fst z)%R with (x * (fst y - fst z))%R by ring. rewrite Rabs_mult. eapply Rle_lt_trans, (proj1 Hy). rewrite -(Rmult_1_l (abs _)). apply Rmult_le_compat_r. by apply abs_ge_0. rewrite Rabs_pos_eq ; apply Hx. rewrite /ball /= /AbsRing_ball. change minus with Rminus ; change abs with Rabs. change scal with Rmult ; replace ((1 - x) * snd z + x * snd y - snd z)%R with (x * (snd y - snd z))%R by ring. rewrite Rabs_mult. eapply Rle_lt_trans, (proj2 Hy). rewrite -(Rmult_1_l (abs _)). apply Rmult_le_compat_r. by apply abs_ge_0. rewrite Rabs_pos_eq ; apply Hx. rewrite /e /= ; field. by apply Rgt_not_eq, norm_factor_gt_0. apply locally_C. move: (locally_C_segm _ _ (oU z Hz)). apply filter_imp ; intros. by apply H0, complex_segment_swap. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)