last fixes

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -4,11 +4,6 @@
 
 ### Added
 
-### Changed
-
-- in `Rstruct.v`
-  + instantiate `GRinv.inv` by `Rinv` instead of `Rinvx`
-
 - in `mathcomp_extra.v`:
   + lemmas `prodr_ile1`, `nat_int`
 
@@ -119,6 +114,15 @@
 - new file `measurable_realfun.v`
   + with as contents the first half of the file `lebesgue_measure.v`
 
+- in `set_interval.v`:
+  + lemma `set_itv_splitU`
+
+- in `normedtype.v`:
+  + lemma `lt_nbhsr`
+
+- in `realfun.v`:
+  + lemmas `lhopital_at_left`, `lhopital_at_left`, `lhopital`,
+
 ### Changed
 
 - in `lebesgue_integral.v`
@@ -148,6 +152,9 @@
 - file `lebesgue_measure.v`
   + first half moved to a new file `measurable_realfun.v`
 
+- in `Rstruct.v`
+  + instantiate `GRinv.inv` by `Rinv` instead of `Rinvx`
+
 ### Renamed
 
 - in `measure.v`
@@ -171,6 +178,10 @@
 - in `lebesgue_integral.v`:
   + `Rintegral_setU_EFin` -> `Rintegral_setU`
 
+- in `normedtype.v`:
+  + `nbhs_lt` -> `lt_nbhsl_lt`
+  + `nbhs_le` -> `lt_nbhsl_le`
+
 ### Generalized
 
 - in `sequences.v`,

classical/set_interval.v

@@ -234,7 +234,7 @@ Notation subset_itvS := subset_itvScc (only parsing).
 
 Section set_itv_orderType.
 Variables (d : Order.disp_t) (T : orderType d).
-Implicit Types a x y : itv_bound T.
+Implicit Types a b x y : itv_bound T.
 
 Lemma itv_bndbnd_setU a x y : (a <= x)%O -> (x <= y)%O ->
   ([set` Interval a y] = [set` Interval a x] `|` [set` Interval x y])%classic.
@@ -293,6 +293,26 @@ move: a ax => [b t /= tx| [/= oox|/= oox]].
 - by move: x => [[|] x|[|]//]/= in xy oox *.
 Qed.
 
+Lemma set_itv_splitU a b (c : T) : c \in Interval a b ->
+  [set` Interval a b] `\ c =
+    [set` Interval a (BLeft c)] `|` [set` Interval (BRight c) b].
+Proof.
+move=> cab; apply/seteqP; split => [x /= [xab /eqP]|x[|]]/=.
+- rewrite neq_lt => /orP[xc|cx]; [left|right].
+  + move: cab xab; rewrite !itv_boundlr => /andP[ac cb] /andP[ax xb].
+    by rewrite ax/= bnd_simp.
+  + move: cab xab; rewrite !itv_boundlr => /andP[ac cb] /andP[ax xb].
+    by rewrite xb andbT bnd_simp.
+- move: cab; rewrite !itv_boundlr => /andP[ac cb] /andP[ax].
+  rewrite bnd_simp => xc.
+  rewrite ax/= (le_trans _ cb) ?bnd_simp ?(ltW xc)//; split => //.
+  by apply/eqP; rewrite lt_eqF.
+- move: cab; rewrite !itv_boundlr => /andP[ac cb] /andP[+ xb].
+  rewrite bnd_simp => cx.
+  rewrite xb/= andbT (le_trans ac)/= ?bnd_simp ?(ltW cx)//; split => //.
+  by apply/eqP; rewrite gt_eqF.
+Qed.
+
 End set_itv_orderType.
 
 Lemma set_itv_ge disp [T : porderType disp] [b1 b2 : itv_bound T] :

theories/ftc.v

@@ -521,7 +521,8 @@ have /ifab : (mu `[a, c] < d%:E)%E.
 move=> /(_ (measurable_itv _)) {ifab}.
 apply: le_lt_trans.
 have acbc : `[a, c] `<=` `[a, b].
-  by apply: subset_itvl; rewrite bnd_simp; move: ac; near: c; exact: nbhs_le.
+  apply: subset_itvl; rewrite bnd_simp; move: ac; near: c.
+  exact: lt_nbhsl_le.
 rewrite -lee_fin fineK; last first.
   apply: integral_fune_fin_num => //=.
   rewrite (_ : (fun _ => _) = abse \o ((EFin \o f) \_ `[a, b])); last first.

theories/normedtype.v

@@ -1198,10 +1198,10 @@ Arguments cvgr0_norm_le {_ _ _ F FF}.
   H : x \is_near _ |- _ => near: x; exact: cvgr0_norm_le end : core.
 
 Section nbhs_lt_le.
-Context {R : realType}.
+Context {R : numFieldType}.
 Implicit Types x z : R.
 
-Lemma nbhs_lt x z : x < z -> \forall y \near x, x <= y -> y < z.
+Lemma lt_nbhsl_lt x z : x < z -> \forall y \near x, x <= y -> y < z.
 Proof.
 move=> xz; near=> y.
 rewrite le_eqVlt => /predU1P[<-//|].
@@ -1210,12 +1210,27 @@ move=> y/= /[swap] xy; rewrite ltr0_norm ?subr_lt0//.
 by rewrite opprD addrC ltrBlDr subrK opprK.
 Unshelve. all: by end_near. Qed.
 
-Lemma nbhs_le x z : x < z -> \forall y \near x, x <= y -> y <= z.
+Lemma lt_nbhsl_le x z : x < z -> \forall y \near x, x <= y -> y <= z.
 Proof.
-by move=> xz; apply: filterS (nbhs_lt xz) => y /[apply] /ltW.
+by move=> xz; apply: filterS (lt_nbhsl_lt xz) => y /[apply] /ltW.
 Qed.
 
 End nbhs_lt_le.
+(*#[deprecated(since="mathcomp-analysis 1.9.0", note="use `lt_nbhsl_lt` instead")]
+Notation nbhs_lt := lt_nbhsl_lt (only parsing).
+#[deprecated(since="mathcomp-analysis 1.9.0", note="use `lt_nbhsl_le` instead")]
+Notation nbhs_le := lt_nbhsl_le (only parsing).*)
+
+Lemma lt_nbhsr {R : realFieldType} (a z : R) : a < z ->
+  \forall x \near z, a < x.
+Proof.
+rewrite -subr_gt0 => za0; exists (z - a) => //= u/=.
+rewrite ltrBrDl addrC -ltrBrDl => /lt_le_trans; apply.
+rewrite lerBlDl.
+have [uz|uz] := leP u z.
+  by rewrite ger0_norm ?subr_ge0// subrK.
+by rewrite ltr0_norm ?subr_lt0// opprB addrAC -lerBlDr opprK lerD// ?ltW.
+Qed.
 
 Section open_closed_sets.
 (* TODO: duplicate theory within the subspace topology of Num.real

theories/realfun.v

@@ -12,7 +12,8 @@ From mathcomp Require Import sequences real_interval.
 (* # Real-valued functions over reals                                         *)
 (*                                                                            *)
 (* This file provides properties of standard real-valued functions over real  *)
-(* numbers (e.g., the continuity of the inverse of a continuous function).    *)
+(* numbers (e.g., the continuity of the inverse of a continuous function,     *)
+(* L'Hopital's rule).                                                         *)
 (*                                                                            *)
 (* ```                                                                        *)
 (*      nondecreasing_fun f == the function f is non-decreasing               *)
@@ -41,9 +42,6 @@ From mathcomp Require Import sequences real_interval.
 (*   lime_sup f a/lime_inf f a == limit sup/inferior of the extended real-    *)
 (*                             valued function f at point a                   *)
 (* ```                                                                        *)
-(*               cauchy_MVT == Cauchy's mean value theorem                    *)
-(*           lhopital_right == L'Hopital rule (limit taken on the right)      *)
-(*            lhopital_left == L'Hopital rule (limit taken on the left)       *)
 (*                                                                            *)
 (* Discontinuities:                                                           *)
 (* ```                                                                        *)
@@ -2875,6 +2873,7 @@ Unshelve. all: end_near. Qed.
 
 End discontinuity_countable.
 
+(** Cauchy's mean value theorem *)
 Section Cauchy_MVT.
 Context {R : realType}.
 Variables (f df g dg : R -> R) (a b c : R).
@@ -2970,22 +2969,6 @@ by apply: DeriveDef => //; exact: near_eq_derivable fav.
 Qed.
 (* /NB: PR in progress *)
 
-(* TODO: rename, move *)
-Lemma nbhs_lt' {R : realType} (a z : R) : a < z -> \forall x \near nbhs z, a < x.
-Proof.
-rewrite -subr_gt0 => za0.
-exists (z - a) => //=.
-move=> u/=.
-rewrite ltrBrDl addrC -ltrBrDl.
-move=> /lt_le_trans; apply.
-rewrite lerBlDl.
-have [uz|uz] := leP u z.
-  rewrite ger0_norm ?subr_ge0//.
-  by rewrite subrK.
-rewrite ltr0_norm ?subr_lt0//.
-by rewrite opprB addrAC -lerBlDr opprK lerD// ?ltW.
-Qed.
-
 Section lhopital_at_right.
 Context {R : realType}.
 Variables (f df g dg : R -> R) (a b : R) (l : R) (ab : a < b).
@@ -3034,7 +3017,7 @@ Proof.
 move=> yb zay; apply: (@near_eq_is_derive _ _ _ g) => //; last first.
   by apply: gdg; move: z zay; apply: subset_itvSoo; rewrite bnd_simp.
 near=> u do rewrite /g0 gt_eqF//.
-by move: zay; rewrite in_itv/= => /andP[+ _]; exact: nbhs_lt'.
+by move: zay; rewrite in_itv/= => /andP[+ _]; exact: lt_nbhsr.
 Unshelve. all: by end_near. Qed.
 
 Let wcont_g0 y : a < y -> y < b -> {within `[a, y], continuous g0}.
@@ -3221,28 +3204,6 @@ Unshelve. all: by end_near. Qed.
 
 End lhopital_at_left.
 
-(* TODO: move *)
-Lemma set_itv_splitU {R : realType} (a b : itv_bound R) (c : R) :
-  c \in Interval a b ->
-  [set` Interval a b] `\ c =
-    [set` Interval a (BLeft c)] `|` [set` Interval (BRight c) b].
-Proof.
-move=> cab; apply/seteqP; split => [x /= [xab /eqP]|x[|]]/=.
-- rewrite neq_lt => /orP[xc|cx]; [left|right].
-  + move: cab xab; rewrite !itv_boundlr=> /andP[ac cb] /andP[ax xb].
-    by rewrite ax/= bnd_simp.
-  + move: cab xab; rewrite !itv_boundlr=> /andP[ac cb] /andP[ax xb].
-    by rewrite xb andbT bnd_simp.
-- move: cab; rewrite !itv_boundlr => /andP[ac cb] /andP[ax].
-  rewrite bnd_simp => xc.
-  rewrite ax/= (le_trans _ cb) ?bnd_simp ?(ltW xc)//; split => //.
-  by apply/eqP; rewrite lt_eqF.
-- move: cab; rewrite !itv_boundlr => /andP[ac cb] /andP[+ xb].
-  rewrite bnd_simp => cx.
-  rewrite xb/= andbT (le_trans ac)/= ?bnd_simp ?(ltW cx)//; split => //.
-  by apply/eqP; rewrite gt_eqF.
-Qed.
-
 Section lhopital.
 Context {R : realType}.
 Variables (f df g dg : R -> R) (a b c : R) (l : R).
@@ -3275,99 +3236,3 @@ move=> fgcl; apply/cvg_at_right_left_dnbhs.
 Qed.
 
 End lhopital.
-
-Section lhopital0.
-Context {R : realType}.
-Variables (f df g dg : R -> R) (a : R) (U : set R) (Ua : nbhs a U).
-Hypotheses (fdf : forall x, x \in U -> is_derive x 1 f (df x))
-           (gdg : forall x, x \in U -> is_derive x 1 g (dg x)).
-Hypotheses (fa0 : f a = 0) (ga0 : g a = 0)
-           (cdg : \forall x \near a^', dg x != 0).
-
-Lemma lhopital_right (l : R) :
-  df x / dg x @[x --> a^'+] --> l -> f x / g x @[x --> a^'+] --> l.
-Proof.
-case: Ua => e/= e0 aeU.
-case: cdg => d/= d0 cdg'.
-pose D := minr e d.
-have := @lhopital_at_right R f df g dg a (a + D).
-rewrite ltrDl.
-have D0 : 0 < D by rewrite lt_min e0 d0.
-move=> /(_ _ D0).
-have H (x : R) (G : R) : 0 < G -> x \in `]a, (a + G)%E[ -> `|a - x| < G.
-  move=> G0 xae.
-  rewrite ltr_norml; apply/andP; split.
-    move: xae; rewrite in_itv/= => /andP[_].
-    by rewrite ltrBrDl ltrBlDl addrC.
-  move: xae; rewrite in_itv/= => /andP[+ _].
-  rewrite -subr_lt0 => /lt_le_trans; apply.
-  exact: ltW.
-apply.
-- move=> x xae; apply: fdf.
-  rewrite inE; apply: aeU => /=; apply: H => //.
-  by move: x xae; apply: subset_itvl; rewrite bnd_simp lerD2l ge_min lexx.
-- move=> x xae; apply: gdg.
-  rewrite inE; apply: aeU => /=; apply: H => //.
-  by move: x xae; apply: subset_itvl; rewrite bnd_simp lerD2l ge_min lexx.
-- rewrite -fa0; apply: cvg_at_right_filter.
-  suff : {for a, continuous f} by [].
-  apply/differentiable_continuous/derivable1_diffP.
-  apply: ex_derive; apply: fdf.
-  rewrite inE.
-  by case: Ua => r /= r0; apply; rewrite /= subrr normr0.
-- rewrite -ga0.
-  apply: cvg_at_right_filter.
-  suff : {for a, continuous g} by [].
-  apply/differentiable_continuous/derivable1_diffP.
-  apply: ex_derive; apply: gdg.
-  rewrite inE.
-  by case: Ua => r /= r0; apply; rewrite /= subrr normr0.
-- move=> x xae; apply: cdg' => /=.
-    apply: H => //.
-    by move: x xae; apply: subset_itvl; rewrite bnd_simp lerD2l ge_min lexx orbT.
-  rewrite gt_eqF//.
-  by move: xae; rewrite in_itv/= => /andP[].
-Qed.
-
-End lhopital0.
-
-Section lhopital1.
-Context {R : realType}.
-Variables (f df g dg : R -> R) (a : R) (U : set R) (Ua : nbhs a U).
-Hypotheses (fdf : forall x, x \in U -> is_derive x 1 f (df x))
-           (gdg : forall x, x \in U -> is_derive x 1 g (dg x)).
-Hypotheses (fa0 : f a = 0) (ga0 : g a = 0)
-           (cdg : \forall x \near a^', dg x != 0).
-
-Lemma lhopital_left (l : R) :
-  df x / dg x @[x --> a^'-] --> l -> f x / g x @[x --> a^'-] --> l.
-Proof.
-move=> fgbl; apply/cvg_at_leftNP.
-set h := (X in X x @[x --> _]).
-rewrite (_ : h = (fun x => (fun y => (f \o -%R) y / (g \o -%R) y) x))//.
-have := @lhopital_right R (f \o -%R) (fun x => (df (- x)) * -1)
-  (g \o -%R) (fun x => (dg (- x)) * -1) (- a) (-%R @` U).
-apply.
-- by rewrite nbhsNimage/=; exists U.
-- move=> x; rewrite inE/= => -[r Ur] <-{x}.
-  rewrite opprK; apply: is_derive1_comp.
-  by rewrite opprK; apply: fdf; exact: mem_set.
-- move=> x; rewrite inE/= => -[r Ur] <-{x}.
-  rewrite opprK; apply: is_derive1_comp.
-  by rewrite opprK; apply: gdg; exact: mem_set.
-- by rewrite /= opprK.
-- by rewrite /= opprK.
-- case: cdg => e/= e0 H; near=> x.
-  rewrite mulrN1 oppr_eq0.
-  apply: H => /=.
-    rewrite -normrN opprB addrC.
-    by near: x; exists e.
-  rewrite eqr_oppLR.
-  by near: x; exact: nbhs_dnbhs_neq.
-- apply/cvg_at_rightNP.
-  rewrite opprK/=; apply: cvg_trans fgbl.
-  apply: near_eq_cvg; near=> x.
-  by rewrite /= opprK !mulrN1 mulNr invrN mulrN opprK.
-Unshelve. all: by end_near. Qed.
-
-End lhopital1.

theories/trigo.v

@@ -1230,21 +1230,3 @@ by rewrite ltrNl oppr0 divr_gt0// pi_gt0.
 Qed.
 
 End Atan.
-
-Section lhopital_examples.
-Variable R : realType.
-
-Example cvg_mulsinV0 : sin x / x @[x --> 0^'] --> (1:R).
-Proof.
-apply: (@lhopital _ sin cos id 1 (-1) 1 0 1).
-- by rewrite in_itv/= ltrN10 ltr01.
-- rewrite -[X in _ --> X]sin0.
-  exact: continuous_sin.
-- exact: cvg_id.
-- by move=> ? _; exact: oner_neq0.
-- rewrite -[X in _ --> X]cos0.
-  under eq_fun do rewrite invr1 mulr1.
-  exact: continuous_cos.
-Qed.
-
-End lhopital_examples.