proposition: Lemma deriveE (f : V -> W) (a v : V) : differentiable f a -> 'D_v f a = 'd f a v.
proof: Proof. rewrite /derive => /diff_locally -> /=; set k := 'o _. evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=; last first. rewrite funeqE=> h; rewrite !scalerDr scalerN /cst /=. by rewrite addrC !addrA addNr add0r linearZ /= scalerA /g. apply: cvg_lim => //. pose g1 : R -> W := fun h => (h^-1 * h) *: 'd f a v. pose g2 : R -> W := fun h : R => h^-1 *: k (h *: v ). rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: cvgD. rewrite -(scale1r (_ _ v)); apply: cvgZl => /= X [e e0]. rewrite /ball_ /= => eX. apply/nbhs_ballP. by exists e => //= x _ x0; apply eX; rewrite mulVr // ?unitfE //= subrr normr0. rewrite /g2. have [/eqP ->|v0] := boolP (v == 0). rewrite (_ : (fun _ => _) = cst 0); first exact: cvg_cst. by rewrite funeqE => ?; rewrite scaler0 /k littleo_lim0 // scaler0. apply/cvgrPdist_lt => e e0. rewrite nearE /=; apply/nbhs_ballP. have /(littleoP [littleo of k]) /nbhs_ballP[i i0 Hi] : 0 < e / (2 * `|v|). by rewrite divr_gt0 // pmulr_rgt0 // normr_gt0. exists (i / `|v|); first by rewrite /= divr_gt0 // normr_gt0. move=> /= j; rewrite /ball /= /ball_ add0r normrN. rewrite ltr_pdivlMr ?normr_gt0 // => jvi j0. rewrite add0r normrN normrZ -ltr_pdivlMl ?normr_gt0 ?invr_neq0 //. have /Hi/le_lt_trans -> // : ball 0 i (j *: v). by rewrite -ball_normE/= add0r normrN (le_lt_trans _ jvi) // normrZ. rewrite -(mulrC e) -mulrA -ltr_pdivlMl // mulrA mulVr ?unitfE ?gt_eqF //. rewrite normrV ?unitfE // div1r invrK ltr_pdivrMl; last first. by rewrite pmulr_rgt0 // normr_gt0. rewrite normrZ mulrC -mulrA. by rewrite ltr_pMl ?ltr1n // pmulr_rgt0 ?normm_gt0 // normr_gt0. 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