diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6fd33768e4..6638a5a47a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -51,6 +51,12 @@ - in `functions.v`: + lemma `natmulfctE` +- in `ereal.v`: + + lemmas `ereal_infEN`, `ereal_supN`, `ereal_infN`, `ereal_supEN` + + lemmas `ereal_supP`, `ereal_infP`, `ereal_sup_gtP`, `ereal_inf_ltP`, + `ereal_inf_leP`, `ereal_sup_geP`, `lb_ereal_infNy_adherent`, + `ereal_sup_real`, `ereal_inf_real` + ### Changed - in `pi_irrational`: @@ -79,11 +85,9 @@ - in `functions.v`: + `fct_sumE`, `addrfctE`, `sumrfctE` (from `zmodType` to `nmodType`) + `scalerfctE` (from `pointedType` to `Type`) -- in `ereal.v`: - + lemmas `ereal_infEN`, `ereal_supN`, `ereal_infN`, `ereal_supEN` - + lemmas `ereal_supP`, `ereal_infP`, `ereal_sup_gtP`, `ereal_inf_ltP`, - `ereal_inf_leP`, `ereal_sup_geP`, `lb_ereal_infNy_adherent`, - `ereal_sup_real`, `ereal_inf_real` + +- in `measurable_realfun.v` + + lemma `measurable_ln` ### Deprecated @@ -92,6 +96,21 @@ - in `functions.v`: + definitions `fct_ringMixin`, `fct_ringMixin` (was only used in an `HB.instance`) +- in `measurable_realfun.v`: + + notation `measurable_fun_ln` (deprecated since 0.6.3) + + notations `emeasurable_itv_bnd_pinfty`, `emeasurable_itv_ninfty_bnd` (deprecated since 0.6.2) + + notation `measurable_fun_lim_sup` (deprecated since 0.6.6) + + notation `measurable_fun_max` (deprecated since 0.6.3) + + notation `measurable_fun_er_map` (deprecated since 0.6.3) + + notations `emeasurable_funN`, `emeasurable_fun_max`, `emeasurable_fun_min`, + `emeasurable_fun_funepos`, `emeasurable_fun_funeneg` (deprecated since 0.6.3) + + notation `measurable_fun_lim_esup` (deprecated since 0.6.6) + +- in `measure.v`: + + notation `measurable_fun_ext` (deprecated since 0.6.2) + + notations `measurable_fun_id`, `measurable_fun_cst`, `measurable_fun_comp` (deprecated since 0.6.3) + + notation `measurable_funT_comp` (deprecated since 0.6.3) + ### Infrastructure ### Misc diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 4b7cfff1b4..ad7f02c589 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -391,10 +391,6 @@ Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1| apply: emeasurable_set1] : core. #[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 (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.2", note="use `emeasurable_itv` instead")] -Notation emeasurable_itv_ninfty_bnd := emeasurable_itv (only parsing). Lemma fine_measurable (R : realType) (D : set (\bar R)) : measurable D -> measurable_fun D fine. @@ -1125,27 +1121,20 @@ by rewrite -[_ @^-1` _]setTI; exact: m1. 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 (only parsing). -Lemma measurable_ln (R : realType) : measurable_fun [set~ (0:R)] (@ln R). +Lemma measurable_ln (R : realType) : measurable_fun [set: R] (@ln R). Proof. -rewrite (_ : [set~ 0] = `]-oo, 0[ `|` `]0, +oo[); last first. - by rewrite -(setCitv `[0, 0]); apply/seteqP; split => [|]x/=; - rewrite in_itv/= -eq_le eq_sym; [move/eqP/negbTE => ->|move/negP/eqP]. +rewrite -set_itvNyy (@itv_bndbnd_setU _ _ _ (BRight 0))//. apply/measurable_funU => //; split. - apply/measurable_restrictT => //=. rewrite (_ : _ \_ _ = cst 0)//; apply/funext => y; rewrite patchE. by case: ifPn => //; rewrite inE/= in_itv/= => y0; rewrite ln0// ltW. -- have : {in `]0, +oo[%classic, continuous (@ln R)}. - by move=> x; rewrite inE/= in_itv/= andbT => x0; exact: continuous_ln. - rewrite -continuous_open_subspace; last exact: interval_open. - by move/subspace_continuous_measurable_fun; apply; exact: measurable_itv. +- apply: subspace_continuous_measurable_fun => //. + rewrite continuous_open_subspace; last exact: interval_open. + by move=> x; rewrite inE/= in_itv/= andbT => x0; exact: continuous_ln. 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 (only parsing). Lemma measurable_expR (R : realType) : measurable_fun [set: R] expR. Proof. by apply: continuous_measurable_fun; exact: continuous_expR. Qed. @@ -1170,13 +1159,11 @@ Notation measurable_fun_pow := measurable_funX (only parsing). Lemma measurable_powR (R : realType) p : measurable_fun [set: R] (@powR R ^~ p). Proof. -apply: measurable_fun_if => //. +apply: measurable_fun_ifT => //. - apply: (measurable_fun_bool true). rewrite (_ : _ @^-1` _ = [set 0]) ?setTI//. by apply/seteqP; split => [_ /eqP ->//|_ -> /=]; rewrite eqxx. -- rewrite setTI; apply: measurableT_comp => //. - rewrite (_ : _ @^-1` _ = [set~ 0]); first exact: measurableT_comp. - by apply/seteqP; split => [x /negP/negP/eqP|x x0]//=; exact/negbTE/eqP. +- by apply: measurableT_comp => //; exact: measurable_funM. Qed. #[global] Hint Extern 0 (measurable_fun _ (@powR _ ^~ _)) => solve [apply: measurable_powR] : core. @@ -1192,9 +1179,6 @@ rewrite /powR; apply: measurable_fun_if => //. exact: mulrr_measurable. Qed. -#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxr` instead")] -Notation measurable_fun_max := measurable_maxr (only parsing). - Module NGenCInfty. Section ngencinfty. Implicit Types x y z : nat. @@ -1457,8 +1441,6 @@ apply: measurable_fun_ifT => //=. + by apply: (measurable_fun_bool true); exact/emeasurable_fin_num. + exact/measurable_EFinP/measurableT_comp. Qed. -#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_er_map`")] -Notation measurable_fun_er_map := measurable_er_map (only parsing). Section emeasurable_fun. Local Open Scope ereal_scope. @@ -1547,19 +1529,6 @@ Qed. 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 (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_maxe` instead")] -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 (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_funepos` instead")] -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 (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_esup`")] -Notation measurable_fun_lim_esup := measurable_fun_limn_esup (only parsing). - Section open_itv_cover. Context {R : realType}. Implicit Types (A : set R). diff --git a/theories/measure.v b/theories/measure.v index 1cde392724..8a077a7127 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1589,14 +1589,6 @@ End measurable_fun. solve [apply: measurable_id] : core. Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}. Arguments measurable_fun_eqP {d1 d2 T1 T2 D} f {g}. -#[deprecated(since="mathcomp-analysis 0.6.2", note="renamed `eq_measurable_fun`")] -Notation measurable_fun_ext := eq_measurable_fun (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_id`")] -Notation measurable_fun_id := measurable_id (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_cst`")] -Notation measurable_fun_cst := measurable_cst (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_comp`")] -Notation measurable_fun_comp := measurable_comp (only parsing). Section measurable_fun_measurableType. Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2) @@ -1708,8 +1700,6 @@ End measurable_fun_measurableType. solve [apply: measurable_id] : core. Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}. Arguments measurable_fun_bool {d1 T1 D f} b. -#[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurableT_comp`")] -Notation measurable_funT_comp := measurableT_comp (only parsing). Section measurability.