lint by reynald, tentative near

Author: mkerjean

Diff for: theories/normedtype.v

@@ -4153,47 +4153,105 @@ rewrite !near_simpl near_withinE near_simpl => Pf; near=> y.
 by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y].
 Grab Existential Variables. all: end_near. Qed.
 
+(* NB: technical lemma that comes in handy in Banach-Steinhaus' PR *)
+Lemma normrZV (R : numFieldType) (V : normedModType R) (x : V) :
+  x != 0 -> `| `| x|^-1 *: x | = 1.
+Proof.
+move=> x0; rewrite normmZ normrV ?unitfE ?normr_eq0 //=.
+by rewrite normr_id mulVr // unitfE normr_eq0.
+Qed.
+
 Section LinearContinuousBounded.
 
-Variables (R: numFieldType) (V  W: normedModType R).
+Variables (R : numFieldType) (V W : normedModType R).
+
+
+(*drafts for another PR *)
+Definition absorbed (A B : set V) :=
+  exists (r : R),  A `<=` [ set x : V | exists y : V, B y /\ x = r *: y ].
+
+Definition strong_bornology :=
+  [ set A | (forall (B : set V), (nbhs (0:V) B -> absorbed A B))].
+
+Lemma normed_bornological (A : set V) :  bounded_set A <->
+                     (forall (B : set V), (nbhs (0:V) B -> absorbed A B)).
+Proof.
+Admitted.
+(*To be generalized to any topological space, with a theory of bounded*)
+
+
+Definition bounded_fun_on (f : V -> W) (B : set (set V)):=
+  forall A, (B A -> (exists M : R, \forall x \near (0 :V), (`|f x| <= M))).
+
+
+Lemma linear_bounded (f : {linear V -> W} ):
+  ( bounded_on f (nbhs (0 : V))) <->
+        (*exists r : R, 0 <= r /\ (forall x : V, `|f x| <= r * `|x|).*)
+     \forall r \near +oo, (forall x : V, `|f x| <= r * `|x|).
+Proof.
+split; last first.
+  move=> /pinfty_ex_gt0 [r [r0 Bf]]; rewrite /bounded_on; near=> M; rewrite -nearE.
+  near=> x; apply: le_trans; first by apply: Bf.
+  apply: (le_trans (y :=r)).
+    apply: ler_pimulr; apply: ltW; first by [].
+    near: x; rewrite nearE.
+    suff <-: ball_ normr 0 1 = (fun x : V => `|x| < 1) by apply: nbhs_ball_norm.
+    by apply: funext => x /=; rewrite sub0r normrN.
+  near: M; rewrite nearE /=; exists r; split; first by apply: gtr0_real.
+  by move => x; apply: ltW. (* much longer *)
+rewrite /bounded_on => Bf; near=> r => x.
+have [->|x0] := eqVneq x 0; first by rewrite linear0 !normr0 mulr0.
+rewrite -ler_pdivr_mulr ; last by rewrite normr_gt0.
+rewrite -(normr_id x) mulrC.
+rewrite -normrV  ?unitfE ?normr_eq0 // -normmZ -linearZ.
+move:x x0; near: r. 
+ (* hell on earth *)
+(* how to use hypothesis with near *) 
+(* split => [[M /nbhs_ballP[a a0 Ba0]]|[r [r0 fr]]]; last first. *)
+(*   exists r; apply/nbhs_ballP; exists 1 => // x. *)
+(*   rewrite -ball_normE //= sub0r normrN => x1; apply: (le_trans (fr _)). *)
+(*   by rewrite ler_pimulr // ltW.  *)
+(* exists (M * 2 * a^-1); split. *)
+(* - rewrite !mulr_ge0 //= ?invr_ge0 ; last by apply: ltW. *)
+(*   by move: (Ba0 0 (ballxx 0 a0)); rewrite linear0 normr0. *)
+(* - move=> x; rewrite mulrAC ler_pdivl_mulr //=. *)
+(*   have [/eqP ->|x0] := boolP (x == 0). *)
+(*   + by rewrite linear0 !(normr0,mulr0,mul0r). *)
+(*   + rewrite mulrAC -lter_pdivr_mulr // -lter_pdivr_mulr ?normr_gt0 //. *)
+(*     rewrite [X in X <= _](_ : _ = `|f (a / 2 / `|x| *: x)|); last first. *)
+(*       rewrite linearZ normmZ 2!normrM (gtr0_norm a0) gtr0_norm //. *)
+(*       by rewrite normrV ?unitfE ?normr_eq0 // normr_id -2!mulrA mulrC mulrA. *)
+(*     apply: Ba0; rewrite -ball_normE /= sub0r normrN. *)
+(*     rewrite normmZ normrM (@normrV _ `|x|) ?unitfE ?normr_eq0 // normr_id. *)
+(*     rewrite -mulrA mulVr ?mulr1 ?unitfE ?normr_eq0 //. *)
+(*     by rewrite normrM 2?gtr0_norm// gtr_pmulr // invf_lt1 // ltr1n. *)
+(* Qed. *)
+Admitted.
+
 
-Lemma linear_boundedP (f: {linear V -> W}) : bounded_on f (nbhs (0:V)) <->
-        (exists r, 0 <= r /\ (forall x : V, `|f x| <=  `|x| * r )).
+Lemma linear_boundedP  (f : {linear V -> W}) :
+  (bounded_on f (nbhs (0 : V))) <->
+        exists r : R, 0 <= r /\ (forall x : V, `|f x| <= r * `|x|).
 Proof.
-  split.
-  -  move => /ex_bound [M /nbhs_ballP [a a0 Ba0]] //=.
-     exists (M * 2 *a^-1).
-     split.
-     - rewrite !mulr_ge0 //= ?invr_ge0 ; last by apply: ltW.
-       move : (Ba0 0 (ballxx 0 a0 )); rewrite linear0 normr0 //=.
-     - move => x. rewrite mulrA ler_pdivl_mulr //=.
-       case: (boolp.EM (x=0)).
-       - by move => ->; rewrite linear0 !normr0 !mul0r.
-       - move => /eqP x0 ; rewrite -lter_pdivr_mull ?normr_gt0 //=.
-         rewrite [X in ( _ <= X)]mulrC -lter_pdivr_mull //=.
-         have ->: 2^-1 *(`|x|^-1 * (`|f x| * a))=`|f ((2^-1 * `|x|^-1 * a)*:x)|.
-           rewrite linearZ normmZ !normrM !ger0_norm ?invr_ge0 //= ?ltW //=.
-           by rewrite mulrA mulrA mulrAC.
-         apply: Ba0 ;rewrite -ball_normE /= sub0r normrN ?normr_gt0 //=.
-         rewrite normmZ !normrM !normrV ?unitfE ?normrE // !ger0_norm ?ltW //=.
-         rewrite mulrAC -mulrA -mulrA [_ * (_ * a)]mulrA.
-         rewrite mulVr ?unitf_gt0 //= ?normr_gt0 //= mul1r.
-         rewrite mulrC gtr_pmulr ?invr_lte1 //= ?unitfE ?ltr_spaddr //=.
-     - move => [r [r0 fr]]; apply/ex_bound; exists r.
-       rewrite nbhs_ballP; exists 1; first by [].
-       move=> x; rewrite -ball_normE //= sub0r normrN => x1; apply: le_trans.
-       apply: fr.
-       rewrite -[X in _ <= X]mul1r; apply: ler_pmul; rewrite ?normr_ge0 //=.
-       by apply: ltW.
-Qed.
+split => [/linear_bounded | B].
+  by move=> /pinfty_ex_gt0  [M [M0 B]]; exists M; split; first by apply: ltW.
+apply/linear_bounded; near_simpl. Admitted.
 
 Lemma linear_continuous0 (f : {linear V -> W}) :
-  {for 0, continuous f} -> bounded_on f (nbhs (0:V)).
-Proof.
-move=> /cvg_ballP /(_ _ ltr01) .
+  {for 0, continuous f} -> bounded_on f (nbhs (0 : V)).
+Proof.
+(* move=> /cvg_distP; rewrite linear0 /= => Bf. *)
+(* apply/linear_boundedP; near=> r => x. *)
+(* have [->|x0] := eqVneq x 0; first by rewrite linear0 !normr0 mulr0. *)
+(* rewrite -ler_pdivr_mulr; last by rewrite normr_gt0. *)
+(* rewrite -(normr_id x) mulrC. *)
+(* rewrite -normrV  ?unitfE ?normr_eq0 // -normmZ -linearZ. *)
+(* apply: ltW. move: (Bf r) x x0; near: r. apply/near_pinfty_div2. *)
+move=> /cvg_ballP /(_ _ ltr01).
 rewrite linear0 /= nearE => /nbhs_ex[tp ball_f]; apply/linear_boundedP.
-pose t := tp%:num; exists (2 * t^-1); split => // x.
-have [->|x0] := eqVneq x 0; first by rewrite linear0 !normr0 mul0r.
+pose t := tp%:num; exists (2 * t^-1); split => [|x].
+  by apply: divr_ge0.
+have [->|x0] := eqVneq x 0; first by rewrite linear0 !normr0 mulr0.
 have /ball_f : ball 0 t ((`|x|^-1 * t /2) *: x).
   apply: ball_sym; rewrite -ball_normE /ball_  subr0 normmZ mulrC 2!normrM.
   rewrite 2!mulrA normrV ?unitfE ?normr_eq0 // normr_id.
@@ -4202,110 +4260,78 @@ have /ball_f : ball 0 t ((`|x|^-1 * t /2) *: x).
 rewrite -ball_normE //= sub0r normrN linearZ /= normmZ -mulrA normrM.
 rewrite normrV ?unitfE ?normr_eq0 // normr_id -mulrA.
 rewrite ltr_pdivr_mull ?mulr1 ?normr_gt0 // -ltr_pdivl_mull ?normr_gt0 //.
-by rewrite gtr0_norm // invf_div mulrC => /ltW.
+rewrite gtr0_norm // invf_div => /ltW H. apply: le_trans; first by exact: H.
+by apply: ler_pmul.
 Qed.
 
 Lemma linear_bounded0 (f : {linear V -> W}) :
- bounded_on f (nbhs (0:V)) -> {for 0, continuous f} .
+  bounded_on f (nbhs (0 : V)) -> {for 0, continuous f} .
 Proof.
 move=> /linear_boundedP [r]; rewrite le0r=>  [[/orP r0]]; case: r0.
 - move/eqP => -> fr; apply: near_cst_continuous; near=> y.
-  by move: (fr y); rewrite mulr0 normr_le0; apply/eqP.
+  by move: (fr y); rewrite mul0r normr_le0; apply/eqP.
 - move => r0 fr;  apply/cvg_ballP => e e0.
   rewrite nearE linear0 /= nbhs_ballP.
   exists (e / 2 / r); first by rewrite !divr_gt0.
   move=> x; rewrite -2!ball_normE /= 2!sub0r 2!normrN => xr.
   have /le_lt_trans -> // : `|f x| <= e / 2.
-  by rewrite (le_trans (fr x)) // -ler_pdivl_mulr // ltW.
+  by rewrite (le_trans (fr x)) // mulrC -ler_pdivl_mulr // ltW.
   by rewrite gtr_pmulr // invr_lt1 // ?unitfE // ltr1n.
-  Grab Existential Variables. by end_near.
-Qed.
+Grab Existential Variables. by end_near. Qed.
 
 Lemma continuousfor0_continuous (f : {linear V -> W}) :
   {for 0, continuous f} -> continuous f.
 Proof.
-move=> /(linear_continuous0) /linear_boundedP [r].
-rewrite le0r=>  [[/orP r0]]; case: r0  => /eqP.
-- move => ->;  move : f  =>  [f linf] f0 //=. (* Linear linf = f ?? *)
-  suff: f  = fun x => 0 by move => ->; apply: cst_continuous.
-    by apply: funext => x; move: (f0 x); rewrite mulr0 normr_le0; apply/eqP .
-- move/eqP => //= r0 fr x.
-  rewrite cvg_to_locally => e e0; rewrite nearE /= nbhs_ballP.
-  exists (e / r).
-   - by rewrite mulr_gt0 //= invr_gt0.
-   - move=> y; rewrite -!ball_normE //= => xy; rewrite -linearB.
-     by rewrite (le_lt_trans (fr (x - y))) // -ltr_pdivl_mulr.
+move=> /linear_continuous0 /linear_boundedP [r []].
+rewrite le_eqVlt => /orP[/eqP <- f0|r0 fr x].
+- suff : f = (fun _ => 0) :> (_ -> _) by move=> ->; exact: cst_continuous.
+  by rewrite funeqE => x; move: (f0 x); rewrite mul0r normr_le0 => /eqP.
+- rewrite cvg_to_locally => e e0; rewrite nearE /= nbhs_ballP.
+  exists (e / r); first by rewrite divr_gt0.
+  move=> y; rewrite -!ball_normE //= => xy; rewrite -linearB.
+  by rewrite (le_lt_trans (fr (x - y))) // mulrC -ltr_pdivl_mulr.
 Qed.
 
 Lemma linear_bounded_continuous (f : {linear V -> W}) :
   bounded_on f (nbhs (0 : V)) <-> continuous f.
 Proof.
-  split; first by move=> /linear_bounded0; apply continuousfor0_continuous.
-  by move => /(_ 0) /linear_continuous0 /=.
+split=> [/linear_bounded0|/(_ 0)/linear_continuous0//].
+exact: continuousfor0_continuous.
 Qed.
 
-Definition bounded_fun_norm (f: V -> W) := forall r, exists M,
-      forall x, (`|x| <= r) -> (`|(f x)| <= M).
+Definition bounded_fun_norm (f : V -> W) :=
+  forall r, exists M, forall x, `|x| <= r -> `|f x| <= M.
+(*bounded_fun_on bounded_sets is harder to use*)
 
-Definition pointwise_bounded (F: (V -> W) -> Prop) := forall x, exists M,
-      forall f , F f ->  (`|f x| <= M)%O.
+(* Definition pointwise_bounded (F : set (V -> W)) := *)
+(*   forall x, exists M, forall f, F f -> `|f x| <= M. *)
 
-Definition uniform_bounded (F: (V -> W) -> Prop) := forall r, exists M,
-      forall f, F f -> forall x, (`|x| <= r)  -> (`|f x| <= M)%O.
+(* Definition uniform_bounded (F : set (V -> W)) := *)
+(*   forall r, exists M, forall f, F f -> forall x, `|x| <= r -> `|f x| <= M. *)
 
 Lemma bounded_funP (f : {linear V -> W}):
-  bounded_fun_norm f <-> bounded_on f (nbhs (0:V)).
-Proof.
-split.
-- move => /(_ 1) [M Bf]; apply /linear_boundedP.
-  have M0: (0 <= M) by move: (Bf 0); rewrite  linear0 !normr0//= => /(_ ler01).
-  exists M; split; first by [].
-  move: M0; rewrite le0r => /orP; case.
-  - move=> /eqP M0; move: M0 Bf =>  -> Bf x; rewrite mulr0 normr_le0.
-    case: (EM (`|x| = 0)); move=>/eqP; rewrite normr_eq0=> /eqP x0.
-    - by rewrite x0 linear0.
-    - have x00: x != 0 by apply/eqP.
-      have : `| `|x|^-1 *: x | <= 1.
-        rewrite normmZ normrV ?unitf_gt0 ?normrE //=.
-        by rewrite mulrC mulrV ?unitf_gt0 ?normrE //=.
-      move=> /Bf; rewrite linearZ normr_le0 scaler_eq0 invr_eq0 => /orP.
-      by case ; rewrite ?normr_eq0  //=; move => /eqP ->; rewrite linear0.
- - move => M0 x.
-   case: (EM ( x = 0)).
-   - by move=> ->;rewrite normr0 mul0r normr_le0 linear0.
-   - move => /eqP  x0; rewrite mulrC -ler_pdivr_mulr ?normr_gt0 //= mulrC.
-     have <- : `| (`|x|^-1) | = `|x|^-1.
-     by apply/eqP; rewrite eqr_norm_id invr_ge0 normr_ge0.
-     rewrite -normmZ -linearZ; apply: (Bf (`|x|^-1 *: x)).
-     rewrite normmZ normrV ?unitf_gt0 ?normrE //=.
-     rewrite mulrC mulrV  ?unitf_gt0 ?normrE //=.
- - move => /linear_boundedP [r [r0 Bf]]; rewrite /bounded_fun_norm => e.
-   exists (e * r) => x xe; apply: le_trans; first by apply: Bf.
-   by apply: ler_pmul; rewrite ?normr_ge0 //=.
-Qed.
-
-
-
-(* Lemma bounded_landau (f :{linear V->W}) : *)
-(*   bounded_fun_norm f <-> ((f : V -> W) =O_ (0:V) cst (1 : K^o)). *)
-(* Proof. *)
-(*   split. *)
-(*   - rewrite eqOP => bf. *)
-(*     move: (bf 1) => [M bm]. *)
-(*     rewrite !nearE /=; exists M; split. by  apply : num_real. *)
-(*     move => x Mx; rewrite nearE nbhs_normP /=. *)
-(*     exists 1; first by []. *)
-(*     move => y /=. rewrite -ball_normE /ball_ sub0r normrN /cst normr1 mulr1 => y1. *)
-(*     apply: (@le_trans _ _ M _ _). *)
-(*     apply: (bm y); by apply: ltW. *)
-(*     by apply: ltW. *)
-(*   - rewrite eqOP /= ; move => Bf; apply/bounded_funP; rewrite /bounded_on. *)
-(*     near=>M. *)
-(*     set P :=  (X in (nbhs _ X)). *)
-(*     have -> : P  = (fun x : V => (`|f x| <= M * `|cst 1%R x|)%O). *)
-(*       by apply: funext => x; rewrite /cst normr1 mulr1. *)
-(*     by near: M. *)
-(* Grab Existential Variables. all: end_near. Qed. *)
-
+  bounded_fun_norm f <-> bounded_on f (nbhs (0 : V)).
+Proof.
+split => [/(_ 1) [M Bf]|/linear_boundedP [r [r0 Bf]] e]; last first.
+  by exists (e * r) => x xe; rewrite (le_trans (Bf _)) // mulrC ler_pmul.
+apply/linear_boundedP.
+have M0 : 0 <= M by move: (Bf 0); rewrite linear0 !normr0 => /(_ ler01).
+exists M; split => //.
+move: M0; rewrite le0r => /orP[/eqP|] M0 x.
+- rewrite M0 mul0r normr_le0.
+  have [/eqP ->|x0] := boolP (x == 0); first by rewrite linear0.
+  have /Bf : `| `|x|^-1 *: x | <= 1.
+    rewrite normmZ normrV ?unitf_gt0 ?normrE //=.
+    by rewrite mulrC mulrV ?unitf_gt0 ?normrE.
+  rewrite linearZ M0 normr_le0 scaler_eq0 invr_eq0 => /orP[|//].
+  by rewrite normr_eq0 => /eqP ->; rewrite linear0.
+- have [/eqP ->|x0] := boolP (x == 0).
+  + by rewrite normr0 mulr0 normr_le0 linear0.
+  + rewrite -ler_pdivr_mulr ?normr_gt0 //= mulrC.
+     have xx1 : `| `|x|^-1 | = `|x|^-1.
+       by rewrite normrV ?unitfE ?normr_eq0 // normr_id.
+     rewrite -xx1 -normmZ -linearZ; apply: (Bf (`|x|^-1 *: x)).
+     by rewrite normmZ xx1 mulVr // unitfE normr_eq0.
+Qed.
 
 End LinearContinuousBounded.