differentiation under integral

CHANGELOG_UNRELEASED.md

@@ -4,8 +4,6 @@
 
 ### Added
 
-### Changed
-
 - in `mathcomp_extra.v`:
   + lemmas `prodr_ile1`, `nat_int`
 
@@ -26,6 +24,39 @@
   + module `pi_irrational`
   + lemma `pi_irrationnal`
 
+- in `constructive_ereal.v`:
+  + lemma `abse_EFin`
+
+- in `normedtype.v`:
+  + lemmas `bounded_cst`, `subr_cvg0`
+
+- in `lebesgue_integral.v`:
+  + lemma `RintegralB`
+
+- 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
 
 - in `lebesgue_integrale.v`
@@ -36,6 +67,9 @@
 
 ### Renamed
 
+- in `normedtype.v`:
+  + `cvge_sub0` -> `sube_cvg0`
+
 ### Generalized
 
 ### Deprecated

_CoqProject

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

reals/constructive_ereal.v

@@ -700,6 +700,9 @@ Proof. by move=> [? [?| |]| |]. Qed.
 Lemma fine_lt : {in fin_num &, {homo @fine R : x y / x < y >-> (x < y)%R}}.
 Proof. by move=> [? [?| |]| |]. Qed.
 
+Lemma abse_EFin r : `|r%:E|%E = `|r|%:E.
+Proof. by []. Qed.
+
 Lemma fine_abse : {in fin_num, {morph @fine R : x / `|x| >-> `|x|%R}}.
 Proof. by case. Qed.
 

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

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

theories/all_analysis.v

@@ -24,3 +24,4 @@ From mathcomp Require Export convex.
 From mathcomp Require Export charge.
 From mathcomp Require Export kernel.
 From mathcomp Require Export pi_irrational.
+From mathcomp Require Export gauss_integral.

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.
@@ -29,6 +33,176 @@ Import numFieldNormedType.Exports.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
+Section differentiation_under_integral.
+
+Definition partial1 {R : realType} {T : Type} (f : R -> T -> R) y : R -> R :=
+  (f ^~ y)^`().
+
+Local Notation "'d1 f" := (partial1 f).
+
+Local Open Scope ring_scope.
+Context {R : realType} d {Y : measurableType d}
+  {mu : {measure set Y -> \bar R}}.
+Variable f : R -> Y -> R.
+Variable B : set Y.
+Hypothesis mB : measurable B.
+Variable a u v : R.
+Let I : set R := `]u, v[.
+Hypothesis Ia : I a.
+
+Hypothesis intf : forall x, I x -> mu.-integrable B (EFin \o f x).
+
+Hypothesis derf1 : forall x y, I x -> B y -> derivable (f ^~ y) x 1.
+
+Variable G : Y -> R.
+Hypothesis G_ge0 : forall y, 0 <= G y.
+Hypothesis intG : mu.-integrable B (EFin \o G).
+Hypothesis G_ub : forall x y, I x -> B y -> `|'d1 f y x| <= G y.
+
+Let F x' := \int[mu]_(y in B) f x' y.
+
+Lemma cvg_differentiation_under_integral :
+  h^-1 *: (F (h + a) - F a) @[h --> 0^'] --> \int[mu]_(y in B) ('d1 f) y a.
+Proof.
+apply/cvgr_dnbhsP => t [t_neq0 t_cvg0].
+suff: forall x_, (forall n : nat, x_ n != a) ->
+      x_ n @[n --> \oo] --> a -> (forall n, I (x_ n)) ->
+    (x_ n - a)^-1 *: (F (x_ n) - F a) @[n --> \oo] -->
+      \int[mu]_(y in B) ('d1 f) y a.
+  move=> suf.
+  apply/cvgrPdist_le => /= r r0.
+  have [rho /= rho0 arhouv] := near_in_itvoo Ia.
+  move/cvgr_dist_lt : (t_cvg0) => /(_ _ rho0)[m _ t_cvg0'].
+  near \oo => N.
+  pose x k := a + t (N + k)%N.
+  have x_a n : x n != a by rewrite /x addrC eq_sym -subr_eq subrr eq_sym t_neq0.
+  have x_cvg_a : x n @[n --> \oo] --> a.
+    apply: cvg_zero.
+    rewrite [X in X @ _ --> _](_ : _ = (fun n => t (n + N)%N)); last first.
+      by apply/funext => n; rewrite /x fctE addrAC subrr add0r addnC.
+    by rewrite cvg_shiftn.
+  have Ix n : I (x n).
+    apply: arhouv => /=.
+    rewrite /x opprD addrA subrr.
+    apply: t_cvg0' => //=.
+    by rewrite (@leq_trans N) ?leq_addr//; near: N; exists m.
+  have /cvgrPdist_le/(_ _ r0)[n _ /=] := suf x x_a x_cvg_a Ix.
+  move=> {}suf.
+  near=> M.
+  have /suf : (n <= M - N)%N.
+    by rewrite leq_subRL; near: M; exact: nbhs_infty_ge.
+  rewrite /x subnKC; last by near: M; exact: nbhs_infty_ge.
+  by rewrite (addrC a) addrK.
+move=> {t t_neq0 t_cvg0} x_ x_neqa x_cvga Ix_.
+pose g_ n y : R := (f (x_ n) y - f a y) / (x_ n - a).
+have mg_ n : measurable_fun B (fun y => (g_ n y)%:E).
+  apply/measurable_EFinP/measurable_funM => //.
+  apply: measurable_funB.
+    by have /integrableP[/measurable_EFinP] := intf (Ix_ n).
+  by have /integrableP[/measurable_EFinP] := intf Ia.
+have intg_ m : mu.-integrable B (EFin \o g_ m).
+  rewrite /g_ /comp/=.
+  under eq_fun do rewrite EFinM.
+  apply: integrableMl => //.
+    under eq_fun do rewrite EFinB.
+    by apply: integrableB; [by []|exact:intf..].
+  exact: bounded_cst.
+have Bg_G : {ae mu, forall y n, B y -> (`|(g_ n y)%:E| <= (EFin \o G) y)%E}.
+  apply/aeW => y n By; rewrite /g_.
+  have [axn|axn|<-] := ltgtP a (x_ n).
+  - have axnI : `[a, (x_ n)] `<=` I.
+      apply: subset_itvSoo; rewrite bnd_simp.
+      + by have := Ia; rewrite /I/= in_itv/= => /andP[].
+      + by have := Ix_ n; rewrite /I/= in_itv/= => /andP[].
+    have x_fd1f x : x \in `]a, (x_ n)[ -> is_derive x 1 (f^~ y) (('d1 f) y x).
+      move=> xax_n; apply: DeriveDef.
+        by apply: derf1 => //; exact/axnI/subset_itv_oo_cc.
+      by rewrite /partial1 derive1E.
+    have cf : {within `[a, (x_ n)], continuous (f^~ y)}.
+      have : {within I, continuous (f^~ y)}.
+        by apply: derivable_within_continuous => /= r Ir; exact: derf1.
+      by apply: continuous_subspaceW; exact: axnI.
+    have [C caxn ->] := @MVT _ (f^~ y) (('d1 f) y) _ _ axn x_fd1f cf.
+    rewrite -mulrA divff// ?subr_eq0// mulr1 lee_fin G_ub//.
+    by move/subset_itv_oo_cc : caxn => /axnI.
+  - have xnaI : `[(x_ n), a] `<=` I.
+      apply: subset_itvSoo; rewrite bnd_simp.
+      + by have := Ix_ n; rewrite /I/= in_itv/= => /andP[].
+      + by have := Ia; rewrite /I/= in_itv/= => /andP[].
+    have x_fd1f x : x \in `](x_ n), a[ -> is_derive x 1 (f^~ y) (('d1 f) y x).
+      move=> xax_n; apply: DeriveDef.
+        by apply: derf1 => //; exact/xnaI/subset_itv_oo_cc.
+      by rewrite /partial1 derive1E.
+    have cf : {within `[(x_ n), a], continuous (f^~ y)}.
+      have : {within I, continuous (f^~ y)}.
+        by apply: derivable_within_continuous => /= r Ir; exact: derf1.
+      by apply: continuous_subspaceW; exact: xnaI.
+    have [C caxn] := @MVT _ (f^~ y) (('d1 f) y) _ _ axn x_fd1f cf.
+    rewrite abse_EFin normrM distrC => ->.
+    rewrite normrM -mulrA distrC normfV divff// ?normr_eq0 ?subr_eq0//.
+    rewrite mulr1 lee_fin G_ub//.
+    by move/subset_itv_oo_cc : caxn => /xnaI.
+  - by rewrite subrr mul0r abse0 lee_fin.
+have g_cvg_d1f : forall y, B y -> (g_ n y)%:E @[n --> \oo] --> (('d1 f) y a)%:E.
+  move=> y By; apply/fine_cvgP; split; first exact: nearW.
+  rewrite /comp/=.
+  have /cvg_ex[/= l fayl] := derf1 Ia By.
+  have d1fyal : ('d1 f) y a = l.
+    apply/cvg_lim => //.
+    by move: fayl; under eq_fun do rewrite scaler1.
+  have xa0 : (forall n, x_ n - a != 0) /\ x_ n - a @[n --> \oo] --> 0.
+    by split=> [x|]; [rewrite subr_eq0|exact/subr_cvg0].
+  move: fayl => /cvgr_dnbhsP/(_ _ xa0).
+  under [in X in X -> _]eq_fun do rewrite scaler1 subrK.
+  move=> xa_l.
+  suff : (f (x_ x) y - f a y) / (x_ x - a) @[x --> \oo] --> ('d1 f) y a by [].
+  rewrite d1fyal.
+  by under eq_fun do rewrite mulrC.
+have mdf : measurable_fun B (fun y => (('d1 f) y a)%:E).
+  by apply: emeasurable_fun_cvg g_cvg_d1f => m; exact: mg_.
+have [intd1f g_d1f_0 _] := @dominated_convergence _ _ _ mu _ mB
+  (fun n y => (g_ n y)%:E) _ (EFin \o G) mg_ mdf (aeW _ g_cvg_d1f) intG
+  Bg_G.
+rewrite /= in g_d1f_0.
+rewrite [X in X @ _ --> _](_ : _ =
+    (fun h => \int[mu]_(z in B) g_ h z)); last first.
+  apply/funext => m; rewrite /F -RintegralB; [|by []|exact: intf..].
+  rewrite -[LHS]RintegralZl; [|by []|].
+  - by apply: eq_Rintegral => y _; rewrite mulrC.
+  - rewrite /comp; under eq_fun do rewrite EFinB.
+    by apply: integrableB => //; exact: intf.
+apply/subr_cvg0.
+rewrite [X in X @ _ --> _](_ : _ =
+    (fun x => \int[mu]_(z in B) (g_ x z - ('d1 f) z a)))%R; last first.
+  by apply/funext => n; rewrite RintegralB.
+apply: norm_cvg0.
+have {}g_d1f_0 : (\int[mu]_(x in B) `|g_ n x - ('d1 f) x a|) @[n --> \oo] --> 0.
+  exact/fine_cvg.
+apply: (@squeeze_cvgr _ _ _ _ (cst 0) _ _ _ _ _ g_d1f_0) => //.
+- apply/nearW => n.
+  rewrite /= normr_ge0/= le_normr_integral//.
+  rewrite /comp; under eq_fun do rewrite EFinB.
+  by apply: integrableB => //; exact: intg_.
+- exact: cvg_cst.
+Unshelve. all: end_near. Qed.
+
+Lemma differentiation_under_integral :
+  F^`() a = \int[mu]_(y in B) ('d1 f y) a.
+Proof.
+rewrite /derive1.
+by have /cvg_lim-> //:= cvg_differentiation_under_integral.
+Qed.
+
+Lemma derivable_under_integral : derivable F a 1.
+Proof.
+apply/cvg_ex => /=; exists (\int[mu]_(y in B) ('d1 f y) a).
+under eq_fun do rewrite scaler1.
+exact: cvg_differentiation_under_integral.
+Qed.
+
+End differentiation_under_integral.
+Notation "'d1 f" := (partial1 f).
+
 Section FTC.
 Context {R : realType}.
 Notation mu := (@lebesgue_measure R).