diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5ab0033e1..2fca05f1b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 diff --git a/_CoqProject b/_CoqProject index a8b38635c..a406c9edd 100644 --- a/_CoqProject +++ b/_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 diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index a119e963f..33893d1bf 100644 --- a/reals/constructive_ereal.v +++ b/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. diff --git a/reals/real_interval.v b/reals/real_interval.v index a9ca280f6..dfaf36926 100644 --- a/reals/real_interval.v +++ b/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)]. diff --git a/theories/Make b/theories/Make index 35f6699fb..236f4186e 100644 --- a/theories/Make +++ b/theories/Make @@ -57,5 +57,6 @@ convex.v charge.v kernel.v pi_irrational.v +gauss_integral.v all_analysis.v showcase/summability.v diff --git a/theories/all_analysis.v b/theories/all_analysis.v index 3eb98668d..b567c7690 100644 --- a/theories/all_analysis.v +++ b/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. diff --git a/theories/ftc.v b/theories/ftc.v index bbc908701..43f98fa2a 100644 --- a/theories/ftc.v +++ b/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). diff --git a/theories/gauss_integral.v b/theories/gauss_integral.v new file mode 100644 index 000000000..4e5a4c163 --- /dev/null +++ b/theories/gauss_integral.v @@ -0,0 +1,436 @@ +(* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop signed reals ereal. +From mathcomp Require Import topology tvs normedtype sequences real_interval. +From mathcomp Require Import esum measure lebesgue_measure numfun realfun. +From mathcomp Require Import exp trigo lebesgue_integral derive charge ftc. + +(**md**************************************************************************) +(* # Gauss integral *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldNormedType.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +(* NB: move to ftc.v? *) +Section oneDsqr. +Context {R : realType}. +Implicit Type x : R. + +Definition oneDsqr x : R := 1 + x ^+ 2. + +Lemma oneDsqr_gt0 x : 0 < oneDsqr x :> R. +Proof. by rewrite ltr_pwDl// sqr_ge0. Qed. + +Lemma oneDsqr_ge0 x : 0 <= oneDsqr x :> R. +Proof. by rewrite ltW// oneDsqr_gt0. Qed. + +Lemma oneDsqr_ge1 x : 1 <= oneDsqr x :> R. +Proof. by rewrite lerDl sqr_ge0. Qed. + +Lemma oneDsqr_neq0 x : oneDsqr x != 0. +Proof. by rewrite gt_eqF// oneDsqr_gt0. Qed. + +Lemma oneDsqrV_le1 x : oneDsqr\^-1 x <= 1. +Proof. by rewrite invr_le1// ?oneDsqr_ge1 ?unitf_gt0 ?oneDsqr_gt0. 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: oneDsqr_neq0|exact: continuous_oneDsqr]. +Qed. + +Lemma integral01_atan : + \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 (0 < oneDsqr _)%R => solve[apply: oneDsqr_gt0] : core. +#[global] Hint Extern 0 (0 <= oneDsqr _)%R => solve[apply: oneDsqr_ge0] : core. +#[global] Hint Extern 0 (1 <= oneDsqr _)%R => solve[apply: oneDsqr_ge1] : core. +#[global] Hint Extern 0 (oneDsqr _ != 0)%R => solve[apply: oneDsqr_ge1] : core. + +Section gauss. +Context {R : realType}. +Local Open Scope ring_scope. + +Definition gauss (x : R) := expR (- x ^+ 2). + +Lemma gauss_ge0 (x : R) : 0 <= gauss x. Proof. exact: expR_ge0. Qed. + +Lemma gauss_le1 (x : R) : gauss x <= 1. +Proof. by rewrite -expR0 ler_expR lerNl oppr0 sqr_ge0. Qed. + +Lemma cvg_gauss : gauss x @[x --> +oo%R] --> (0:R). +Proof. +apply: (@cvg_comp _ _ _ (fun x => x ^+ 2) (fun x => expR (- x))); last first. + exact: cvgr_expR. +(* NB: should this become a lemma? *) +apply/cvgryPge => M. +near=> x. +rewrite (@le_trans _ _ x)//. + near: x. + by apply: nbhs_pinfty_ge => //; rewrite num_real. +by rewrite expr2 ler_peMl. +Unshelve. all: end_near. Qed. + +Lemma measurable_gauss : measurable_fun setT gauss. +Proof. by apply: measurableT_comp => //; exact: measurableT_comp. Qed. + +Lemma continuous_gauss : continuous gauss. +Proof. +move=> x; apply: (@continuous_comp _ _ _ (fun x : R => - x ^+ 2) expR). + apply: cvgN; apply: (@cvg_comp _ _ _ (fun z => z) (fun z => z ^+ 2)). + exact: cvg_id. + exact: exprn_continuous. +exact: continuous_expR. +Qed. + +End gauss. + +Module gauss_integral_proof. +Section gauss_integral_proof. +Context {R : realType}. +Local Open Scope ring_scope. +Implicit Type x : R. + +Let mu : {measure set _ -> \bar R} := @lebesgue_measure R. + +Definition integral0y_gauss := \int[mu]_(x in `[0%R, +oo[) gauss x. + +Let integral0y_gauss_ge0 : 0 <= integral0y_gauss. +Proof. by apply: Rintegral_ge0 => //= x _; rewrite gauss_ge0. Qed. + +Definition integral0_gauss x := \int[mu]_(t in `[0, x]) gauss t. + +Lemma integral0_gauss_ge0 x : 0 <= integral0_gauss x. +Proof. by apply: Rintegral_ge0 => //= r _; rewrite expR_ge0. Qed. + +Let continuous_integral0_gauss x : (0 < x)%R -> + {within `[0, x], continuous integral0_gauss}. +Proof. +move=> x0; rewrite /integral0_gauss. +apply: parameterized_integral_continuous => //=. +apply: continuous_compact_integrable => //; first exact: segment_compact. +by apply: continuous_subspaceT; exact: continuous_gauss. +Qed. + +Definition u x t := expR (- x ^+ 2 * oneDsqr t) / oneDsqr t. + +Let u_ge0 x t : 0 <= u x t. +Proof. by rewrite /u divr_ge0// ?expR_ge0// oneDsqr_ge0. Qed. + +Let measurable_u x : measurable_fun setT (u x). +Proof. +apply: measurable_funM => //=. + apply: measurableT_comp => //=; apply: measurable_funM => //=. + exact: measurable_funD. +apply: measurable_funTS. +by apply: continuous_measurable_fun; exact: continuous_oneDsqrV. +Qed. + +Let partial1_u x t : ('d1 u t) x = - 2 * x * gauss x * gauss (t * x). +Proof. +rewrite /partial1 /u /= derive1E deriveMr//= -derive1E. +rewrite derive1_comp// [in X in _ * (_ * X)]derive1E deriveMr//=. +rewrite mulrCA (mulrA (oneDsqr _)^-1) mulVf ?oneDsqr_neq0 ?mul1r//. +rewrite deriveN// exp_derive expr1 mulrC !mulNr; congr -%R. +rewrite -mulrA scaler1; congr *%R. +rewrite -expRD /oneDsqr mulrDr mulr1 exprMn opprD mulrC. +by rewrite derive1E -[in RHS]derive_expR. +Qed. + +Let continuous_NsqrM x : continuous (fun r : R => - (r * x) ^+ 2). +Proof. +move=> z; apply: cvgN => /=. +apply: (@cvg_comp _ _ _ (fun z => z * x) (fun z => z ^+ 2)). + by apply: cvgMl; exact: cvg_id. +exact: exprn_continuous. +Qed. + +Let continuous_gaussM x : continuous (fun r : R => gauss (r * x)). +Proof. +move=> x0. +apply: (@continuous_comp _ _ _ (fun r : R => - (r * x) ^+ 2) expR). + exact: continuous_NsqrM. +exact: continuous_expR. +Qed. + +Let continuous_u x : continuous (u x). +Proof. +rewrite /u /= => y; rewrite /continuous_at. +apply: cvgM; last exact: continuous_oneDsqrV. +apply: continuous_comp => /=; last exact: continuous_expR. +by apply: cvgMr; exact: continuous_oneDsqr. +Qed. + +Definition integral01_u x := \int[mu]_(t in `[0, 1]) u x t. + +Let integral01_u_ge0 x : 0 <= integral01_u x. +Proof. +rewrite /Rintegral fine_ge0// integral_ge0//= => t t01. +by rewrite lee_fin u_ge0. +Qed. + +Let partial1_u_local_ub c (e : R) : 0 < e -> + exists2 M : R, 0 < M & + forall x0 y, x0 \in `](c - e), (c + e)[ -> `|('d1 u) y x0| <= M. +Proof. +move=> e0 /=. +near (pinfty_nbhs R) => M. +exists M => // x y. +rewrite in_itv/= => /andP[cex xce]. +rewrite partial1_u !mulNr normrN -!mulrA normrM ger0_norm//. +rewrite -expRD exprMn_comm; last by rewrite /GRing.comm mulrC. +rewrite -opprD. +rewrite -{1}(mul1r (x ^+ 2)) -mulrDl. +rewrite (@le_trans _ _ (2 * `|x * gauss x|))//. + rewrite ler_pM2l// normrM [leRHS]normrM. + rewrite ler_wpM2l//. + do 2 rewrite ger0_norm ?expR_ge0//. + by rewrite ler_expR// lerN2 ler_peMl ?sqr_ge0// lerDl sqr_ge0. +rewrite normrM (ger0_norm (expR_ge0 _)). +have ? : `|x| <= maxr `|c + e| `|c - e|. + rewrite le_max. + have [x0|x0] := lerP 0 x. + by rewrite ger0_norm// ler_normr (ltW xce). + rewrite ltr0_norm//; apply/orP; right. + move/ltW : cex. + rewrite -lerN2 => /le_trans; apply. + by rewrite -normrN ler_norm. +rewrite (@le_trans _ _ (2 * ((maxr `|c + e| `|c - e|) * expR (- 0 ^+ 2))))//. + rewrite ler_pM2l// ler_pM ?expR_ge0//. + by rewrite expr0n/= oppr0 expR0 gauss_le1. +near: M. +by apply: nbhs_pinfty_ge; rewrite num_real. +Unshelve. all: end_near. Qed. + +Let cvg_dintegral01_u x : + h^-1 *: (integral01_u (h + x)%E - integral01_u x) @[h --> 0^'] --> + - 2 * x * gauss x * \int[mu]_(t in `[0, 1]) gauss (t * x). +Proof. +have [c [e e0 cex]] : exists c : R, exists2 e : R, 0 < e & ball c e x. + exists x, 1 => //. + exact: ballxx. +have [M M0 HM] := partial1_u_local_ub c e0. +rewrite [X in _ --> X](_ : _ = + \int[mu]_(y in `[0, 1]) ('d1 u) y x)//; last first. + rewrite /= -RintegralZl//; last first. + apply: continuous_compact_integrable => /=; first exact: segment_compact. + by apply/continuous_subspaceT => x0; exact: continuous_gaussM. + by apply: eq_Rintegral => z z01; rewrite partial1_u. +have /= := @cvg_differentiation_under_integral + R _ _ mu u `[0, 1] _ x _ _ _ _ _ _ _ _ (fun x y H _ => HM x y H). +apply => //=. +- by rewrite ball_itv/= in cex. +- move=> z z01; apply: continuous_compact_integrable => //. + exact: segment_compact. + by apply: continuous_subspaceT; exact: continuous_u. +- by move=> _; exact: ltW. +- apply: continuous_compact_integrable => //; first exact: segment_compact. + by apply: continuous_subspaceT; exact: cst_continuous. +Unshelve. all: end_near. Qed. + +Let derivable_integral01_u x : derivable integral01_u x 1. +Proof. +apply/cvg_ex; eexists. +rewrite /integral01_u/=. +under eq_fun do rewrite scaler1. +exact: cvg_dintegral01_u. +Qed. + +Let derive_integral01_u x : integral01_u^`() x = + - 2 * x * gauss x * \int[mu]_(t in `[0, 1]) gauss (t * x). +Proof. by apply/cvg_lim => //=; exact: cvg_dintegral01_u. Qed. + +Let derive_integral0_gauss x : 0 < x -> + derivable integral0_gauss x 1 /\ integral0_gauss^`() x = gauss x. +Proof. +move=> x0. +apply: (@continuous_FTC1 R gauss (BLeft 0) _ (x + 1) _ _ _ _). +- by rewrite ltrDl. +- apply: continuous_compact_integrable => //; first exact: segment_compact. + by apply: continuous_subspaceT; exact: continuous_gauss. +- by rewrite /=; rewrite lte_fin. +- by move=> ?; exact: continuous_gauss. +Qed. + +Definition h x := integral01_u x + (integral0_gauss x) ^+ 2. + +Let derive_h x : 0 < x -> h^`() x = 0. +Proof. +move=> x0. +rewrite /h derive1E deriveD//=; last first. + apply/diff_derivable. + apply: (@differentiable_comp _ _ _ _ integral0_gauss (fun x => x ^+ 2)). + apply/derivable1_diffP. + by have [] := derive_integral0_gauss x0. + by apply/derivable1_diffP; exact: exprn_derivable. +rewrite -derive1E derive_integral01_u -derive1E. +rewrite (@derive1_comp _ integral0_gauss (fun z => z ^+ 2))//; last first. + by have [] := derive_integral0_gauss x0. +rewrite derive1E exp_derive. +rewrite (derive_integral0_gauss _).2//. +rewrite expr1 scaler1. +rewrite addrC !mulNr; apply/eqP; rewrite subr_eq0; apply/eqP. +rewrite -!mulrA; congr *%R. +rewrite [LHS]mulrC. +rewrite [RHS]mulrCA; congr *%R. +rewrite /integral0_gauss [in LHS]/Rintegral. +have derM : ( *%R^~ x)^`() = cst x. + apply/funext => z. + by rewrite derive1E deriveMr// derive_id mulr1. +have := @integration_by_substitution_increasing R (fun t => t * x) gauss 0 1 ltr01. +rewrite -/mu mul0r mul1r => ->//=; last 6 first. + - move=> a b; rewrite !in_itv/= => /andP[a0 a1] /andP[b0 b1] ab. + by rewrite ltr_pM2r. + - by rewrite derM => z _; exact: cvg_cst. + - by rewrite derM; exact: is_cvg_cst. + - by rewrite derM; exact: is_cvg_cst. + - split => //. + + apply: cvg_at_right_filter. + by apply: cvgM => //; exact: cvg_cst. + + apply: cvg_at_left_filter. + by apply: cvgM => //; exact: cvg_cst. + - by apply: continuous_subspaceT; exact: continuous_gauss. +rewrite derM. +under eq_integral do rewrite fctE/= EFinM. +have ? : mu.-integrable `[0, 1] (fun y => (gauss (y * x))%:E). + apply: continuous_compact_integrable => //; first exact: segment_compact. + by apply: continuous_subspaceT => z; exact: continuous_gaussM. +rewrite integralZr//= fineM//=; last exact: integral_fune_fin_num. +by rewrite mulrC. +Qed. + +Let h0 : h 0 = pi / 4. +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_atan. +Qed. + +Let u_gauss t x : u x t <= gauss x. +Proof. +rewrite ler_pdivrMr ?oneDsqr_gt0 //. +rewrite (@le_trans _ _ (gauss x))//. + by rewrite ler_expR// mulNr lerN2 ler_peMr// ?sqr_ge0 ?oneDsqr_ge1. +by rewrite ler_peMr// ?expR_ge0 ?oneDsqr_ge1. +Qed. + +Let integral01_u_gauss x : integral01_u x <= gauss x. +Proof. +have -> : gauss x = \int[mu]_(t in `[0, 1]) gauss x. + rewrite /Rintegral integral_cst//. (* TODO: lemma Rintegral_cst *) + by rewrite /mu/= lebesgue_measure_itv//= lte01 oppr0 adde0 mule1. +rewrite fine_le//. +- apply: integral_fune_fin_num => //=. + apply: continuous_compact_integrable; first exact: segment_compact. + by apply: continuous_in_subspaceT => z _; exact: continuous_u. +- apply: integral_fune_fin_num => //=. + apply: continuous_compact_integrable; first exact: segment_compact. + by apply: continuous_subspaceT => z; exact: cvg_cst. +apply: ge0_le_integral => //=. +- by move=> y _; rewrite lee_fin u_ge0. +- by apply/measurable_EFinP => /=; apply/measurable_funTS; exact: measurable_u. +- by move=> y _; rewrite lee_fin expR_ge0. +- by move=> y _; rewrite lee_fin u_gauss. +Qed. + +Let cvg_integral01_u : integral01_u x @[x --> +oo] --> 0. +Proof. +apply: (@squeeze_cvgr _ _ _ _ (cst 0) gauss). +- by near=> n => /=; rewrite integral01_u_gauss integral01_u_ge0. +- exact: cvg_cst. +- exact: cvg_gauss. +Unshelve. all: end_near. Qed. + +Lemma cvg_integral0_gauss_sqr : (integral0_gauss x) ^+ 2 @[x --> +oo] --> pi / 4. +Proof. +have h_h0 x : 0 < x -> h x = h 0. + move=> x0. + have [] := @MVT _ h h^`() 0 x x0. + - move=> r; rewrite in_itv/= => /andP[r0 rx]. + apply: DeriveDef. + apply: derivableD => /=. + exact: derivable_integral01_u. + under eq_fun do rewrite expr2//=. + by apply: derivableM; have [] := derive_integral0_gauss r0. + by rewrite derive1E. + - rewrite /h => z. + apply: continuousD; last first. + rewrite /prop_for /continuous_at expr2. + under [X in X @ _ --> _]eq_fun do rewrite expr2. + by apply: cvgM; exact: continuous_integral0_gauss. + by apply: derivable_within_continuous => u _; exact: derivable_integral01_u. + move=> c; rewrite in_itv/= => /andP[c0 cx]. + by rewrite derive_h// mul0r => /eqP; rewrite subr_eq0 => /eqP. +have Ig2 x : 0 < x -> (integral0_gauss x) ^+ 2 = pi / 4 - integral01_u x. + move/h_h0/eqP; rewrite {1}/h eq_sym addrC -subr_eq => /eqP/esym. + by rewrite h0. +suff: pi / 4 - integral01_u x @[x --> +oo] --> pi / 4. + apply: cvg_trans; apply: near_eq_cvg. + by near=> x; rewrite Ig2. +rewrite -[in X in _ --> X](subr0 (pi / 4)). +by apply: cvgB => //; exact: cvg_cst. +Unshelve. end_near. Qed. + +End gauss_integral_proof. +End gauss_integral_proof. + +Section gauss_integral. +Context {R : realType}. +Import gauss_integral_proof. +Let mu := @lebesgue_measure R. + +Lemma integral0y_gauss_pi2 : + \int[mu]_(x in `[0%R, +oo[) gauss x = Num.sqrt pi / 2. +Proof. +have cvg_Ig : @integral0_gauss R x @[x --> +oo] --> Num.sqrt pi / 2. + have : Num.sqrt (@integral0_gauss R x ^+ 2) @[x --> +oo] + --> Num.sqrt (pi / 4). + apply: continuous_cvg => //; + [exact: sqrt_continuous|exact: cvg_integral0_gauss_sqr]. + rewrite sqrtrM ?pi_ge0// sqrtrV// (_ : 4 = 2 ^+ 2); last first. + by rewrite expr2 -natrM. + rewrite sqrtr_sqr ger0_norm//. + rewrite (_ : (fun _ => Num.sqrt _) = integral0_gauss)//. + apply/funext => r; rewrite sqrtr_sqr// ger0_norm//. + exact: integral0_gauss_ge0. +have /cvg_lim := @ge0_cvg_integral R mu gauss gauss_ge0 measurable_gauss. +rewrite /integral0y_gauss /Rintegral => <-//. +suff: limn (fun n => (\int[mu]_(x in `[0%R, n%:R]) (gauss x)%:E)%E) = + (Num.sqrt pi / 2)%:E. + by move=> ->. +apply/cvg_lim => //. +have H : (n%:R : R) @[n --> \oo] --> +oo. + (* NB: should this be a lemma? *) + by apply/cvgryPge => M; exact: nbhs_infty_ger. +move/cvg_pinftyP : cvg_Ig => /(_ _ H). +move/neq0_fine_cvgP; apply. +by rewrite gt_eqF// divr_gt0// sqrtr_gt0 pi_gt0. +Qed. + +End gauss_integral. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 5c9855232..5caade897 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -3440,6 +3440,77 @@ Qed. End integrable_lemmas. Arguments integrable_mkcond {d T R mu D} f. +Section ge0_cvg_integral. +Local Open Scope ereal_scope. +Context {R : realType}. +Variable mu : {measure set (@measurableTypeR R) -> \bar R}. +Variable f : R -> R. +Hypothesis f0 : (forall x, 0 <= f x)%R. +Hypothesis mf : measurable_fun setT f. + +Let ge0_integral_ereal_sup : + \int[mu]_(x in `[0%R, +oo[) (f x)%:E = + ereal_sup [set \int[mu]_(x in `[0%R, i.+1%:R]) (f x)%:E | i in [set: nat]]. +Proof. +apply/eqP; rewrite eq_le; apply/andP; split; last first. + apply: ub_ereal_sup => /=_ [n _ <-]. + apply: ge0_subset_integral => //=. + - by apply/measurable_EFinP; exact: measurable_funS mf. + - by move=> ? _; rewrite lee_fin f0. + - exact: subset_itvl. +rewrite itv_bnd_infty_bigcup0S. +rewrite seqDU_bigcup_eq ge0_integral_bigcup//; last 3 first. +- by move=> ?; apply: measurableD => //; exact: bigsetU_measurable. +- by apply: measurable_funTS; exact/measurable_EFinP. +- by move=> x; rewrite lee_fin f0//. +apply: lime_le => /=. + apply: is_cvg_nneseries => n _. + by apply: integral_ge0 => k _; exact: f0. +apply: nearW => n. +rewrite -ge0_integral_bigsetU//=; first last. +- by move=> ? _; rewrite lee_fin ?expR_ge0. +- by apply/measurable_EFinP; exact: measurableT_comp. +- exact: (@sub_trivIset _ _ _ [set: nat]). +- exact: iota_uniq. +- by move=> k; apply: measurableD => //; exact: bigsetU_measurable. +rewrite big_mkord -bigsetU_seqDU. +move: n => [|n]. + rewrite big_ord0 integral_set0. + apply: ereal_sup_le. + exists (\int[mu]_(x in `[0%R, 1%:R]) (f x)%:E) => //. + apply: integral_ge0. + by move=> ? _; rewrite lee_fin f0. +rewrite [X in \int[_]_(_ in X) _](_ : _ = `[0%R, n.+1%:R]%classic); last first. + rewrite eqEsubset; split => x/=; rewrite in_itv/=. + rewrite -(bigcup_mkord _ (fun k => `[0%R, k.+1%:R]%classic)). + move=> [k /= kSn]. + rewrite in_itv/= => /andP[-> xSk]/=. + by rewrite (le_trans xSk)// ler_nat. + move=> /andP[x0 Snx]. + rewrite -(bigcup_mkord _ (fun k => `[0%R, k.+1%:R]%classic)). + exists n => //=. + by rewrite in_itv/= x0 Snx. +apply: ereal_sup_le. +exists (\int[mu]_(x in `[0%R, n.+1%:R]) (f x)%:E); first by exists n. +apply: ge0_subset_integral => //=. + by apply/measurable_EFinP; exact: measurableT_comp. +by move=> ? _; rewrite lee_fin f0. +Qed. + +Lemma ge0_cvg_integral : + (fun n => \int[mu]_(x in `[0%R, n%:R]) (f x)%:E) @ \oo --> + \int[mu]_(x in `[0%R, +oo[) (f x)%:E. +Proof. +rewrite -cvg_shiftS/= ge0_integral_ereal_sup//. +apply/ereal_nondecreasing_cvgn/nondecreasing_seqP => n. +apply: (@ge0_subset_integral _ _ _ mu) => //. +- by apply: measurable_funTS; exact: measurableT_comp. +- by move => ? _; exact: f0. +- by apply: subset_itvl; rewrite bnd_simp ler_nat. +Qed. + +End ge0_cvg_integral. + Lemma finite_measure_integrable_cst d (T : measurableType d) (R : realType) (mu : {finite_measure set T -> \bar R}) k : mu.-integrable [set: T] (EFin \o cst k). @@ -4392,7 +4463,7 @@ Let cvg_g_ x : D x -> g_ ^~ x @ \oo --> 0. Proof. move=> Dx; rewrite -abse0; apply: cvg_abse. move: (f_f Dx); case: (f x) => [r|/=|/=]. -- by move=> f_r; apply/cvge_sub0. +- by move=> f_r; exact/sube_cvg0. - move/cvgeyPge/(_ (fine (g x) + 1)%R) => [n _]/(_ _ (leqnn n))/= h. have : (fine (g x) + 1)%:E <= g x. by rewrite (le_trans h)// (le_trans _ (absfg n Dx))// lee_abs. @@ -4475,7 +4546,7 @@ have h n : `| \int[mu]_(x in D) f_ n x - \int[mu]_(x in D) f x | by apply: le_integrable ig => // x Dx /=; rewrite (gee0_abs (g0 Dx)) absfg. by apply: le_abse_integral => //; exact: emeasurable_funB. suff: `| \int[mu]_(x in D) f_ n x - \int[mu]_(x in D) f x | @[n \oo] --> 0. - move/cvg_abse0P/cvge_sub0; apply. + move/cvg_abse0P/sube_cvg0; apply. rewrite fin_numElt (_ : -oo = - +oo)// -lte_absl. move: dominated_integrable => /integrableP[?]; apply: le_lt_trans. by apply: (le_trans _ (@le_abse_integral _ _ _ mu D f mD _)). @@ -4680,6 +4751,15 @@ move=> mD mf1 mf2 f12; rewrite /Rintegral fine_le//. - by apply/le_integral => // x xD; rewrite lee_fin f12//; exact/set_mem. Qed. +Lemma RintegralB D f1 f2 : measurable D -> + mu.-integrable D (EFin \o f1) -> mu.-integrable D (EFin \o f2) -> + \int[mu]_(x in D) (f1 x - f2 x) = + \int[mu]_(x in D) f1 x - \int[mu]_(x in D) f2 x. +Proof. +move=> mD if1 if2. +by rewrite /Rintegral integralB_EFin// fineB//; exact: integral_fune_fin_num. +Qed. + End Rintegral. Section ae_ge0_le_integral. @@ -4702,7 +4782,7 @@ apply: ge0_le_integral; first exact: measurableD. - exact: measurable_funS mf1. - by move=> t [Dt _]; exact: f20. - exact: measurable_funS mf2. -- by move=> t [Dt Nt]; move/subsetCl : f1f2N; apply. +- by move=> t [Dt Nt]; move/subsetCl : f1f2N; exact. Qed. End ae_ge0_le_integral. @@ -7102,7 +7182,7 @@ Proof. move=> mA; have := lebesgue_differentiation (locally_integrable_indic openT mA). apply: filter_app; first exact: (ae_filter_ringOfSetsType mu). apply: aeW => /= x Ax. -apply: (cvge_sub0 _ _).1 => //. +apply: (sube_cvg0 _ _).1 => //. move: Ax; rewrite /lebesgue_pt /davg /= -/mu => Ax. have : (fine (mu (ball x r)))^-1%:E * `|\int[mu]_(y in ball x r) (\1_A y - \1_A x)%:E | @[r --> 0^'+] --> 0. @@ -7204,7 +7284,7 @@ Lemma nice_lebesgue_differentiation (f : R -> R) : (fine (mu (E x n)))^-1%:E * \int[mu]_(y in E x n) (f y)%:E @[n --> \oo] --> (f x)%:E. Proof. -move=> locf x fx; apply: (cvge_sub0 _ _).1 => //=; apply/cvg_abse0P. +move=> locf x fx; apply: (sube_cvg0 _ _).1 => //=; apply/cvg_abse0P. pose r_ x : {posnum R} ^nat := (sval (cid (hE x).2)).2. pose C := (sval (cid (hE x).2)).1. have C_gt0 : (0 < C)%R by rewrite /C /sval/=; case: cid => -[? ?] []. diff --git a/theories/normedtype.v b/theories/normedtype.v index b87600267..6b7efb2e4 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -1892,6 +1892,13 @@ Notation "[ 'bounded' E | x 'in' A ]" := Notation bounded_set := [set A | [bounded x | x in A]]. Notation bounded_fun := [set f | [bounded f x | x in setT]]. +Lemma bounded_cst (K : numFieldType) {V : pseudoMetricNormedZmodType K} + (k : V) T (A : set T) : [bounded k | _ in A]. +Proof. +rewrite /bounded_near; near=> M => t At /=. +by near: M; exact: nbhs_pinfty_ge. +Unshelve. all: end_near. Qed. + Lemma bounded_fun_has_ubound (T : Type) (R : realFieldType) (a : T -> R) : bounded_fun a -> has_ubound (range a). Proof. @@ -2602,7 +2609,6 @@ Unshelve. all: by end_near. Qed. End NVS_continuity_mul. Section cvg_composition_pseudometric. - Context {K : numFieldType} {V : pseudoMetricNormedZmodType K} {T : Type}. Context (F : set_system T) {FF : Filter F}. Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a b : V). @@ -2654,6 +2660,12 @@ Qed. Lemma cvg_zero f a : (f - cst a) @ F --> (0 : V) -> f @ F --> a. Proof. by move=> Cfa; apply: cvg_sub0 Cfa (cvg_cst _). Qed. +Lemma subr_cvg0 f a : (fun x => f x - a) @ F --> 0 <-> f @ F --> a. +Proof. +split=> [?|fFk]; first exact: cvg_zero. +by rewrite -(@subrr _ a)//; apply: cvgB => //; exact: cvg_cst. +Qed. + Lemma cvg_norm f a : f @ F --> a -> `|f x| @[x --> F] --> (`|a| : K). Proof. by apply: continuous_cvg; apply: norm_continuous. Qed. @@ -3029,7 +3041,7 @@ Lemma cvgeB f g a b : a +? - b -> f @ F --> a -> g @ F --> b -> f \- g @ F --> a - b. Proof. by move=> ab fa gb; apply: cvgeD => //; exact: cvgeN. Qed. -Lemma cvge_sub0 f (k : \bar R) : +Lemma sube_cvg0 f (k : \bar R) : k \is a fin_num -> (fun x => f x - k) @ F --> 0 <-> f @ F --> k. Proof. move=> kfin; split. @@ -3206,6 +3218,8 @@ move=> [:apoo] [:bnoo] [:poopoo] [:poonoo]; move: a b => [a| |] [b| |] //. Unshelve. all: end_near. Qed. End ecvg_realFieldType. +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `sube_cvg0`")] +Notation cvge_sub0 := sube_cvg0 (only parsing). Section max_cts. Context {R : realType} {T : topologicalType}. diff --git a/theories/sequences.v b/theories/sequences.v index 285fb6255..b3c010a90 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1827,7 +1827,7 @@ Proof. exact: is_cvgeD. Qed. Lemma __deprecated__ereal_cvg_sub0 (R : realFieldType) (f : (\bar R)^nat) (k : \bar R) : k \is a fin_num -> (fun x => f x - k) @ \oo --> 0 <-> f @ \oo --> k. -Proof. exact: cvge_sub0. Qed. +Proof. exact: sube_cvg0. Qed. Lemma __deprecated__ereal_limD (R : realFieldType) (f g : (\bar R)^nat) : cvgn f -> cvgn g -> limn f +? limn g -> @@ -1956,7 +1956,7 @@ move/cvg_ex => [[l fl||/cvg_lim fnoo]] /=; last 2 first. rewrite [X in X @ _ --> _](_ : _ = fun N => l%:E - \sum_(0 <= k < N | P k) f k). apply/cvgeNP; rewrite oppe0. under eq_fun => ? do rewrite oppeD// oppeK addeC. - exact/cvge_sub0. + exact/sube_cvg0. apply/funext => N; apply/esym/eqP; rewrite sube_eq//. by rewrite addeC -nneseries_split_cond//; exact/eqP/esym/cvg_lim. by rewrite ge0_adde_def//= ?inE; [exact: nneseries_ge0|exact: sume_ge0]. diff --git a/theories/trigo.v b/theories/trigo.v index 5da3ff7ce..0eaca2d42 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -1187,6 +1187,9 @@ apply: (@is_derive_inverse R tan). exact/lt0r_neq0/ltr_pwDl/sqr_ge0. Unshelve. all: by end_near. Qed. +Lemma derivable_atan x : derivable atan x 1. +Proof. exact: ex_derive. Qed. + Lemma derive1_atan : atan^`() =1 (fun x => (1 + x ^+ 2)^-1). Proof. by move=> x; rewrite derive1E derive_val. Qed.