proposition: Lemma derivable_nbhs (f : V -> W) a v : derivable f a v -> (fun h => (f \o shift a) (h *: v)) = (cst (f a)) + (fun h => h *: ('D_v f a)) +o_ (nbhs (0 :R)) id.
proof: Proof. move=> df; apply/eqaddoP => _/posnumP[e]. rewrite -nbhs_nearE nbhs_simpl /= dnbhsE; split; last first. rewrite /at_point opprD -![(_ + _ : _ -> _) _]/(_ + _) scale0r add0r. by rewrite addrA subrr add0r normrN scale0r !normr0 mulr0. have /eqolimP := df. move=> /eqaddoP /(_ e%:num) /(_ [gt0 of e%:num]). apply: filter_app; rewrite /= !near_simpl near_withinE; near=> h => hN0. rewrite /= opprD -![(_ + _ : _ -> _) _]/(_ + _) -![(- _ : _ -> _) _]/(- _). rewrite /cst /= [`|1|]normr1 mulr1 => dfv. rewrite addrA -[X in X + _]scale1r -(@mulVf _ h) //. rewrite mulrC -scalerA -scalerBr normrZ. rewrite -ler_pdivlMl; last by rewrite normr_gt0. by rewrite mulrCA mulVf ?mulr1; last by rewrite normr_eq0. 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