normal_prob cont./reproductive property

CHANGELOG_UNRELEASED.md

@@ -95,6 +95,23 @@
 
 - in `reals.v`:
   + lemmas `sup_ge0`, `has_sup_wpZl`, `gt0_has_supZl`, `has_sup_Mn`, `sup_Mn`
+- in `normal_distribution.v`:
+  + lemma `normal_funN`
+  + lemma `normal_fun_sym`
+  + lemma `normal_fun0abs`
+  + lemma `normal_pdf_sym`
+  + lemma `normal_fun_center_new`
+  + lemma `normal_fun_shift`
+  + lemma `normal_pdf_uniq_ae`
+  + lemma `normal_prob_continuous`
+  + lemma `integral_normal_prob`
+  + lemma `measurable_normal_prob`
+  + lemma `emeasurable_bounded_integrable`
+  + lemmas `integrable_normal_probD1`, `normal_probD1`, `normal_probD2`, `normal_probD`
+
+- in `ftc.v`:
+  + lemma `ge0_integration_by_substitution_shift_itvy`,
+    `ge0_integration_by_substitution_shift_itvNy`
 
 ### Changed
 
@@ -185,6 +202,8 @@
   + lemmas `Radon_NikodymE`, `Radon_Nikodym_fin_num`, `Radon_Nikodym_integrable`,
     `ae_eq_Radon_Nikodym_SigmaFinite`, `Radon_Nikodym_change_of_variables`,
     `Radon_Nikodym_cscale`, `Radon_Nikodym_cadd`, `Radon_Nikodym_chain_rule`
+- in `normal_distribution.v:
+  + `normal_fun_center` -> `normal_fun_center0`
 
 ### Renamed
 

rocq-mathcomp-analysis.opam

@@ -19,6 +19,7 @@ depends: [
   "rocq-mathcomp-solvable"
   "rocq-mathcomp-field"
   "rocq-mathcomp-bigenough" { (>= "1.0.0") }
+  "rocq-mathcomp-algebra-tactics" { (>= "1.2.7") }
   "rocq-navi" {= "0.4.1" & with-doc}
 ]
 

theories/ftc.v

@@ -1793,6 +1793,53 @@ Qed.
 
 End integration_by_substitution.
 
+
+Section ge0_integration_by_substitution_shift.
+Context {R : realType}.
+Notation mu := (@lebesgue_measure R).
+
+Lemma ge0_integration_by_substitution_shift_itvy (f : R -> R) (r e : R) :
+  {within `[r + e, +oo[, continuous f} ->
+  {in `]r + e, +oo[, forall x : R, 0 <= f x} ->
+  (\int[mu]_(x in `[(r + e)%R, +oo[) (f x)%:E =
+  \int[mu]_(x in `[r, +oo[) ((f \o shift e) x)%:E)%E.
+Proof.
+move=> cf f0.
+have dshiftE : (shift e)^`() = cst 1.
+  by apply/funext => x; rewrite derive1E -(derive_shift 1 e).
+rewrite (@increasing_ge0_integration_by_substitutiony _ (shift e))//=.
+- by move=> x y _ _ xy; rewrite ltr_leD.
+- by rewrite dshiftE => ? _; exact: cst_continuous.
+- by rewrite dshiftE; exact: is_cvg_cst.
+- by rewrite dshiftE; exact: is_cvg_cst.
+- split; first by move=> x _; exact: ex_derive.
+  by apply/cvg_at_right_filter; apply: cvgD => //; exact: cvg_cst.
+- exact: cvg_addrr.
+by rewrite dshiftE mulr1.
+Qed.
+
+Lemma ge0_integration_by_substitution_shift_itvNy (f : R -> R) (r e : R) :
+  {within `]-oo, r + e], continuous f} ->
+  {in `]-oo, r + e[, forall x : R, 0 <= f x} ->
+  (\int[mu]_(x in `]-oo, (r + e)%R]) (f x)%:E =
+   \int[mu]_(x in `]-oo, r]) ((f \o shift e) x)%:E)%E.
+Proof.
+move=> cf f0.
+have dshiftE : (shift e)^`() = cst 1.
+  by apply/funext => x; rewrite derive1E -(derive_shift 1 e).
+rewrite (@increasing_ge0_integration_by_substitutionNy _ (shift e))//.
+- by move=> x y _ _ xy; rewrite ltr_leD.
+- by rewrite dshiftE => ? _; exact: cst_continuous.
+- by rewrite dshiftE; exact: is_cvg_cst.
+- by rewrite dshiftE; exact: cvg_cst.
+- split; first by move=> x _; exact: ex_derive.
+  by apply/cvg_at_left_filter; apply: cvgD => //; exact: cvg_cst.
+- exact: cvg_addrr_Ny.
+by rewrite dshiftE mulr1.
+Qed.
+
+End ge0_integration_by_substitution_shift.
+
 Section integration_by_substitution_onem.
 Context {R : realType}.
 Let mu := (@lebesgue_measure R).