proposition: Lemma derivable_nbhsP (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. split; first exact: derivable_nbhs. move=> df; apply/cvg_ex; exists ('D_v f a). apply/(@eqolimP _ _ _ (dnbhs_filter_on _))/eqaddoP => _/posnumP[e]. have /eqaddoP /(_ e%:num) /(_ [gt0 of e%:num]) := df. rewrite /= !(near_simpl, near_withinE); apply: filter_app; near=> h. rewrite /= opprD -![(_ + _ : _ -> _) _]/(_ + _) -![(- _ : _ -> _) _]/(- _). rewrite /cst /= [`|1|]normr1 mulr1 addrA => dfv hN0. rewrite -[X in _ - X]scale1r -(@mulVf _ h) //. rewrite -scalerA -scalerBr normrZ normfV ler_pdivrMl ?normr_gt0 //. by rewrite mulrC. 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