From 13c501f8e73d6f1162204c2bc319e17de2ab9f67 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 10 Aug 2024 10:50:45 +0900 Subject: [PATCH] enforcing naming conventions (change at minima) --- CHANGELOG_UNRELEASED.md | 15 ++++++++++++--- theories/derive.v | 6 +++--- theories/lebesgue_measure.v | 32 +++++++++++++++++--------------- theories/probability.v | 2 +- 4 files changed, 33 insertions(+), 22 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4a91a9187..5c593eb11 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -6,7 +6,7 @@ - in `derive.v`: + lemma `derive_id` - + lemmas `deriveX_id`, `derive1X_id` + + lemmas `exp_derive`, `exp_derive1` + lemma `derive_cst` + lemma `deriveMr`, `deriveMl` @@ -17,9 +17,13 @@ ### Renamed +- in `lebesgue_measure.v`: + + `measurable_exprn` -> `exprn_measurable` + + `measurable_mulrl` -> `mulrl_measurable` + + `measurable_mulrr` -> `mulrr_measurable` + + `measurable_fun_pow` -> `measurable_funX` + ### Generalized -- in `reals.v`: - + lemma `rat_in_itvoo` - in `derive.v`: + lemma `derivable_cst` @@ -28,6 +32,11 @@ ### Removed +- in `lebesgue_measure.v`: + + notation `measurable_fun_sqr` (was deprecated since 0.6.3) + + notation `measurable_fun_exprn` (was deprecated since 0.6.3) + + notation `measurable_funrM` (was deprecated since 0.6.3) + ### Infrastructure ### Misc diff --git a/theories/derive.v b/theories/derive.v index 231c7c40d..7936fe84a 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1379,16 +1379,16 @@ End Derive_lemmasVR. Lemma derive1_cst {R : numFieldType} (k : R) t : (cst k)^`() t = 0. Proof. by rewrite derive1E derive_cst. Qed. -Lemma deriveX_id {R : numFieldType} n x v : +Lemma exp_derive {R : numFieldType} n x v : 'D_v (@GRing.exp R ^~ n.+1) x = n.+1%:R *: x ^+ n *: v. Proof. have /= := @deriveX R R id n x v (@derivable_id _ _ _ _). by rewrite fctE => ->; rewrite derive_id. Qed. -Lemma derive1X_id {R : numFieldType} n x : +Lemma exp_derive1 {R : numFieldType} n x : (@GRing.exp R ^~ n.+1)^`() x = n.+1%:R *: x ^+ n. -Proof. by rewrite derive1E deriveX_id [LHS]mulr1. Qed. +Proof. by rewrite derive1E exp_derive [LHS]mulr1. Qed. Lemma EVT_max (R : realType) (f : R -> R) (a b : R) : (* TODO : Filter not infered *) a <= b -> {within `[a, b], continuous f} -> exists2 c, c \in `[a, b]%R & diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index f08883ee5..e6ffaa3ee 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1641,19 +1641,19 @@ rewrite [X in measurable X](_ : _ = setT)// predeqE => r. by split => // _; rewrite /= in_itv /= andbT (lt_le_trans x0). Qed. -Lemma measurable_mulrl D (k : R) : measurable_fun D ( *%R k). +Lemma mulrl_measurable D (k : R) : measurable_fun D ( *%R k). Proof. apply: measurable_funTS => /=. by apply: continuous_measurable_fun; exact: mulrl_continuous. Qed. -Lemma measurable_mulrr D (k : R) : measurable_fun D (fun x => x * k). +Lemma mulrr_measurable D (k : R) : measurable_fun D (fun x => x * k). Proof. apply: measurable_funTS => /=. by apply: continuous_measurable_fun; exact: mulrr_continuous. Qed. -Lemma measurable_exprn D n : measurable_fun D (fun x => x ^+ n). +Lemma exprn_measurable D n : measurable_fun D (fun x => x ^+ n). Proof. apply measurable_funTS => /=. by apply continuous_measurable_fun; exact: exprn_continuous. @@ -1665,21 +1665,21 @@ End standard_measurable_fun. #[global] Hint Extern 0 (measurable_fun _ normr) => solve [exact: measurable_normr] : core. #[global] Hint Extern 0 (measurable_fun _ ( *%R _)) => - solve [exact: measurable_mulrl] : core. + solve [exact: mulrl_measurable] : core. #[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 (only parsing). + solve [exact: exprn_measurable] : core. #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_oppr` instead")] 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 (only parsing). #[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_normr` instead")] 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 (only parsing). -#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_mulrl` instead")] -Notation measurable_funrM := measurable_mulrl (only parsing). +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `exprn_measurable` instead")] +Notation measurable_exprn := exprn_measurable (only parsing). +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `mulrl_measurable` instead")] +Notation measurable_mulrl := mulrl_measurable (only parsing). +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `mulrr_measurable` instead")] +Notation measurable_mulrr := mulrr_measurable (only parsing). Section measurable_fun_realType. Context d (T : measurableType d) (R : realType). @@ -1714,11 +1714,11 @@ move=> mf mg; rewrite (_ : (_ \* _) = (fun x => 2%:R^-1 * (f x + g x) ^+ 2) \- (fun x => 2%:R^-1 * (f x ^+ 2)) \- (fun x => 2%:R^-1 * (g x ^+ 2))). apply: measurable_funB; first apply: measurable_funB. - apply: measurableT_comp => //. - by apply: measurableT_comp (measurable_exprn _) _; exact: measurable_funD. + by apply: measurableT_comp (exprn_measurable _) _; exact: measurable_funD. - apply: measurableT_comp => //. - exact: measurableT_comp (measurable_exprn _) _. + exact: measurableT_comp (exprn_measurable _) _. - apply: measurableT_comp => //. - exact: measurableT_comp (measurable_exprn _) _. + exact: measurableT_comp (exprn_measurable _) _. rewrite funeqE => x /=; rewrite -2!mulrBr sqrrD (addrC (f x ^+ 2)) -addrA. rewrite -(addrA (f x * g x *+ 2)) -opprB opprK (addrC (g x ^+ 2)) addrK. by rewrite -(mulr_natr (f x * g x)) -(mulrC 2) mulrA mulVr ?mul1r// unitfE. @@ -1842,7 +1842,7 @@ under eq_fun do rewrite -mulr_natr. by do 2 apply: measurable_funM => //. Qed. -Lemma measurable_fun_pow {R : realType} D (f : R -> R) n : measurable_fun D f -> +Lemma measurable_funX {R : realType} D (f : R -> R) n : measurable_fun D f -> measurable_fun D (fun x => f x ^+ n). Proof. move=> mf. @@ -1868,6 +1868,8 @@ Notation measurable_fun_power_pos := measurable_powR (only parsing). 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 (only parsing). +#[deprecated(since="mathcomp-analysis 1.4.0", note="use `measurable_funX` instead")] +Notation measurable_fun_pow := measurable_funX (only parsing). Section standard_emeasurable_fun. Variable R : realType. diff --git a/theories/probability.v b/theories/probability.v index 0ba7a79ab..077e23912 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -1016,7 +1016,7 @@ Lemma measurable_binomial_pmf {R : realType} D n k : Proof. apply: (@measurableT_comp _ _ _ _ _ _ (fun x : R => x *+ 'C(n, k))%R) => /=. exact: measurable_natmul. -apply: measurable_funM => //=; apply: measurable_fun_pow. +apply: measurable_funM => //=; apply: measurable_funX. exact: measurable_funB. Qed.