From eb5fce34396d05fa069ecf8294744f4445da5e19 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 25 Oct 2023 10:10:02 +0900 Subject: [PATCH] add only parsing --- theories/lebesgue_measure.v | 56 +++++++-------- theories/sequences.v | 136 ++++++++++++++++++------------------ 2 files changed, 96 insertions(+), 96 deletions(-) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 13f8e38f7..4d093aa3b 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -548,23 +548,23 @@ Qed. Lemma __deprecated__itv_cpinfty_pinfty : `[+oo%E, +oo[%classic = [set +oo%E] :> set (\bar R). Proof. by rewrite itv_cyy. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_cyy`")] -Notation itv_cpinfty_pinfty := __deprecated__itv_cpinfty_pinfty. +Notation itv_cpinfty_pinfty := __deprecated__itv_cpinfty_pinfty (only parsing). Lemma __deprecated__itv_opinfty_pinfty : `]+oo%E, +oo[%classic = set0 :> set (\bar R). Proof. by rewrite itv_oyy. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_oyy`")] -Notation itv_opinfty_pinfty := __deprecated__itv_opinfty_pinfty. +Notation itv_opinfty_pinfty := __deprecated__itv_opinfty_pinfty (only parsing). Lemma __deprecated__itv_cninfty_pinfty : `[-oo%E, +oo[%classic = setT :> set (\bar R). Proof. by rewrite itv_cNyy. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_cNyy`")] -Notation itv_cninfty_pinfty := __deprecated__itv_cninfty_pinfty. +Notation itv_cninfty_pinfty := __deprecated__itv_cninfty_pinfty (only parsing). Lemma __deprecated__itv_oninfty_pinfty : `]-oo%E, +oo[%classic = ~` [set -oo]%E :> set (\bar R). Proof. by rewrite itv_oNyy. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `itv_oNyy`")] -Notation itv_oninfty_pinfty := __deprecated__itv_oninfty_pinfty. +Notation itv_oninfty_pinfty := __deprecated__itv_oninfty_pinfty (only parsing). Let emeasurable_itv_bndy b (y : \bar R) : measurable [set` Interval (BSide b y) +oo%O]. @@ -695,9 +695,9 @@ Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1| #[global] Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. #[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")] -Notation emeasurable_itv_bnd_pinfty := emeasurable_itv. +Notation emeasurable_itv_bnd_pinfty := emeasurable_itv (only parsing). #[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")] -Notation emeasurable_itv_ninfty_bnd := emeasurable_itv. +Notation emeasurable_itv_ninfty_bnd := emeasurable_itv (only parsing). Lemma measurable_fine (R : realType) (D : set (\bar R)) : measurable D -> measurable_fun D fine. @@ -717,7 +717,7 @@ Qed. #[global] Hint Extern 0 (measurable_fun _ fine) => solve [exact: measurable_fine] : core. #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_fine` instead")] -Notation measurable_fun_fine := measurable_fine. +Notation measurable_fun_fine := measurable_fine (only parsing). Section lebesgue_measure_itv. Variable R : realType. @@ -1459,17 +1459,17 @@ End standard_measurable_fun. #[global] Hint Extern 0 (measurable_fun _ (fun x => x ^+ _)) => solve [exact: measurable_exprn] : core. #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_exprn` instead")] -Notation measurable_fun_sqr := measurable_exprn. +Notation measurable_fun_sqr := measurable_exprn (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_oppr` instead")] -Notation measurable_fun_opp := measurable_oppr. +Notation measurable_fun_opp := measurable_oppr (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_oppr` instead")] -Notation measurable_funN := measurable_oppr. +Notation measurable_funN := measurable_oppr (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_normr` instead")] -Notation measurable_fun_normr := measurable_normr. +Notation measurable_fun_normr := measurable_normr (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_exprn` instead")] -Notation measurable_fun_exprn := measurable_exprn. +Notation measurable_fun_exprn := measurable_exprn (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_mulrl` instead")] -Notation measurable_funrM := measurable_mulrl. +Notation measurable_funrM := measurable_mulrl (only parsing). Section measurable_fun_realType. Context d (T : measurableType d) (R : realType). @@ -1600,7 +1600,7 @@ Qed. End measurable_fun_realType. #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_sup`")] -Notation measurable_fun_lim_sup := measurable_fun_limn_sup. +Notation measurable_fun_lim_sup := measurable_fun_limn_sup (only parsing). Lemma measurable_ln (R : realType) : measurable_fun [set~ (0:R)] (@ln R). Proof. @@ -1619,7 +1619,7 @@ Qed. #[global] Hint Extern 0 (measurable_fun _ (@ln _)) => solve [apply: measurable_ln] : core. #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_ln` instead")] -Notation measurable_fun_ln := measurable_ln. +Notation measurable_fun_ln := measurable_ln (only parsing). Lemma measurable_expR (R : realType) : measurable_fun [set: R] expR. Proof. by apply: continuous_measurable_fun; exact: continuous_expR. Qed. @@ -1639,11 +1639,11 @@ Qed. #[global] Hint Extern 0 (measurable_fun _ (@powR _ ^~ _)) => solve [apply: measurable_powR] : core. #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_powR` instead")] -Notation measurable_fun_power_pos := measurable_powR. +Notation measurable_fun_power_pos := measurable_powR (only parsing). #[deprecated(since="mathcomp-analysis 0.6.4", note="use `measurable_powR` instead")] -Notation measurable_power_pos := measurable_powR. +Notation measurable_power_pos := measurable_powR (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxr` instead")] -Notation measurable_fun_max := measurable_maxr. +Notation measurable_fun_max := measurable_maxr (only parsing). Section standard_emeasurable_fun. Variable R : realType. @@ -1689,11 +1689,11 @@ End standard_emeasurable_fun. #[global] Hint Extern 0 (measurable_fun _ (-%E)) => solve [exact: measurable_oppe] : core. #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_oppe` instead")] -Notation emeasurable_fun_minus := measurable_oppe. +Notation emeasurable_fun_minus := measurable_oppe (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_abse` instead")] -Notation measurable_fun_abse := measurable_abse. +Notation measurable_fun_abse := measurable_abse (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_EFin` instead")] -Notation measurable_fun_EFin := measurable_EFin. +Notation measurable_fun_EFin := measurable_EFin (only parsing). (* NB: real-valued function *) Lemma EFin_measurable_fun d (T : measurableType d) (R : realType) (D : set T) @@ -1720,7 +1720,7 @@ apply: measurable_fun_ifT => //=. + exact/EFin_measurable_fun/measurableT_comp. Qed. #[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_er_map`")] -Notation measurable_fun_er_map := measurable_er_map. +Notation measurable_fun_er_map := measurable_er_map (only parsing). Section emeasurable_fun. Local Open Scope ereal_scope. @@ -1806,17 +1806,17 @@ End emeasurable_fun. Arguments emeasurable_fun_cvg {d T R D} f_. #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurableT_comp` instead")] -Notation emeasurable_funN := measurableT_comp. +Notation emeasurable_funN := measurableT_comp (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxe` instead")] -Notation emeasurable_fun_max := measurable_maxe. +Notation emeasurable_fun_max := measurable_maxe (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_mine` instead")] -Notation emeasurable_fun_min := measurable_mine. +Notation emeasurable_fun_min := measurable_mine (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_funepos` instead")] -Notation emeasurable_fun_funepos := measurable_funepos. +Notation emeasurable_fun_funepos := measurable_funepos (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_funeneg` instead")] -Notation emeasurable_fun_funeneg := measurable_funeneg. +Notation emeasurable_fun_funeneg := measurable_funeneg (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_esup`")] -Notation measurable_fun_lim_esup := measurable_fun_limn_esup. +Notation measurable_fun_lim_esup := measurable_fun_limn_esup (only parsing). Section lebesgue_regularity. Context {d : measure_display} {R : realType}. diff --git a/theories/sequences.v b/theories/sequences.v index d27679827..f5aedde57 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -387,59 +387,59 @@ Lemma __deprecated__squeeze T (f g h : T -> R) (a : filter_on T) : Proof. exact: squeeze_cvgr. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `squeeze_cvgr`")] -Notation squeeze := __deprecated__squeeze. +Notation squeeze := __deprecated__squeeze (only parsing). Lemma __deprecated__cvgPpinfty (u_ : R ^nat) : u_ --> +oo <-> forall A, \forall n \near \oo, A <= u_ n. Proof. exact: cvgryPge. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgryPge`, and generalized to any filter")] -Notation cvgPpinfty := __deprecated__cvgPpinfty. +Notation cvgPpinfty := __deprecated__cvgPpinfty (only parsing). Lemma __deprecated__cvgNpinfty u_ : (- u_ --> +oo) = (u_ --> -oo). Proof. exact/propeqP/cvgNry. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgNry` instead")] -Notation cvgNpinfty := __deprecated__cvgNpinfty. +Notation cvgNpinfty := __deprecated__cvgNpinfty (only parsing). Lemma __deprecated__cvgNninfty u_ : (- u_ --> -oo) = (u_ --> +oo). Proof. exact/propeqP/cvgNrNy. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgNrNy` instead")] -Notation cvgNninfty := __deprecated__cvgNninfty. +Notation cvgNninfty := __deprecated__cvgNninfty (only parsing). Lemma __deprecated__cvgPninfty (u_ : R ^nat) : u_ --> -oo <-> forall A, \forall n \near \oo, A >= u_ n. Proof. exact: cvgrNyPle. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgrNyPle`, and generalized to any filter")] -Notation cvgPninfty := __deprecated__cvgPninfty. +Notation cvgPninfty := __deprecated__cvgPninfty (only parsing). Lemma __deprecated__ger_cvg_pinfty u_ v_ : (\forall n \near \oo, u_ n <= v_ n) -> u_ --> +oo -> v_ --> +oo. Proof. exact: ger_cvgy. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `ger_cvgy`, and generalized to any filter")] -Notation ger_cvg_pinfty := __deprecated__ger_cvg_pinfty. +Notation ger_cvg_pinfty := __deprecated__ger_cvg_pinfty (only parsing). Lemma __deprecated__ler_cvg_ninfty v_ u_ : (\forall n \near \oo, u_ n <= v_ n) -> v_ --> -oo -> u_ --> -oo. Proof. exact: ler_cvgNy. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `ler_cvgNy`, and generalized to any filter")] -Notation ler_cvg_ninfty := __deprecated__ler_cvg_ninfty. +Notation ler_cvg_ninfty := __deprecated__ler_cvg_ninfty (only parsing). Lemma __deprecated__lim_ge x u : cvg u -> (\forall n \near \oo, x <= u n) -> x <= lim u. Proof. exact: limr_ge. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `limr_ge`, and generalized to any proper filter")] -Notation lim_ge := __deprecated__lim_ge. +Notation lim_ge := __deprecated__lim_ge (only parsing). Lemma __deprecated__lim_le x u : cvg u -> (\forall n \near \oo, x >= u n) -> x >= lim u. Proof. exact: limr_le. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `limr_le`, and generalized to any proper filter")] -Notation lim_le := __deprecated__lim_le. +Notation lim_le := __deprecated__lim_le (only parsing). Lemma lt_lim u (M : R) : nondecreasing_seq u -> cvg u -> M < lim u -> \forall n \near \oo, M <= u n. @@ -496,42 +496,42 @@ Lemma __deprecated__cvgPpinfty_lt (u_ : R ^nat) : Proof. exact: cvgryPgt. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgryPgt`, and generalized to any proper filter")] -Notation cvgPpinfty_lt := __deprecated__cvgPpinfty_lt. +Notation cvgPpinfty_lt := __deprecated__cvgPpinfty_lt (only parsing). Lemma __deprecated__cvgPninfty_lt (u_ : R ^nat) : u_ --> -oo%R <-> forall A, \forall n \near \oo, (A > u_ n)%R. Proof. exact: cvgrNyPlt. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgrNyPlt`, and generalized to any proper filter")] -Notation cvgPninfty_lt := __deprecated__cvgPninfty_lt. +Notation cvgPninfty_lt := __deprecated__cvgPninfty_lt (only parsing). Lemma __deprecated__cvgPpinfty_near (u_ : R ^nat) : u_ --> +oo%R <-> \forall A \near +oo, \forall n \near \oo, (A <= u_ n)%R. Proof. exact: cvgryPgey. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgryPgey`, and generalized to any proper filter")] -Notation cvgPpinfty_near := __deprecated__cvgPpinfty_near. +Notation cvgPpinfty_near := __deprecated__cvgPpinfty_near (only parsing). Lemma __deprecated__cvgPninfty_near (u_ : R ^nat) : u_ --> -oo%R <-> \forall A \near -oo, \forall n \near \oo, (A >= u_ n)%R. Proof. exact: cvgrNyPleNy. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgrNyPleNy`, and generalized to any proper filter")] -Notation cvgPninfty_near := __deprecated__cvgPninfty_near. +Notation cvgPninfty_near := __deprecated__cvgPninfty_near (only parsing). Lemma __deprecated__cvgPpinfty_lt_near (u_ : R ^nat) : u_ --> +oo%R <-> \forall A \near +oo, \forall n \near \oo, (A < u_ n)%R. Proof. exact: cvgryPgty. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgryPgty`, and generalized to any proper filter")] -Notation cvgPpinfty_lt_near := __deprecated__cvgPpinfty_lt_near. +Notation cvgPpinfty_lt_near := __deprecated__cvgPpinfty_lt_near (only parsing). Lemma __deprecated__cvgPninfty_lt_near (u_ : R ^nat) : u_ --> -oo%R <-> \forall A \near -oo, \forall n \near \oo, (A > u_ n)%R. Proof. exact: cvgrNyPltNy. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgrNyPltNy`, and generalized to any proper filter")] -Notation cvgPninfty_lt_near := __deprecated__cvgPninfty_lt_near. +Notation cvgPninfty_lt_near := __deprecated__cvgPninfty_lt_near (only parsing). End sequences_R_lemmas_realFieldType. @@ -540,14 +540,14 @@ Lemma __deprecated__invr_cvg0 (R : realFieldType) (u : R^nat) : Proof. by move=> ?; rewrite gtr0_cvgV0//; apply: nearW. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `gtr0_cvgV0` and generalized")] -Notation invr_cvg0 := __deprecated__invr_cvg0. +Notation invr_cvg0 := __deprecated__invr_cvg0 (only parsing). Lemma __deprecated__invr_cvg_pinfty (R : realFieldType) (u : R^nat) : (forall i, 0 < u i) -> ((u i)^-1 @[i --> \oo] --> +oo) <-> (u --> 0). Proof. by move=> ?; rewrite cvgrVy//; apply: nearW. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgrVy` and generalized")] -Notation invr_cvg_pinfty := __deprecated__invr_cvg_pinfty. +Notation invr_cvg_pinfty := __deprecated__invr_cvg_pinfty (only parsing). Section partial_sum. Variables (V : zmodType) (u_ : V ^nat). @@ -1258,14 +1258,14 @@ Lemma __deprecated__nat_dvg_real (R : realType) (u_ : nat ^nat) : u_ --> \oo -> Proof. by move=> ?; apply/cvgrnyP. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgrnyP` and generalized")] -Notation nat_dvg_real := __deprecated__nat_dvg_real. +Notation nat_dvg_real := __deprecated__nat_dvg_real (only parsing). Lemma __deprecated__nat_cvgPpinfty (u : nat^nat) : u --> \oo <-> forall A, \forall n \near \oo, (A <= u n)%N. Proof. exact: cvgnyPge. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgnyPge` and generalized")] -Notation nat_cvgPpinfty:= __deprecated__nat_cvgPpinfty. +Notation nat_cvgPpinfty:= __deprecated__nat_cvgPpinfty (only parsing). Lemma nat_nondecreasing_is_cvg (u_ : nat^nat) : nondecreasing_seq u_ -> has_ubound (range u_) -> cvg u_. @@ -1422,34 +1422,34 @@ Lemma __deprecated__ereal_cvg_abs0 (R : realFieldType) (f : (\bar R)^nat) : Proof. by move/cvg_abse0P. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvg_abse0P` and generalized")] -Notation ereal_cvg_abs0 := __deprecated__ereal_cvg_abs0. +Notation ereal_cvg_abs0 := __deprecated__ereal_cvg_abs0 (only parsing). Lemma __deprecated__ereal_cvg_ge0 (R : realFieldType) (f : (\bar R)^nat) (a : \bar R) : (forall n, 0 <= f n) -> f --> a -> 0 <= a. Proof. by move=> f_ge0; apply: cvge_ge; apply: nearW. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvge_ge` instead")] -Notation ereal_cvg_ge0 := __deprecated__ereal_cvg_ge0. +Notation ereal_cvg_ge0 := __deprecated__ereal_cvg_ge0 (only parsing). Lemma __deprecated__ereal_lim_ge (R : realFieldType) x (u_ : (\bar R)^nat) : cvg u_ -> (\forall n \near \oo, x <= u_ n) -> x <= lim u_. Proof. exact: lime_ge. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `lime_ge` and generalized")] -Notation ereal_lim_ge := __deprecated__ereal_lim_ge. +Notation ereal_lim_ge := __deprecated__ereal_lim_ge (only parsing). Lemma __deprecated__ereal_lim_le (R : realFieldType) x (u_ : (\bar R)^nat) : cvg u_ -> (\forall n \near \oo, u_ n <= x) -> lim u_ <= x. Proof. exact: lime_le. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `lime_le` and generalized")] -Notation ereal_lim_le := __deprecated__ereal_lim_le. +Notation ereal_lim_le := __deprecated__ereal_lim_le (only parsing). Lemma __deprecated__dvg_ereal_cvg (R : realFieldType) (u_ : R ^nat) : u_ --> +oo%R -> [sequence (u_ n)%:E]_n --> +oo. Proof. by rewrite cvgeryP. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgeryP` and generalized")] -Notation dvg_ereal_cvg := __deprecated__dvg_ereal_cvg. +Notation dvg_ereal_cvg := __deprecated__dvg_ereal_cvg (only parsing). Lemma __deprecated__ereal_cvg_real (R : realFieldType) (f : (\bar R)^nat) a : {near \oo, forall x, f x \is a fin_num} /\ @@ -1457,7 +1457,7 @@ Lemma __deprecated__ereal_cvg_real (R : realFieldType) (f : (\bar R)^nat) a : Proof. by rewrite fine_cvgP. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `fine_cvgP` and generalized")] -Notation ereal_cvg_real := __deprecated__ereal_cvg_real. +Notation ereal_cvg_real := __deprecated__ereal_cvg_real (only parsing). Lemma ereal_nondecreasing_cvg (R : realType) (u_ : (\bar R)^nat) : nondecreasing_seq u_ -> u_ --> ereal_sup (range u_). @@ -1713,7 +1713,7 @@ by split=> [/cvgeyPge//|u_ge]; apply/cvgeyPgey; near=> x; apply: u_ge. Unshelve. all: by end_near. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeyPge` or a variant instead")] -Notation ereal_cvgPpinfty := __deprecated__ereal_cvgPpinfty. +Notation ereal_cvgPpinfty := __deprecated__ereal_cvgPpinfty (only parsing). Lemma __deprecated__ereal_cvgPninfty (R : realFieldType) (u_ : (\bar R)^nat) : u_ --> -oo <-> (forall A, (A < 0)%R -> \forall n \near \oo, u_ n <= A%:E). @@ -1722,7 +1722,7 @@ by split=> [/cvgeNyPle//|u_ge]; apply/cvgeNyPleNy; near=> x; apply: u_ge. Unshelve. all: by end_near. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeNyPle` or a variant instead")] -Notation ereal_cvgPninfty := __deprecated__ereal_cvgPninfty. +Notation ereal_cvgPninfty := __deprecated__ereal_cvgPninfty (only parsing). Lemma __deprecated__ereal_squeeze (R : realType) (f g h : (\bar R)^nat) : (\forall x \near \oo, f x <= g x <= h x) -> forall (l : \bar R), @@ -1730,7 +1730,7 @@ Lemma __deprecated__ereal_squeeze (R : realType) (f g h : (\bar R)^nat) : Proof. by move=> ? ?; apply: squeeze_cvge. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `squeeze_cvge` and generalized")] -Notation ereal_squeeze := __deprecated__ereal_squeeze. +Notation ereal_squeeze := __deprecated__ereal_squeeze (only parsing). Lemma nneseries_pinfty (R : realType) (u_ : (\bar R)^nat) (P : pred nat) k : (forall n, P n -> 0 <= u_ n) -> P k -> @@ -1767,32 +1767,32 @@ Lemma __deprecated__ereal_cvgD_pinfty_fin (R : realFieldType) (f g : (\bar R)^na f --> +oo -> g --> b%:E -> f \+ g --> +oo. Proof. exact: cvgeD. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")] -Notation ereal_cvgD_pinfty_fin := __deprecated__ereal_cvgD_pinfty_fin. +Notation ereal_cvgD_pinfty_fin := __deprecated__ereal_cvgD_pinfty_fin (only parsing). Lemma __deprecated__ereal_cvgD_ninfty_fin (R : realFieldType) (f g : (\bar R)^nat) b : f --> -oo -> g --> b%:E -> f \+ g --> -oo. Proof. exact: cvgeD. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")] -Notation ereal_cvgD_ninfty_fin := __deprecated__ereal_cvgD_ninfty_fin. +Notation ereal_cvgD_ninfty_fin := __deprecated__ereal_cvgD_ninfty_fin (only parsing). Lemma __deprecated__ereal_cvgD_pinfty_pinfty (R : realFieldType) (f g : (\bar R)^nat) : f --> +oo -> g --> +oo -> f \+ g --> +oo. Proof. exact: cvgeD. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")] -Notation ereal_cvgD_pinfty_pinfty := __deprecated__ereal_cvgD_pinfty_pinfty. +Notation ereal_cvgD_pinfty_pinfty := __deprecated__ereal_cvgD_pinfty_pinfty (only parsing). Lemma __deprecated__ereal_cvgD_ninfty_ninfty (R : realFieldType) (f g : (\bar R)^nat) : f --> -oo -> g --> -oo -> f \+ g --> -oo. Proof. exact: cvgeD. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")] -Notation ereal_cvgD_ninfty_ninfty := __deprecated__ereal_cvgD_ninfty_ninfty. +Notation ereal_cvgD_ninfty_ninfty := __deprecated__ereal_cvgD_ninfty_ninfty (only parsing). Lemma __deprecated__ereal_cvgD (R : realFieldType) (f g : (\bar R)^nat) a b : a +? b -> f --> a -> g --> b -> f \+ g --> a + b. Proof. exact: cvgeD. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgeD` and generalized")] -Notation ereal_cvgD := __deprecated__ereal_cvgD. +Notation ereal_cvgD := __deprecated__ereal_cvgD (only parsing). Section nneseries_split. @@ -1801,21 +1801,21 @@ Lemma __deprecated__ereal_cvgB (R : realFieldType) (f g : (\bar R)^nat) a b : Proof. exact: cvgeB. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgeB` and generalized")] -Notation ereal_cvgB := __deprecated__ereal_cvgB. +Notation ereal_cvgB := __deprecated__ereal_cvgB (only parsing). Lemma __deprecated__ereal_is_cvgD (R : realFieldType) (u v : (\bar R)^nat) : lim u +? lim v -> cvg u -> cvg v -> cvg (u \+ v). Proof. exact: is_cvgeD. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `is_cvgeD` and generalized")] -Notation ereal_is_cvgD := __deprecated__ereal_is_cvgD. +Notation ereal_is_cvgD := __deprecated__ereal_is_cvgD (only parsing). Lemma __deprecated__ereal_cvg_sub0 (R : realFieldType) (f : (\bar R)^nat) (k : \bar R) : k \is a fin_num -> (fun x => f x - k) --> 0 <-> f --> k. Proof. exact: cvge_sub0. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvge_sub0` and generalized")] -Notation ereal_cvg_sub0 := __deprecated__ereal_cvg_sub0. +Notation ereal_cvg_sub0 := __deprecated__ereal_cvg_sub0 (only parsing). Lemma __deprecated__ereal_limD (R : realFieldType) (f g : (\bar R)^nat) : cvg f -> cvg g -> lim f +? lim g -> @@ -1823,7 +1823,7 @@ Lemma __deprecated__ereal_limD (R : realFieldType) (f g : (\bar R)^nat) : Proof. exact: limeD. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `limeD` and generalized")] -Notation ereal_limD := __deprecated__ereal_limD. +Notation ereal_limD := __deprecated__ereal_limD (only parsing). Lemma __deprecated__ereal_cvgM_gt0_pinfty (R : realFieldType) (f g : (\bar R)^nat) b : (0 < b)%R -> f --> +oo -> g --> b%:E -> f \* g --> +oo. @@ -1832,7 +1832,7 @@ move=> b_lt0 fl gl; have /= := cvgeM _ fl gl; rewrite gt0_mulye//; apply. by rewrite mule_def_infty_neq0// gt_eqF. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")] -Notation ereal_cvgM_gt0_pinfty := __deprecated__ereal_cvgM_gt0_pinfty. +Notation ereal_cvgM_gt0_pinfty := __deprecated__ereal_cvgM_gt0_pinfty (only parsing). Lemma __deprecated__ereal_cvgM_lt0_pinfty (R : realFieldType) (f g : (\bar R)^nat) b : (b < 0)%R -> f --> +oo -> g --> b%:E -> f \* g --> -oo. @@ -1841,7 +1841,7 @@ move=> b_lt0 fl gl; have /= := cvgeM _ fl gl; rewrite lt0_mulye//; apply. by rewrite mule_def_infty_neq0// lt_eqF. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")] -Notation ereal_cvgM_lt0_pinfty := __deprecated__ereal_cvgM_lt0_pinfty. +Notation ereal_cvgM_lt0_pinfty := __deprecated__ereal_cvgM_lt0_pinfty (only parsing). Lemma __deprecated__ereal_cvgM_gt0_ninfty (R : realFieldType) (f g : (\bar R)^nat) b : (0 < b)%R -> f --> -oo -> g --> b%:E -> f \* g --> -oo. @@ -1850,7 +1850,7 @@ move=> b_lt0 fl gl; have /= := cvgeM _ fl gl; rewrite gt0_mulNye//; apply. by rewrite mule_def_infty_neq0// gt_eqF. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")] -Notation ereal_cvgM_gt0_ninfty := __deprecated__ereal_cvgM_gt0_ninfty. +Notation ereal_cvgM_gt0_ninfty := __deprecated__ereal_cvgM_gt0_ninfty (only parsing). Lemma __deprecated__ereal_cvgM_lt0_ninfty (R : realFieldType) (f g : (\bar R)^nat) b : (b < 0)%R -> f --> -oo -> g --> b%:E -> f \* g --> +oo. @@ -1859,14 +1859,14 @@ move=> b_lt0 fl gl; have /= := cvgeM _ fl gl; rewrite lt0_mulNye//; apply. by rewrite mule_def_infty_neq0// lt_eqF. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")] -Notation ereal_cvgM_lt0_ninfty := __deprecated__ereal_cvgM_lt0_ninfty. +Notation ereal_cvgM_lt0_ninfty := __deprecated__ereal_cvgM_lt0_ninfty (only parsing). Lemma __deprecated__ereal_cvgM (R : realType) (f g : (\bar R) ^nat) (a b : \bar R) : a *? b -> f --> a -> g --> b -> f \* g --> a * b. Proof. exact: cvgeM. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgeM` and generalized")] -Notation ereal_cvgM := __deprecated__ereal_cvgM. +Notation ereal_cvgM := __deprecated__ereal_cvgM (only parsing). Lemma __deprecated__ereal_lim_sum (R : realFieldType) (I : Type) (r : seq I) (f : I -> (\bar R)^nat) (l : I -> \bar R) (P : pred I) : @@ -1878,7 +1878,7 @@ by move=> f0 ?; apply: cvg_nnesum => // ? ?; apply: nearW => ?; apply: f0. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvg_nnesum` and generalized")] -Notation ereal_lim_sum := __deprecated__ereal_lim_sum. +Notation ereal_lim_sum := __deprecated__ereal_lim_sum (only parsing). Let lim_shift_cst (R : realFieldType) (u : (\bar R) ^nat) (l : \bar R) : cvg u -> (forall n, 0 <= u n) -> -oo < l -> lim (fun x => l + u x) = l + lim u. @@ -1977,13 +1977,13 @@ Proof. by congr (lim _); apply: eq_fun => n /=; apply: big_mkcond. Qed. End sequences_ereal. #[deprecated(since="analysis 0.6.0", note="Use eseries0 instead.")] -Notation nneseries0 := eseries0. +Notation nneseries0 := eseries0 (only parsing). #[deprecated(since="analysis 0.6.0", note="Use eq_eseriesr instead.")] -Notation eq_nneseries := eq_eseriesr. +Notation eq_nneseries := eq_eseriesr (only parsing). #[deprecated(since="analysis 0.6.0", note="Use eseries_pred0 instead.")] -Notation nneseries_pred0 := eseries_pred0. +Notation nneseries_pred0 := eseries_pred0 (only parsing). #[deprecated(since="analysis 0.6.0", note="Use eseries_mkcond instead.")] -Notation nneseries_mkcond := eseries_mkcond. +Notation nneseries_mkcond := eseries_mkcond (only parsing). Definition sdrop T (u : T^nat) n := [set u k | k in [set k | k >= n]]%N. @@ -2300,29 +2300,29 @@ Qed. End limn_sup_limn_inf. #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_sup`")] -Notation lim_sup := limn_sup. +Notation lim_sup := limn_sup (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_inf`")] -Notation lim_inf := limn_sup. +Notation lim_inf := limn_sup (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_infN`")] -Notation lim_infN := limn_infN. +Notation lim_infN := limn_infN (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_supE`")] -Notation lim_supE := limn_supE. +Notation lim_supE := limn_supE (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_infE`")] -Notation lim_infE := limn_infE. +Notation lim_infE := limn_infE (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_inf_sup`")] -Notation lim_inf_le_lim_sup := limn_inf_sup. +Notation lim_inf_le_lim_sup := limn_inf_sup (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `cvg_limn_infE`")] -Notation cvg_lim_infE := cvg_limn_infE. +Notation cvg_lim_infE := cvg_limn_infE (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `cvg_limn_supE`")] -Notation cvg_lim_supE := cvg_limn_supE. +Notation cvg_lim_supE := cvg_limn_supE (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `le_limn_supD`")] -Notation le_lim_supD := le_limn_supD. +Notation le_lim_supD := le_limn_supD (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `le_limn_infD`")] -Notation le_lim_infD := le_limn_infD. +Notation le_lim_infD := le_limn_infD (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_supD`")] -Notation lim_supD := limn_supD. +Notation lim_supD := limn_supD (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_infD`")] -Notation lim_infD := limn_infD. +Notation lim_infD := limn_infD (only parsing). Section esups_einfs. Variable R : realType. @@ -2540,23 +2540,23 @@ Qed. End lim_esup_inf. #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_einf_shift`")] -Notation lim_einf_shift := limn_einf_shift. +Notation lim_einf_shift := limn_einf_shift (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_esup_le_cvg`")] -Notation lim_esup_le_cvg := limn_esup_le_cvg. +Notation lim_esup_le_cvg := limn_esup_le_cvg (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_einfN`")] -Notation lim_einfN := limn_einfN. +Notation lim_einfN := limn_einfN (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_esupN`")] -Notation lim_esupN := limn_esupN. +Notation lim_esupN := limn_esupN (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_einf_sup`")] -Notation lim_einf_sup := limn_einf_sup. +Notation lim_einf_sup := limn_einf_sup (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `cvgNy_limn_einf_sup`")] -Notation cvgNy_lim_einf_sup := cvgNy_limn_einf_sup. +Notation cvgNy_lim_einf_sup := cvgNy_limn_einf_sup (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `cvg_limn_einf_sup`")] -Notation cvg_lim_einf_sup := cvg_limn_einf_sup. +Notation cvg_lim_einf_sup := cvg_limn_einf_sup (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `is_cvg_limn_einfE`")] -Notation is_cvg_lim_einfE := is_cvg_limn_einfE. +Notation is_cvg_lim_einfE := is_cvg_limn_einfE (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `is_cvg_limn_esupE`")] -Notation is_cvg_lim_esupE := is_cvg_limn_esupE. +Notation is_cvg_lim_esupE := is_cvg_limn_esupE (only parsing). Lemma geometric_le_lim {R : realType} (n : nat) (a x : R) : 0 <= a -> 0 < x -> `|x| < 1 -> series (geometric a x) n <= a * (1 - x)^-1.