proposition: Lemma diff_unique (V W : normedModType R) (f : V -> W) (df : {linear V -> W}) x : continuous df -> f \o shift x = cst (f x) + df +o_ (0 : V) id -> 'd f x = df :> (V -> W).
proof: Proof. move=> dfc dxf; apply/subr0_eq; rewrite -[LHS]/(_ \- _). apply/littleo_linear0/eqoP/eq_some_oP => /=; rewrite funeqE => y /=. have hdf h : (f \o shift x = cst (f x) + h +o_ (0 : V) id) -> h = f \o shift x - cst (f x) +o_ (0 : V) id. move=> hdf; apply: eqaddoE. rewrite hdf addrAC -!addrA addrC !addrA subrK. rewrite -[LHS]addr0 -addrA; congr (_ + _). by apply/eqP; rewrite eq_sym addrC addr_eq0 oppo. rewrite (hdf _ dxf). suff /diff_locally /hdf -> : differentiable f x. by rewrite opprD addrCA -(addrA (_ - _)) addKr oppox addox. apply/diffP => /=. apply: (@getPex _ (fun (df : {linear V -> W}) => continuous df /\ forall y, f y = f (lim (nbhs x)) + df (y - lim (nbhs x)) +o_(y \near x) (y - lim (nbhs x)))). exists df; split=> //; apply: eqaddoEx => z. rewrite (hdf _ dxf) !addrA lim_id // /(_ \o _) /= subrK [f _ + _]addrC addrK. rewrite -addrA -[LHS]addr0; congr (_ + _). apply/eqP; rewrite eq_sym addrC addr_eq0 oppox; apply/eqP. by rewrite littleo_center0 (comp_centerK x id) -[- _ in RHS](comp_centerK x). 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