Skip to content

Commit

Permalink
normedType on numFieldType
Browse files Browse the repository at this point in the history 
erasing ^o wip

Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
  • Loading branch information
@pi8027
mkerjean and pi8027 committed Nov 21, 2020
1 parent 41b3e54 commit 02447a1
Show file tree
Hide file tree
Showing 3 changed files with 1,228 additions and 122 deletions.
94 changes: 49 additions & 45 deletions theories/derive.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -167,8 +167,8 @@ Lemma differentiable_continuous (x : V) (f : V -> W) :
differentiable f x -> {for x, continuous f}.
Proof.
move=> /diff_locallyP [dfc]; rewrite -addrA.
rewrite (littleo_bigO_eqo (cst (1 : R^o))); last first.
apply/eqOP; near=> k; rewrite /cst [`|1 : R^o|]normr1 mulr1.
rewrite (littleo_bigO_eqo (cst (1 : R))); last first.
apply/eqOP; near=> k; rewrite /cst [`|1|]normr1 mulr1.
near=> y; rewrite ltW //; near: y; apply/nbhs_normP.
exists k; first by near: k; exists 0; rewrite real0.
by move=> ? /=; rewrite -ball_normE /= sub0r normrN.
Expand All @@ -180,10 +180,10 @@ Section littleo_lemmas.

Variables (X Y Z : normedModType R).

Lemma normm_littleo x (f : X -> Y) : `| [o_(x \near x) (1 : R^o) of f x]| = 0.
Lemma normm_littleo x (f : X -> Y) : `| [o_(x \near x) (1 : R) of f x]| = 0.
Proof.
rewrite /cst /=; have [e /(_ (`|e x|/2) _)/nbhs_singleton /=] := littleo.
rewrite pmulr_lgt0 // [`|1 : R^o|]normr1 mulr1 [X in X <= _]splitr.
rewrite pmulr_lgt0 // [`|1|]normr1 mulr1 [X in X <= _]splitr.
rewrite ger_addr pmulr_lle0 // => /implyP.
case : real_ltgtP; rewrite ?realE ?normrE //=.
by apply/orP; left.
Expand All @@ -205,8 +205,8 @@ Section diff_locally_converse_tentative.
(* indeed the differential being b *: idfun is locally bounded *)
(* and thus a littleo of 1, and so is id *)
(* This can be generalized to any dimension *)
Lemma diff_locally_converse_part1 (f : R^o -> R^o) (a : R^o) (b : R^o) (x : R^o) :
f \o shift x = cst a + b *: idfun +o_ (0 : [filteredType R^o of R^o]) id -> f x = a.
Lemma diff_locally_converse_part1 (f : R -> R) (a b x : R) :
f \o shift x = cst a + b *: idfun +o_ (0 : R) id -> f x = a.
Proof.
rewrite funeqE => /(_ 0) /=; rewrite add0r => ->.
by rewrite -[LHS]/(_ 0 + _ 0 + _ 0) /cst [X in a + X]scaler0 littleo_lim0 ?addr0.
Expand All @@ -215,13 +215,13 @@ Qed.
End diff_locally_converse_tentative.

Definition derive (f : V -> W) a v :=
lim ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ nbhs' (0 : R^o)).
lim ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ nbhs' 0).

Local Notation "''D_' v f" := (derive f ^~ v).
Local Notation "''D_' v f c" := (derive f c v). (* printing *)

Definition derivable (f : V -> W) a v :=
cvg ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ nbhs' (0 : R^o)).
cvg ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ nbhs' 0).

Class is_derive (a v : V) (f : V -> W) (df : W) := DeriveDef {
ex_derive : derivable f a v;
Expand All @@ -231,7 +231,7 @@ Class is_derive (a v : V) (f : V -> W) (df : W) := DeriveDef {
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 : [filteredType R^o of R^o])) id.
(fun h => h *: ('D_v f a)) +o_ (nbhs (0 :R)) id.
Proof.
move=> df; apply/eqaddoP => _/posnumP[e].
rewrite -nbhs_nearE nbhs_simpl /= nbhsE'; split; last first.
Expand All @@ -241,7 +241,7 @@ have /eqolimP := df; rewrite -[lim _]/(derive _ _ _).
move=> /eqaddoP /(_ e%:num) /(_ [gt0 of e%:num]).
apply: filter_app; rewrite /= !near_simpl near_withinE; near=> h => hN0.
rewrite /= opprD -![(_ + _ : _ -> _) _]/(_ + _) -![(- _ : _ -> _) _]/(- _).
rewrite /cst /= [`|1 : R^o|]normr1 mulr1 => dfv.
rewrite /cst /= [`|1|]normr1 mulr1 => dfv.
rewrite addrA -[X in X + _]scale1r -(@mulVf _ h) //.
rewrite mulrC -scalerA -scalerBr normmZ.
rewrite -ler_pdivl_mull; last by rewrite normr_gt0.
Expand All @@ -251,31 +251,31 @@ Grab Existential Variables. all: end_near. Qed.
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 : [filteredType R^o of R^o])) id.
(fun h => h *: ('D_v f a)) +o_ (nbhs (0 : R)) id.
Proof.
split; first exact: derivable_nbhs.
move=> df; apply/cvg_ex; exists ('D_v f a).
apply/(@eqolimP _ R^o _ (nbhs'_filter_on _))/eqaddoP => _/posnumP[e].
apply/(@eqolimP _ _ _ (nbhs'_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 : R^o|]normr1 mulr1 addrA => dfv hN0.
rewrite /cst /= [`|1|]normr1 mulr1 addrA => dfv hN0.
rewrite -[X in _ - X]scale1r -(@mulVf _ h) //.
rewrite -scalerA -scalerBr normmZ normfV ler_pdivr_mull ?normr_gt0 //.
by rewrite mulrC.
Grab Existential Variables. all: end_near. Qed.

Lemma derivable_nbhsx (f : V -> W) a v :
derivable f a v -> forall h, f (a + h *: v) = f a + h *: 'D_v f a
+o_(h \near (nbhs (0 : [filteredType R^o of R^o]))) h.
+o_(h \near (nbhs (0 : R))) h.
Proof.
move=> /derivable_nbhs; rewrite funeqE => df.
by apply: eqaddoEx => h; have /= := (df h); rewrite addrC => ->.
Qed.

Lemma derivable_nbhsxP (f : V -> W) a v :
derivable f a v <-> forall h, f (a + h *: v) = f a + h *: 'D_v f a
+o_(h \near (nbhs (0 : [filteredType R^o of R^o]))) h.
+o_(h \near (nbhs (0 :R))) h.
Proof.
split; first exact: derivable_nbhsx.
move=> df; apply/derivable_nbhsP; apply/eqaddoE; rewrite funeqE => h.
Expand All @@ -301,7 +301,7 @@ evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=; last first.
apply: cvg_map_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 _ _ [topologicalType of R^o]).
rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: cvgD.
rewrite -(scale1r (_ _ v)); apply: cvgZl => /= X [e e0].
rewrite /ball_ /= => eX.
apply/nbhs_ballP.
Expand Down Expand Up @@ -333,23 +333,23 @@ Section DifferentialR2.
Variable R : numFieldType.
Implicit Type (V : normedModType R).

Lemma derivemxE m n (f : 'rV[R]_m.+1 -> 'rV[R]_n.+1) (a v : 'rV[R^o]_m.+1) :
Lemma derivemxE m n (f : 'rV[R]_m.+1 -> 'rV[R]_n.+1) (a v : 'rV[R]_m.+1) :
differentiable f a -> 'D_ v f a = v *m jacobian f a.
Proof. by move=> /deriveE->; rewrite /jacobian mul_rV_lin1. Qed.

Definition derive1 V (f : R -> V) (a : R) :=
lim ((fun h => h^-1 *: (f (h + a) - f a)) @ nbhs' (0 : R^o)).
lim ((fun h => h^-1 *: (f (h + a) - f a)) @ nbhs' 0).

Local Notation "f ^` ()" := (derive1 f).

Lemma derive1E V (f : R -> V) a : f^`() a = 'D_1 (f : R^o -> _) a.
Lemma derive1E V (f : R -> V) a : f^`() a = 'D_1 f a.
Proof.
rewrite /derive1 /derive; set d := (fun _ : R => _); set d' := (fun _ : R => _).
by suff -> : d = d' by []; rewrite funeqE=> h; rewrite /d /d' /= [h%:A](mulr1).
Qed.

(* Is it necessary? *)
Lemma derive1E' V f a : differentiable (f : R^o -> V) a ->
Lemma derive1E' V f a : differentiable (f : R -> V) a ->
f^`() a = 'd f a 1.
Proof. by move=> ?; rewrite derive1E deriveE. Qed.

Expand Down Expand Up @@ -420,14 +420,14 @@ by rewrite -[(k *: f) _]/(_ *: _) diff_locallyx // !scalerDr scaleox.
Qed.

(* NB: could be generalized with K : absRingType instead of R; DONE? *)
Fact dscalel (k : V -> R^o) (f : W) x :
Fact dscalel (k : V -> R) (f : W) x :
differentiable k x ->
continuous (fun z : V => 'd k x z *: f) /\
(fun z => k z *: f) \o shift x =
cst (k x *: f) + (fun z => 'd k x z *: f) +o_ (0 : V) id.
Proof.
move=> df; split.
move=> ?; exact/continuousZl/(@diff_continuous _ _ [normedModType R of R^o]).
move=> ?; exact/continuousZl/diff_continuous.
apply/eqaddoE; rewrite funeqE => y /=.
by rewrite diff_locallyx //= !scalerDl scaleolx.
Qed.
Expand Down Expand Up @@ -484,7 +484,7 @@ Grab Existential Variables. all: end_near. Qed.
End DifferentialR3.

Section DifferentialR3_realFieldType.
Variable R : realFieldType.
Variable R : realFieldType. (*TODO : take ^o out, join with realField *)

Lemma littleo_linear0 (V W : normedModType R) (f : {linear V -> W}) :
(f : V -> W) =o_ (0 : V) id -> f = cst 0 :> (V -> W).
Expand Down Expand Up @@ -619,7 +619,7 @@ move=> dfx; apply: DiffDef; first exact: differentiableZ.
by rewrite diffZ // diff_val.
Qed.

Lemma diffZl (k : V -> R^o) (f : W) x : differentiable k x ->
Lemma diffZl (k : V -> R^o) (f : W) x : differentiable k x -> (*TODO: take ^o out*)
'd (fun z => k z *: f) x = (fun z => 'd k x z *: f) :> (_ -> _).
Proof.
move=> df; set g := RHS; have glin : linear g.
Expand Down Expand Up @@ -656,19 +656,19 @@ apply: DiffDef; first exact/linear_differentiable/scaler_continuous.
by rewrite diff_lin //; apply: scaler_continuous.
Qed.

Global Instance is_diff_scalel (x k : [filteredType R^o of R^o]) :
Global Instance is_diff_scalel (x k : R^o) :
is_diff k ( *:%R ^~ x) ( *:%R ^~ x).
Proof.
have -> : *:%R ^~ x = GRing.scale_linear [lmodType R of R^o] x.
have -> : *:%R ^~ x = GRing.scale_linear R x.
by rewrite funeqE => ? /=; rewrite [_ *: _]mulrC.
apply: DiffDef; first exact/linear_differentiable/scaler_continuous.
by rewrite diff_lin //; apply: scaler_continuous.
Qed.

Lemma differentiable_coord m n (M : 'M[R^o]_(m.+1, n.+1)) i j :
differentiable (fun N : 'M[R]_(m.+1, n.+1) => N i j : R^o) M.
Lemma differentiable_coord m n (M : 'M[R]_(m.+1, n.+1)) i j :
differentiable (fun N : 'M[R]_(m.+1, n.+1) => N i j : R^o ) M.
Proof.
have @f : {linear 'M[R]_(m.+1, n.+1) -> R^o}.
have @f : {linear 'M[R]_(m.+1, n.+1) -> R}.
by exists (fun N : 'M[R]_(_, _) => N i j); eexists; move=> ? ?; rewrite !mxE.
rewrite (_ : (fun _ => _) = f) //; exact/linear_differentiable/coord_continuous.
Qed.
Expand Down Expand Up @@ -821,18 +821,18 @@ Definition Rmult_rev (y x : R) := x * y.
Canonical rev_Rmult := @RevOp _ _ _ Rmult_rev (@GRing.mul [ringType of R])
(fun _ _ => erefl).

Lemma Rmult_is_linear x : linear (@GRing.mul [ringType of R] x : R^o -> R^o).
Lemma Rmult_is_linear x : linear (@GRing.mul [ringType of R] x : R -> R).
Proof. by move=> ???; rewrite mulrDr scalerAr. Qed.
Canonical Rmult_linear x := Linear (Rmult_is_linear x).

Lemma Rmult_rev_is_linear y : linear (Rmult_rev y : R^o -> R^o).
Lemma Rmult_rev_is_linear y : linear (Rmult_rev y : R -> R).
Proof. by move=> ???; rewrite /Rmult_rev mulrDl scalerAl. Qed.
Canonical Rmult_rev_linear y := Linear (Rmult_rev_is_linear y).

Canonical Rmult_bilinear :=
[bilinear of (@GRing.mul [ringType of [lmodType R of R^o]])].
[bilinear of (@GRing.mul [ringType of [lmodType R of R]])].

Global Instance is_diff_Rmult (p : [filteredType R^o * R^o of R^o * R^o]) :
Global Instance is_diff_Rmult (p : R*R ) :
is_diff p (fun q => q.1 * q.2) (fun q => p.1 * q.2 + q.1 * p.2).
Proof.
apply: DiffDef; last by rewrite diff_bilin // => ?; apply: mul_continuous.
Expand Down Expand Up @@ -890,15 +890,16 @@ move=> dfx dgx; apply: DiffDef; first exact: differentiable_pair.
by rewrite diff_pair // !diff_val.
Qed.

Global Instance is_diffM (f g df dg : V -> R^o) x :
Global Instance is_diffM (f g df dg : V -> R^o) x : (*TODO : ^o out *)
is_diff x f df -> is_diff x g dg -> is_diff x (f * g) (f x *: dg + g x *: df).
Proof.
move=> dfx dgx.
have -> : f * g = (fun p => p.1 * p.2) \o (fun y => (f y, g y)) by [].
(* TODO: type class inference should succeed or fail, not leave an evar *)
apply: is_diff_eq; do ?exact: is_diff_comp.
by rewrite funeqE => ?; rewrite /= [_ * g _]mulrC.
Qed.
have -> : f * g = (fun p => p.1 * p.2) \o (fun y => (f y, g y)) by [].
(* TODO: type class inference should succeed or fail, not leave an evar *)
apply: is_diff_eq; do ?exact: is_diff_comp. admit.
(* rewrite funeqE => ?; rewrite /= [_ * g _]mulrC. *)
(* Qed. *)
Admitted.

Lemma diffM (f g : V -> R^o) x :
differentiable f x -> differentiable g x ->
Expand Down Expand Up @@ -961,10 +962,10 @@ rewrite ler_subr_addr -ler_subr_addl (splitr `|x : R^o|).
by rewrite normrM normfV (@ger0_norm _ 2) // -addrA subrr addr0; apply: ltW.
Grab Existential Variables. all: end_near. Qed.

Lemma diff_Rinv (x : [filteredType R^o of R^o]) : x != 0 ->
'd GRing.inv x = (fun h => - x ^- 2 *: h) :> (R^o -> R^o).
Lemma diff_Rinv (x : R^o) : x != 0 ->
'd GRing.inv x = (fun h : R => - x ^- 2 *: h) :> (R^o -> R^o).
Proof.
move=> xn0; have -> : (fun h : R^o => - x ^- 2 *: h) =
move=> xn0; have -> : (fun h : R => - x ^- 2 *: h) =
GRing.scale_linear _ (- x ^- 2) by [].
by apply: diff_unique; have [] := dinv xn0.
Qed.
Expand Down Expand Up @@ -1388,12 +1389,13 @@ by rewrite ltr0_norm // addrC subrr.
Grab Existential Variables. all: end_near. Qed.

Lemma ler0_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T))
(FF : ProperFilter F) (f : T -> R^o) :
(FF : ProperFilter F) (f : T -> R) :
(\forall x \near F, f x <= 0) -> cvg (f @ F) -> lim (f @ F) <= 0.
Proof.
move=> fle0 fcv; rewrite -oppr_ge0.
have limopp : - lim (f @ F) = lim (- f @ F).
by apply: Logic.eq_sym; apply: cvg_map_lim => //; apply: cvgN.
apply: Logic.eq_sym; apply: cvg_map_lim; first by apply: Rhausdorff.
by apply: (@cvgN _ (regular_numFieldType_normedModType R)). (*TODO: simplify *)
rewrite limopp; apply: le0r_cvg_map; last by rewrite -limopp; apply: cvgN.
by move: fle0; apply: filterS => x; rewrite oppr_ge0.
Qed.
Expand All @@ -1405,7 +1407,9 @@ Lemma ler_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T)) (F
Proof.
move=> lefg fcv gcv; rewrite -subr_ge0.
have eqlim : lim (g @ F) - lim (f @ F) = lim ((g - f) @ F).
by apply/esym; apply: cvg_map_lim => //; apply: cvgD => //; apply: cvgN.
apply/esym; apply: cvg_map_lim => //; first by apply: Rhausdorff.
apply: (@cvgD _ ( (regular_numFieldType_normedModType R))) => //. (*TODO: simplify *)
by apply: cvgN.
rewrite eqlim; apply: le0r_cvg_map; last first.
by rewrite /(cvg _) -eqlim /=; apply: cvgD => //; apply: cvgN.
by move: lefg; apply: filterS => x; rewrite subr_ge0.
Expand Down
Loading

0 comments on commit 02447a1

Please sign in to comment.