proposition: Lemma derive1_at_max (R : realFieldType) (f : R -> R) (a b c : R) : a <= b -> (forall t, t \in `]a, b[%R -> derivable f t 1) -> c \in `]a, b[%R -> (forall t, t \in `]a, b[%R -> f t <= f c) -> is_derive c 1 f 0.
proof: Proof. move=> leab fdrvbl cab cmax; apply: DeriveDef; first exact: fdrvbl. apply/eqP; rewrite eq_le; apply/andP; split. rewrite ['D_1 f c]cvg_at_rightE; last exact: fdrvbl. apply: limr_le. have /fdrvbl dfc := cab. rewrite -(cvg_at_rightE (fun h : R => h^-1 *: ((f \o shift c) _ - f c))) //. apply: cvg_trans dfc; apply: cvg_app. move=> A [e egt0 Ae]; exists e => // x xe xgt0; apply: Ae => //. exact/lt0r_neq0. near=> h; apply: mulr_ge0_le0. by rewrite invr_ge0; apply: ltW; near: h; exists 1 => /=. rewrite subr_le0 [_%:A]mulr1; apply: cmax; near: h. exists (b - c); first by rewrite /= subr_gt0 (itvP cab). move=> h; rewrite /= distrC subr0 /= in_itv /= -ltrBrDr. move=> /(le_lt_trans (ler_norm _)) -> /ltr_pDl -> //. by rewrite (itvP cab). rewrite ['D_1 f c]cvg_at_leftE; last exact: fdrvbl. apply: limr_ge. have /fdrvbl dfc := cab; rewrite -(cvg_at_leftE (fun h => h^-1 *: ((f \o shift c) _ - f c))) //. apply: cvg_trans dfc; apply: cvg_app. move=> A [e egt0 Ae]; exists e => // x xe xgt0; apply: Ae => //. exact/ltr0_neq0. near=> h; apply: mulr_le0. by rewrite invr_le0; apply: ltW; near: h; exists 1 => /=. rewrite subr_le0 [_%:A]mulr1; apply: cmax; near: h. exists (c - a); first by rewrite /= subr_gt0 (itvP cab). move=> h; rewrite /= distrC subr0. move=> /ltr_normlP []; rewrite ltrBrDl ltrBlDl in_itv /= => -> _. by move=> /ltr_nDl -> //; rewrite (itvP cab). Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms