integral of (1 + x^2)^-1 over [0, +oo[

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

CHANGELOG_UNRELEASED.md

@@ -4,8 +4,17 @@
 
 ### Added
 
+- in `trigo.v`:
+  + lemma `integral0oo_atan`
+
 ### Changed
 
+- moved from `gauss_integral` to `trigo.v`:
+  + `oneDsqr`, `oneDsqr_ge1`, `oneDsqr_inum`, `oneDsqrV_le1`,
+    `continuous_oneDsqr`, `continuous_oneDsqr`
+- moved, generalized, and renamed from `gauss_integral` to `trigo.v`:
+  + `integral01_oneDsqr` -> `integral0_oneDsqr`
+
 ### Renamed
 
 ### Generalized

theories/gauss_integral.v

@@ -21,48 +21,6 @@ Import numFieldNormedType.Exports.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
-(* NB: move to trigo.v? *)
-Section oneDsqr.
-Context {R : realType}.
-Implicit Type x : R.
-
-Definition oneDsqr x : R := 1 + x ^+ 2.
-
-Lemma oneDsqr_ge1 x : 1 <= oneDsqr x :> R.
-Proof. by rewrite lerDl sqr_ge0. Qed.
-
-#[local]
-Hint Extern 0 (is_true (1 <= oneDsqr _)) => solve[apply: oneDsqr_ge1] : core.
-
-Canonical oneDsqr_inum x : {itv R & `[1, +oo[} := @ItvReal R (oneDsqr x)
-  (BLeft 1%Z) (BInfty _ false) (oneDsqr_ge1 x) erefl.
-
-Lemma oneDsqrV_le1 x : oneDsqr\^-1 x <= 1. Proof. by rewrite invf_le1. Qed.
-
-Lemma continuous_oneDsqr : continuous oneDsqr.
-Proof. by move=> x; apply: cvgD; [exact: cvg_cst|exact: exprn_continuous]. Qed.
-
-Lemma continuous_oneDsqrV : continuous (oneDsqr\^-1).
-Proof. by move=> x; apply: cvgV => //; exact: continuous_oneDsqr. Qed.
-
-Lemma integral01_oneDsqr :
-  \int[@lebesgue_measure R]_(x in `[0, 1]) (oneDsqr x)^-1 = atan 1.
-Proof.
-rewrite /Rintegral (@continuous_FTC2 _ _ atan)//.
-- by rewrite atan0 sube0.
-- by apply: continuous_in_subspaceT => x ?; exact: continuous_oneDsqrV.
-- split.
-  + by move=> x _; exact: derivable_atan.
-  + by apply: cvg_at_right_filter; exact: continuous_atan.
-  + by apply: cvg_at_left_filter; exact: continuous_atan.
-- move=> x x01.
-  by rewrite derive1_atan// mul1r.
-Qed.
-
-End oneDsqr.
-#[global]
-Hint Extern 0 (is_true (1 <= oneDsqr _)) => solve [apply: oneDsqr_ge1] : core.
-
 Section gauss_fun.
 Context {R : realType}.
 Local Open Scope ring_scope.
@@ -316,7 +274,7 @@ Proof.
 rewrite /h /integral0_gauss set_itv1 Rintegral_set1 expr0n addr0.
 rewrite -atan1 /integral01_u.
 under eq_Rintegral do rewrite /u expr0n/= oppr0 mul0r expR0 mul1r.
-exact: integral01_oneDsqr.
+exact: integral0_oneDsqr.
 Qed.
 
 Let u_gauss_fun t x : u x t <= gauss_fun x.

theories/trigo.v

@@ -5,7 +5,8 @@ From mathcomp Require Import interval rat.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import reals ereal nsatz_realtype interval_inference.
 From mathcomp Require Import topology normedtype landau sequences derive.
-From mathcomp Require Import realfun exp.
+From mathcomp Require Import realfun exp measure lebesgue_measure.
+From mathcomp Require Import lebesgue_integral ftc.
 
 (**md**************************************************************************)
 (* # Theory of trigonometric functions                                        *)
@@ -1083,6 +1084,33 @@ HB.lock Definition atan {R : realType} (x : R) : R :=
   get [set y | -(pi / 2) < y < pi / 2 /\ tan y = x].
 Canonical locked_atan := Unlockable atan.unlock.
 
+Section oneDsqr.
+Context {R : realType}.
+Implicit Type x : R.
+
+Definition oneDsqr x : R := 1 + x ^+ 2.
+
+Lemma oneDsqr_ge1 x : 1 <= oneDsqr x :> R.
+Proof. by rewrite lerDl sqr_ge0. Qed.
+
+#[local]
+Hint Extern 0 (is_true (1 <= oneDsqr _)) => solve[apply: oneDsqr_ge1] : core.
+
+Canonical oneDsqr_inum x : {itv R & `[1, +oo[} := @ItvReal R (oneDsqr x)
+  (BLeft 1%Z) (BInfty _ false) (oneDsqr_ge1 x) erefl.
+
+Lemma oneDsqrV_le1 x : oneDsqr\^-1 x <= 1. Proof. by rewrite invf_le1. Qed.
+
+Lemma continuous_oneDsqr : continuous oneDsqr.
+Proof. by move=> x; apply: cvgD; [exact: cvg_cst|exact: exprn_continuous]. Qed.
+
+Lemma continuous_oneDsqrV : continuous (oneDsqr\^-1).
+Proof. by move=> x; apply: cvgV => //; exact: continuous_oneDsqr. Qed.
+
+End oneDsqr.
+#[global]
+Hint Extern 0 (is_true (1 <= oneDsqr _)) => solve [apply: oneDsqr_ge1] : core.
+
 Section Atan.
 Variable R : realType.
 Implicit Type x : R.
@@ -1230,4 +1258,36 @@ rewrite tanK// in_itv/= xpi2 andbT (lt_le_trans _ x0)//.
 by rewrite ltrNl oppr0 divr_gt0// pi_gt0.
 Qed.
 
+Let mu := @lebesgue_measure R.
+
+Lemma integral0_oneDsqr b : 0 <= b ->
+  \int[mu]_(x in `[0, b]) (oneDsqr x)^-1 = atan b.
+Proof.
+rewrite le_eqVlt => /predU1P[<-|b0].
+  by rewrite set_itv1 Rintegral_set1 atan0.
+rewrite /Rintegral (@continuous_FTC2 _ _ atan)//.
+- by rewrite atan0 sube0.
+- by apply: continuous_in_subspaceT => x ?; exact: continuous_oneDsqrV.
+- split.
+  + by move=> x _; exact: derivable_atan.
+  + by apply: cvg_at_right_filter; exact: continuous_atan.
+  + by apply: cvg_at_left_filter; exact: continuous_atan.
+- move=> x x01.
+  by rewrite derive1_atan// mul1r.
+Qed.
+
+Lemma integral0y_oneDsqr :
+  (\int[mu]_(x in `[0%R, +oo[) (oneDsqr x)^-1%:E = (pi / 2)%:E)%E.
+Proof.
+rewrite (ge0_continuous_FTC2y _ _ cvgy_atan)/=.
+- by rewrite atan0 oppr0 addr0.
+- by move=> x _; rewrite invr_ge0.
+- apply/continuous_within_itvcyP; split.
+    by move=> x x0; apply: continuous_oneDsqrV.
+  by apply: cvg_at_right_filter; exact: continuous_oneDsqrV.
+- move=> x x0; apply: ex_derive.
+- by apply: cvg_at_right_filter; exact: continuous_atan.
+- by move=> x _; rewrite derive1E; exact: derive_val.
+Qed.
+
 End Atan.