gauss integral

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

CHANGELOG_UNRELEASED.md

@@ -49,6 +49,27 @@
 
 - in `ftc.v`:
   + lemmas `differentiation_under_integral`, `derivable_under_integral`
+  + definition `partial1`, notation `'d1`
+
+- in `real_interval.v`:
+  + lemma `itv_bnd_infty_bigcup0S`
+
+- in `lebesgue_integral.v`:
+  + lemma `ge0_cvg_integral`
+
+- in `trigo.v`:
+  + lemma `derivable_atan`
+
+- new file `gauss_integral.v`:
+  + definition `oneDsqr`
+  + lemmas `oneDsqr_gt0`, `oneDsqr_ge0`, `oneDsqr_ge1`, `oneDsqr_neq0`,
+    `oneDsqrV_le1`, `continuous_oneDsqr`, `continuous_oneDsqrV`,
+    `integral01_atan`
+  + definition `gauss`
+  + lemmas `gauss_ge0`, `gauss_le1`, `cvg_gauss`, `measurable_gauss`,
+    `continuous_gauss`
+  + module `gauss_integral_proof`
+  + lemma `integral0y_gauss_pi2`
 
 ### Changed
 

_CoqProject

@@ -89,6 +89,7 @@ theories/probability.v
 theories/convex.v
 theories/charge.v
 theories/kernel.v
+theories/gauss_integral.v
 theories/showcase/summability.v
 analysis_stdlib/Rstruct_topology.v
 analysis_stdlib/showcase/uniform_bigO.v

reals/real_interval.v

@@ -302,6 +302,17 @@ rewrite natr_absz ger0_norm ?ceil_ge//.
 by rewrite -(ceil0 R) ceil_le// subr_ge0 (lteifW xy).
 Qed.
 
+Lemma itv_bnd_infty_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].
+exists i => //=.
+apply: subset_itvl zi.
+by rewrite bnd_simp/= add0r ler_nat.
+Qed.
+
 Lemma itv_infty_bnd_bigcup (R : realType) b (x : R) :
   [set` Interval -oo%O (BSide b x)] =
   \bigcup_i [set` Interval (BLeft (x - i%:R)) (BSide b x)].

theories/Make

@@ -56,5 +56,6 @@ lebesgue_stieltjes_measure.v
 convex.v
 charge.v
 kernel.v
+gauss_integral.v
 all_analysis.v
 showcase/summability.v

theories/ftc.v

@@ -16,10 +16,14 @@ From mathcomp Require Import lebesgue_integral derive charge.
 (* for the Lebesgue integral. We derive from this theorem a corollary to      *)
 (* compute the definite integral of continuous functions.                     *)
 (*                                                                            *)
+(*             'd1 f == first partial derivative of f                         *)
+(*                      f has type R -> T -> R for R : realType               *)
 (* parameterized_integral mu a x f := \int[mu]_(t \in `[a, x] f t)            *)
 (*                                                                            *)
 (******************************************************************************)
 
+Reserved Notation "'d1 f" (at level 10, f at next level, format "''d1'  f").
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -31,9 +35,7 @@ Local Open Scope ring_scope.
 
 Section differentiation_under_integral.
 
-Reserved Notation "'d1 f" (at level 10, f at next level, format "''d1'  f").
-
-Let partial1 {R : realType} {T : Type} (f : R -> T -> R) y : R -> R :=
+Definition partial1 {R : realType} {T : Type} (f : R -> T -> R) y : R -> R :=
   (f ^~ y)^`().
 
 Local Notation "'d1 f" := (partial1 f).
@@ -199,6 +201,7 @@ exact: cvg_differentiation_under_integral.
 Qed.
 
 End differentiation_under_integral.
+Notation "'d1 f" := (partial1 f).
 
 Section FTC.
 Context {R : realType}.