new derive.v lemmas

CHANGELOG_UNRELEASED.md

@@ -126,6 +126,8 @@
 
 - in `filter.v`:
   + mixin `isSubNbhs`, structure `SubNbhs`, notation `subNbhsType`
+  + new lemmas `near_eq_cvgE`, `near_eq_is_cvg`, `near_eq_lim`, 
+    `cvg_to_eq`, `cvg_to_withinP`, and `within_cvg_to_within`.
 
 - in `topology_structure.v`:
   + structure `SubTopological`, notation `subTopologicalType`
@@ -234,6 +236,19 @@
 - in `measurable_structure.v`:
   + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable`
 
+- in file `normed_module.v`,
+  + new lemmas `cvg1MC`, `cvg1M`, `cvgCM1`, `cvgM1`, `cvg0MC`, `cvg0M`, 
+    `cvgCM0`, and `cvgM0`.
+- in file `pseudometric_normed_Zmodule.v`,
+  + new lemmas `cvgDl`, `cvgDr`, `cvgBl`, `cvgBr`, `cvg0D`, `cvg0DC`, 
+    `cvgD0`, `cvgCD0`, `cvg0B`, `cvg0BC`, `cvgB0`, `cvgCB0`, and `cvgN0`.
+
+- in `derive.v`
+  + new lemmas `derive1Dn`, `der1_scaleLR`, `deriveZLR`, `derivableZLR`, 
+    `derivable_shiftf`, `derive_shiftf`, `is_derive_shiftf`, `derive1_shiftf`, 
+    `near_eq_derive1n_near`, `near_eq_derive1_near`, `near_eq_derive1n`, and 
+    `near_eq_derive1`.
+
 ### Changed
 
 - in `realsum.v`:
@@ -354,6 +369,9 @@
 - in `classical_sets.v`
   + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`)
 
+- moved from `realfun.v` to `derive.v`: 
+  + lemmas `is_deriveV`, `is_derive1_comp`.
+
 ### Renamed
 
 - in `tvs.v`:

classical/filter.v

@@ -925,10 +925,23 @@ Lemma near_eq_cvg {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) :
   {near F, f =1 g} -> g @ F `=>` f @ F.
 Proof. by move=> eq_fg P /=; apply: filterS2 eq_fg => x /= <-. Qed.
 
+Lemma near_eq_cvgE {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) :
+  {near F, f =1 g} -> f @ F = g @ F.
+Proof.
+move=> eq_fg.
+apply/seteqP; split; apply: near_eq_cvg => //.
+by near do symmetry.
+Unshelve. all: by end_near.
+Qed.
+
 Lemma eq_cvg (T T' : Type) (F : set_system T) (f g : T -> T') (x : set_system T') :
   f =1 g -> (f @ F --> x) = (g @ F --> x).
 Proof. by move=> /funext->. Qed.
 
+Lemma near_eq_is_cvg (T : Type) (T' : pnbhsType) (F : set_system T) (f g : T -> T') : 
+  Filter F -> {near F, g =1 f} -> cvg (f x @[x --> F]) -> cvg(g x @[x --> F]).
+Proof. by move=> /@near_eq_cvgE /[apply] ->. Qed.
+
 Lemma eq_is_cvg_in (T T' : Type) (fT : pfilteredType T') (F : set_system T) (f g : T -> T') :
   f =1 g -> [cvg (f @ F) in fT] = [cvg (g @ F) in fT].
 Proof. by move=> /funext->. Qed.
@@ -937,6 +950,14 @@ Lemma eq_is_cvg (T : Type) (T' : pnbhsType) (F : set_system T) (f g : T -> T') :
   f =1 g -> cvg (f @ F) = cvg (g @ F).
 Proof. by move=> /funext->. Qed.
 
+Lemma near_eq_lim (T : Type) (T' : pnbhsType) {F : set_system T} {FF : Filter F} (f g : T -> T') :
+  {near F, f =1 g} -> lim (f @ F) = lim (g @ F).
+Proof. by move=> /near_eq_cvgE ->. Qed.
+
+Lemma cvg_to_eq {T : nbhsType} {F : set_system T} (l l' : T) :
+  F --> l' -> l = l' -> F --> l.
+Proof. by move=> + ->. Qed.
+
 Lemma neari_eq_loc {T U} {F : set_system T} {FF : Filter F} (f g : T -> set U) :
   {near F, f =2 g} -> g `@ F `=>` f `@ F.
 Proof.
@@ -1197,6 +1218,25 @@ Qed.
 
 End within.
 
+Lemma cvg_to_withinP (T U : Type) {F : set_system T} {FF : Filter F} {G : set_system U} {FG : Filter G} 
+    (f : T -> U) (A : set U) :
+  (f @ F --> within A G) <-> (f @ F --> G /\ \forall x \near F, A (f x)).
+Proof.
+split.
+  move=> cvg_w; split.
+  - apply: (cvg_trans cvg_w).
+    exact: cvg_within.
+  - apply: cvg_w.
+    exact: withinT.
+move=> [cvgT nearfA] P. 
+rewrite !nbhs_nearE near_withinE.
+move: cvgT => /[apply].
+rewrite near_map appfilter nbhs_nearE => nearF_AP.
+near=> x.
+suff : A (f x) by near: x.
+by near: x.
+Unshelve. all: by end_near. Qed.
+
 Global Instance within_filter T D F : Filter F -> Filter (@within T D F).
 Proof.
 move=> FF; rewrite /within; constructor => /=.
@@ -1210,6 +1250,18 @@ Qed.
 Canonical within_filter_on T D (F : filter_on T) :=
   FilterType (within D F) (within_filter _ _).
 
+Lemma within_cvg_to_within (T U : Type) {F : set_system T} {FF : Filter F} {G : set_system U} {FG : Filter G}
+    (f : T -> U) (A : set T) (B : set U) :
+  (\forall x \near F, A x -> B (f x)) -> f @ F --> G -> f @ within A F --> within B G.
+Proof.
+move=> near_hom cvgT.
+apply/cvg_to_withinP; split.
+- apply: cvg_trans cvgT.
+  apply: cvg_app.
+  exact: cvg_within.
+- by rewrite near_withinE.
+Qed. 
+
 Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T)
   (F : set_system T) (P : set T) :
   Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) ->

theories/derive.v

@@ -408,6 +408,9 @@ Proof. by []. Qed.
 Lemma derive1Sn V (f : R -> V) n : f^`(n.+1) = f^`()^`(n).
 Proof. exact: iterSr. Qed.
 
+Lemma derive1Dn V (f : R -> V) (i j : nat) : f^`(i + j) = f^`(j)^`(i).
+Proof. by rewrite /derive1n iterD. Qed.
+
 End DifferentialR2.
 Notation "f ^` ()" := (derive1 f) : classical_set_scope.
 Notation "f ^` ( n )" := (derive1n n f) : classical_set_scope.
@@ -1254,6 +1257,58 @@ move=> dfx; apply: DeriveDef; first exact: derivableZ.
 by rewrite deriveZ // derive_val.
 Qed.
 
+Lemma der1_scaleLR (k : R -> R) (f : R -> V) (x : R) :
+  derivable k x 1 -> derivable f x 1 ->
+  h^-1 *: (((fun x0 : R => k x0 *: f x0) \o  shift x) h%:A - k x *: f x) 
+  @[h --> 0^'] --> 'D_1 k x *: f x + k x *: 'D_1 f x.
+Proof.
+move=> der_k der_f.
+rewrite /comp/=.
+apply: cvg_trans.
+  apply: near_eq_cvg.
+  near=> h.
+  rewrite -[X in _ = _ *: X](addrKA (- (k x *: f (h%:A + x)))) opprD opprK.
+  rewrite -scalerBl -scalerBr scalerDr [in X in _ = X + _]scalerA.
+  by rewrite scalerA (mulrC h^-1 (k x)) -[in X in _ = _ + X]scalerA.
+apply: cvgD.
+- apply: cvgZ; first exact: der_k.
+  apply: (cvg_comp _ _ (G := nbhs x)).
+  + apply: cvg0DC.
+    apply: cvg0MC.
+    by apply: cvg_within_filter.
+  + change (continuous_at x f).
+    by apply/differentiable_continuous/derivable1_diffP.
+- apply: cvgZl_tmp.
+    exact: der_f.
+Unshelve. all: by end_near. Qed.
+
+Global Instance is_derive1ZLR (k : R -> R) (f : R -> V) (x dk : R) (df : V) :
+  is_derive x 1 k dk -> is_derive x 1 f df -> is_derive x 1 (fun x => k x *: f x) (dk *: f x + k x *: df).
+Proof.
+move=> [der_k vdk] [der_f vdf].
+constructor.
+- apply: cvgP.
+  by apply: der1_scaleLR.
+- apply: norm_cvg_lim.
+  apply: cvg_to_eq; first by apply: der1_scaleLR.
+  by rewrite vdk vdf.
+Qed.
+
+Lemma deriveZLR (k : R -> R) (f : R -> V) (x : R) : 
+  derivable k x 1 -> derivable f x 1 ->
+  'D_1 (fun x => k x *: f x) x = 'D_1 k x *: f x + k x *: 'D_1 f x.
+Proof.
+move=> dk df.
+by apply: derive_val; apply: is_derive1ZLR; apply: derivableP.
+Qed.
+
+Lemma derivableZLR (k : R -> R) (f : R -> V) (x : R) : 
+  derivable k x 1 -> derivable f x 1 -> derivable (fun x => k x *: f x) x 1.
+Proof.
+move=> dk df.
+by apply: ex_derive; apply: is_derive1ZLR; apply: derivableP.
+Qed.
+
 Lemma derive_cst (k : W) (x v : V) : 'D_v (cst k) x = 0.
 Proof. by rewrite derive_val. Qed.
 
@@ -1398,6 +1453,15 @@ move=> df dg; apply/cvg_ex; exists (- (f x) ^- 2 *: 'D_v f x).
 exact: der_inv.
 Qed.
 
+Lemma is_deriveV f (x v : V) (df : R) :
+  f x != 0 -> is_derive x v f df ->
+  is_derive x v (fun y => (f y)^-1) (- (f x) ^- 2 *: df).
+Proof.
+move=> fxNZ Df.
+constructor; first by apply: derivableV => //; case: Df.
+by rewrite deriveV //; case: Df => _ ->.
+Qed.
+
 End Derive_lemmasVR.
 
 Lemma derive_shift {R : numFieldType} (v k : R) :
@@ -1410,6 +1474,38 @@ Lemma is_derive_shift {R : numFieldType} x v (k : R) :
   is_derive x v (shift k) v.
 Proof. by apply: DeriveDef => //; rewrite derive_val addr0. Qed.
 
+Section derive_shiftf.
+Context (R : numFieldType) (V : normedModType R) (f : R -> V).
+Implicit Types (x a v : R).
+
+Lemma derivable_shiftf x a v : 
+  derivable f (x + a) v -> derivable (f \o shift a) x v.
+Proof.
+rewrite /derivable/=.
+by under eq_is_cvg do rewrite addrA.
+Qed.
+
+Lemma derive_shiftf x a v : 
+  'D_v (f \o shift a) x = 'D_v f (x + a).
+Proof.
+  rewrite /derive/=.
+  by under [in RHS]eq_fun do rewrite addrA.
+Qed.
+
+Lemma is_derive_shiftf x a (df : V) : 
+  is_derive (x + a) 1 f df -> is_derive x 1 (f \o shift a) df.
+Proof.
+  move=> [/derivable_shiftf derf +].
+  rewrite -derive_shiftf => derf_val.
+  by constructor.
+Qed.
+
+Lemma derive1_shiftf x a : 
+  (f \o shift a)^`() x = f^`() (x + a).
+Proof. by rewrite !derive1E derive_shiftf. Qed.
+
+End derive_shiftf.
+
 Lemma derive1_cst {R : numFieldType} (V : normedModType R) (k : V) t :
   (cst k)^`() t = 0.
 Proof. by rewrite derive1E derive_cst. Qed.
@@ -1440,6 +1536,10 @@ have /= := @deriveX R R id n x v (@derivable_id _ _ _ _).
 by rewrite fctE => ->; rewrite derive_id.
 Qed.
 
+Global Instance is_derive_exp (R : numFieldType) n x v :
+  is_derive x v (@GRing.exp R ^~ n) (n%:R *: x ^+ n.-1 *: v).
+Proof. by constructor; [ exact: exprn_derivable | exact: exp_derive ]. Qed.
+
 Lemma exp_derive1 {R : numFieldType} n x :
   (@GRing.exp R ^~ n)^`() x = n%:R *: x ^+ n.-1.
 Proof. by rewrite derive1E exp_derive [LHS]mulr1. Qed.
@@ -2068,6 +2168,15 @@ rewrite diff_comp // !derive1E' //= -[X in 'd  _ _ X = _]mulr1.
 by rewrite [LHS]linearZ mulrC.
 Qed.
 
+Global Instance is_derive1_comp (R : realFieldType) (f g : R -> R) (x a b : R) :
+  is_derive (g x) 1 f a -> is_derive x 1 g b -> is_derive x 1 (f \o g) (a * b).
+Proof.
+move=> [fgxv <-{a}] [gv <-{b}]; apply: (@DeriveDef _ _ _ _ _ (f \o g)).
+  apply/derivable1_diffP/differentiable_comp; first exact/derivable1_diffP.
+  by move/derivable1_diffP in fgxv.
+by rewrite -derive1E (derive1_comp gv fgxv) 2!derive1E.
+Qed.
+
 Lemma near_eq_growth_rate (R : numFieldType) (V W : normedModType R)
     (f g : V -> W) (a v : V) : {near a, f =1 g} ->
    \forall h \near 0,
@@ -2105,6 +2214,30 @@ move=> fg [fav <-]; rewrite (near_eq_derive _ fg).
 by apply: DeriveDef => //; exact: near_eq_derivable fav.
 Qed.
 
+Lemma near_eq_derive1n_near (R : numFieldType) (V : normedModType R) (k : nat) (f g : R -> V) (x : R) : 
+  {near x, f =1 g} -> {near x, f^`(k) =1 g^`(k)}.
+Proof.
+move=> near_eq.
+elim: k => [//|k IH].
+near=> y.
+rewrite !derive1nS !derive1E.
+apply: near_eq_derive.
+near: y.
+by rewrite near_nbhs; apply: near_join.
+Unshelve. all: by end_near. Qed.
+
+Lemma near_eq_derive1_near (R : numFieldType) (V : normedModType R) (f g : R -> V) (x : R) :
+  {near x, f =1 g} -> {near x, f^`() =1 g^`()}.
+Proof. rewrite -!derive1n1; exact: near_eq_derive1n_near. Qed.
+
+Lemma near_eq_derive1n (R : numFieldType) (V : normedModType R) (k : nat) (f g : R -> V) (x : R) : 
+  {near x, f =1 g} -> f^`(k) x = g^`(k) x.
+Proof. by move/near_eq_derive1n_near => /(_ k) /nbhs_singleton. Qed.
+
+Lemma near_eq_derive1 (R : numFieldType) (V : normedModType R) (f g : R -> V) (x : R) : 
+  {near x, f =1 g} -> f^`() x = g^`() x.
+Proof. by rewrite -!derive1n1; exact: near_eq_derive1n. Qed.
+
 Section Derive_max.
 Context {K : realType} {V W : normedModType K}.
 Implicit Types f g : V -> K^o.
@@ -2506,4 +2639,4 @@ move=> dfx dgx; apply: DiffDef; first exact: differentiable_row_mx.
 by rewrite diff_row_mx// !diff_val.
 Qed.
 
-End is_diff_row_mx.
+End is_diff_row_mx.

theories/normedtype_theory/normed_module.v

@@ -642,6 +642,30 @@ Proof. exact: cvgZr_tmp. Qed.
 Lemma cvgMl_tmp g a b : g @ F --> b -> a * g x @[x --> F] --> a * b.
 Proof. exact: cvgZl_tmp. Qed.
 
+Lemma cvg1MC f a : f @ F --> (1 :> K) -> f x * a @[x --> F] --> a.
+Proof. by move/(cvgMr_tmp (b := a)); rewrite mul1r. Qed.
+
+Lemma cvg1M f g a : f @ F --> (1 :> K) -> g @ F --> a -> f \* g @ F --> a.
+Proof. by move=> /cvgM /[apply]; rewrite mul1r. Qed.
+
+Lemma cvgCM1 f a : f @ F --> (1 :> K) -> a * f x @[x --> F] --> a.
+Proof. by move/(cvgMl_tmp (a := a)); rewrite mulr1. Qed.
+
+Lemma cvgM1 f g a : f @ F --> a -> g @ F --> (1 :> K) -> f \* g @ F --> a.
+Proof. by move=> /cvgM /[apply]; rewrite mulr1. Qed.
+
+Lemma cvg0MC f a : f @ F --> 0 -> f x * a @[x --> F] --> 0.
+Proof. by move/(cvgMr_tmp (b := a)); rewrite mul0r. Qed.
+
+Lemma cvg0M f g a : f @ F --> 0 -> g @ F --> a -> f \* g @ F --> 0.
+Proof. by move=> /cvgM /[apply]; rewrite mul0r. Qed.
+
+Lemma cvgCM0 f a : f @ F --> 0 -> a * f x @[x --> F] --> 0.
+Proof. by move/(cvgMl_tmp (a := a)); rewrite mulr0. Qed.
+
+Lemma cvgM0 f g a : f @ F --> a -> g @ F --> 0 -> f \* g @ F --> 0.
+Proof. by move=> /cvgM /[apply]; rewrite mulr0. Qed.
+
 Lemma is_cvgM f g : cvg (f @ F) -> cvg (g @ F) -> cvg (f \* g @ F).
 Proof. exact: is_cvgZ. Qed.
 

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -1098,6 +1098,45 @@ Qed.
 Lemma is_cvgDrE f g : cvg (f @ F) -> cvg ((f + g) @ F) = cvg (g @ F).
 Proof. by rewrite addrC; apply: is_cvgDlE. Qed.
 
+Lemma cvgDl f a b : f @ F --> b -> a + f x @[x --> F] --> a + b.
+Proof. apply: cvgD; exact: cvg_cst. Qed.
+
+Lemma cvgDr f a b : f @ F --> a -> f x + b @[x --> F] --> a + b.
+Proof. move/cvgD; apply; exact: cvg_cst. Qed.
+
+Lemma cvgBl f a b : f @ F --> b -> a - f x @[x --> F] --> a - b.
+Proof. by move/cvgN; apply: cvgDl. Qed.
+
+Lemma cvgBr f a b : f @ F --> a -> f x - b @[x --> F] --> a - b.
+Proof. exact: cvgDr. Qed.
+
+Lemma cvg0D f g a : f @ F --> 0 -> g @ F --> a -> f x + g x @[x --> F] --> a.
+Proof. by move=> /cvgD /[apply]; rewrite add0r. Qed.
+
+Lemma cvg0DC f a : f @ F --> 0 -> f x + a @[x --> F] --> a.
+Proof. by move=> /(cvgDr (b := a)); rewrite add0r. Qed.
+
+Lemma cvgD0 f g a : f @ F --> a -> g @ F --> 0 -> f x + g x @[x --> F] --> a.
+Proof. by move=> /cvgD /[apply]; rewrite addr0. Qed.
+
+Lemma cvgCD0 f a : f @ F --> 0 -> a + f x @[x --> F] --> a.
+Proof. by move/(@cvgDl _ a); rewrite addr0. Qed.
+
+Lemma cvg0B f g a : f @ F --> 0 -> g @ F --> a -> f x - g x @[x --> F] --> -a.
+Proof. by move=> /cvgB /[apply]; rewrite add0r. Qed.
+
+Lemma cvg0BC f a : f @ F --> 0 -> f x - a @[x --> F] --> -a.
+Proof. by move=> /(cvgBr (b := a)); rewrite add0r. Qed.
+
+Lemma cvgB0 f g a : f @ F --> a -> g @ F --> 0 -> f x - g x @[x --> F] --> a.
+Proof. by move=> /cvgB /[apply]; rewrite subr0. Qed.
+
+Lemma cvgCB0 f a : f @ F --> 0 -> a - f x @[x --> F] --> a.
+Proof. by move/(@cvgBl _ a); rewrite subr0. Qed.
+
+Lemma cvgN0 f : f @ F --> 0 -> - f @ F --> 0.
+Proof. by rewrite -{2}oppr0; exact: cvgN. Qed.
+
 Lemma cvg_sub0 f g a : (f - g) @ F --> (0 : V) -> g @ F --> a -> f @ F --> a.
 Proof.
 by move=> Cfg Cg; have := cvgD Cfg Cg; rewrite subrK add0r; apply.

theories/probability_theory/beta_distribution.v

@@ -77,7 +77,6 @@ Lemma derive_onemXn n x :
   (fun y => y.~ ^+ n)^`()%classic x = - n%:R * x.~ ^+ n.-1.
 Proof.
 rewrite (@derive1_comp _ (@onem _) (fun x => x ^+ n))//.
-  exact: exprn_derivable.
 rewrite derive1E exp_derive// derive1E deriveB// -derive1E.
 by rewrite derive1_cst derive_id sub0r mulrN1 [in RHS]mulNr scaler1.
 Qed.