diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 08df059ce0..b7c04b703d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -140,6 +140,12 @@ - in `normedtype.v`: + `cvge_sub0` -> `sube_cvg0` +- in `measure.v`: + + `setDI_closed` -> `setD_closed` + + `setDI_semi_setD_closed` -> `setD_semi_setD_closed` + + `sedDI_closedP` -> `setD_closedP` + + `setringDI` -> `setringD` + ### Generalized - in `sequences.v`, @@ -184,6 +190,45 @@ - in file `pseudometric_structure.v`, removed `discrete_ball_center`, `discrete_topology_type`, and `discrete_space_discrete`. +- in `measure.v`: + + notation `caratheodory_lim_lee` (was deprecated since 0.6.0) + +- in `lebesgue_measure.v`: + + notations `itv_cpinfty_pinfty`, `itv_opinfty_pinfty`, `itv_cninfty_pinfty`, + `itv_oninfty_pinfty` (were deprecated since 0.6.0) + + lemmas `__deprecated__itv_cpinfty_pinfty`, `__deprecated__itv_opinfty_pinfty`, + `__deprecated__itv_cninfty_pinfty`, `__deprecated__itv_oninfty_pinfty` + (were deprecated since 0.6.0) + +- in `sequences.v`: + + notations `cvgPpinfty_lt`, `cvgPninfty_lt`, `cvgPpinfty_near`, + `cvgPninfty_near`, `cvgPpinfty_lt_near`, `cvgPninfty_lt_near`, + `ereal_cvgD_ninfty_ninfty`, `invr_cvg0`, `invr_cvg_pinfty`, + `nat_dvg_real`, `nat_cvgPpinfty`, `ereal_squeeze`, `ereal_cvgD_pinfty_fin`, + `ereal_cvgD_ninfty_fin`, `ereal_cvgD_pinfty_pinfty`, `ereal_cvgD`, + `ereal_cvgB`, `ereal_is_cvgD`, `ereal_cvg_sub0`, `ereal_limD`, + `ereal_cvgM_gt0_pinfty`, `ereal_cvgM_lt0_pinfty`, `ereal_cvgM_gt0_ninfty`, + `ereal_cvgM_lt0_ninfty`, `ereal_cvgM`, `ereal_lim_sum`, `ereal_cvg_abs0`, + `ereal_cvg_ge0`, `ereal_lim_ge`, `ereal_lim_le`, `dvg_ereal_cvg`, + `ereal_cvg_real` + (were deprecated since 0.6.0) + + lemmas `__deprecated__cvgPpinfty_lt`, `__deprecated__cvgPninfty_lt`, + `__deprecated__cvgPpinfty_near`, `__deprecated__cvgPninfty_near`, + `__deprecated__cvgPpinfty_lt_near`, `__deprecated__cvgPninfty_lt_near`, + `__deprecated__invr_cvg0`, `__deprecated__invr_cvg_pinfty`, + `__deprecated__nat_dvg_real`, `__deprecated__nat_cvgPpinfty`, + `__deprecated__ereal_squeeze`, `__deprecated__ereal_cvgD_pinfty_fin`, + `__deprecated__ereal_cvgD_ninfty_fin`, `__deprecated__ereal_cvgD_pinfty_pinfty`, + `__deprecated__ereal_cvgD`, `__deprecated__ereal_cvgB`, `__deprecated__ereal_is_cvgD`, + `__deprecated__ereal_cvg_sub0`, `__deprecated__ereal_limD`, + `__deprecated__ereal_cvgM_gt0_pinfty`, `__deprecated__ereal_cvgM_lt0_pinfty`, + `__deprecated__ereal_cvgM_gt0_ninfty`, `__deprecated__ereal_cvgM_lt0_ninfty`, + `__deprecated__ereal_cvgM`, `__deprecated__ereal_lim_sum`, + `__deprecated__ereal_cvg_abs0`, `__deprecated__ereal_cvg_ge0`, + `__deprecated__ereal_lim_ge`, `__deprecated__ereal_lim_le`, + `__deprecated__dvg_ereal_cvg`, `__deprecated__ereal_cvg_real` + (were deprecated since 0.6.0) + ### Infrastructure ### Misc diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index d02b5f20eb..802b4b3655 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -320,27 +320,6 @@ case: x => [r| |]. Qed. #[local] Hint Resolve emeasurable_set1 : core. -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 (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 (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 (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 (only parsing). - Let emeasurable_itv_bndy b (y : \bar R) : measurable [set` Interval (BSide b y) +oo%O]. Proof. diff --git a/theories/measure.v b/theories/measure.v index 013b1a8047..c20af032e1 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -185,7 +185,7 @@ From HB Require Import structures. (* setC_closed G == the set of sets G is closed under complement *) (* setSD_closed G == the set of sets G is closed under proper *) (* difference *) -(* setDI_closed G == the set of sets G is closed under difference *) +(* setD_closed G == the set of sets G is closed under difference *) (* setY_closed G == the set of sets G is closed under symmetric *) (* difference *) (* ndseq_closed G == the set of sets G is closed under non-decreasing *) @@ -354,7 +354,7 @@ Definition setC_closed := forall A, G A -> G (~` A). Definition setI_closed := forall A B, G A -> G B -> G (A `&` B). Definition setU_closed := forall A B, G A -> G B -> G (A `|` B). Definition setSD_closed := forall A B, B `<=` A -> G A -> G B -> G (A `\` B). -Definition setDI_closed := forall A B, G A -> G B -> G (A `\` B). +Definition setD_closed := forall A B, G A -> G B -> G (A `\` B). Definition setY_closed := forall A B, G A -> G B -> G (A `+` B). Definition fin_bigcap_closed := @@ -373,7 +373,7 @@ Definition fin_bigcup_closed := Definition semi_setD_closed := forall A B, G A -> G B -> exists D, [/\ finite_set D, D `<=` G, A `\` B = \bigcup_(X in D) X & trivIset D id]. -Lemma setDI_semi_setD_closed : setDI_closed -> semi_setD_closed. +Lemma setD_semi_setD_closed : setD_closed -> semi_setD_closed. Proof. move=> mD A B Am Bm; exists [set A `\` B]; split; rewrite ?bigcup_set1//. by move=> X ->; apply: mD. @@ -394,9 +394,9 @@ Definition fin_trivIset_closed := forall I (D : set I) (F : I -> set T), finite_set D -> trivIset D F -> (forall i, D i -> G (F i)) -> G (\bigcup_(k in D) F k). -Definition setring := [/\ G set0, setU_closed & setDI_closed]. +Definition setring := [/\ G set0, setU_closed & setD_closed]. -Definition sigma_ring := [/\ G set0, setDI_closed & +Definition sigma_ring := [/\ G set0, setD_closed & (forall A : (set T)^nat, (forall n, G (A n)) -> G (\bigcup_k A k))]. Definition sigma_algebra := @@ -416,8 +416,12 @@ Definition monotone := ndseq_closed /\ niseq_closed. End set_systems. #[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `lambda_system`")] Notation monotone_class := lambda_system (only parsing). -#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `setSD_closed`")] -Notation setD_closed := setSD_closed (only parsing). +(*#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `setSD_closed`")] +Notation setD_closed := setSD_closed (only parsing).*) +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed `setD_closed`")] +Notation setDI_closed := setD_closed (only parsing). +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed `setD_semi_setD_closed`")] +Notation setDI_semi_setD_closed := setD_semi_setD_closed (only parsing). Lemma powerset_sigma_ring (T : Type) (D : set T) : sigma_ring [set X | X `<=` D]. @@ -485,8 +489,8 @@ rewrite in_fset_set// inE => -[Dj /eqP nij] GAB. by rewrite setICA; apply: GI => //; apply: GA. Qed. -Lemma sedDI_closedP T (G : set (set T)) : - setDI_closed G <-> (setI_closed G /\ setSD_closed G). +Lemma setD_closedP T (G : set (set T)) : + setD_closed G <-> (setI_closed G /\ setSD_closed G). Proof. split=> [GDI|[GI GD]]. by split=> A B => [|AB] => GA GB; rewrite -?setDD//; do ?apply: (GDI). @@ -494,6 +498,8 @@ move=> A B GA GB; suff <- : A `\` (A `&` B) = A `\` B. by apply: GD => //; apply: GI. by rewrite setDE setCI setIUr -setDE setDv set0U. Qed. +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed `setD_closed`")] +Notation sedDI_closedP := setD_closed (only parsing). Lemma sigma_algebra_bigcap T (I : choiceType) (D : set T) (F : I -> set (set T)) (J : set I) : @@ -594,7 +600,7 @@ Lemma sub_setring : G `<=` <>. Proof. exact: sub_smallest. Qed. Lemma setring0 : <> set0. Proof. by case: smallest_setring. Qed. -Lemma setringDI : setDI_closed <>. +Lemma setringD : setD_closed <>. Proof. by case: smallest_setring. Qed. Lemma setringU : setU_closed <>. @@ -607,6 +613,8 @@ Qed. End generated_setring. #[global] Hint Resolve smallest_setring setring0 : core. +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed `setringD`")] +Notation setringDI := setringD (only parsing). Lemma g_sigma_algebra_lambda_system T (G : set (set T)) (D : set T) : (forall X, <> X -> X `<=` D) -> @@ -1112,7 +1120,7 @@ HB.structure Definition SigmaRing d := HB.factory Record isSigmaRing (d : measure_display) T of Pointed T := { measurable : set (set T) ; measurable0 : measurable set0 ; - measurableD : setDI_closed measurable ; + measurableD : setD_closed measurable ; bigcupT_measurable : forall F : (set T)^nat, (forall i, measurable (F i)) -> measurable (\bigcup_i (F i)) }. @@ -1122,10 +1130,10 @@ HB.builders Context d T of isSigmaRing d T. Let m0 : measurable set0. Proof. exact: measurable0. Qed. Let mI : setI_closed measurable. -Proof. by have [] := (sedDI_closedP measurable).1 measurableD. Qed. +Proof. by have [] := (setD_closedP measurable).1 measurableD. Qed. Let mD : semi_setD_closed measurable. -Proof. by apply: setDI_semi_setD_closed; exact: measurableD. Qed. +Proof. by apply: setD_semi_setD_closed; exact: measurableD. Qed. HB.instance Definition _ := isSemiRingOfSets.Build d T m0 mI mD. @@ -1141,17 +1149,17 @@ HB.factory Record isRingOfSets (d : measure_display) T of Pointed T := { measurable : set (set T) ; measurable0 : measurable set0 ; measurableU : setU_closed measurable; - measurableD : setDI_closed measurable; + measurableD : setD_closed measurable; }. HB.builders Context d T of isRingOfSets d T. Implicit Types (A B C D : set T). Lemma mI : setI_closed measurable. -Proof. by have [] := (sedDI_closedP measurable).1 measurableD. Qed. +Proof. by have [] := (setD_closedP measurable).1 measurableD. Qed. Lemma mD : semi_setD_closed measurable. -Proof. by apply: setDI_semi_setD_closed; exact: measurableD. Qed. +Proof. by apply: setD_semi_setD_closed; exact: measurableD. Qed. HB.instance Definition _ := @isSemiRingOfSets.Build d T measurable measurable0 mI mD. @@ -1182,7 +1190,7 @@ move=> A B mA mB; rewrite -setYU. by apply: measurable_setY; [exact: measurable_setY|exact: measurable_setI]. Qed. -Let mD : setDI_closed measurable. +Let mD : setD_closed measurable. Proof. move=> A B mA mB; rewrite -setYD. by apply: measurable_setY => //; exact: measurable_setI. @@ -1201,7 +1209,7 @@ HB.factory Record isAlgebraOfSets (d : measure_display) T of Pointed T := { HB.builders Context d T of isAlgebraOfSets d T. -Lemma mD : setDI_closed measurable. +Lemma mD : setD_closed measurable. Proof. move=> A B mA mB; rewrite setDE -[A]setCK -setCU. by do ?[apply: measurableU | apply: measurableC]. @@ -1220,7 +1228,7 @@ HB.end. HB.factory Record isAlgebraOfSets_setD (d : measure_display) T of Pointed T := { measurable : set (set T) ; measurableT : measurable [set: T] ; - measurableD : setDI_closed measurable + measurableD : setD_closed measurable }. HB.builders Context d T of isAlgebraOfSets_setD d T. @@ -1291,7 +1299,7 @@ rewrite -bigsetU_fset_set// big_seq; apply: bigsetU_measurable => i. by rewrite in_fset_set ?inE// => *; apply: Fm. Qed. -Lemma measurableD : setDI_closed (@measurable d T). +Lemma measurableD : setD_closed (@measurable d T). Proof. move=> A B mA mB; case: (semi_measurableD A B) => // [D [Dfin Dl -> _]]. by apply: fin_bigcup_measurable. @@ -2632,7 +2640,7 @@ Notation rT := (type T). HB.instance Definition _ := Pointed.on rT. #[export] HB.instance Definition _ := isRingOfSets.Build (display d) rT - (@setring0 T measurable) (@setringU T measurable) (@setringDI T measurable). + (@setring0 T measurable) (@setringU T measurable) (@setringD T measurable). Local Notation "d .-ring" := (display d) (at level 1, format "d .-ring"). Local Notation "d .-ring.-measurable" := @@ -2681,7 +2689,7 @@ have mdU : fin_trivIset_closed measurable_fin_trivIset. by rewrite {i}eqij in Di Gi *; have [_ _ _ /(_ _ _ _ _ XYN0)->] := GP j Dj. apply: Ftriv => //; have [-> _ _ _] := GP j Dj; have [-> _ _ _] := GP i Di. by case: XYN0 => [x [Xx Yx]]; exists x; split; [exists X|exists Y]. -have mdDI : setDI_closed measurable_fin_trivIset. +have mdDI : setD_closed measurable_fin_trivIset. move=> A B mA mB; have [F [-> Fm Ffin Ftriv]] := mA. have [F' [-> F'm F'fin F'triv]] := mB. have [->|/set0P F'N0] := eqVneq F' set0. @@ -4444,9 +4452,6 @@ apply: (@le_trans _ _ (\sum_(k < n) mu (X `&` A k) + mu (X `&` ~` B n))). rewrite [in leRHS](caratheodory_measurable_bigsetU MA n) leeD2r//. by rewrite caratheodory_additive. Qed. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed `caratheodory_lime_le`")] -Notation caratheodory_lim_lee := caratheodory_lime_le (only parsing). Lemma caratheodory_measurable_trivIset_bigcup (A : (set T) ^nat) : (forall n, M (A n)) -> trivIset setT A -> M (\bigcup_k (A k)). diff --git a/theories/sequences.v b/theories/sequences.v index 6e8e8fb05e..eead6b72b7 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -473,48 +473,6 @@ Qed. Lemma cvg_has_inf u_ : cvgn u_ -> has_inf (u_ @` setT). Proof. by move/is_cvgN/cvg_has_sup; rewrite -has_inf_supN image_comp. Qed. -Lemma __deprecated__cvgPpinfty_lt (u_ : R ^nat) : - u_ @ \oo --> +oo%R <-> forall A, \forall n \near \oo, (A < u_ n)%R. -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 (only parsing). - -Lemma __deprecated__cvgPninfty_lt (u_ : R ^nat) : - u_ @ \oo --> -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 (only parsing). - -Lemma __deprecated__cvgPpinfty_near (u_ : R ^nat) : - u_ @ \oo --> +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 (only parsing). - -Lemma __deprecated__cvgPninfty_near (u_ : R ^nat) : - u_ @ \oo --> -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 (only parsing). - -Lemma __deprecated__cvgPpinfty_lt_near (u_ : R ^nat) : - u_ @ \oo --> +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 (only parsing). - -Lemma __deprecated__cvgPninfty_lt_near (u_ : R ^nat) : - u_ @ \oo --> -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 (only parsing). - End sequences_R_lemmas_realFieldType. #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `nonincreasing_cvgn_ge`")] @@ -523,20 +481,6 @@ Notation nonincreasing_cvg_ge := nonincreasing_cvgn_ge (only parsing). note="renamed to `nondecreasing_cvgn_le`")] Notation nondecreasing_cvg_le := nondecreasing_cvgn_le (only parsing). -Lemma __deprecated__invr_cvg0 (R : realFieldType) (u : R^nat) : - (forall i, 0 < u i) -> ((u i)^-1 @[i --> \oo] --> 0) <-> (u @ \oo --> +oo). -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 (only parsing). - -Lemma __deprecated__invr_cvg_pinfty (R : realFieldType) (u : R^nat) : - (forall i, 0 < u i) -> ((u i)^-1 @[i --> \oo] --> +oo) <-> (u @ \oo--> 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 (only parsing). - Section partial_sum. Variables (V : zmodType) (u_ : V ^nat). @@ -1269,20 +1213,6 @@ Definition expR {R : realType} (x : R) : R := limn (series (exp_coeff x)). (** Sequences of natural numbers *) -Lemma __deprecated__nat_dvg_real (R : realType) (u_ : nat ^nat) : - u_ @ \oo --> \oo -> ([sequence (u_ n)%:R : R^o]_n @ \oo --> +oo)%R. -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 (only parsing). - -Lemma __deprecated__nat_cvgPpinfty (u : nat^nat) : - u @ \oo --> \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 (only parsing). - Lemma nat_nondecreasing_is_cvg (u_ : nat^nat) : nondecreasing_seq u_ -> has_ubound (range u_) -> cvgn u_. Proof. @@ -1445,31 +1375,6 @@ Notation ereal_nondecreasing_opp := ereal_nondecreasing_oppn (only parsing). Section sequences_ereal. Local Open Scope ereal_scope. -Lemma __deprecated__ereal_cvg_abs0 (R : realFieldType) (f : (\bar R)^nat) : - abse \o f @ \oo --> 0 -> f @ \oo --> 0. -Proof. by move/cvg_abse0P. Qed. - -Lemma __deprecated__ereal_cvg_ge0 (R : realFieldType) (f : (\bar R)^nat) (a : \bar R) : - (forall n, 0 <= f n) -> f @ \oo --> a -> 0 <= a. -Proof. by move=> f_ge0; apply: cvge_ge; apply: nearW. Qed. - -Lemma __deprecated__ereal_lim_ge (R : realFieldType) x (u_ : (\bar R)^nat) : - cvgn u_ -> (\forall n \near \oo, x <= u_ n) -> x <= limn u_. -Proof. exact: lime_ge. Qed. - -Lemma __deprecated__ereal_lim_le (R : realFieldType) x (u_ : (\bar R)^nat) : - cvgn u_ -> (\forall n \near \oo, u_ n <= x) -> limn u_ <= x. -Proof. exact: lime_le. Qed. - -Lemma __deprecated__dvg_ereal_cvg (R : realFieldType) (u_ : R ^nat) : - u_ @ \oo --> +oo%R -> [sequence (u_ n)%:E]_n @ \oo --> +oo. -Proof. by rewrite cvgeryP. Qed. - -Lemma __deprecated__ereal_cvg_real (R : realFieldType) (f : (\bar R)^nat) a : - {near \oo, forall x, f x \is a fin_num} /\ - (fine \o f @ \oo --> a) <-> f @ \oo --> a%:E. -Proof. by rewrite fine_cvgP. Qed. - Lemma ereal_nondecreasing_cvgn (R : realType) (u_ : (\bar R)^nat) : nondecreasing_seq u_ -> u_ @ \oo --> ereal_sup (range u_). Proof. @@ -1737,11 +1642,6 @@ move=> f0 g0; rewrite /adde_def !negb_and; apply/andP; split; apply/orP. - by left; apply/eqP => Pf; have := nneseries_ge0 m f0; rewrite Pf. Qed. -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), - f @ \oo --> l -> h @ \oo --> l -> g @ \oo --> l. -Proof. by move=> ? ?; apply: squeeze_cvge. Qed. - Lemma nneseries_pinfty (R : realType) (u_ : (\bar R)^nat) (P : pred nat) k : (forall n, P n -> 0 <= u_ n) -> P k -> u_ k = +oo -> \sum_(i u0 Puv; apply: lee_lim. - by near=> n; exact: lee_sum. Unshelve. all: by end_near. Qed. -Lemma __deprecated__ereal_cvgD_pinfty_fin (R : realFieldType) (f g : (\bar R)^nat) b : - f @ \oo --> +oo -> g @ \oo --> b%:E -> f \+ g @ \oo --> +oo. -Proof. exact: cvgeD. Qed. - -Lemma __deprecated__ereal_cvgD_ninfty_fin (R : realFieldType) (f g : (\bar R)^nat) b : - f @ \oo --> -oo -> g @ \oo --> b%:E -> f \+ g @ \oo --> -oo. -Proof. exact: cvgeD. Qed. - -Lemma __deprecated__ereal_cvgD_pinfty_pinfty (R : realFieldType) (f g : (\bar R)^nat) : - f @ \oo --> +oo -> g @ \oo --> +oo -> f \+ g @ \oo --> +oo. -Proof. exact: cvgeD. Qed. - -Lemma __deprecated__ereal_cvgD_ninfty_ninfty (R : realFieldType) (f g : (\bar R)^nat) : - f @ \oo --> -oo -> g @ \oo --> -oo -> f \+ g @ \oo --> -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 (only parsing). - -Lemma __deprecated__ereal_cvgD (R : realFieldType) (f g : (\bar R)^nat) a b : - a +? b -> f @ \oo --> a -> g @ \oo --> b -> f \+ g @ \oo --> a + b. -Proof. exact: cvgeD. Qed. - -Lemma __deprecated__ereal_cvgB (R : realFieldType) (f g : (\bar R)^nat) a b : - a +? - b -> f @ \oo --> a -> g @ \oo --> b -> f \- g @ \oo --> a - b. -Proof. exact: cvgeB. Qed. - -Lemma __deprecated__ereal_is_cvgD (R : realFieldType) (u v : (\bar R)^nat) : - limn u +? limn v -> cvgn u -> cvgn v -> cvgn (u \+ v). -Proof. exact: is_cvgeD. Qed. - -Lemma __deprecated__ereal_cvg_sub0 (R : realFieldType) (f : (\bar R)^nat) (k : \bar R) : - k \is a fin_num -> (fun x => f x - k) @ \oo --> 0 <-> f @ \oo --> k. -Proof. exact: sube_cvg0. Qed. - -Lemma __deprecated__ereal_limD (R : realFieldType) (f g : (\bar R)^nat) : - cvgn f -> cvgn g -> limn f +? limn g -> - limn (f \+ g) = limn f + limn g. -Proof. exact: limeD. Qed. - -Lemma __deprecated__ereal_cvgM_gt0_pinfty (R : realFieldType) (f g : (\bar R)^nat) b : - (0 < b)%R -> f @ \oo --> +oo -> g @ \oo --> b%:E -> f \* g @ \oo --> +oo. -Proof. -move=> b_lt0 fl gl; have /= := cvgeM _ fl gl; rewrite gt0_mulye//; apply. -by rewrite mule_def_infty_neq0// gt_eqF. -Qed. - -Lemma __deprecated__ereal_cvgM_lt0_pinfty (R : realFieldType) (f g : (\bar R)^nat) b : - (b < 0)%R -> f @ \oo --> +oo -> g @ \oo --> b%:E -> f \* g @ \oo --> -oo. -Proof. -move=> b_lt0 fl gl; have /= := cvgeM _ fl gl; rewrite lt0_mulye//; apply. -by rewrite mule_def_infty_neq0// lt_eqF. -Qed. - -Lemma __deprecated__ereal_cvgM_gt0_ninfty (R : realFieldType) (f g : (\bar R)^nat) b : - (0 < b)%R -> f @ \oo --> -oo -> g @ \oo --> b%:E -> f \* g @ \oo --> -oo. -Proof. -move=> b_lt0 fl gl; have /= := cvgeM _ fl gl; rewrite gt0_mulNye//; apply. -by rewrite mule_def_infty_neq0// gt_eqF. -Qed. - -Lemma __deprecated__ereal_cvgM_lt0_ninfty (R : realFieldType) (f g : (\bar R)^nat) b : - (b < 0)%R -> f @ \oo --> -oo -> g @ \oo --> b%:E -> f \* g @ \oo --> +oo. -Proof. -move=> b_lt0 fl gl; have /= := cvgeM _ fl gl; rewrite lt0_mulNye//; apply. -by rewrite mule_def_infty_neq0// lt_eqF. -Qed. - -Lemma __deprecated__ereal_cvgM (R : realType) (f g : (\bar R) ^nat) (a b : \bar R) : - a *? b -> f @ \oo --> a -> g @ \oo --> b -> f \* g @ \oo --> a * b. -Proof. exact: cvgeM. Qed. - -Lemma __deprecated__ereal_lim_sum (R : realFieldType) (I : Type) (r : seq I) - (f : I -> (\bar R)^nat) (l : I -> \bar R) (P : pred I) : - (forall k n, P k -> 0 <= f k n) -> - (forall k, P k -> f k @ \oo --> l k) -> - (fun n => \sum_(k <- r | P k) f k n) @ \oo --> \sum_(k <- r | P k) l k. -Proof. -by move=> f0 ?; apply: cvg_nnesum => // ? ?; apply: nearW => ?; apply: f0. -Qed. - Let lim_shift_cst (R : realFieldType) (u : (\bar R) ^nat) (l : \bar R) : cvgn u -> (forall n, 0 <= u n) -> -oo < l -> limn (fun x => l + u x) = l + limn u. @@ -2024,61 +1844,6 @@ by move/(lt_le_trans Ml); rewrite ltxx. Unshelve. all: by end_near. Qed. End sequences_ereal. -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `squeeze_cvge` and generalized")] -Notation ereal_squeeze := __deprecated__ereal_squeeze (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")] -Notation ereal_cvgD_pinfty_fin := __deprecated__ereal_cvgD_pinfty_fin (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")] -Notation ereal_cvgD_ninfty_fin := __deprecated__ereal_cvgD_ninfty_fin (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")] -Notation ereal_cvgD_pinfty_pinfty := __deprecated__ereal_cvgD_pinfty_pinfty (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `cvgeD` and generalized")] -Notation ereal_cvgD := __deprecated__ereal_cvgD (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `cvgeB` and generalized")] -Notation ereal_cvgB := __deprecated__ereal_cvgB (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `is_cvgeD` and generalized")] -Notation ereal_is_cvgD := __deprecated__ereal_is_cvgD (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `cvge_sub0` and generalized")] -Notation ereal_cvg_sub0 := __deprecated__ereal_cvg_sub0 (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `limeD` and generalized")] -Notation ereal_limD := __deprecated__ereal_limD (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")] -Notation ereal_cvgM_gt0_pinfty := __deprecated__ereal_cvgM_gt0_pinfty (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")] -Notation ereal_cvgM_lt0_pinfty := __deprecated__ereal_cvgM_lt0_pinfty (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")] -Notation ereal_cvgM_gt0_ninfty := __deprecated__ereal_cvgM_gt0_ninfty (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")] -Notation ereal_cvgM_lt0_ninfty := __deprecated__ereal_cvgM_lt0_ninfty (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `cvgeM` and generalized")] -Notation ereal_cvgM := __deprecated__ereal_cvgM (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `cvg_nnesum` and generalized")] -Notation ereal_lim_sum := __deprecated__ereal_lim_sum (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `cvg_abse0P` and generalized")] -Notation ereal_cvg_abs0 := __deprecated__ereal_cvg_abs0 (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvge_ge` instead")] -Notation ereal_cvg_ge0 := __deprecated__ereal_cvg_ge0 (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `lime_ge` and generalized")] -Notation ereal_lim_ge := __deprecated__ereal_lim_ge (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `lime_le` and generalized")] -Notation ereal_lim_le := __deprecated__ereal_lim_le (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `cvgeryP` and generalized")] -Notation dvg_ereal_cvg := __deprecated__dvg_ereal_cvg (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.0", - note="renamed to `fine_cvgP` and generalized")] -Notation ereal_cvg_real := __deprecated__ereal_cvg_real (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `ereal_nondecreasing_cvgn`")] Notation ereal_nondecreasing_cvg := ereal_nondecreasing_cvgn (only parsing).