gen of int. by subst + normal distribution (#1450)

* integration by subst. over R

---------

Co-authored-by: IshiguroYoshihiro <[email protected]>

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -213,6 +213,49 @@
 
 - in `derive.v`:
   + lemmas `near_eq_derivable`, `near_eq_derive`, `near_eq_is_derive`
+- in `derive.v`:
+  + lemmas `derive1N`, `derivable_opp`, `derive1_id`
+
+- in `normedtype.v`:
+  + lemmas `cvg_compNP`, `decreasing_itvNyo_bigcup`, `decreasing_itvoo_bigcup`,
+    `increasing_itvNyo_bigcup`, `increasing_itvoc_bigcup`
+
+- in `num_topology.v`:
+  + lemmas `lt_nbhsl`, `Nlt_nbhsl`
+
+- in `measurable_realfun.v`:
+  + lemmas `measurable_fun_itv_bndo_bndc`, `measurable_fun_itv_obnd_cbnd`
+
+- in `real_interval.v`:
+  + lemma `itv_bndy_bigcup_BLeft_shift`
+
+- in `realfun.v`:
+  + definitions `derivable_Nyo_continuous_bnd`, `derivable_oy_continuous_bnd `
+
+- in `ftc.v`:
+  + lemmas
+    `decreasing_ge0_integration_by_substitutiony`,
+    `ge0_integration_by_substitutionNy`,
+    `increasing_ge0_integration_by_substitutiony`,
+    `ge0_integration_by_substitutionNy`,
+    `increasing_ge0_integration_by_substitutionT`,
+    `ge0_symfun_integralT`
+
+- in `gauss_integral`:
+  + lemmas `integralT_gauss`, `integrableT_gauss`
+
+- in `probability.v`:
+  + definition `normal_pdf`
+  + lemmas `normal_pdf_ge0`, `normal_pdf_gt0`, `measurable_normal_pdf`,
+    `continuous_normal_pdf`, `normal_pdf_ub`
+  + definition `normal_prob`, equipped with the structure of probability measure
+  + lemmas `integral_normal_pdf`, `normal_prob_dom`
+
+- in `realfun.v`:
+  + lemma `cvg_addrr_Ny`
+
+- in `normedtype.v`:
+  + lemmas `gt0_cvgMlNy`, `gt0_cvgMly`
 
 ### Changed
 
@@ -331,6 +374,14 @@
   + `inum_lt` -> `num_lt`
   + `inum_min` -> `num_min`
   + `inum_max` -> `num_max`
+- in `real_interval.v`:
+  + `itv_bnd_infty_bigcup` -> `itv_bndy_bigcup_BRight`
+  + `itv_bnd_infty_bigcup0S` -> `itv0y_bigcup0S`
+  + `itv_infty_bnd_bigcup` -> `itvNy_bnd_bigcup_BLeft`
+
+- in `set_interval.v`:
+  + `opp_itv_bnd_infty` -> `opp_itv_bndy`
+  + `opp_itv_infty_bnd` -> `opp_itvNy_bnd`
 
 ### Generalized
 
@@ -367,6 +418,12 @@
 - in `lebesgue_measure.v`:
   + definition `vitali_cover`, lemma `vitali_coverS`
 
+- in `ftc.v`:
+  + lemmas `increasing_cvg_at_right_comp`,
+    `increasing_cvg_at_left_comp`,
+    `decreasing_cvg_at_right_comp`,
+    `decreasing_cvg_at_left_comp`
+
 ### Deprecated
 - in `Rstruct.v`
   + lemma `Rinvx`
@@ -377,6 +434,9 @@
 - in `itv.v`:
   + notation `%:inum` (use `%:num` instead)
 
+- in `lebesgue_measure.v`:
+  + lemmas `measurable_fun_itv_co`, `measurable_fun_itv_oc`
+
 ### Removed
 
 - in `sequences.v`:
@@ -442,6 +502,14 @@
     `__deprecated__cvg_gt_ge`, `__deprecated__cvg_lt_le`,
     `__deprecated__linear_bounded0 `
     (deprecated since 0.6.0)
+- in `normedtype.v`:
+  + notations `cvg_distP`, `cvg_distW`, `continuous_cvg_dist`, `cvg_dist2P`,
+    `cvg_gt_ge`, `cvg_lt_le_`, `linear_bounded0`
+    (were deprecated since 0.6.0)
+  + lemmas `__deprecated__cvg_distW`, `__deprecated__continuous_cvg_dist`,
+    `__deprecated__cvg_gt_ge`, `__deprecated__cvg_lt_le`,
+    `__deprecated__linear_bounded0`
+    (were deprecated since 0.6.0)
 
 - in `interval_inference.v`
   + reserved notations `[lb of _]`, `[ub of _]`, `[lbe of _]` and `[ube of _]`

classical/set_interval.v

@@ -442,7 +442,7 @@ Hint Extern 0 (~ has_lbound _) => solve[by apply: hasNlbound_itv] : core.
 #[global]
 Hint Extern 0 (~ has_ubound _) => solve[by apply: hasNubound_itv] : core.
 
-Lemma opp_itv_bnd_infty (R : numDomainType) (x : R) b :
+Lemma opp_itv_bndy (R : numDomainType) (x : R) b :
   -%R @` [set` Interval (BSide b x) +oo%O] =
   [set` Interval -oo%O (BSide (negb b) (- x))].
 Proof.
@@ -451,8 +451,10 @@ rewrite predeqE => /= r; split=> [[y xy <-]|xr].
 exists (- r); rewrite ?opprK //.
 by case: b xr; rewrite !in_itv/= andbT (lerNr, ltrNr).
 Qed.
+#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `opp_itv_bndy`")]
+Notation opp_itv_bnd_infty := opp_itv_bndy (only parsing).
 
-Lemma opp_itv_infty_bnd (R : numDomainType) (x : R) b :
+Lemma opp_itvNy_bnd (R : numDomainType) (x : R) b :
   -%R @` [set` Interval -oo%O (BSide b x)] =
   [set` Interval (BSide (negb b) (- x)) +oo%O].
 Proof.
@@ -461,6 +463,8 @@ rewrite predeqE => /= r; split=> [[y xy <-]|xr].
 exists (- r); rewrite ?opprK //.
 by case: b xr; rewrite !in_itv/= andbT (lerNl, ltrNl).
 Qed.
+#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `opp_itvNy_bnd`")]
+Notation opp_itv_infty_bnd := opp_itvNy_bnd (only parsing).
 
 Lemma opp_itv_bnd_bnd (R : numDomainType) a b (x y : R) :
   -%R @` [set` Interval (BSide a x) (BSide b y)] =

reals/real_interval.v

@@ -291,7 +291,22 @@ apply eq_bigcupr => k _; apply/seteqP; split=> [_/= [y ysr] <-|x/= xsr].
 by exists (- x); rewrite ?oppr_itv//= opprK// negbK opprB opprK addrC.
 Qed.
 
-Lemma itv_bnd_infty_bigcup (R : realType) b (x : R) :
+Lemma itv_bndy_bigcup_BLeft_shift {R : realType} (b : bool) (x : R) (n : nat):
+  [set` Interval (BSide b x) +oo%O] =
+  \bigcup_i [set` Interval (BSide b x) (BLeft (x + (i + n)%:R))].
+Proof.
+apply/seteqP; split=> y; rewrite /= !in_itv/= andbT; last first.
+  by move=> [k _ /=]; move: b => [|] /=; rewrite in_itv/= => /andP[//] /ltW.
+move=> xy; exists `|Num.ceil (y - x)|.+1 => //=.
+rewrite in_itv/= xy/= natrD -natr1 natr_absz intr_norm -addrA nat1r addrA.
+apply: ltr_pwDr; first by rewrite ltr0n.
+rewrite -lterBDl (le_trans (le_ceil _)) //= le_eqVlt; apply/predU1P; left.
+apply/esym/normr_idP.
+rewrite ler0z -ceil_ge0 (lt_le_trans (@ltrN10 R))// subr_ge0.
+by case: b xy => //= /ltW.
+Qed.
+
+Lemma itv_bndy_bigcup_BRight (R : realType) b (x : R) :
   [set` Interval (BSide b x) +oo%O] =
   \bigcup_i [set` Interval (BSide b x) (BRight (x + i%:R))].
 Proof.
@@ -301,28 +316,34 @@ move=> xy; exists `|ceil (y - x)|%N => //=; rewrite in_itv/= xy/= -lerBlDl.
 rewrite natr_absz ger0_norm ?ceil_ge//.
 by rewrite -(ceil0 R) ceil_le// subr_ge0 (lteifW xy).
 Qed.
+#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `itv_bndy_bigcup_BRight`")]
+Notation itv_bnd_infty_bigcup := itv_bndy_bigcup_BRight (only parsing).
 
-Lemma itv_bnd_infty_bigcup0S (R : realType) :
+Lemma itv0y_bigcup0S (R : realType) :
   `[0%R, +oo[%classic = \bigcup_i `[0%R, i.+1%:R]%classic :> set R.
 Proof.
 rewrite eqEsubset; split; last first.
   by move=> /= x [n _]/=; rewrite !in_itv/= => /andP[->].
-rewrite itv_bnd_infty_bigcup => z [i _ /= zi].
+rewrite itv_bndy_bigcup_BRight => z [i _ /= zi].
 exists i => //=.
 apply: subset_itvl zi.
 by rewrite bnd_simp/= add0r ler_nat.
 Qed.
+#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `itv0y_bigcup0S`")]
+Notation itv_bnd_infty_bigcup0S := itv0y_bigcup0S (only parsing).
 
-Lemma itv_infty_bnd_bigcup (R : realType) b (x : R) :
+Lemma itvNy_bnd_bigcup_BLeft (R : realType) b (x : R) :
   [set` Interval -oo%O (BSide b x)] =
   \bigcup_i [set` Interval (BLeft (x - i%:R)) (BSide b x)].
 Proof.
-have /(congr1 (fun x => -%R @` x)) := itv_bnd_infty_bigcup (~~ b) (- x).
+have /(congr1 (fun x => -%R @` x)) := itv_bndy_bigcup_BRight (~~ b) (- x).
 rewrite opp_itv_bnd_infty negbK opprK => ->; rewrite image_bigcup.
 apply eq_bigcupr => k _; apply/seteqP; split=> [_ /= -[r rbxk <-]|y/= yxkb].
   by rewrite oppr_itv/= opprB addrC.
 by exists (- y); [rewrite oppr_itv/= negbK opprD opprK|rewrite opprK].
 Qed.
+#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `itvNy_bnd_bigcup_BLeft`")]
+Notation itv_infty_bnd_bigcup := itvNy_bnd_bigcup_BLeft (only parsing).
 
 Lemma bigcup_itvT {R : realType} b :
   \bigcup_i [set` Interval (BSide b (- i%:R)) (BRight i%:R)] = [set: R].

theories/derive.v

@@ -1907,6 +1907,16 @@ Qed.
 
 End near_derive.
 
+Lemma derive1N {R : realFieldType} (f : R -> R) (x : R) :
+  derivable f x 1 -> (- f)^`() x = (- f^`()%classic x).
+Proof. by move=> fx; rewrite !derive1E deriveN. Qed.
+
+Lemma derivable_opp {R : realFieldType} (x : R) v : derivable -%R x v.
+Proof. by apply: derivableN; exact: derivable_id. Qed.
+
+Lemma derive1_id {R : realFieldType} (x : R) : id^`() x = 1.
+Proof. by rewrite derive1E derive_id. Qed.
+
 (* Trick to trigger type class resolution *)
 Lemma trigger_derive (R : realType) (f : R -> R) x x1 y1 :
   is_derive x (1 : R) f x1 -> x1 = y1 -> is_derive x 1 f y1.