From 9b029aadafe2d9faf4717a0163c4cabfe8e5f0d4 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 7 Jan 2025 22:14:02 +0900 Subject: [PATCH 01/11] tentative gen of int. by subst Co-authored-by: IshiguroYoshihiro --- theories/ftc.v | 528 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 528 insertions(+) diff --git a/theories/ftc.v b/theories/ftc.v index 24ed05fb8..c7f0e3b63 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1,6 +1,7 @@ (* mathcomp analysis (c) 2023 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 archimedean. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop reals interval_inference ereal. From mathcomp Require Import topology tvs normedtype sequences real_interval. @@ -1111,6 +1112,135 @@ Unshelve. all: end_near. Qed. End integration_by_substitution_preliminaries. +(* PR in progress *) +Section integral_setU_EFin. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}). + +Lemma integral_bigsetU_EFin (I : eqType) (F : I -> set T) (f : T -> R) + (s : seq I) : + (forall i, d.-measurable (F i)) -> + uniq s -> trivIset [set` s] F -> + let D := \big[setU/set0]_(i <- s) F i in + measurable_fun D (EFin \o f) -> + \int[mu]_(x in D) (f x)%:E = (\sum_(i <- s) (\int[mu]_(x in F i) (f x)%:E)). +Proof. +move=> mF; elim: s => [|h t ih] us tF D mf. + by rewrite /D 2!big_nil integral_set0. +rewrite /D big_cons integral_setU_EFin//. +- rewrite big_cons ih//. + + by move: us => /= /andP[]. + + by apply: sub_trivIset tF => /= i /= it; rewrite inE it orbT. + + apply: measurable_funS mf => //; first exact: bigsetU_measurable. + by rewrite /D big_cons; exact: subsetUr. +- exact: bigsetU_measurable. +- by move/measurable_EFinP : mf; rewrite /D big_cons. +- apply/eqP; rewrite big_distrr/= big_seq big1// => i it. + move/trivIsetP : tF; apply => //=; rewrite ?mem_head//. + + by rewrite inE it orbT. + + by apply/eqP => hi; move: us => /=; rewrite hi it. +Qed. + +End integral_setU_EFin. + +Section PR_in_progress. +Local Open Scope ereal_scope. +Context {R : realType}. + +Lemma decr_derive1_le0 (f : R -> R) (D : set R) (x : R) : + {in (interior D) : set R, forall x : R, derivable f x 1%R} -> + {in D &, {homo f : x y /~ (x < y)%R}} -> + (interior D) x -> (f^`() x <= 0)%R. +Proof. +move=> df decrf Dx. +apply: limr_le. + under eq_fun. + move=> h. + rewrite {2}(_:h = h%:A :> R^o); last first. + by rewrite /GRing.scale/= mulr1. + over. + by apply: df; rewrite inE. +have := open_subball (@open_interior R^o D) Dx. +move=> [e /= e0 Hball]. +have/normr_idP normr2E : (@GRing.zero R <= 2)%R by []. +near=> h. +have hneq0 : h != 0%R by near: h; exact: nbhs_dnbhs_neq. +have Dohx : (interior D) (h + x). + move: (Hball (`|2 * h|%R)). + apply => //. + rewrite /= sub0r normrN !normrM !normr_id normr2E -ltr_pdivlMl//. + near: h. + apply: (@dnbhs0_lt _ R^o). + exact: mulr_gt0. + by rewrite normrM normr2E mulr_gt0// normr_gt0. + apply: ball_sym; rewrite /ball/= addrK. + rewrite normrM normr2E ltr_pMl ?normr_gt0//. + by rewrite (_:1%R = 1%:R)// ltr_nat. +move: hneq0; rewrite neq_lt => /orP[h0|h0]. ++ rewrite nmulr_rle0 ?invr_lt0// subr_ge0 ltW//. + apply: decrf; rewrite ?in_itv/= ?andbT ?ltW ?gtrDr// inE; exact: interior_subset. ++ rewrite pmulr_rle0 ?invr_gt0// subr_le0 ltW//. + apply: decrf; rewrite ?in_itv/= ?andbT ?ltW ?ltrDr// inE; exact: interior_subset. +Unshelve. end_near. Qed. + +Section itv_interior. + +Lemma itv_interior_bounded (x y : R) (a b : bool) : + (x < y)%R -> + [set` (Interval (BSide a x) (BSide b y))]^° = `]x, y[%classic. +Proof. +move=> xy. +rewrite interval_bounded_interior//; last exact: interval_is_interval. +rewrite inf_itv; last by case: a; case b; rewrite bnd_simp ?ltW. +rewrite sup_itv; last by case: a; case b; rewrite bnd_simp ?ltW. +exact: set_itvoo. +Qed. + +Lemma itv_interior_pinfty (x : R) (a : bool) : + [set` (Interval (BSide a x) (BInfty _ false))]^° = `]x, +oo[%classic. +Proof. +rewrite interval_right_unbounded_interior//; first last. + by apply: hasNubound_itv; rewrite lt_eqF. + exact: interval_is_interval. +rewrite inf_itv; last by case: a; rewrite bnd_simp ?ltW. +by rewrite set_itv_o_infty. +Qed. + +Lemma itv_interior_ninfty (y : R) (b : bool) : + [set` (Interval (BInfty _ true) (BSide b y))]^° = `]-oo, y[%classic. +Proof. +rewrite interval_left_unbounded_interior//; first last. + by apply: hasNlbound_itv; rewrite gt_eqF. + exact: interval_is_interval. +rewrite sup_itv; last by case b; rewrite bnd_simp ?ltW. +by apply: set_itv_infty_o. +Qed. + +Definition itv_interior := + (itv_interior_bounded, itv_interior_pinfty, itv_interior_ninfty). + +End itv_interior. + +Lemma decr_derive1_le0_itv (f : R^o -> R^o) (z : R) (x0 x1 : R) (b0 b1 : bool) : + {in `]x0, x1[, forall x : R, derivable f x 1%R} -> + {in (Interval (BSide b0 x0) (BSide b1 x1)) &, {homo f : x y /~ (x < y)%R}} -> + z \in `]x0, x1[ -> (f^`() z <= 0)%R. +Proof. +have [x10|x01] := leP x1 x0. + move=> _ _. + by move/lt_in_itv; rewrite bnd_simp le_gtF. +set itv := Interval (BSide b0 x0) (BSide b1 x1). +move=> df decrf xx0x1. +apply: (@decr_derive1_le0 _ [set` itv]). + rewrite itv_interior//. + by move=> ?; rewrite inE/=; apply: df. + move=> ? ?; rewrite !inE/=; apply: decrf. +by rewrite itv_interior/=. +Qed. + +End PR_in_progress. + Section integration_by_substitution. Local Open Scope ereal_scope. Context {R : realType}. @@ -1340,4 +1470,402 @@ apply: eq_integral => x /[!inE] xab; rewrite !fctE !opprK derive1E deriveN. - by case: Fab => + _ _; exact. Unshelve. all: end_near. Qed. +(* TODO: rename *) +Lemma decreasing_fun_itv_infty_bnd_bigcup F (x : R) : + {in `[x, +oo[ &, {homo F : x y /~ (x < y)%R}} -> + F x @[x --> +oo%R] --> -oo%R -> + `]-oo, F x]%classic = \bigcup_i `](F (x + i.+1%:R)%R), F x]%classic. +Proof. +move=> dF nyF. +rewrite itv_infty_bnd_bigcup eqEsubset; split. +- move=> y/= [n _]/=; rewrite in_itv/= => /andP[Fxny yFx]. + have [i iFxn] : exists i, (F (x + i.+1%:R) < F x - n%:R)%R. + move/cvgrNy_lt : nyF. + move/(_ (F x - n%:R)%R) => [z [zreal zFxn]]. + exists `| ceil (z - x) |%N. + apply: zFxn. + rewrite -ltrBlDl (le_lt_trans (le_ceil _))// (le_lt_trans (ler_norm _))//. + by rewrite -natr1 -intr_norm ltrDl. + exists i => //=. + rewrite in_itv/=; apply/andP; split => //. + exact: lt_le_trans Fxny. +- move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fxnz zFx]. + exists `| ceil (F (x + n.+1%:R) - F x)%R |%N.+1 => //=. + rewrite in_itv/= zFx andbT lerBlDr -lerBlDl (le_trans _ (abs_ceil_ge _))//. + by rewrite ler_normr orbC opprB lerB// ltW. +Qed. + +Lemma itv_bnd_infty_bigcup_shiftn (b : bool) (x : R) (n : nat): + [set` Interval (BSide b x) +oo%O] = + \bigcup_i [set` Interval (BSide b x) (BLeft (x + (i + n.+1)%:R))]. +Proof. +apply/seteqP; split=> y; rewrite /= !in_itv/= andbT; last first. + by move=> [k _ /=]; move: b => [|] /=; rewrite in_itv/= => /andP[//] /ltW. +move=> xy; exists (`|Num.ceil (y - x)|)%N => //=. +rewrite in_itv/= xy/= natrD natr_absz intr_norm addrA. +apply: ltr_pwDr; first by rewrite (_ : 0%R = 0%:R)// ltr_nat. +rewrite -lterBDl. +apply: (le_trans (le_ceil _)) => //=. +rewrite le_eqVlt; apply/predU1P; left. +apply/esym/normr_idP. +rewrite ler0z -ceil_ge0 (lt_le_trans (@ltrN10 R))// subr_ge0. +by case: b xy => //= /ltW. +Qed. + +Lemma itv_bnd_infty_bigcup_shiftS (b : bool) (x : R): + [set` Interval (BSide b x) +oo%O] = + \bigcup_i [set` Interval (BSide b x) (BLeft (x + i.+1%:R))]. +Proof. +under eq_bigcupr do rewrite -addn1. +exact: itv_bnd_infty_bigcup_shiftn. +Qed. + +Lemma decreasing_ge0_integration_by_substitutiony F G a : + {in `[a, +oo[ &, {homo F : x y /~ (x < y)%R}} -> + {in `]a, +oo[, continuous F^`()} -> + cvg (F^`() x @[x --> a^'+]) -> + cvg (F^`() x @[x --> +oo%R]) -> + (* derivable_oo_continuous_bnd F a +oo *) + F x @[x --> a^'+] --> F a -> + {in `]a, +oo[, forall x, derivable F x 1%R} -> + {within `]-oo, F a], continuous G} -> + (* {in `]-oo, F a[, continuous G} -> + (G x @[x --> (F a)^'-] --> G (F a)) -> *) + F x @[x --> +oo%R] --> -oo%R -> + {in `]-oo, F a], forall x, (0 <= G x)%R} -> + \int[mu]_(x in `]-oo, F a]) (G x)%:E = + \int[mu]_(x in `[a, +oo[) (((G \o F) * - F^`()) x)%:E. +Proof. +move=> decrF cdF /cvg_ex[/= dFa cdFa] /cvg_ex[/= dFoo cdFoo]. +move=> cFa dF /continuous_within_itvNycP[cG cGFa] Fny G0. +have mG n : measurable_fun `](F (a + n.+1%:R)), (F a)] G. + apply: (@measurable_fun_itv_oc _ _ _ false true). + apply: open_continuous_measurable_fun; first exact: interval_open. + move=> x; rewrite inE/= in_itv/= => /andP[_ xFa]. + by apply: cG; rewrite in_itv/=. +have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)[ ((G \o F) * - F^`())%R. + apply: (@measurable_fun_itv_co _ _ _ false true). + apply: open_continuous_measurable_fun; first exact: interval_open. + move=> x; rewrite inE/= in_itv/= => /andP[ax _]. + apply: continuousM; last first. + apply: continuousN. + by apply: cdF; rewrite in_itv/= andbT. + apply: continuous_comp. + have := derivable_within_continuous dF. + rewrite continuous_open_subspace; last exact: interval_open. + by apply; rewrite inE/= in_itv/= andbT. + by apply: cG; rewrite in_itv/=; apply: decrF; rewrite ?in_itv/= ?lexx ?ltW. +transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a]) (G x)%:E)). + rewrite (decreasing_fun_itv_infty_bnd_bigcup decrF Fny). + rewrite seqDU_bigcup_eq. + rewrite ge0_integral_bigcup/=; first last. + - exact: trivIset_seqDU. + - rewrite -seqDU_bigcup_eq. + move=> x [n _ /=]; rewrite in_itv/= => /andP[_ xFa]. + exact: G0. + - rewrite -seqDU_bigcup_eq. + exact/measurable_EFinP/measurable_fun_bigcup. + - by move=> n; apply: measurableD => //;exact: bigsetU_measurable. + apply: congr_lim; apply/funext => n. + rewrite -ge0_integral_bigsetU//=; last 5 first. + - by move=> m; apply: measurableD => //; exact: bigsetU_measurable. + - exact: iota_uniq. + - exact: (@sub_trivIset _ _ _ [set: nat]). + - apply/measurable_EFinP. + rewrite big_mkord -bigsetU_seqDU. + apply: (measurable_funS _ + (@bigsetU_bigcup _ (fun k =>`]F (a + k.+1%:R)%R, _]%classic) _)). + exact: bigcup_measurable. + exact/measurable_fun_bigcup. + - move=> x xFaSkFa. + apply: G0. + have : (x \in `]-oo, F a]%classic -> x \in `]-oo, F a]) by rewrite inE. + apply. + rewrite (decreasing_fun_itv_infty_bnd_bigcup decrF Fny). + apply: mem_set. + apply: (@bigsetU_bigcup _ _ n). + rewrite (bigsetU_seqDU (fun i => `](F (a + i.+1%:R)), (F a)]%classic)). + by rewrite -(@big_mkord _ _ _ _ xpredT + (seqDU (fun i => `](F (a + i.+1%:R)), (F a)]%classic))). + rewrite -integral_itv_obnd_cbnd; last first. + case: n => //. + by rewrite addr0 set_interval.set_itvoc0; apply: measurable_fun_set0. + congr (integral _). + rewrite big_mkord -bigsetU_seqDU. + rewrite -(bigcup_mkord n (fun k => `](F (a + k.+1%:R)), (F a)]%classic)). + rewrite eqEsubset; split. + move=> x [k /= kn]. + rewrite !in_itv/= => /andP[FaSkx ->]. + rewrite andbT. + rewrite (le_lt_trans _ FaSkx)//. + move: kn. + rewrite leq_eqVlt => /predU1P[-> //|Skn]. + apply/ltW/decrF; rewrite ?in_itv/= ?andbT ?ltW ?ltrDl ?ler_ltD ?ltr_nat//. + by rewrite ltr0n (leq_trans _ Skn). + case: n => [|n]; first by rewrite addr0 set_interval.set_itvoc0. + by apply: (@bigcup_sup _ _ n) => /=. +transitivity (limn (fun n => + \int[mu]_(x in `]a, (a + n%:R)%R[) (((G \o F) * - F^`()) x)%:E)); last first. + rewrite -integral_itv_obnd_cbnd; last first. + rewrite itv_bnd_infty_bigcup_shiftS. + apply/measurable_fun_bigcup => // n. + apply: measurable_funS (mGFNF' n) => //. + exact: subset_itv_oo_co. + rewrite itv_bnd_infty_bigcup_shiftS. + rewrite seqDU_bigcup_eq. + rewrite ge0_integral_bigcup/=; last 4 first. + - by move=> n; apply: measurableD => //; exact: bigsetU_measurable. + - rewrite -seqDU_bigcup_eq. + apply/measurable_fun_bigcup => // n. + apply/measurable_EFinP. + apply: measurable_funS (mGFNF' n) => //. + exact: subset_itv_oo_co. + - move=> x ax. + have {}ax : (a < x)%R. + move: ax. + rewrite -seqDU_bigcup_eq => -[? _]/=. + by rewrite in_itv/= => /andP[]. + rewrite fctE. + apply: mulr_ge0. + + apply: G0. + rewrite in_itv/= ltW//. + by apply: decrF; rewrite ?in_itv/= ?lexx// ltW. + + rewrite oppr_ge0. + apply: (@decr_derive1_le0 _ _ `[a, +oo[). + * rewrite itv_interior. + by move=> ?; rewrite inE/=; apply: dF. + * by move=> ? ?; rewrite !inE/=; apply: decrF. + * by rewrite itv_interior/= in_itv/= andbT. + - exact: trivIset_seqDU. + apply: congr_lim; apply/funext => n. + rewrite -integral_bigsetU_EFin/=; last 4 first. + - by move=> k; apply: measurableD => //; exact: bigsetU_measurable. + - exact: iota_uniq. + - exact: (@sub_trivIset _ _ _ [set: nat]). + - apply/measurable_EFinP. + apply: (measurable_funS (measurable_itv `]a, (a + n.+1%:R)[)). + rewrite big_mkord. + rewrite -bigsetU_seqDU. + rewrite -(bigcup_mkord _ (fun k => `]a, (a + k.+1%:R)[%classic)). + move=> x [k /= kn]. + rewrite !in_itv/= => /andP[-> xaSk]/=. + apply: (lt_trans xaSk). + by rewrite ler_ltD// ltr_nat. + apply: measurable_funS (mGFNF' n) => //. + exact: subset_itv_oo_co. + congr (integral _). + rewrite big_mkord -bigsetU_seqDU. + rewrite -(bigcup_mkord n (fun k => `]a, (a + k.+1%:R)[%classic)). + rewrite eqEsubset; split. + case: n; first by rewrite addr0 set_itvoo0. + move=> n. + by apply: (@bigcup_sup _ _ n) => /=. + move=> x [k /= kn]. + rewrite !in_itv/= => /andP[-> xaSk]/=. + rewrite (lt_le_trans xaSk)//. + move: kn. + rewrite leq_eqVlt => /orP[/eqP -> //|Skn]. + apply/ltW. + by rewrite ler_ltD// ltr_nat. +apply: congr_lim; apply/funext => -[|n]. + by rewrite addr0 set_itv1 integral_set1 set_itv_ge -?leNgt ?bnd_simp// integral_set0. +rewrite integration_by_substitution_decreasing. +- rewrite integral_itv_bndo_bndc// ?integral_itv_obnd_cbnd//. + + rewrite -setUitv1; last by rewrite bnd_simp ltrDl. + rewrite measurable_funU//; split; last exact: measurable_fun_set1. + by apply: measurable_funS (mGFNF' n) => //; exact: subset_itv_oo_co. + + by apply: measurable_funS (mGFNF' n) => //; exact: subset_itv_oo_co. +- by rewrite ltrDl. +- move=> x y /=; rewrite !in_itv/= => /andP[ax _] /andP[ay _] yx. + by apply: decrF; rewrite //in_itv/= ?ax ?ay. +- move=> x; rewrite in_itv/= => /andP[ax _]. + by apply: cdF; rewrite in_itv/= ax. +- exact: (cvgP dFa). +- apply: (cvgP (F^`() (a + n.+1%:R))). + apply: cvg_at_left_filter. + apply: cdF. + by rewrite in_itv/= andbT ltr_pwDr. +- split. + + move=> x; rewrite in_itv/= => /andP[ax _]. + by apply: dF; rewrite in_itv/= ax. + + exact: cFa. + + apply: cvg_at_left_filter. + apply: differentiable_continuous. + apply/derivable1_diffP. + apply: dF. + by rewrite in_itv/= andbT ltr_pwDr. +- apply/continuous_within_itvP. + + apply: decrF. + * by rewrite in_itv/= andbT lerDl. + * by rewrite in_itv/= lexx. + * by rewrite ltr_pwDr. + + split. + * move=> y; rewrite in_itv/= => /andP[_ yFa]. + by apply: cG; rewrite in_itv/= yFa. + * apply: cvg_at_right_filter. + apply/cG. + rewrite in_itv/=. + apply: decrF. + - by rewrite in_itv/= andbT lerDl. + - by rewrite in_itv/= lexx. + - by rewrite ltr_pwDr. + * exact: cGFa. +Qed. + +Lemma ge0_integration_by_substitutionNy G a : + {within `]-oo, (- a)%R], continuous G} -> + (* {in `]-oo, (- a)%R[, continuous G} -> + (G x @[x --> (- a)%R^'-] --> G (- a)%R) -> *) + {in `]-oo, (- a)%R], forall x, (0 <= G x)%R} -> + \int[mu]_(x in `]-oo, (- a)%R]) (G x)%:E = + \int[mu]_(x in `[a, +oo[) ((G \o -%R) x)%:E. +Proof. +move=> /continuous_within_itvNycP[cG GNa] G0. +have Dopp : (@GRing.opp R)^`() = cst (-1). + by apply/funext => z; rewrite derive1E derive_val. +rewrite decreasing_ge0_integration_by_substitutiony//; last 7 first. +- by move=> x y _ _; rewrite ltrN2. +- by rewrite Dopp => ? _; exact: cst_continuous. +- rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst. +- rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst. + apply: cvgN; exact: cvg_at_right_filter. +- exact/continuous_within_itvNycP. +- exact/cvgNrNy. +apply: eq_integral => x _; congr EFin. +rewrite fctE -[RHS]mulr1; congr (_ * _)%R. +rewrite -[RHS]opprK; congr -%R. +rewrite derive1E. +exact: derive_val. +Qed. + +Lemma increasing_ge0_integration_by_substitutiony F G a : + {in `[a, +oo[ &, {homo F : x y / (x < y)%R}} -> + {in `]a, +oo[, continuous F^`()} -> + cvg (F^`() x @[x --> a^'+]) -> + cvg (F^`() x @[x --> +oo%R]) -> + (* derivable_oo_continuous_bnd F a +oo *) + F x @[x --> a^'+] --> F a -> + {in `]a, +oo[, forall x, derivable F x 1%R} -> + {within `[F a, +oo[, continuous G} -> + (* {in `]F a, +oo[, continuous G} -> + (G x @[x --> (F a)^'+] --> G (F a)) -> *) + F x @[x --> +oo%R] --> +oo%R -> + {in `[F a, +oo[, forall x, (0 <= G x)%R} -> + \int[mu]_(x in `[F a, +oo[) (G x)%:E = + \int[mu]_(x in `[a, +oo[) (((G \o F) * F^`()) x)%:E. +Proof. +move=> incrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'ool] cFa dF. +move=> /continuous_within_itvcyP[cG cGFa] Fny G0. +transitivity (\int[mu]_(x in `[F a, +oo[) (((G \o -%R) \o -%R) x)%:E). + by apply/eq_integral => x ? /=; rewrite opprK. +have cGN : {in `]-oo, - F a[%R, continuous (G \o -%R)}. + move=> x; rewrite in_itv/= ltrNr => FaNx. + apply: continuous_comp; first exact: continuousN. + by apply: cG; rewrite in_itv/= FaNx. +rewrite -ge0_integration_by_substitutionNy//; last 2 first. + apply/continuous_within_itvNycP; split => //. + apply/cvg_at_rightNP. + apply: cvg_toP; first by apply/cvg_ex; exists (G (F a)). + by move/cvg_lim: cGFa => -> //; rewrite fctE opprK. + by move=> x; rewrite in_itv/= lerNr => FaNx; apply: G0; rewrite in_itv/= FaNx. +rewrite (@decreasing_ge0_integration_by_substitutiony (- F)%R); first last. +- move=> y. + rewrite in_itv/= lerNr => FaNy. + by apply: G0; rewrite in_itv/= FaNy. +- exact/cvgNrNy. +- apply/continuous_within_itvNycP; split => //. + rewrite fctE opprK. + exact/cvg_at_rightNP. +- move=> x ax; apply: derivableN. + exact: dF. +- exact: cvgN. +- apply/cvg_ex; exists (- l)%R. + have := (cvgN F'ool). + move/(_ (@filter_filter R _ proper_pinfty_nbhs)). + apply: cvg_trans. + apply: near_eq_cvg. + near=> z. + rewrite derive1E deriveN -?derive1E//. + apply: dF; rewrite in_itv/= andbT. + near: z. + rewrite near_nbhs. + apply: nbhs_pinfty_gt. + exact: num_real. +- apply/cvg_ex; exists (- r)%R. + have := cvgN F'ar. + move/(_ (@filter_filter R _ (at_right_proper_filter a))). + apply: cvg_trans. + apply: near_eq_cvg. + near=> z. + rewrite derive1E deriveN -?derive1E//. + by apply: dF; rewrite in_itv/= andbT. +- move=> x ax. + rewrite /continuous_at. + rewrite derive1E deriveN -?derive1E; last exact: dF. + have := cvgN (cF' x ax). + move/(_ (nbhs_filter x)). + apply: cvg_trans. + apply: near_eq_cvg. + rewrite near_simpl/=. + near=> z. + rewrite derive1E deriveN -?derive1E//. + apply: dF. + near: z. + rewrite near_nbhs. + apply: (@open_in_nearW _ _ `]a, +oo[). + + exact: interval_open. + + by move=> ?; rewrite inE/=. + + by rewrite inE. +- move=> x y ax ay yx. + rewrite ltrN2. + exact: incrF. +have mGF : measurable_fun `]a, +oo[ (G \o F). + apply: (@measurable_comp _ _ _ _ _ _ `]F a, +oo[%classic) => //. + - move=> /= _ [x] /[!in_itv]/= /andP[ax xb] <-. + by rewrite incrF ?incrF// in_itv/= ?lexx/= ?(ltW ab)//= ?(ltW ax) ?(ltW xb). + - apply: open_continuous_measurable_fun; first exact: interval_open. + by move=> x; rewrite inE/= => Fax; exact: cG. + - apply: subspace_continuous_measurable_fun => //. + apply: derivable_within_continuous => x. + exact: dF. +have mF' : measurable_fun `]a, +oo[ (- F)%R^`(). + apply: open_continuous_measurable_fun; first exact: interval_open. + move=> x; rewrite inE/= => ax. + rewrite /continuous_at. + rewrite derive1E deriveN; last exact: dF. + rewrite -derive1E. + under eq_cvg do rewrite -(opprK ((- F)%R^`() _)); apply: cvgN. + move: (cF' x ax). + apply: cvg_trans. + apply: near_eq_cvg => /=. + rewrite near_simpl. + near=> z. + rewrite !derive1E deriveN ?opprK//. + apply: dF. + near: z. + rewrite near_nbhs. + exact: near_in_itvoy. +rewrite -!integral_itv_obnd_cbnd; last 2 first. + apply: measurable_funM => //. + apply: open_continuous_measurable_fun; first exact: interval_open. + by move=> x; rewrite inE/=; exact: cF'. + apply: measurable_funM. + apply: (measurable_comp (measurable_itv `]-oo, (- F a)%R[)). + move=> _/=[x + <-]. + rewrite !in_itv/= andbT=> ax. + rewrite ltrN2. + by apply: incrF; rewrite ?in_itv/= ?lexx ?ltW. + apply: open_continuous_measurable_fun; first exact: interval_open. + by move=> x; rewrite inE/=; exact: cGN. + apply: measurableT_comp => //. + apply: subspace_continuous_measurable_fun => //. + exact: derivable_within_continuous. + exact: measurableT_comp. +apply: eq_integral => x/=; rewrite inE/= => ax. +congr EFin. +rewrite !fctE/= opprK; congr (_ * _)%R. +rewrite !derive1E deriveN ?opprK//. +exact: dF. +Unshelve. all: end_near. Qed. + End integration_by_substitution. From 32bf2536901bd8329103f708dda089319ada9ce4 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 13 Jan 2025 23:51:32 +0900 Subject: [PATCH 02/11] app --- theories/ftc.v | 142 ++++++++++++++++++++++++------------------------- 1 file changed, 71 insertions(+), 71 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index c7f0e3b63..38d11de21 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1471,7 +1471,7 @@ apply: eq_integral => x /[!inE] xab; rewrite !fctE !opprK derive1E deriveN. Unshelve. all: end_near. Qed. (* TODO: rename *) -Lemma decreasing_fun_itv_infty_bnd_bigcup F (x : R) : +Lemma decreasing_fun_itvNy_bnd_bigcup F (x : R) : {in `[x, +oo[ &, {homo F : x y /~ (x < y)%R}} -> F x @[x --> +oo%R] --> -oo%R -> `]-oo, F x]%classic = \bigcup_i `](F (x + i.+1%:R)%R), F x]%classic. @@ -1495,7 +1495,7 @@ rewrite itv_infty_bnd_bigcup eqEsubset; split. by rewrite ler_normr orbC opprB lerB// ltW. Qed. -Lemma itv_bnd_infty_bigcup_shiftn (b : bool) (x : R) (n : nat): +Lemma itv_bndy_bigcup_shiftn (b : bool) (x : R) (n : nat): [set` Interval (BSide b x) +oo%O] = \bigcup_i [set` Interval (BSide b x) (BLeft (x + (i + n.+1)%:R))]. Proof. @@ -1512,12 +1512,12 @@ rewrite ler0z -ceil_ge0 (lt_le_trans (@ltrN10 R))// subr_ge0. by case: b xy => //= /ltW. Qed. -Lemma itv_bnd_infty_bigcup_shiftS (b : bool) (x : R): +Lemma itv_bndy_bigcup_shiftS (b : bool) (x : R): [set` Interval (BSide b x) +oo%O] = \bigcup_i [set` Interval (BSide b x) (BLeft (x + i.+1%:R))]. Proof. under eq_bigcupr do rewrite -addn1. -exact: itv_bnd_infty_bigcup_shiftn. +exact: itv_bndy_bigcup_shiftn. Qed. Lemma decreasing_ge0_integration_by_substitutiony F G a : @@ -1556,7 +1556,7 @@ have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)[ ((G \o F) * - F^`())%R. by apply; rewrite inE/= in_itv/= andbT. by apply: cG; rewrite in_itv/=; apply: decrF; rewrite ?in_itv/= ?lexx ?ltW. transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a]) (G x)%:E)). - rewrite (decreasing_fun_itv_infty_bnd_bigcup decrF Fny). + rewrite (decreasing_fun_itvNy_bnd_bigcup decrF Fny). rewrite seqDU_bigcup_eq. rewrite ge0_integral_bigcup/=; first last. - exact: trivIset_seqDU. @@ -1581,7 +1581,7 @@ transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a]) (G x)%:E)). apply: G0. have : (x \in `]-oo, F a]%classic -> x \in `]-oo, F a]) by rewrite inE. apply. - rewrite (decreasing_fun_itv_infty_bnd_bigcup decrF Fny). + rewrite (decreasing_fun_itvNy_bnd_bigcup decrF Fny). apply: mem_set. apply: (@bigsetU_bigcup _ _ n). rewrite (bigsetU_seqDU (fun i => `](F (a + i.+1%:R)), (F a)]%classic)). @@ -1594,24 +1594,20 @@ transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a]) (G x)%:E)). rewrite big_mkord -bigsetU_seqDU. rewrite -(bigcup_mkord n (fun k => `](F (a + k.+1%:R)), (F a)]%classic)). rewrite eqEsubset; split. - move=> x [k /= kn]. - rewrite !in_itv/= => /andP[FaSkx ->]. - rewrite andbT. - rewrite (le_lt_trans _ FaSkx)//. - move: kn. - rewrite leq_eqVlt => /predU1P[-> //|Skn]. - apply/ltW/decrF; rewrite ?in_itv/= ?andbT ?ltW ?ltrDl ?ler_ltD ?ltr_nat//. - by rewrite ltr0n (leq_trans _ Skn). - case: n => [|n]; first by rewrite addr0 set_interval.set_itvoc0. + apply: bigcup_sub => k/= kn. + apply: subset_itvr; rewrite bnd_simp. + move: kn; rewrite leq_eqVlt => /predU1P[<-//|kn]. + by rewrite ltW// decrF ?in_itv/= ?andbT ?lerDl//= ltrD2l ltr_nat. + move: n => [|n]; first by rewrite addr0 set_interval.set_itvoc0. by apply: (@bigcup_sup _ _ n) => /=. transitivity (limn (fun n => \int[mu]_(x in `]a, (a + n%:R)%R[) (((G \o F) * - F^`()) x)%:E)); last first. rewrite -integral_itv_obnd_cbnd; last first. - rewrite itv_bnd_infty_bigcup_shiftS. + rewrite itv_bndy_bigcup_shiftS. apply/measurable_fun_bigcup => // n. apply: measurable_funS (mGFNF' n) => //. exact: subset_itv_oo_co. - rewrite itv_bnd_infty_bigcup_shiftS. + rewrite itv_bndy_bigcup_shiftS. rewrite seqDU_bigcup_eq. rewrite ge0_integral_bigcup/=; last 4 first. - by move=> n; apply: measurableD => //; exact: bigsetU_measurable. @@ -1625,11 +1621,9 @@ transitivity (limn (fun n => move: ax. rewrite -seqDU_bigcup_eq => -[? _]/=. by rewrite in_itv/= => /andP[]. - rewrite fctE. - apply: mulr_ge0. + rewrite fctE lee_fin mulr_ge0//. + apply: G0. - rewrite in_itv/= ltW//. - by apply: decrF; rewrite ?in_itv/= ?lexx// ltW. + by rewrite in_itv/= ltW// decrF ?in_itv ?andbT ?lexx//= ltW. + rewrite oppr_ge0. apply: (@decr_derive1_le0 _ _ `[a, +oo[). * rewrite itv_interior. @@ -1647,26 +1641,18 @@ transitivity (limn (fun n => rewrite big_mkord. rewrite -bigsetU_seqDU. rewrite -(bigcup_mkord _ (fun k => `]a, (a + k.+1%:R)[%classic)). - move=> x [k /= kn]. - rewrite !in_itv/= => /andP[-> xaSk]/=. - apply: (lt_trans xaSk). - by rewrite ler_ltD// ltr_nat. + apply: bigcup_sub => k/= kn. + by apply: subset_itvl; rewrite bnd_simp/= lerD2l ler_nat ltnS ltnW. apply: measurable_funS (mGFNF' n) => //. exact: subset_itv_oo_co. congr (integral _). rewrite big_mkord -bigsetU_seqDU. rewrite -(bigcup_mkord n (fun k => `]a, (a + k.+1%:R)[%classic)). rewrite eqEsubset; split. - case: n; first by rewrite addr0 set_itvoo0. - move=> n. + move: n => [|n]; first by rewrite addr0 set_itvoo0. by apply: (@bigcup_sup _ _ n) => /=. - move=> x [k /= kn]. - rewrite !in_itv/= => /andP[-> xaSk]/=. - rewrite (lt_le_trans xaSk)//. - move: kn. - rewrite leq_eqVlt => /orP[/eqP -> //|Skn]. - apply/ltW. - by rewrite ler_ltD// ltr_nat. + apply: bigcup_sub => k/= kn; apply: subset_itvl. + by rewrite bnd_simp/= lerD2l ler_nat. apply: congr_lim; apply/funext => -[|n]. by rewrite addr0 set_itv1 integral_set1 set_itv_ge -?leNgt ?bnd_simp// integral_set0. rewrite integration_by_substitution_decreasing. @@ -1689,26 +1675,16 @@ rewrite integration_by_substitution_decreasing. + move=> x; rewrite in_itv/= => /andP[ax _]. by apply: dF; rewrite in_itv/= ax. + exact: cFa. - + apply: cvg_at_left_filter. - apply: differentiable_continuous. - apply/derivable1_diffP. - apply: dF. + + apply/cvg_at_left_filter/differentiable_continuous. + apply/derivable1_diffP/dF. by rewrite in_itv/= andbT ltr_pwDr. - apply/continuous_within_itvP. - + apply: decrF. - * by rewrite in_itv/= andbT lerDl. - * by rewrite in_itv/= lexx. - * by rewrite ltr_pwDr. + + by rewrite decrF ?ltr_pwDr ?in_itv ?andbT//= lerDl. + split. * move=> y; rewrite in_itv/= => /andP[_ yFa]. by apply: cG; rewrite in_itv/= yFa. - * apply: cvg_at_right_filter. - apply/cG. - rewrite in_itv/=. - apply: decrF. - - by rewrite in_itv/= andbT lerDl. - - by rewrite in_itv/= lexx. - - by rewrite ltr_pwDr. + * apply/cvg_at_right_filter/cG. + by rewrite in_itv/= decrF ?in_itv/= ?andbT ?lerDl// ltr_pwDr. * exact: cGFa. Qed. @@ -1724,18 +1700,17 @@ move=> /continuous_within_itvNycP[cG GNa] G0. have Dopp : (@GRing.opp R)^`() = cst (-1). by apply/funext => z; rewrite derive1E derive_val. rewrite decreasing_ge0_integration_by_substitutiony//; last 7 first. -- by move=> x y _ _; rewrite ltrN2. -- by rewrite Dopp => ? _; exact: cst_continuous. -- rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst. -- rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst. - apply: cvgN; exact: cvg_at_right_filter. -- exact/continuous_within_itvNycP. -- exact/cvgNrNy. + by move=> x y _ _; rewrite ltrN2. + by rewrite Dopp => ? _; exact: cst_continuous. + by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst. + by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst. + by apply: cvgN; exact: cvg_at_right_filter. + exact/continuous_within_itvNycP. + exact/cvgNrNy. apply: eq_integral => x _; congr EFin. -rewrite fctE -[RHS]mulr1; congr (_ * _)%R. -rewrite -[RHS]opprK; congr -%R. -rewrite derive1E. -exact: derive_val. +rewrite fctE -[RHS]mulr1; congr *%R. +by rewrite fctE derive1E deriveN// opprK derive_id. + Qed. Lemma increasing_ge0_integration_by_substitutiony F G a : @@ -1780,8 +1755,7 @@ rewrite (@decreasing_ge0_integration_by_substitutiony (- F)%R); first last. exact: dF. - exact: cvgN. - apply/cvg_ex; exists (- l)%R. - have := (cvgN F'ool). - move/(_ (@filter_filter R _ proper_pinfty_nbhs)). + have /(_ (@filter_filter R _ proper_pinfty_nbhs)) := cvgN F'ool. apply: cvg_trans. apply: near_eq_cvg. near=> z. @@ -1802,8 +1776,7 @@ rewrite (@decreasing_ge0_integration_by_substitutiony (- F)%R); first last. - move=> x ax. rewrite /continuous_at. rewrite derive1E deriveN -?derive1E; last exact: dF. - have := cvgN (cF' x ax). - move/(_ (nbhs_filter x)). + have /(_ (nbhs_filter x)) := cvgN (cF' x ax). apply: cvg_trans. apply: near_eq_cvg. rewrite near_simpl/=. @@ -1816,9 +1789,7 @@ rewrite (@decreasing_ge0_integration_by_substitutiony (- F)%R); first last. + exact: interval_open. + by move=> ?; rewrite inE/=. + by rewrite inE. -- move=> x y ax ay yx. - rewrite ltrN2. - exact: incrF. +- by move=> x y ax ay yx; rewrite ltrN2; exact: incrF. have mGF : measurable_fun `]a, +oo[ (G \o F). apply: (@measurable_comp _ _ _ _ _ _ `]F a, +oo[%classic) => //. - move=> /= _ [x] /[!in_itv]/= /andP[ax xb] <-. @@ -1835,8 +1806,7 @@ have mF' : measurable_fun `]a, +oo[ (- F)%R^`(). rewrite derive1E deriveN; last exact: dF. rewrite -derive1E. under eq_cvg do rewrite -(opprK ((- F)%R^`() _)); apply: cvgN. - move: (cF' x ax). - apply: cvg_trans. + apply: cvg_trans (cF' x ax). apply: near_eq_cvg => /=. rewrite near_simpl. near=> z. @@ -1853,8 +1823,7 @@ rewrite -!integral_itv_obnd_cbnd; last 2 first. apply: (measurable_comp (measurable_itv `]-oo, (- F a)%R[)). move=> _/=[x + <-]. rewrite !in_itv/= andbT=> ax. - rewrite ltrN2. - by apply: incrF; rewrite ?in_itv/= ?lexx ?ltW. + by rewrite ltrN2 incrF// ?in_itv/= ?andbT// ltW. apply: open_continuous_measurable_fun; first exact: interval_open. by move=> x; rewrite inE/=; exact: cGN. apply: measurableT_comp => //. @@ -1869,3 +1838,34 @@ exact: dF. Unshelve. all: end_near. Qed. End integration_by_substitution. + +Section ge0_integralT_even. +Context {R : realType}. +Let mu := @lebesgue_measure R. +Local Open Scope ereal_scope. + +Lemma ge0_integralT_even (f : R -> R) : (forall x, 0 <= f x)%R -> + continuous f -> + f =1 f \o -%R -> + \int[mu]_x (f x)%:E = 2%:E * \int[mu]_(x in [set x | (0 <= x)%R]) (f x)%:E. +Proof. +move=> f0 cf evenf. +have mf : measurable_fun [set: R] f by exact: continuous_measurable_fun. +have mposnums : measurable [set x : R | 0 <= x]%R. + by rewrite -set_itv_c_infty. +rewrite -(setUv [set x : R | 0 <= x]%R) ge0_integral_setU//= ; last 4 first. + exact: measurableC. + by apply/measurable_EFinP; rewrite setUv. + by move=> x _; rewrite lee_fin. + exact/disj_setPCl. +rewrite mule_natl mule2n; congr +%E. +rewrite -set_itv_c_infty// setCitvr. +rewrite integral_itv_bndo_bndc; last exact: measurable_funTS. +rewrite -{1}oppr0 ge0_integration_by_substitutionNy//. +- apply: eq_integral => /= x. + rewrite inE/= in_itv/= andbT => x0. + by rewrite (evenf x). +- exact: continuous_subspaceT. +Qed. + +End ge0_integralT_even. From 7d9d592637e77151411ef2d44e98f81d43825b2f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 15 Jan 2025 08:15:53 +0900 Subject: [PATCH 03/11] wip --- theories/ftc.v | 138 +++++++++++++++++++++++++++---------------------- 1 file changed, 75 insertions(+), 63 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 38d11de21..b83cba484 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1470,14 +1470,18 @@ apply: eq_integral => x /[!inE] xab; rewrite !fctE !opprK derive1E deriveN. - by case: Fab => + _ _; exact. Unshelve. all: end_near. Qed. -(* TODO: rename *) -Lemma decreasing_fun_itvNy_bnd_bigcup F (x : R) : +Lemma decreasing_bigcup_itvS_Ny F (x : R) : {in `[x, +oo[ &, {homo F : x y /~ (x < y)%R}} -> F x @[x --> +oo%R] --> -oo%R -> - `]-oo, F x]%classic = \bigcup_i `](F (x + i.+1%:R)%R), F x]%classic. + \bigcup_i `](F (x + i.+1%:R)%R), F x]%classic = `]-oo, F x]%classic. Proof. move=> dF nyF. +(* TODO: itv_infty_bnd_bigcup -> esym *) rewrite itv_infty_bnd_bigcup eqEsubset; split. +- move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fxnz zFx]. + exists `| ceil (F (x + n.+1%:R) - F x)%R |%N.+1 => //=. + rewrite in_itv/= zFx andbT lerBlDr -lerBlDl (le_trans _ (abs_ceil_ge _))//. + by rewrite ler_normr orbC opprB lerB// ltW. - move=> y/= [n _]/=; rewrite in_itv/= => /andP[Fxny yFx]. have [i iFxn] : exists i, (F (x + i.+1%:R) < F x - n%:R)%R. move/cvgrNy_lt : nyF. @@ -1489,10 +1493,21 @@ rewrite itv_infty_bnd_bigcup eqEsubset; split. exists i => //=. rewrite in_itv/=; apply/andP; split => //. exact: lt_le_trans Fxny. -- move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fxnz zFx]. - exists `| ceil (F (x + n.+1%:R) - F x)%R |%N.+1 => //=. - rewrite in_itv/= zFx andbT lerBlDr -lerBlDl (le_trans _ (abs_ceil_ge _))//. - by rewrite ler_normr orbC opprB lerB// ltW. +Qed. + +Lemma decreasing_bigcup_itvS_bnd F a n : + {in `[a, +oo[ &, {homo F : x y /~ (x < y)%R}} -> + \bigcup_(i < n) `](F (a + i.+1%:R)), (F a)]%classic = + `](F (a + n%:R)), (F a)]%classic. +Proof. +move=> decrF. +rewrite eqEsubset; split. + apply: bigcup_sub => k/= kn. + apply: subset_itvr; rewrite bnd_simp. + move: kn; rewrite leq_eqVlt => /predU1P[<-//|kn]. + by rewrite ltW// decrF ?in_itv/= ?andbT ?lerDl//= ltrD2l ltr_nat. +move: n => [|n]; first by rewrite addr0 set_interval.set_itvoc0. +by apply: (@bigcup_sup _ _ n) => /=. Qed. Lemma itv_bndy_bigcup_shiftn (b : bool) (x : R) (n : nat): @@ -1520,29 +1535,28 @@ under eq_bigcupr do rewrite -addn1. exact: itv_bndy_bigcup_shiftn. Qed. +Definition derivable_oy_continuous_bnd {R' : numFieldType} + (f : R' -> R') (x : R') := + {in `]x, +oo[, forall x, derivable f x 1} /\ f @ x^'+ --> f x. + Lemma decreasing_ge0_integration_by_substitutiony F G a : {in `[a, +oo[ &, {homo F : x y /~ (x < y)%R}} -> {in `]a, +oo[, continuous F^`()} -> cvg (F^`() x @[x --> a^'+]) -> cvg (F^`() x @[x --> +oo%R]) -> - (* derivable_oo_continuous_bnd F a +oo *) - F x @[x --> a^'+] --> F a -> - {in `]a, +oo[, forall x, derivable F x 1%R} -> + derivable_oy_continuous_bnd F a -> F x @[x --> +oo%R] --> -oo%R -> {within `]-oo, F a], continuous G} -> - (* {in `]-oo, F a[, continuous G} -> - (G x @[x --> (F a)^'-] --> G (F a)) -> *) - F x @[x --> +oo%R] --> -oo%R -> {in `]-oo, F a], forall x, (0 <= G x)%R} -> \int[mu]_(x in `]-oo, F a]) (G x)%:E = \int[mu]_(x in `[a, +oo[) (((G \o F) * - F^`()) x)%:E. Proof. move=> decrF cdF /cvg_ex[/= dFa cdFa] /cvg_ex[/= dFoo cdFoo]. -move=> cFa dF /continuous_within_itvNycP[cG cGFa] Fny G0. +move=> [dF cFa] Fny /continuous_within_itvNycP[cG cGFa] G0. have mG n : measurable_fun `](F (a + n.+1%:R)), (F a)] G. apply: (@measurable_fun_itv_oc _ _ _ false true). apply: open_continuous_measurable_fun; first exact: interval_open. move=> x; rewrite inE/= in_itv/= => /andP[_ xFa]. - by apply: cG; rewrite in_itv/=. + by apply: cG; rewrite in_itv. have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)[ ((G \o F) * - F^`())%R. apply: (@measurable_fun_itv_co _ _ _ false true). apply: open_continuous_measurable_fun; first exact: interval_open. @@ -1556,22 +1570,21 @@ have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)[ ((G \o F) * - F^`())%R. by apply; rewrite inE/= in_itv/= andbT. by apply: cG; rewrite in_itv/=; apply: decrF; rewrite ?in_itv/= ?lexx ?ltW. transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a]) (G x)%:E)). - rewrite (decreasing_fun_itvNy_bnd_bigcup decrF Fny). + rewrite -(decreasing_bigcup_itvS_Ny decrF Fny). rewrite seqDU_bigcup_eq. rewrite ge0_integral_bigcup/=; first last. - exact: trivIset_seqDU. - - rewrite -seqDU_bigcup_eq. - move=> x [n _ /=]; rewrite in_itv/= => /andP[_ xFa]. - exact: G0. + - rewrite -seqDU_bigcup_eq => x Fax; rewrite lee_fin G0//; move: x Fax. + by apply: bigcup_sub => i _; exact: subset_itvr. - rewrite -seqDU_bigcup_eq. exact/measurable_EFinP/measurable_fun_bigcup. - by move=> n; apply: measurableD => //;exact: bigsetU_measurable. apply: congr_lim; apply/funext => n. rewrite -ge0_integral_bigsetU//=; last 5 first. - - by move=> m; apply: measurableD => //; exact: bigsetU_measurable. - - exact: iota_uniq. - - exact: (@sub_trivIset _ _ _ [set: nat]). - - apply/measurable_EFinP. + by move=> m; apply: measurableD => //; exact: bigsetU_measurable. + exact: iota_uniq. + exact: (@sub_trivIset _ _ _ [set: nat]). + apply/measurable_EFinP. rewrite big_mkord -bigsetU_seqDU. apply: (measurable_funS _ (@bigsetU_bigcup _ (fun k =>`]F (a + k.+1%:R)%R, _]%classic) _)). @@ -1579,27 +1592,19 @@ transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a]) (G x)%:E)). exact/measurable_fun_bigcup. - move=> x xFaSkFa. apply: G0. - have : (x \in `]-oo, F a]%classic -> x \in `]-oo, F a]) by rewrite inE. - apply. - rewrite (decreasing_fun_itvNy_bnd_bigcup decrF Fny). - apply: mem_set. - apply: (@bigsetU_bigcup _ _ n). - rewrite (bigsetU_seqDU (fun i => `](F (a + i.+1%:R)), (F a)]%classic)). - by rewrite -(@big_mkord _ _ _ _ xpredT - (seqDU (fun i => `](F (a + i.+1%:R)), (F a)]%classic))). + move: xFaSkFa. + rewrite big_mkord. + rewrite -bigsetU_seqDU. + rewrite -(bigcup_mkord _ (fun k => `](F (a + k.+1%:R)), (F a)]%classic)). + move: x. + by apply: bigcup_sub => k/= nk; exact: subset_itvr. rewrite -integral_itv_obnd_cbnd; last first. case: n => //. - by rewrite addr0 set_interval.set_itvoc0; apply: measurable_fun_set0. + by rewrite addr0 set_interval.set_itvoc0; exact: measurable_fun_set0. congr (integral _). rewrite big_mkord -bigsetU_seqDU. - rewrite -(bigcup_mkord n (fun k => `](F (a + k.+1%:R)), (F a)]%classic)). - rewrite eqEsubset; split. - apply: bigcup_sub => k/= kn. - apply: subset_itvr; rewrite bnd_simp. - move: kn; rewrite leq_eqVlt => /predU1P[<-//|kn]. - by rewrite ltW// decrF ?in_itv/= ?andbT ?lerDl//= ltrD2l ltr_nat. - move: n => [|n]; first by rewrite addr0 set_interval.set_itvoc0. - by apply: (@bigcup_sup _ _ n) => /=. + rewrite -(bigcup_mkord _ (fun k => `](F (a + k.+1%:R)), (F a)]%classic)). + exact: decreasing_bigcup_itvS_bnd. transitivity (limn (fun n => \int[mu]_(x in `]a, (a + n%:R)%R[) (((G \o F) * - F^`()) x)%:E)); last first. rewrite -integral_itv_obnd_cbnd; last first. @@ -1690,8 +1695,6 @@ Qed. Lemma ge0_integration_by_substitutionNy G a : {within `]-oo, (- a)%R], continuous G} -> - (* {in `]-oo, (- a)%R[, continuous G} -> - (G x @[x --> (- a)%R^'-] --> G (- a)%R) -> *) {in `]-oo, (- a)%R], forall x, (0 <= G x)%R} -> \int[mu]_(x in `]-oo, (- a)%R]) (G x)%:E = \int[mu]_(x in `[a, +oo[) ((G \o -%R) x)%:E. @@ -1704,13 +1707,14 @@ rewrite decreasing_ge0_integration_by_substitutiony//; last 7 first. by rewrite Dopp => ? _; exact: cst_continuous. by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst. by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst. - by apply: cvgN; exact: cvg_at_right_filter. - exact/continuous_within_itvNycP. + split. + - by []. + - by apply: cvgN; exact: cvg_at_right_filter. exact/cvgNrNy. + exact/continuous_within_itvNycP. apply: eq_integral => x _; congr EFin. rewrite fctE -[RHS]mulr1; congr *%R. by rewrite fctE derive1E deriveN// opprK derive_id. - Qed. Lemma increasing_ge0_integration_by_substitutiony F G a : @@ -1718,19 +1722,14 @@ Lemma increasing_ge0_integration_by_substitutiony F G a : {in `]a, +oo[, continuous F^`()} -> cvg (F^`() x @[x --> a^'+]) -> cvg (F^`() x @[x --> +oo%R]) -> - (* derivable_oo_continuous_bnd F a +oo *) - F x @[x --> a^'+] --> F a -> - {in `]a, +oo[, forall x, derivable F x 1%R} -> + derivable_oy_continuous_bnd F a -> F x @[x --> +oo%R] --> +oo%R-> {within `[F a, +oo[, continuous G} -> - (* {in `]F a, +oo[, continuous G} -> - (G x @[x --> (F a)^'+] --> G (F a)) -> *) - F x @[x --> +oo%R] --> +oo%R -> {in `[F a, +oo[, forall x, (0 <= G x)%R} -> \int[mu]_(x in `[F a, +oo[) (G x)%:E = \int[mu]_(x in `[a, +oo[) (((G \o F) * F^`()) x)%:E. Proof. -move=> incrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'ool] cFa dF. -move=> /continuous_within_itvcyP[cG cGFa] Fny G0. +move=> incrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'ool]. +move=> [dF cFa] Fny /continuous_within_itvcyP[cG cGFa] G0. transitivity (\int[mu]_(x in `[F a, +oo[) (((G \o -%R) \o -%R) x)%:E). by apply/eq_integral => x ? /=; rewrite opprK. have cGN : {in `]-oo, - F a[%R, continuous (G \o -%R)}. @@ -1747,13 +1746,14 @@ rewrite (@decreasing_ge0_integration_by_substitutiony (- F)%R); first last. - move=> y. rewrite in_itv/= lerNr => FaNy. by apply: G0; rewrite in_itv/= FaNy. -- exact/cvgNrNy. - apply/continuous_within_itvNycP; split => //. rewrite fctE opprK. exact/cvg_at_rightNP. -- move=> x ax; apply: derivableN. - exact: dF. -- exact: cvgN. +- exact/cvgNrNy. +- split. + + move=> x ax; apply: derivableN. + exact: dF. + + exact: cvgN. - apply/cvg_ex; exists (- l)%R. have /(_ (@filter_filter R _ proper_pinfty_nbhs)) := cvgN F'ool. apply: cvg_trans. @@ -1761,13 +1761,9 @@ rewrite (@decreasing_ge0_integration_by_substitutiony (- F)%R); first last. near=> z. rewrite derive1E deriveN -?derive1E//. apply: dF; rewrite in_itv/= andbT. - near: z. - rewrite near_nbhs. - apply: nbhs_pinfty_gt. - exact: num_real. + by near: z; apply: nbhs_pinfty_gt; exact: num_real. - apply/cvg_ex; exists (- r)%R. - have := cvgN F'ar. - move/(_ (@filter_filter R _ (at_right_proper_filter a))). + have /(_ (@filter_filter R _ (at_right_proper_filter a))) := cvgN F'ar. apply: cvg_trans. apply: near_eq_cvg. near=> z. @@ -1837,6 +1833,22 @@ rewrite !derive1E deriveN ?opprK//. exact: dF. Unshelve. all: end_near. Qed. +Lemma increasing_ge0_integration_by_substitution F G a : + {homo F : x y / (x < y)%R} -> + continuous F^`() -> + cvg (F^`() x @[x --> -oo%R]) -> + cvg (F^`() x @[x --> +oo%R]) -> + (forall x, derivable F x 1) -> + F x @[x --> -oo%R] --> -oo%R -> + F x @[x --> +oo%R] --> +oo%R -> + continuous G -> + (forall x, (0 <= G x)%R) -> + \int[mu]_x (G x)%:E = + \int[mu]_x (((G \o F) * F^`()) x)%:E. +Proof. +move=> ndF cdF cvgFNy cvgFy dF FNyNy Fyy cG G0. +Abort. + End integration_by_substitution. Section ge0_integralT_even. From 2f3a8ff9f76054a18bedab401705d4cd05aa1aa0 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Wed, 15 Jan 2025 15:04:03 +0900 Subject: [PATCH 04/11] wip --- theories/ftc.v | 126 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 126 insertions(+) diff --git a/theories/ftc.v b/theories/ftc.v index b83cba484..0beff1986 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1833,6 +1833,80 @@ rewrite !derive1E deriveN ?opprK//. exact: dF. Unshelve. all: end_near. Qed. +(* move to PR *) +Lemma incr_derive1_ge0 (f : R -> R) (D : set R) (x : R): + {in (interior D) : set R, forall x : R, derivable f x 1%R} -> + {in D &, {homo f : x y / (x < y)%R}} -> + (interior D) x -> (0 <= f^`() x)%R. +Proof. +move=> df incrf Dx. +rewrite -[leRHS]opprK oppr_ge0. +have dfx : derivable f x 1 by apply: df; rewrite inE. +rewrite derive1E -deriveN// -derive1E. +apply: (@decr_derive1_le0 _ _ D). +- move=> y Dy. + apply: derivableN. + exact: df. +- move=> y z Dy Dz yz. + rewrite ltrN2. + exact: incrf. +- exact: Dx. +Qed. + +Lemma incr_derive1_ge0_itv (f : R^o -> R^o) (z : R) (x0 x1 : R) (b0 b1 : bool) : + {in `]x0, x1[, forall x : R, derivable f x 1%R} -> + {in (Interval (BSide b0 x0) (BSide b1 x1)) &, {homo f : x y / (x < y)%R}} -> + z \in `]x0, x1[ -> (0 <= f^`() z)%R. +Proof. +have [x10|x01] := leP x1 x0. + move=> _ _. + by move/lt_in_itv; rewrite bnd_simp le_gtF. +set itv := Interval (BSide b0 x0) (BSide b1 x1). +move=> df incrf xx0x1. +apply: (@incr_derive1_ge0 _ [set` itv]). + rewrite itv_interior//. + by move=> ?; rewrite inE/=; apply: df. + move=> ? ?; rewrite !inE/=; apply: incrf. +by rewrite itv_interior/=. +Qed. + +(* PR? *) +Lemma interiorT {T : topologicalType} : interior (@setT T) = setT. +Proof. +rewrite eqEsubset; split; first exact: interior_subset. +rewrite -open_subsetE//. +exact: openT. +Qed. + +Lemma derivable_within_continuousT (f : R -> R) : + (forall x, derivable f x 1) -> continuous f. +Proof. +move=> df. +apply/continuous_subspace_setT. +rewrite -(@RhullK _ setT); last by rewrite inE. +apply: derivable_within_continuous. +move=> x _. +exact: df. +Qed. + +Definition derivable_yo_continuous_bnd {R' : numFieldType} + (f : R' -> R') (x : R') := + {in `]-oo, x[, forall x, derivable f x 1} /\ f @ x^'- --> f x. + +Lemma increasing_ge0_integration_by_substitutionNy F G b : + {in `]-oo, b] &, {homo F : x y / (x < y)%R}} -> + {in `]-oo, b[, continuous F^`()} -> + cvg (F^`() x @[x --> -oo%R]) -> + cvg (F^`() x @[x --> b^'-]) -> + derivable_yo_continuous_bnd F b -> F x @[x --> -oo%R] --> -oo%R-> + {within `]-oo, F b], continuous G} -> + {in `]-oo, F b], forall x, (0 <= G x)%R} -> + \int[mu]_(x in `]-oo, F b]) (G x)%:E = + \int[mu]_(x in `]-oo, b]) (((G \o F) * F^`()) x)%:E. +Proof. +move=> ndF cdF cvgFNy cvgFb [dF Fb] FNyNy cG G0. +Admitted. + Lemma increasing_ge0_integration_by_substitution F G a : {homo F : x y / (x < y)%R} -> continuous F^`() -> @@ -1847,6 +1921,58 @@ Lemma increasing_ge0_integration_by_substitution F G a : \int[mu]_x (((G \o F) * F^`()) x)%:E. Proof. move=> ndF cdF cvgFNy cvgFy dF FNyNy Fyy cG G0. +have mGFF' : measurable_fun setT ((G \o F) * F^`())%R. + apply: measurable_funM. + apply: measurableT_comp. + exact: continuous_measurable_fun. + apply: continuous_measurable_fun. + exact: derivable_within_continuousT. + exact: continuous_measurable_fun cdF. +rewrite -{2}setC0 -(set_itvoc0 0%R) setCitv/=. +rewrite ge0_integral_setU//=; first last. +- rewrite -(@RhullK _ `]-oo, 0%R]%classic); last first. + by rewrite inE/=; apply: interval_is_interval. + rewrite -(@RhullK _ `]0%R, +oo[%classic)//; last first. + by rewrite inE/=; apply: interval_is_interval. + apply: disj_itv_Rhull; first last. + 1, 2: apply: interval_is_interval. + rewrite eqEsubset; split => x//= []; rewrite !in_itv/= andbT => x0. + move/(le_lt_trans x0). + by rewrite ltxx. +- move=> x _. + apply: mulr_ge0; last first. + apply: (@incr_derive1_ge0 _ setT). + - by move=> ? _; apply: dF. + - by move=> ? ? _ _; apply: ndF. + - by rewrite interiorT. +- exact: G0. +- apply/measurable_EFinP. + rewrite -setCitvr setvU. + exact: mGFF'. +rewrite integral_itv_obnd_cbnd; last by apply: measurable_funTS; apply: mGFF'. +rewrite -(increasing_ge0_integration_by_substitutiony _ _ _ cvgFy); first last. +- admit. +- admit. +- admit. +- admit. +- admit. +- admit. +- admit. +rewrite -(increasing_ge0_integration_by_substitutionNy _ _ cvgFNy); first last. +- admit. +- admit. +- admit. +- admit. +- admit. +- admit. +- admit. +rewrite -integral_itv_obnd_cbnd; last first. + admit. +rewrite -ge0_integral_setU//=; first last. +- admit. +- admit. +- admit. +by rewrite -setCitvr setvU. Abort. End integration_by_substitution. From 41bd22e71347694f72eb05ddf931d1fa6ff7d1f7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 16 Jan 2025 11:40:00 +0900 Subject: [PATCH 05/11] integration by subst. over R --- CHANGELOG_UNRELEASED.md | 44 ++ classical/set_interval.v | 8 +- reals/real_interval.v | 31 +- theories/derive.v | 10 + theories/ftc.v | 829 ++++++++++++------------ theories/lebesgue_integral.v | 18 +- theories/lebesgue_measure.v | 4 +- theories/measurable_realfun.v | 81 ++- theories/normedtype.v | 75 +++ theories/realfun.v | 10 + theories/topology_theory/num_topology.v | 17 + 11 files changed, 654 insertions(+), 473 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index fbce21e52..a93fdb2be 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -213,6 +213,33 @@ - in `derive.v`: + lemmas `near_eq_derivable`, `near_eq_derive`, `near_eq_is_derive` +- in `derive.v`: + + lemmas `derive1N`, `derivable_opp`, `derive1_id` + +- in `normedtype.v`: + + lemmas `cvg_compNP`, `decreasing_itvNyo_bigcup`, `decreasing_itvoo_bigcup`, + `increasing_itvNyo_bigcup`, `increasing_itvoc_bigcup` + +- in `num_topology.v`: + + lemmas `nbhs_lt_trans`, `nbhs_lt_transN` + +- in `measurable_realfun.v`: + + lemmas `measurable_fun_itv_bndo_bndc`, `measurable_fun_itv_obnd_cbnd` + +- in `real_interval.v`: + + lemma `itv_bndy_bigcup_BLeft_shift` + +- in `realfun.v`: + + definitions `derivable_Nyo_continuous_bnd`, `derivable_oy_continuous_bnd ` + +- in `ftc.v`: + + lemmas + `decreasing_ge0_integration_by_substitutiony`, + `ge0_integration_by_substitutionNy`, + `increasing_ge0_integration_by_substitutiony`, + `ge0_integration_by_substitutionNy`, + `increasing_ge0_integration_by_substitutionT`, + `ge0_symfun_integralT` ### Changed @@ -331,6 +358,14 @@ + `inum_lt` -> `num_lt` + `inum_min` -> `num_min` + `inum_max` -> `num_max` +- in `real_interval.v`: + + `itv_bnd_infty_bigcup` -> `itv_bndy_bigcup_BRight` + + `itv_bnd_infty_bigcup0S` -> `itv0y_bigcup0S` + + `itv_infty_bnd_bigcup` -> `itvNy_bnd_bigcup_BLeft` + +- in `set_interval.v`: + + `opp_itv_bnd_infty` -> `opp_itv_bndy` + + `opp_itv_infty_bnd` -> `opp_itvNy_bnd` ### Generalized @@ -367,6 +402,12 @@ - in `lebesgue_measure.v`: + definition `vitali_cover`, lemma `vitali_coverS` +- in `ftc.v`: + + lemmas `increasing_cvg_at_right_comp`, + `increasing_cvg_at_left_comp`, + `decreasing_cvg_at_right_comp`, + `decreasing_cvg_at_left_comp` + ### Deprecated - in `Rstruct.v` + lemma `Rinvx` @@ -377,6 +418,9 @@ - in `itv.v`: + notation `%:inum` (use `%:num` instead) +- in `lebesgue_measure.v`: + + lemmas `measurable_fun_itv_co`, `measurable_fun_itv_oc` + ### Removed - in `sequences.v`: diff --git a/classical/set_interval.v b/classical/set_interval.v index 6f18fa46c..665d2a5fa 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -442,7 +442,7 @@ Hint Extern 0 (~ has_lbound _) => solve[by apply: hasNlbound_itv] : core. #[global] Hint Extern 0 (~ has_ubound _) => solve[by apply: hasNubound_itv] : core. -Lemma opp_itv_bnd_infty (R : numDomainType) (x : R) b : +Lemma opp_itv_bndy (R : numDomainType) (x : R) b : -%R @` [set` Interval (BSide b x) +oo%O] = [set` Interval -oo%O (BSide (negb b) (- x))]. Proof. @@ -451,8 +451,10 @@ rewrite predeqE => /= r; split=> [[y xy <-]|xr]. exists (- r); rewrite ?opprK //. by case: b xr; rewrite !in_itv/= andbT (lerNr, ltrNr). Qed. +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `opp_itv_bndy`")] +Notation opp_itv_bnd_infty := opp_itv_bndy (only parsing). -Lemma opp_itv_infty_bnd (R : numDomainType) (x : R) b : +Lemma opp_itvNy_bnd (R : numDomainType) (x : R) b : -%R @` [set` Interval -oo%O (BSide b x)] = [set` Interval (BSide (negb b) (- x)) +oo%O]. Proof. @@ -461,6 +463,8 @@ rewrite predeqE => /= r; split=> [[y xy <-]|xr]. exists (- r); rewrite ?opprK //. by case: b xr; rewrite !in_itv/= andbT (lerNl, ltrNl). Qed. +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `opp_itvNy_bnd`")] +Notation opp_itv_infty_bnd := opp_itvNy_bnd (only parsing). Lemma opp_itv_bnd_bnd (R : numDomainType) a b (x y : R) : -%R @` [set` Interval (BSide a x) (BSide b y)] = diff --git a/reals/real_interval.v b/reals/real_interval.v index 2ab7975a7..50300e29a 100644 --- a/reals/real_interval.v +++ b/reals/real_interval.v @@ -291,7 +291,22 @@ apply eq_bigcupr => k _; apply/seteqP; split=> [_/= [y ysr] <-|x/= xsr]. by exists (- x); rewrite ?oppr_itv//= opprK// negbK opprB opprK addrC. Qed. -Lemma itv_bnd_infty_bigcup (R : realType) b (x : R) : +Lemma itv_bndy_bigcup_BLeft_shift {R : realType} (b : bool) (x : R) (n : nat): + [set` Interval (BSide b x) +oo%O] = + \bigcup_i [set` Interval (BSide b x) (BLeft (x + (i + n)%:R))]. +Proof. +apply/seteqP; split=> y; rewrite /= !in_itv/= andbT; last first. + by move=> [k _ /=]; move: b => [|] /=; rewrite in_itv/= => /andP[//] /ltW. +move=> xy; exists `|Num.ceil (y - x)|.+1 => //=. +rewrite in_itv/= xy/= natrD -natr1 natr_absz intr_norm -addrA nat1r addrA. +apply: ltr_pwDr; first by rewrite ltr0n. +rewrite -lterBDl (le_trans (le_ceil _)) //= le_eqVlt; apply/predU1P; left. +apply/esym/normr_idP. +rewrite ler0z -ceil_ge0 (lt_le_trans (@ltrN10 R))// subr_ge0. +by case: b xy => //= /ltW. +Qed. + +Lemma itv_bndy_bigcup_BRight (R : realType) b (x : R) : [set` Interval (BSide b x) +oo%O] = \bigcup_i [set` Interval (BSide b x) (BRight (x + i%:R))]. Proof. @@ -301,28 +316,34 @@ move=> xy; exists `|ceil (y - x)|%N => //=; rewrite in_itv/= xy/= -lerBlDl. rewrite natr_absz ger0_norm ?ceil_ge//. by rewrite -(ceil0 R) ceil_le// subr_ge0 (lteifW xy). Qed. +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `itv_bndy_bigcup_BRight`")] +Notation itv_bnd_infty_bigcup := itv_bndy_bigcup_BRight (only parsing). -Lemma itv_bnd_infty_bigcup0S (R : realType) : +Lemma itv0y_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]. +rewrite itv_bndy_bigcup_BRight => z [i _ /= zi]. exists i => //=. apply: subset_itvl zi. by rewrite bnd_simp/= add0r ler_nat. Qed. +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `itv0y_bigcup0S`")] +Notation itv_bnd_infty_bigcup0S := itv0y_bigcup0S (only parsing). -Lemma itv_infty_bnd_bigcup (R : realType) b (x : R) : +Lemma itvNy_bnd_bigcup_BLeft (R : realType) b (x : R) : [set` Interval -oo%O (BSide b x)] = \bigcup_i [set` Interval (BLeft (x - i%:R)) (BSide b x)]. Proof. -have /(congr1 (fun x => -%R @` x)) := itv_bnd_infty_bigcup (~~ b) (- x). +have /(congr1 (fun x => -%R @` x)) := itv_bndy_bigcup_BRight (~~ b) (- x). rewrite opp_itv_bnd_infty negbK opprK => ->; rewrite image_bigcup. apply eq_bigcupr => k _; apply/seteqP; split=> [_ /= -[r rbxk <-]|y/= yxkb]. by rewrite oppr_itv/= opprB addrC. by exists (- y); [rewrite oppr_itv/= negbK opprD opprK|rewrite opprK]. Qed. +#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `itvNy_bnd_bigcup_BLeft`")] +Notation itv_infty_bnd_bigcup := itvNy_bnd_bigcup_BLeft (only parsing). Lemma bigcup_itvT {R : realType} b : \bigcup_i [set` Interval (BSide b (- i%:R)) (BRight i%:R)] = [set: R]. diff --git a/theories/derive.v b/theories/derive.v index 3caaa0978..c7a7517e4 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1907,6 +1907,16 @@ Qed. End near_derive. +Lemma derive1N {R : realFieldType} (f : R -> R) (x : R) : + derivable f x 1 -> (- f)^`() x = (- f^`()%classic x). +Proof. by move=> fx; rewrite !derive1E deriveN. Qed. + +Lemma derivable_opp {R : realFieldType} (x : R) v : derivable -%R x v. +Proof. by apply: derivableN; exact: derivable_id. Qed. + +Lemma derive1_id {R : realFieldType} (x : R) : id^`() x = 1. +Proof. by rewrite derive1E derive_id. Qed. + (* Trick to trigger type class resolution *) Lemma trigger_derive (R : realType) (f : R -> R) x x1 y1 : is_derive x (1 : R) f x1 -> x1 = y1 -> is_derive x 1 f y1. diff --git a/theories/ftc.v b/theories/ftc.v index 0beff1986..9fef7ba2c 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -33,6 +33,16 @@ From mathcomp Require Import derive charge. (* with $F$ decreasing, *) (* $\int_{F(a)}^{F(b)} G(x)dx = \int_a^b G(F(x))f(x)dx$ *) (* with $F$ increasing *) +(* - `{decreasing,increasing}_ge0_integration_by_substitutiony`: *) +(* $\int_{-\infty}^{F(a)} G(x)dx = \int_a^\infty -G(F(x))f(x)dx$ *) +(* with $F$ decreasing, $\lim_{x\to\infty}F(x)=-\infty$, and *) +(* $G$ non-negative, *) +(* $\int_{F(a)}^{\infty} G(x)dx = \int_a^\infty G(F(x))f(x)dx$ *) +(* with $F$ increasing, $\lim_{x\to\infty}F(x)=\infty$, and *) +(* $G$ non-negative *) +(* - `increasing_ge0_integration_by_substitutionT`: *) +(* $\int_{-\infty}^{\infty} G(x)dx = \int_{-\infty}^\infty -G(F(x))f(x)dx$ *) +(* with $F$ increasing and $G$ non-negative *) (* *) (* Detailed documentation: *) (* ``` *) @@ -804,11 +814,11 @@ move=> f_ge0 cf Fxl dF Fa dFE. have mf : measurable_fun `]a, +oo[ f. apply: open_continuous_measurable_fun => //. by move: cf => /continuous_within_itvcyP[/in_continuous_mksetP cf _]. -rewrite -integral_itv_obnd_cbnd// itv_bnd_infty_bigcup seqDU_bigcup_eq. +rewrite -integral_itv_obnd_cbnd// itv_bndy_bigcup_BRight seqDU_bigcup_eq. rewrite ge0_integral_bigcup//=; last 3 first. - by move=> k; apply: measurableD => //; exact: bigsetU_measurable. -- by rewrite -seqDU_bigcup_eq -itv_bnd_infty_bigcup; exact: measurableT_comp. -- move=> x/=; rewrite -seqDU_bigcup_eq -itv_bnd_infty_bigcup/=. +- by rewrite -seqDU_bigcup_eq -itv_bndy_bigcup_BRight; exact: measurableT_comp. +- move=> x/=; rewrite -seqDU_bigcup_eq -itv_bndy_bigcup_BRight/=. by rewrite /= in_itv/= => /andP[/ltW + _]; rewrite lee_fin; exact: f_ge0. have dFEn n : {in `]a + n%:R, a + n.+1%:R[, F^`() =1 f}. apply: in1_subset_itv dFE. @@ -832,7 +842,7 @@ transitivity (\sum_(0 <= i n _. rewrite seqDUE/= integral_itv_obnd_cbnd; last first. - apply: (@measurable_fun_itv_oc _ _ _ false true). + apply: measurable_fun_itv_bndo_bndc. apply: open_continuous_measurable_fun => //. move: cf => /continuous_within_itvcyP[cf _] x. rewrite inE/= in_itv/= => /andP[anx _]. @@ -1038,8 +1048,9 @@ move: xab; rewrite !in_itv/= => /andP[ax xb]. by apply/andP; split; apply: iF; rewrite // in_itv/= ?lexx !ltW. Qed. -Lemma increasing_cvg_at_right_comp F G a b (l : R) : (a < b)%R -> - {in `[a, b[ &, {homo F : x y / (x < y)%R}} -> +Lemma increasing_cvg_at_right_comp F G a (b : itv_bound R) (l : R) : + (BRight a < b)%O -> + {in Interval (BLeft a) b &, {homo F : x y / (x < y)%R}} -> F x @[x --> a^'+] --> F a -> G x @[x --> (F a)^'+] --> l -> (G \o F) x @[x --> a^'+] --> l. @@ -1049,15 +1060,32 @@ apply/cvgrPdist_le => /= e e0. have/cvgrPdist_le /(_ e e0) [d /= d0 {}GFa] := GFa. have := cvg_at_right_within cFa. move=> /cvgrPdist_lt/(_ _ d0)[d' /= d'0 {}cFa]. -near=> t. -apply: GFa; last by apply: incrF; rewrite //in_itv/= ?lexx//; apply/andP; split. -apply: cFa => //=. -rewrite ltr0_norm// ?subr_lt0// opprB. -by near: t; exact: nbhs_right_ltDr. +move: b ab incrF => [[b|b]|[//|]] ab incrF; rewrite bnd_simp in ab. +- near=> t. + apply: GFa; last first. + by apply: incrF; rewrite //in_itv/= ?lexx//; apply/andP; split. + apply: cFa => //=. + rewrite ltr0_norm// ?subr_lt0// opprB. + by near: t; exact: nbhs_right_ltDr. +- near=> t. + apply: GFa; last first. + apply: incrF; rewrite //in_itv/= ?lexx//; apply/andP; split => //. + exact: ltW. + by near: t; exact: nbhs_right_le. + apply: cFa => //=. + rewrite ltr0_norm// ?subr_lt0// opprB. + by near: t; exact: nbhs_right_ltDr. +- near=> t. + apply: GFa; last first. + by apply: incrF; rewrite //in_itv/= ?lexx//; exact/andP. + apply: cFa => //=. + rewrite ltr0_norm// ?subr_lt0// opprB. + by near: t; exact: nbhs_right_ltDr. Unshelve. all: end_near. Qed. -Lemma increasing_cvg_at_left_comp F G a b (l : R) : (a < b)%R -> - {in `]a, b] &, {homo F : x y / (x < y)%R}} -> +Lemma increasing_cvg_at_left_comp F G (a : itv_bound R) b (l : R) : + (a < BLeft b)%O -> + {in Interval a (BRight b) &, {homo F : x y / (x < y)%R}} -> F x @[x --> b^'-] --> F b -> G x @[x --> (F b)^'-] --> l -> (G \o F) x @[x --> b^'-] --> l. @@ -1067,15 +1095,30 @@ apply/cvgrPdist_le => /= e e0. have /cvgrPdist_le /(_ e e0) [d /= d0 {}GFb] := GFb. have := cvg_at_left_within cFb. move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFb]. -near=> t. -apply: GFb; last by apply: incrF; rewrite //in_itv/= ?lexx//; apply/andP; split. -apply: cFb => //=. -rewrite gtr0_norm// ?subr_gt0//. -by near: t; exact: nbhs_left_ltBl. +move: a ab incrF => [[a|a]|[|//]] ab incrF; rewrite bnd_simp in ab. +- near=> t. + apply: GFb; last first. + rewrite incrF// in_itv/= ?lexx ?andbT//. + apply/andP; split => //. + by near: t; exact: nbhs_left_ge. + exact: ltW. + rewrite /ball_/= cFb//= gtr0_norm// ?subr_gt0//. + by near: t; exact: nbhs_left_ltBl. +- near=> t. + apply: GFb; last first. + rewrite incrF// in_itv/= ?lexx ?andbT//. + exact/andP. + rewrite /ball_/= cFb//= gtr0_norm// ?subr_gt0//. + by near: t; exact: nbhs_left_ltBl. +- near=> t. + apply: GFb; last by rewrite incrF// in_itv/=. + apply: cFb => //=; rewrite gtr0_norm// ?subr_gt0//. + by near: t; exact: nbhs_left_ltBl. Unshelve. all: end_near. Qed. -Lemma decreasing_cvg_at_right_comp F G a b (l : R) : (a < b)%R -> - {in `[a, b[ &, {homo F : x y /~ (x < y)%R}} -> +Lemma decreasing_cvg_at_right_comp F G a (b : itv_bound R) (l : R) : + (BRight a < b)%O -> + {in Interval (BLeft a) b &, {homo F : x y /~ (x < y)%R}} -> F x @[x --> a^'+] --> F a -> G x @[x --> (F a)^'-] --> l -> (G \o F) x @[x --> a^'+] --> l. @@ -1085,15 +1128,30 @@ apply/cvgrPdist_le => /= e e0. have /cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFa] := GFa. have := cvg_at_right_within cFa. move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFa]. -near=> t. -apply: GFa; last by apply: decrF; rewrite //in_itv/= ?lexx//; apply/andP; split. -apply: cFa => //=. -rewrite ltr0_norm// ?subr_lt0// opprB. -by near: t; exact: nbhs_right_ltDr. +move: b ab decrF => [[b|b]|[//|]] ab decrF; rewrite bnd_simp in ab. +- near=> t. + apply: GFa; last by rewrite decrF// in_itv/= ?lexx//; apply/andP; split. + apply: cFa => //=; rewrite ltr0_norm// ?subr_lt0// opprB. + by near: t; exact: nbhs_right_ltDr. +- near=> t. + apply: GFa; last first. + rewrite decrF ?in_itv//= ?lexx//; apply/andP; split => //. + by near: t; exact: nbhs_right_le. + exact: ltW. + apply: cFa => //=. + rewrite ltr0_norm// ?subr_lt0// opprB. + by near: t; exact: nbhs_right_ltDr. +- near=> t. + apply: GFa; last first. + by rewrite decrF ?in_itv//= ?lexx//; exact/andP. + apply: cFa => //=. + rewrite ltr0_norm// ?subr_lt0// opprB. + by near: t; exact: nbhs_right_ltDr. Unshelve. all: end_near. Qed. -Lemma decreasing_cvg_at_left_comp F G a b (l : R) : (a < b)%R -> - {in `]a, b] &, {homo F : x y /~ (x < y)%R}} -> +Lemma decreasing_cvg_at_left_comp F G (a : itv_bound R) b (l : R) : + (a < BLeft b)%O -> + {in Interval a (BRight b) &, {homo F : x y /~ (x < y)%R}} -> F x @[x --> b^'-] --> F b -> G x @[x --> (F b)^'+] --> l -> (G \o F) x @[x --> b^'-] --> l. @@ -1103,144 +1161,47 @@ apply/cvgrPdist_le => /= e e0. have /cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFb] := GFb. have := cvg_at_left_within cFb. (* different point from gt0 version *) move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFb]. -near=> t. -apply: GFb; last by apply: decrF; rewrite //in_itv/= ?lexx//; apply/andP; split. -apply: cFb => //=. -rewrite gtr0_norm// ?subr_gt0//. -by near: t; exact: nbhs_left_ltBl. +move: a ab decrF => [[a|a]|[|//]] ab decrF; rewrite bnd_simp in ab. +- near=> t. + apply: GFb; last first. + apply: decrF; rewrite //in_itv/= ?lexx//; apply/andP; split => //. + exact: ltW. + by near: t; exact: nbhs_left_ge. + apply: cFb => //=. + rewrite gtr0_norm// ?subr_gt0//. + by near: t; exact: nbhs_left_ltBl. +- near=> t. + apply: GFb; last by apply: decrF; rewrite //in_itv/= ?lexx//; apply/andP; split. + apply: cFb => //=. + rewrite gtr0_norm// ?subr_gt0//. + by near: t; exact: nbhs_left_ltBl. +- near=> t. + apply: GFb; last by apply: decrF; rewrite //in_itv/= ?lexx//; apply/andP; split. + apply: cFb => //=. + rewrite gtr0_norm// ?subr_gt0//. + by near: t; exact: nbhs_left_ltBl. Unshelve. all: end_near. Qed. End integration_by_substitution_preliminaries. (* PR in progress *) -Section integral_setU_EFin. -Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) - (mu : {measure set T -> \bar R}). - -Lemma integral_bigsetU_EFin (I : eqType) (F : I -> set T) (f : T -> R) - (s : seq I) : - (forall i, d.-measurable (F i)) -> - uniq s -> trivIset [set` s] F -> - let D := \big[setU/set0]_(i <- s) F i in - measurable_fun D (EFin \o f) -> - \int[mu]_(x in D) (f x)%:E = (\sum_(i <- s) (\int[mu]_(x in F i) (f x)%:E)). +Lemma cvgNy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T) + (l : set_system T) : + f x @[x --> -oo] --> l <-> (f \o -%R) x @[x --> +oo] --> l. Proof. -move=> mF; elim: s => [|h t ih] us tF D mf. - by rewrite /D 2!big_nil integral_set0. -rewrite /D big_cons integral_setU_EFin//. -- rewrite big_cons ih//. - + by move: us => /= /andP[]. - + by apply: sub_trivIset tF => /= i /= it; rewrite inE it orbT. - + apply: measurable_funS mf => //; first exact: bigsetU_measurable. - by rewrite /D big_cons; exact: subsetUr. -- exact: bigsetU_measurable. -- by move/measurable_EFinP : mf; rewrite /D big_cons. -- apply/eqP; rewrite big_distrr/= big_seq big1// => i it. - move/trivIsetP : tF; apply => //=; rewrite ?mem_head//. - + by rewrite inE it orbT. - + by apply/eqP => hi; move: us => /=; rewrite hi it. +have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK. +by rewrite (eq_cvg -oo _ f_opp) fmap_comp ninftyN. Qed. -End integral_setU_EFin. - -Section PR_in_progress. -Local Open Scope ereal_scope. -Context {R : realType}. - -Lemma decr_derive1_le0 (f : R -> R) (D : set R) (x : R) : - {in (interior D) : set R, forall x : R, derivable f x 1%R} -> - {in D &, {homo f : x y /~ (x < y)%R}} -> - (interior D) x -> (f^`() x <= 0)%R. -Proof. -move=> df decrf Dx. -apply: limr_le. - under eq_fun. - move=> h. - rewrite {2}(_:h = h%:A :> R^o); last first. - by rewrite /GRing.scale/= mulr1. - over. - by apply: df; rewrite inE. -have := open_subball (@open_interior R^o D) Dx. -move=> [e /= e0 Hball]. -have/normr_idP normr2E : (@GRing.zero R <= 2)%R by []. -near=> h. -have hneq0 : h != 0%R by near: h; exact: nbhs_dnbhs_neq. -have Dohx : (interior D) (h + x). - move: (Hball (`|2 * h|%R)). - apply => //. - rewrite /= sub0r normrN !normrM !normr_id normr2E -ltr_pdivlMl//. - near: h. - apply: (@dnbhs0_lt _ R^o). - exact: mulr_gt0. - by rewrite normrM normr2E mulr_gt0// normr_gt0. - apply: ball_sym; rewrite /ball/= addrK. - rewrite normrM normr2E ltr_pMl ?normr_gt0//. - by rewrite (_:1%R = 1%:R)// ltr_nat. -move: hneq0; rewrite neq_lt => /orP[h0|h0]. -+ rewrite nmulr_rle0 ?invr_lt0// subr_ge0 ltW//. - apply: decrf; rewrite ?in_itv/= ?andbT ?ltW ?gtrDr// inE; exact: interior_subset. -+ rewrite pmulr_rle0 ?invr_gt0// subr_le0 ltW//. - apply: decrf; rewrite ?in_itv/= ?andbT ?ltW ?ltrDr// inE; exact: interior_subset. -Unshelve. end_near. Qed. - -Section itv_interior. - -Lemma itv_interior_bounded (x y : R) (a b : bool) : - (x < y)%R -> - [set` (Interval (BSide a x) (BSide b y))]^° = `]x, y[%classic. -Proof. -move=> xy. -rewrite interval_bounded_interior//; last exact: interval_is_interval. -rewrite inf_itv; last by case: a; case b; rewrite bnd_simp ?ltW. -rewrite sup_itv; last by case: a; case b; rewrite bnd_simp ?ltW. -exact: set_itvoo. -Qed. - -Lemma itv_interior_pinfty (x : R) (a : bool) : - [set` (Interval (BSide a x) (BInfty _ false))]^° = `]x, +oo[%classic. -Proof. -rewrite interval_right_unbounded_interior//; first last. - by apply: hasNubound_itv; rewrite lt_eqF. - exact: interval_is_interval. -rewrite inf_itv; last by case: a; rewrite bnd_simp ?ltW. -by rewrite set_itv_o_infty. -Qed. - -Lemma itv_interior_ninfty (y : R) (b : bool) : - [set` (Interval (BInfty _ true) (BSide b y))]^° = `]-oo, y[%classic. -Proof. -rewrite interval_left_unbounded_interior//; first last. - by apply: hasNlbound_itv; rewrite gt_eqF. - exact: interval_is_interval. -rewrite sup_itv; last by case b; rewrite bnd_simp ?ltW. -by apply: set_itv_infty_o. -Qed. - -Definition itv_interior := - (itv_interior_bounded, itv_interior_pinfty, itv_interior_ninfty). - -End itv_interior. - -Lemma decr_derive1_le0_itv (f : R^o -> R^o) (z : R) (x0 x1 : R) (b0 b1 : bool) : - {in `]x0, x1[, forall x : R, derivable f x 1%R} -> - {in (Interval (BSide b0 x0) (BSide b1 x1)) &, {homo f : x y /~ (x < y)%R}} -> - z \in `]x0, x1[ -> (f^`() z <= 0)%R. +(* PR in progress *) +Lemma cvgy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T) + (l : set_system T) : + f x @[x --> +oo] --> l <-> (f \o -%R) x @[x --> -oo] --> l. Proof. -have [x10|x01] := leP x1 x0. - move=> _ _. - by move/lt_in_itv; rewrite bnd_simp le_gtF. -set itv := Interval (BSide b0 x0) (BSide b1 x1). -move=> df decrf xx0x1. -apply: (@decr_derive1_le0 _ [set` itv]). - rewrite itv_interior//. - by move=> ?; rewrite inE/=; apply: df. - move=> ? ?; rewrite !inE/=; apply: decrf. -by rewrite itv_interior/=. +have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK. +by rewrite (eq_cvg +oo _ f_opp) fmap_comp ninfty. Qed. -End PR_in_progress. - Section integration_by_substitution. Local Open Scope ereal_scope. Context {R : realType}. @@ -1331,16 +1292,14 @@ rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first. exact: interval_open. by move=> z; rewrite inE/= => zab; rewrite fctE fE. + apply: cvgM. - apply: (decreasing_cvg_at_right_comp ab) => //. - * by move=> x y xab yab; apply: decrF; exact: subset_itv_co_cc. + apply: (decreasing_cvg_at_right_comp _ decrF) => //. * by move/continuous_within_itvP : cF => /(_ ab)[]. * by move/continuous_within_itvP : cG => /(_ FbFa)[]. rewrite fctE {2}/f eqxx; apply: cvgN. apply: cvg_trans F'ar; apply: near_eq_cvg. by near=> z; rewrite fE// in_itv/=; apply/andP; split. + apply: cvgM. - apply: (decreasing_cvg_at_left_comp ab). - * by move=> //x y xab yab; apply: decrF; apply: subset_itv_oc_cc. + apply: (decreasing_cvg_at_left_comp _ decrF) => //. * by move/continuous_within_itvP : cF => /(_ ab)[]. * by move/continuous_within_itvP : cG => /(_ FbFa)[]. rewrite fctE {2}/f gt_eqF// eqxx. @@ -1470,75 +1429,6 @@ apply: eq_integral => x /[!inE] xab; rewrite !fctE !opprK derive1E deriveN. - by case: Fab => + _ _; exact. Unshelve. all: end_near. Qed. -Lemma decreasing_bigcup_itvS_Ny F (x : R) : - {in `[x, +oo[ &, {homo F : x y /~ (x < y)%R}} -> - F x @[x --> +oo%R] --> -oo%R -> - \bigcup_i `](F (x + i.+1%:R)%R), F x]%classic = `]-oo, F x]%classic. -Proof. -move=> dF nyF. -(* TODO: itv_infty_bnd_bigcup -> esym *) -rewrite itv_infty_bnd_bigcup eqEsubset; split. -- move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fxnz zFx]. - exists `| ceil (F (x + n.+1%:R) - F x)%R |%N.+1 => //=. - rewrite in_itv/= zFx andbT lerBlDr -lerBlDl (le_trans _ (abs_ceil_ge _))//. - by rewrite ler_normr orbC opprB lerB// ltW. -- move=> y/= [n _]/=; rewrite in_itv/= => /andP[Fxny yFx]. - have [i iFxn] : exists i, (F (x + i.+1%:R) < F x - n%:R)%R. - move/cvgrNy_lt : nyF. - move/(_ (F x - n%:R)%R) => [z [zreal zFxn]]. - exists `| ceil (z - x) |%N. - apply: zFxn. - rewrite -ltrBlDl (le_lt_trans (le_ceil _))// (le_lt_trans (ler_norm _))//. - by rewrite -natr1 -intr_norm ltrDl. - exists i => //=. - rewrite in_itv/=; apply/andP; split => //. - exact: lt_le_trans Fxny. -Qed. - -Lemma decreasing_bigcup_itvS_bnd F a n : - {in `[a, +oo[ &, {homo F : x y /~ (x < y)%R}} -> - \bigcup_(i < n) `](F (a + i.+1%:R)), (F a)]%classic = - `](F (a + n%:R)), (F a)]%classic. -Proof. -move=> decrF. -rewrite eqEsubset; split. - apply: bigcup_sub => k/= kn. - apply: subset_itvr; rewrite bnd_simp. - move: kn; rewrite leq_eqVlt => /predU1P[<-//|kn]. - by rewrite ltW// decrF ?in_itv/= ?andbT ?lerDl//= ltrD2l ltr_nat. -move: n => [|n]; first by rewrite addr0 set_interval.set_itvoc0. -by apply: (@bigcup_sup _ _ n) => /=. -Qed. - -Lemma itv_bndy_bigcup_shiftn (b : bool) (x : R) (n : nat): - [set` Interval (BSide b x) +oo%O] = - \bigcup_i [set` Interval (BSide b x) (BLeft (x + (i + n.+1)%:R))]. -Proof. -apply/seteqP; split=> y; rewrite /= !in_itv/= andbT; last first. - by move=> [k _ /=]; move: b => [|] /=; rewrite in_itv/= => /andP[//] /ltW. -move=> xy; exists (`|Num.ceil (y - x)|)%N => //=. -rewrite in_itv/= xy/= natrD natr_absz intr_norm addrA. -apply: ltr_pwDr; first by rewrite (_ : 0%R = 0%:R)// ltr_nat. -rewrite -lterBDl. -apply: (le_trans (le_ceil _)) => //=. -rewrite le_eqVlt; apply/predU1P; left. -apply/esym/normr_idP. -rewrite ler0z -ceil_ge0 (lt_le_trans (@ltrN10 R))// subr_ge0. -by case: b xy => //= /ltW. -Qed. - -Lemma itv_bndy_bigcup_shiftS (b : bool) (x : R): - [set` Interval (BSide b x) +oo%O] = - \bigcup_i [set` Interval (BSide b x) (BLeft (x + i.+1%:R))]. -Proof. -under eq_bigcupr do rewrite -addn1. -exact: itv_bndy_bigcup_shiftn. -Qed. - -Definition derivable_oy_continuous_bnd {R' : numFieldType} - (f : R' -> R') (x : R') := - {in `]x, +oo[, forall x, derivable f x 1} /\ f @ x^'+ --> f x. - Lemma decreasing_ge0_integration_by_substitutiony F G a : {in `[a, +oo[ &, {homo F : x y /~ (x < y)%R}} -> {in `]a, +oo[, continuous F^`()} -> @@ -1546,19 +1436,19 @@ Lemma decreasing_ge0_integration_by_substitutiony F G a : cvg (F^`() x @[x --> +oo%R]) -> derivable_oy_continuous_bnd F a -> F x @[x --> +oo%R] --> -oo%R -> {within `]-oo, F a], continuous G} -> - {in `]-oo, F a], forall x, (0 <= G x)%R} -> + {in `]-oo, F a[, forall x, (0 <= G x)%R} -> \int[mu]_(x in `]-oo, F a]) (G x)%:E = \int[mu]_(x in `[a, +oo[) (((G \o F) * - F^`()) x)%:E. Proof. move=> decrF cdF /cvg_ex[/= dFa cdFa] /cvg_ex[/= dFoo cdFoo]. move=> [dF cFa] Fny /continuous_within_itvNycP[cG cGFa] G0. have mG n : measurable_fun `](F (a + n.+1%:R)), (F a)] G. - apply: (@measurable_fun_itv_oc _ _ _ false true). + apply: measurable_fun_itv_bndo_bndc. apply: open_continuous_measurable_fun; first exact: interval_open. move=> x; rewrite inE/= in_itv/= => /andP[_ xFa]. by apply: cG; rewrite in_itv. have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)[ ((G \o F) * - F^`())%R. - apply: (@measurable_fun_itv_co _ _ _ false true). + apply: measurable_fun_itv_obnd_cbnd. apply: open_continuous_measurable_fun; first exact: interval_open. move=> x; rewrite inE/= in_itv/= => /andP[ax _]. apply: continuousM; last first. @@ -1569,15 +1459,19 @@ have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)[ ((G \o F) * - F^`())%R. rewrite continuous_open_subspace; last exact: interval_open. by apply; rewrite inE/= in_itv/= andbT. by apply: cG; rewrite in_itv/=; apply: decrF; rewrite ?in_itv/= ?lexx ?ltW. -transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a]) (G x)%:E)). - rewrite -(decreasing_bigcup_itvS_Ny decrF Fny). +rewrite -integral_itv_bndo_bndc; last first. + apply: open_continuous_measurable_fun => // x. + by rewrite inE => /cG. +transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a[) (G x)%:E)). + rewrite (decreasing_itvNyo_bigcup decrF Fny). rewrite seqDU_bigcup_eq. rewrite ge0_integral_bigcup/=; first last. - exact: trivIset_seqDU. - rewrite -seqDU_bigcup_eq => x Fax; rewrite lee_fin G0//; move: x Fax. by apply: bigcup_sub => i _; exact: subset_itvr. - rewrite -seqDU_bigcup_eq. - exact/measurable_EFinP/measurable_fun_bigcup. + apply/measurable_EFinP/measurable_fun_bigcup => //. + by move=> i; apply: measurable_funS (mG i) => //; exact: subset_itvW. - by move=> n; apply: measurableD => //;exact: bigsetU_measurable. apply: congr_lim; apply/funext => n. rewrite -ge0_integral_bigsetU//=; last 5 first. @@ -1587,54 +1481,51 @@ transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a]) (G x)%:E)). apply/measurable_EFinP. rewrite big_mkord -bigsetU_seqDU. apply: (measurable_funS _ - (@bigsetU_bigcup _ (fun k =>`]F (a + k.+1%:R)%R, _]%classic) _)). + (@bigsetU_bigcup _ (fun k =>`]F (a + k.+1%:R)%R, _[%classic) _)). exact: bigcup_measurable. - exact/measurable_fun_bigcup. + apply/measurable_fun_bigcup => //. + by move=> i; apply: measurable_funS (mG i) => //; exact: subset_itvW. - move=> x xFaSkFa. apply: G0. move: xFaSkFa. - rewrite big_mkord. - rewrite -bigsetU_seqDU. - rewrite -(bigcup_mkord _ (fun k => `](F (a + k.+1%:R)), (F a)]%classic)). - move: x. - by apply: bigcup_sub => k/= nk; exact: subset_itvr. + rewrite big_mkord -bigsetU_seqDU. + rewrite -(bigcup_mkord _ (fun k => `]F (a + k.+1%:R), F a[%classic)). + by move: x; apply: bigcup_sub => k/= nk; exact: subset_itvr. rewrite -integral_itv_obnd_cbnd; last first. - case: n => //. - by rewrite addr0 set_interval.set_itvoc0; exact: measurable_fun_set0. + case: n => [|n]. + by rewrite addr0 set_itvoo0; exact: measurable_fun_set0. + by apply: measurable_funS (mG n) => //; exact: subset_itvW. congr (integral _). rewrite big_mkord -bigsetU_seqDU. - rewrite -(bigcup_mkord _ (fun k => `](F (a + k.+1%:R)), (F a)]%classic)). - exact: decreasing_bigcup_itvS_bnd. + rewrite -(bigcup_mkord _ (fun k => `]F (a + k.+1%:R), F a[%classic)). + exact/esym/decreasing_itvoo_bigcup. transitivity (limn (fun n => \int[mu]_(x in `]a, (a + n%:R)%R[) (((G \o F) * - F^`()) x)%:E)); last first. rewrite -integral_itv_obnd_cbnd; last first. - rewrite itv_bndy_bigcup_shiftS. + rewrite (@itv_bndy_bigcup_BLeft_shift _ _ _ 1). + under eq_bigcupr do rewrite addn1. apply/measurable_fun_bigcup => // n. apply: measurable_funS (mGFNF' n) => //. exact: subset_itv_oo_co. - rewrite itv_bndy_bigcup_shiftS. - rewrite seqDU_bigcup_eq. - rewrite ge0_integral_bigcup/=; last 4 first. + rewrite (@itv_bndy_bigcup_BLeft_shift _ _ _ 1). + under eq_bigcupr do rewrite addn1. + rewrite seqDU_bigcup_eq ge0_integral_bigcup/=; last 4 first. - by move=> n; apply: measurableD => //; exact: bigsetU_measurable. - - rewrite -seqDU_bigcup_eq. - apply/measurable_fun_bigcup => // n. - apply/measurable_EFinP. - apply: measurable_funS (mGFNF' n) => //. + - rewrite -seqDU_bigcup_eq; apply/measurable_fun_bigcup => // n. + apply/measurable_EFinP; apply: measurable_funS (mGFNF' n) => //. exact: subset_itv_oo_co. - move=> x ax. have {}ax : (a < x)%R. - move: ax. - rewrite -seqDU_bigcup_eq => -[? _]/=. + move: ax; rewrite -seqDU_bigcup_eq => -[? _]/=. by rewrite in_itv/= => /andP[]. rewrite fctE lee_fin mulr_ge0//. + apply: G0. - by rewrite in_itv/= ltW// decrF ?in_itv ?andbT ?lexx//= ltW. + by rewrite in_itv/= decrF ?in_itv ?andbT ?lexx//= ltW. + rewrite oppr_ge0. apply: (@decr_derive1_le0 _ _ `[a, +oo[). - * rewrite itv_interior. - by move=> ?; rewrite inE/=; apply: dF. + * by rewrite interior_itv => ?; rewrite inE/=; apply: dF. * by move=> ? ?; rewrite !inE/=; apply: decrF. - * by rewrite itv_interior/= in_itv/= andbT. + * by rewrite interior_itv/= in_itv/= andbT. - exact: trivIset_seqDU. apply: congr_lim; apply/funext => n. rewrite -integral_bigsetU_EFin/=; last 4 first. @@ -1643,13 +1534,11 @@ transitivity (limn (fun n => - exact: (@sub_trivIset _ _ _ [set: nat]). - apply/measurable_EFinP. apply: (measurable_funS (measurable_itv `]a, (a + n.+1%:R)[)). - rewrite big_mkord. - rewrite -bigsetU_seqDU. + rewrite big_mkord -bigsetU_seqDU. rewrite -(bigcup_mkord _ (fun k => `]a, (a + k.+1%:R)[%classic)). apply: bigcup_sub => k/= kn. by apply: subset_itvl; rewrite bnd_simp/= lerD2l ler_nat ltnS ltnW. - apply: measurable_funS (mGFNF' n) => //. - exact: subset_itv_oo_co. + by apply: measurable_funS (mGFNF' n) => //; exact: subset_itv_oo_co. congr (integral _). rewrite big_mkord -bigsetU_seqDU. rewrite -(bigcup_mkord n (fun k => `]a, (a + k.+1%:R)[%classic)). @@ -1659,7 +1548,10 @@ transitivity (limn (fun n => apply: bigcup_sub => k/= kn; apply: subset_itvl. by rewrite bnd_simp/= lerD2l ler_nat. apply: congr_lim; apply/funext => -[|n]. - by rewrite addr0 set_itv1 integral_set1 set_itv_ge -?leNgt ?bnd_simp// integral_set0. + by rewrite addr0 set_itvco0 set_itvoo0 !integral_set0. +rewrite integral_itv_bndo_bndc; last first. + apply: measurable_fun_itv_obnd_cbnd; apply: measurable_funS (mG n) => //. + by apply: subset_itvl; rewrite bnd_simp. rewrite integration_by_substitution_decreasing. - rewrite integral_itv_bndo_bndc// ?integral_itv_obnd_cbnd//. + rewrite -setUitv1; last by rewrite bnd_simp ltrDl. @@ -1672,16 +1564,13 @@ rewrite integration_by_substitution_decreasing. - move=> x; rewrite in_itv/= => /andP[ax _]. by apply: cdF; rewrite in_itv/= ax. - exact: (cvgP dFa). -- apply: (cvgP (F^`() (a + n.+1%:R))). - apply: cvg_at_left_filter. - apply: cdF. +- apply: (cvgP (F^`() (a + n.+1%:R))); apply/cvg_at_left_filter/cdF. by rewrite in_itv/= andbT ltr_pwDr. - split. + move=> x; rewrite in_itv/= => /andP[ax _]. by apply: dF; rewrite in_itv/= ax. + exact: cFa. - + apply/cvg_at_left_filter/differentiable_continuous. - apply/derivable1_diffP/dF. + + apply/cvg_at_left_filter/differentiable_continuous/derivable1_diffP/dF. by rewrite in_itv/= andbT ltr_pwDr. - apply/continuous_within_itvP. + by rewrite decrF ?ltr_pwDr ?in_itv ?andbT//= lerDl. @@ -1695,7 +1584,7 @@ Qed. Lemma ge0_integration_by_substitutionNy G a : {within `]-oo, (- a)%R], continuous G} -> - {in `]-oo, (- a)%R], forall x, (0 <= G x)%R} -> + {in `]-oo, (- a)%R[, forall x, (0 <= G x)%R} -> \int[mu]_(x in `]-oo, (- a)%R]) (G x)%:E = \int[mu]_(x in `[a, +oo[) ((G \o -%R) x)%:E. Proof. @@ -1724,7 +1613,7 @@ Lemma increasing_ge0_integration_by_substitutiony F G a : cvg (F^`() x @[x --> +oo%R]) -> derivable_oy_continuous_bnd F a -> F x @[x --> +oo%R] --> +oo%R-> {within `[F a, +oo[, continuous G} -> - {in `[F a, +oo[, forall x, (0 <= G x)%R} -> + {in `]F a, +oo[, forall x, (0 <= G x)%R} -> \int[mu]_(x in `[F a, +oo[) (G x)%:E = \int[mu]_(x in `[a, +oo[) (((G \o F) * F^`()) x)%:E. Proof. @@ -1741,49 +1630,37 @@ rewrite -ge0_integration_by_substitutionNy//; last 2 first. apply/cvg_at_rightNP. apply: cvg_toP; first by apply/cvg_ex; exists (G (F a)). by move/cvg_lim: cGFa => -> //; rewrite fctE opprK. - by move=> x; rewrite in_itv/= lerNr => FaNx; apply: G0; rewrite in_itv/= FaNx. + by move=> x; rewrite in_itv/= ltrNr => FaNx; apply: G0; rewrite in_itv/= FaNx. rewrite (@decreasing_ge0_integration_by_substitutiony (- F)%R); first last. -- move=> y. - rewrite in_itv/= lerNr => FaNy. +- move=> y; rewrite in_itv/= ltrNr => FaNy. by apply: G0; rewrite in_itv/= FaNy. - apply/continuous_within_itvNycP; split => //. - rewrite fctE opprK. - exact/cvg_at_rightNP. + by rewrite fctE opprK; exact/cvg_at_rightNP. - exact/cvgNrNy. - split. - + move=> x ax; apply: derivableN. - exact: dF. + + by move=> x ax; apply: derivableN; exact: dF. + exact: cvgN. - apply/cvg_ex; exists (- l)%R. have /(_ (@filter_filter R _ proper_pinfty_nbhs)) := cvgN F'ool. - apply: cvg_trans. - apply: near_eq_cvg. - near=> z. + apply: cvg_trans; apply: near_eq_cvg; near=> z. rewrite derive1E deriveN -?derive1E//. apply: dF; rewrite in_itv/= andbT. by near: z; apply: nbhs_pinfty_gt; exact: num_real. - apply/cvg_ex; exists (- r)%R. have /(_ (@filter_filter R _ (at_right_proper_filter a))) := cvgN F'ar. - apply: cvg_trans. - apply: near_eq_cvg. - near=> z. + apply: cvg_trans; apply: near_eq_cvg; near=> z. rewrite derive1E deriveN -?derive1E//. by apply: dF; rewrite in_itv/= andbT. - move=> x ax. - rewrite /continuous_at. - rewrite derive1E deriveN -?derive1E; last exact: dF. + rewrite /continuous_at derive1E deriveN -?derive1E; last exact: dF. have /(_ (nbhs_filter x)) := cvgN (cF' x ax). - apply: cvg_trans. - apply: near_eq_cvg. - rewrite near_simpl/=. - near=> z. + apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl/=; near=> z. rewrite derive1E deriveN -?derive1E//. apply: dF. - near: z. - rewrite near_nbhs. + near: z; rewrite near_nbhs. apply: (@open_in_nearW _ _ `]a, +oo[). + exact: interval_open. - + by move=> ?; rewrite inE/=. + + by move=> ?; rewrite inE. + by rewrite inE. - by move=> x y ax ay yx; rewrite ltrN2; exact: incrF. have mGF : measurable_fun `]a, +oo[ (G \o F). @@ -1793,19 +1670,15 @@ have mGF : measurable_fun `]a, +oo[ (G \o F). - apply: open_continuous_measurable_fun; first exact: interval_open. by move=> x; rewrite inE/= => Fax; exact: cG. - apply: subspace_continuous_measurable_fun => //. - apply: derivable_within_continuous => x. - exact: dF. + by apply: derivable_within_continuous => x; exact: dF. have mF' : measurable_fun `]a, +oo[ (- F)%R^`(). apply: open_continuous_measurable_fun; first exact: interval_open. move=> x; rewrite inE/= => ax. - rewrite /continuous_at. - rewrite derive1E deriveN; last exact: dF. + rewrite /continuous_at derive1E deriveN; last exact: dF. rewrite -derive1E. under eq_cvg do rewrite -(opprK ((- F)%R^`() _)); apply: cvgN. apply: cvg_trans (cF' x ax). - apply: near_eq_cvg => /=. - rewrite near_simpl. - near=> z. + apply: near_eq_cvg => /=; rewrite near_simpl; near=> z. rewrite !derive1E deriveN ?opprK//. apply: dF. near: z. @@ -1815,17 +1688,16 @@ rewrite -!integral_itv_obnd_cbnd; last 2 first. apply: measurable_funM => //. apply: open_continuous_measurable_fun; first exact: interval_open. by move=> x; rewrite inE/=; exact: cF'. - apply: measurable_funM. - apply: (measurable_comp (measurable_itv `]-oo, (- F a)%R[)). - move=> _/=[x + <-]. - rewrite !in_itv/= andbT=> ax. - by rewrite ltrN2 incrF// ?in_itv/= ?andbT// ltW. - apply: open_continuous_measurable_fun; first exact: interval_open. - by move=> x; rewrite inE/=; exact: cGN. - apply: measurableT_comp => //. + apply: measurable_funM; last exact: measurableT_comp. + apply: (measurable_comp (measurable_itv `]-oo, (- F a)%R[)). + - move=> _ /= [x + <-]. + rewrite !in_itv/= andbT=> ax. + by rewrite ltrN2 incrF// ?in_itv/= ?andbT// ltW. + - apply: open_continuous_measurable_fun; first exact: interval_open. + by move=> x; rewrite inE/=; exact: cGN. + - apply: measurableT_comp => //. apply: subspace_continuous_measurable_fun => //. exact: derivable_within_continuous. - exact: measurableT_comp. apply: eq_integral => x/=; rewrite inE/= => ax. congr EFin. rewrite !fctE/= opprK; congr (_ * _)%R. @@ -1833,81 +1705,195 @@ rewrite !derive1E deriveN ?opprK//. exact: dF. Unshelve. all: end_near. Qed. -(* move to PR *) -Lemma incr_derive1_ge0 (f : R -> R) (D : set R) (x : R): - {in (interior D) : set R, forall x : R, derivable f x 1%R} -> - {in D &, {homo f : x y / (x < y)%R}} -> - (interior D) x -> (0 <= f^`() x)%R. -Proof. -move=> df incrf Dx. -rewrite -[leRHS]opprK oppr_ge0. -have dfx : derivable f x 1 by apply: df; rewrite inE. -rewrite derive1E -deriveN// -derive1E. -apply: (@decr_derive1_le0 _ _ D). -- move=> y Dy. - apply: derivableN. - exact: df. -- move=> y z Dy Dz yz. - rewrite ltrN2. - exact: incrf. -- exact: Dx. -Qed. - -Lemma incr_derive1_ge0_itv (f : R^o -> R^o) (z : R) (x0 x1 : R) (b0 b1 : bool) : - {in `]x0, x1[, forall x : R, derivable f x 1%R} -> - {in (Interval (BSide b0 x0) (BSide b1 x1)) &, {homo f : x y / (x < y)%R}} -> - z \in `]x0, x1[ -> (0 <= f^`() z)%R. -Proof. -have [x10|x01] := leP x1 x0. - move=> _ _. - by move/lt_in_itv; rewrite bnd_simp le_gtF. -set itv := Interval (BSide b0 x0) (BSide b1 x1). -move=> df incrf xx0x1. -apply: (@incr_derive1_ge0 _ [set` itv]). - rewrite itv_interior//. - by move=> ?; rewrite inE/=; apply: df. - move=> ? ?; rewrite !inE/=; apply: incrf. -by rewrite itv_interior/=. -Qed. - -(* PR? *) -Lemma interiorT {T : topologicalType} : interior (@setT T) = setT. -Proof. -rewrite eqEsubset; split; first exact: interior_subset. -rewrite -open_subsetE//. -exact: openT. -Qed. - -Lemma derivable_within_continuousT (f : R -> R) : - (forall x, derivable f x 1) -> continuous f. -Proof. -move=> df. -apply/continuous_subspace_setT. -rewrite -(@RhullK _ setT); last by rewrite inE. -apply: derivable_within_continuous. -move=> x _. -exact: df. -Qed. - -Definition derivable_yo_continuous_bnd {R' : numFieldType} - (f : R' -> R') (x : R') := - {in `]-oo, x[, forall x, derivable f x 1} /\ f @ x^'- --> f x. - Lemma increasing_ge0_integration_by_substitutionNy F G b : {in `]-oo, b] &, {homo F : x y / (x < y)%R}} -> {in `]-oo, b[, continuous F^`()} -> cvg (F^`() x @[x --> -oo%R]) -> - cvg (F^`() x @[x --> b^'-]) -> - derivable_yo_continuous_bnd F b -> F x @[x --> -oo%R] --> -oo%R-> + F^`() x @[x --> b^'-] --> F^`() b (* TODO: try with cvg (F^`() x @[x --> b^'-]) *) -> + derivable_Nyo_continuous_bnd F b -> F x @[x --> -oo%R] --> -oo%R-> {within `]-oo, F b], continuous G} -> - {in `]-oo, F b], forall x, (0 <= G x)%R} -> + {in `]-oo, F b[, forall x, (0 <= G x)%R} -> \int[mu]_(x in `]-oo, F b]) (G x)%:E = \int[mu]_(x in `]-oo, b]) (((G \o F) * F^`()) x)%:E. Proof. -move=> ndF cdF cvgFNy cvgFb [dF Fb] FNyNy cG G0. -Admitted. +move=> ndF cdF cvgFNy cvgFb [dF Fb] FNyNy. +move=> /continuous_within_itvNycP[cG cGFb] G0. +rewrite -(@opprK _ (F b)). +rewrite (@ge0_integration_by_substitutionNy _ (- F b)%R); last 2 first. +- apply/continuous_within_itvNycP; split; last by rewrite opprK. + by rewrite opprK => x xFb; exact: cG. +- by rewrite opprK. +rewrite -[in LHS](@opprK _ b). +have dFN z : (- z < b)%R -> derivable F (- z) 1. + by move=> zb; apply: dF; rewrite in_itv. +have dFcompN z : (- z < b)%R -> derivable (F \o -%R) z 1. + move=> zb; apply/diff_derivable/differentiable_comp => //. + by apply/derivable1_diffP; exact: dFN. +rewrite (@increasing_ge0_integration_by_substitutiony (\- (F \o -%R))%R); last 8 first. +- move=> x y; rewrite !in_itv/= !andbT => xb yb. + rewrite -ltrN2 => /ndF. + by rewrite /= ltrN2; apply; rewrite !in_itv/= lerNl//. +- move=> x; rewrite in_itv/= andbT ltrNl => xb. + have := cdF (- x)%R. + rewrite in_itv/= => /(_ xb) NxF. + rewrite /continuous_at in NxF *. + rewrite derive1N/=; last exact: dFcompN. + rewrite [X in _ --> X](_ : _ = F^`() (- x))%R; last first. + rewrite derive1_comp; last 2 first. + exact: derivable_opp. + exact: dFN. + rewrite [X in (_ * X)%R]derive1E. + rewrite deriveN; last exact: derivable_id. + by rewrite derive_id mulrN1 opprK. + move/(@cvg_compNP _ _ (F^`()) x (F^`() (- x))) : NxF. + apply: cvg_trans. + apply: near_eq_cvg; rewrite near_simpl; near=> z. + rewrite derive1N; last first. + apply: dFcompN. + by near: z; exact: nbhs_lt_transN. + rewrite [in RHS]derive1_comp; last 2 first. + exact: derivable_opp. + apply: dFN. + by near: z; exact: nbhs_lt_transN. + rewrite derive1N; last exact: derivable_id. + by rewrite derive1_id mulrN1 opprK. +- move: cvgFb => /cvg_at_leftNP cvgFbl. + apply/cvg_ex; exists (F^`() b)%R. + apply: cvg_trans cvgFbl. + apply: near_eq_cvg; near=> z. + rewrite [RHS]derive1N; last first. + apply: dFcompN. + rewrite ltrNl. + by near: z; exact: nbhs_right_gt. + rewrite fctE derive1_comp; last 2 first. + exact: derivable_id. + apply: dFN; rewrite ltrNl. + by near: z; exact: nbhs_right_gt. + rewrite derive1_id mulr1 [in RHS]derive1_comp; last 2 first. + exact: derivable_opp. + apply: dFN; rewrite ltrNl. + by near: z; exact: nbhs_right_gt. + rewrite derive1N; last exact: derivable_id. + by rewrite derive1_id mulrN1 opprK. +- move/cvg_ex : cvgFNy => [/= l cvgFNy]. + apply/cvg_ex; exists l. + move/cvgNy_compNP : cvgFNy. + apply: cvg_trans. + apply: near_eq_cvg; near=> x. + rewrite derive1N; last first. + apply: diff_derivable; apply: differentiable_comp; apply/derivable1_diffP. + exact: derivable_opp. + apply: dFN; rewrite ltrNl. + by near: x; apply: nbhs_pinfty_gt; rewrite num_real. + rewrite /= [in RHS]derive1_comp; last 2 first. + exact: derivable_opp. + apply: dFN; rewrite ltrNl. + by near: x; apply: nbhs_pinfty_gt; rewrite num_real. + rewrite derive1N; last exact: derivable_id. + by rewrite derive1_id mulrN1 opprK. +- split => /=. + move=> z; rewrite in_itv/= andbT => bz. + apply: diff_derivable; apply: differentiable_comp; apply/derivable1_diffP. + apply: diff_derivable; apply: differentiable_comp; apply/derivable1_diffP. + exact: derivable_opp. + by apply: dFN; rewrite ltrNl. + exact: derivable_opp. + rewrite opprK. + apply/cvg_at_rightNP. + rewrite opprK. + apply: cvgN. + apply: cvg_trans Fb. + apply: near_eq_cvg; near=> x. + by rewrite /= opprK. +- move/cvgNy_compNP in FNyNy. + apply/cvgNrNy. + rewrite [X in X @ _ --> _](_ : _ = F \o -%R)//. + by apply: funext => r/=; rewrite fctE opprK. +- apply/continuous_within_itvcyP; split. + move=> x; rewrite in_itv/= opprK andbT => Fbx. + apply: continuous_comp; first exact: opp_continuous. + by apply: cG; rewrite in_itv/= ltrNl. + by rewrite /= !opprK; exact/cvg_at_leftNP. +- move=> z; rewrite in_itv/= opprK andbT => Fbz. + by apply: G0; rewrite in_itv/= ltrNl. +rewrite -[in RHS](opprK b) ge0_integration_by_substitutionNy; last 2 first. + apply/continuous_within_itvNycP; split => //. + move=> z; rewrite in_itv/= opprK => zb. + apply: continuousM; last by apply: cdF; rewrite in_itv. + apply: continuous_comp. + move/derivable_within_continuous: dF. + rewrite continuous_open_subspace; last exact: interval_open. + by apply; rewrite inE/= in_itv. + by apply: cG; rewrite in_itv/= ndF ?in_itv//= ltW. + rewrite opprK; apply: cvgM => //. + exact: (increasing_cvg_at_left_comp _ ndF). + rewrite opprK => x. + rewrite in_itv/= => xb. + rewrite mulr_ge0//. + by apply: G0; rewrite in_itv/= ndF ?in_itv//= ltW. + apply: (@incr_derive1_ge0_itvNy _ _ false b). + - move=> z; rewrite inE/= in_itv/= => zb. + by apply: dF; rewrite in_itv. + - exact: ndF. + - by rewrite in_itv. +have mG : measurable_fun `]-oo, (F b)[ G. + by apply: open_continuous_measurable_fun => // x; rewrite inE => /cG. +have mF : measurable_fun `]-oo, b[ F. + apply: open_continuous_measurable_fun => // x xNyb. + move/derivable_within_continuous : dF. + rewrite continuous_open_subspace; last exact: interval_open. + exact. +rewrite -[RHS]integral_itv_obnd_cbnd; last first. + apply: (@measurable_comp _ _ _ _ _ _ `]-oo, b]) => //=. + rewrite opp_itv_bndy opprK/=. + by apply: subset_itvl; rewrite bnd_simp. + apply: measurable_fun_itv_bndo_bndc; apply: measurable_funM => //. + - apply: (@measurable_comp _ _ _ _ _ _ `]-oo, F b[) => //=. + move=> x/= [r]; rewrite in_itv/= => rb <-{x}. + by rewrite in_itv/= ndF ?in_itv//= ltW. + - apply: open_continuous_measurable_fun; first by []. + by move=> x/=; rewrite inE => /cdF. +rewrite -[LHS]integral_itv_obnd_cbnd; last first. + apply: measurable_funM. + apply: (@measurable_comp _ _ _ _ _ _ `](- F b)%R, +oo[) => //=. + - move=> x/= [r]; rewrite in_itv/= andbT => br <-{x}. + by rewrite in_itv/= andbT ltrN2 ndF ?in_itv//= 1?ltrNl// lerNl ltW. + - apply: (@measurable_comp _ _ _ _ _ _ `]-oo, F b[) => //=. + by rewrite opp_itv_bndy//= opprK. + - apply: measurableT_comp => //. + apply: (@measurable_comp _ _ _ _ _ _ `]-oo, b[) => //=. + by rewrite opp_itv_bndy opprK/=. + have : {in `](- b)%R, +oo[%classic, F^`() \o -%R =1 (\- (F \o -%R))%R^`()}. + move=> z; rewrite inE/= in_itv/= andbT => zb. + rewrite derive1N; last first. + apply: diff_derivable; apply: differentiable_comp; apply/derivable1_diffP. + exact: derivable_opp. + by apply: dFN; rewrite ltrNl. + rewrite [in RHS]derive1_comp; last 2 first. + exact: derivable_opp. + by apply: dFN; rewrite ltrNl. + rewrite derive1N; last exact: derivable_id. + by rewrite derive1_id mulrN1 opprK. + move/eq_measurable_fun; apply. + apply: (@measurable_comp _ _ _ _ _ _ `]-oo, b[) => //=. + by rewrite opp_itv_bndy opprK. + apply: open_continuous_measurable_fun; first by []. + by move=> x; rewrite inE => /cdF. +apply: eq_integral => /= z; rewrite inE/= in_itv/= andbT => bz. +congr EFin. +rewrite !fctE/= opprK; congr *%R. +rewrite derive1N; last first. + apply: diff_derivable; apply: differentiable_comp; apply/derivable1_diffP. + exact: derivable_opp. + by apply: dFN; rewrite ltrNl. +rewrite derive1_comp/=; last 2 first. + exact: derivable_opp. + by apply: dFN; rewrite ltrNl. +rewrite derive1N; last exact: derivable_id. +by rewrite derive1_id mulrN1 opprK. +Unshelve. all: end_near. Qed. -Lemma increasing_ge0_integration_by_substitution F G a : +Lemma increasing_ge0_integration_by_substitutionT F G a : {homo F : x y / (x < y)%R} -> continuous F^`() -> cvg (F^`() x @[x --> -oo%R]) -> @@ -1916,64 +1902,58 @@ Lemma increasing_ge0_integration_by_substitution F G a : F x @[x --> -oo%R] --> -oo%R -> F x @[x --> +oo%R] --> +oo%R -> continuous G -> - (forall x, (0 <= G x)%R) -> + (forall x, 0 <= G x)%R -> \int[mu]_x (G x)%:E = \int[mu]_x (((G \o F) * F^`()) x)%:E. Proof. move=> ndF cdF cvgFNy cvgFy dF FNyNy Fyy cG G0. have mGFF' : measurable_fun setT ((G \o F) * F^`())%R. apply: measurable_funM. - apply: measurableT_comp. - exact: continuous_measurable_fun. - apply: continuous_measurable_fun. - exact: derivable_within_continuousT. + apply: measurableT_comp; first exact: continuous_measurable_fun. + apply: continuous_measurable_fun => x. + exact/differentiable_continuous/derivable1_diffP/dF. exact: continuous_measurable_fun cdF. -rewrite -{2}setC0 -(set_itvoc0 0%R) setCitv/=. -rewrite ge0_integral_setU//=; first last. -- rewrite -(@RhullK _ `]-oo, 0%R]%classic); last first. - by rewrite inE/=; apply: interval_is_interval. - rewrite -(@RhullK _ `]0%R, +oo[%classic)//; last first. - by rewrite inE/=; apply: interval_is_interval. - apply: disj_itv_Rhull; first last. - 1, 2: apply: interval_is_interval. - rewrite eqEsubset; split => x//= []; rewrite !in_itv/= andbT => x0. - move/(le_lt_trans x0). - by rewrite ltxx. -- move=> x _. - apply: mulr_ge0; last first. - apply: (@incr_derive1_ge0 _ setT). - - by move=> ? _; apply: dF. - - by move=> ? ? _ _; apply: ndF. - - by rewrite interiorT. -- exact: G0. -- apply/measurable_EFinP. - rewrite -setCitvr setvU. - exact: mGFF'. +have cF : continuous F. + by move=> x; exact/differentiable_continuous/derivable1_diffP/dF. +rewrite -{2}setC0 -(set_itvoc0 0%R) setCitv/= ge0_integral_setU//=; first last. + rewrite disj_set2E; apply/eqP; rewrite -subset0 => x []/= /[!in_itv]/=. + by rewrite leNgt andbT => /negP. +- move=> x _; apply: mulr_ge0; first exact: G0. + apply: (@incr_derive1_ge0 _ _ setT). + + by move=> ? _; exact: dF. + + by move=> ? ? _ _; exact: ndF. + + by rewrite interiorT. +- by apply/measurable_EFinP; rewrite -setCitvr setvU; exact: mGFF'. rewrite integral_itv_obnd_cbnd; last by apply: measurable_funTS; apply: mGFF'. rewrite -(increasing_ge0_integration_by_substitutiony _ _ _ cvgFy); first last. -- admit. -- admit. -- admit. -- admit. -- admit. -- admit. -- admit. +- by move=> x; rewrite in_itv/= andbT => F0x; exact: G0. +- exact: continuous_subspaceT. +- exact: Fyy. +- split=> [x _|]; first exact: dF. + by apply: cvg_at_right_filter; exact: cF. +- apply/cvg_ex; exists (F^`() 0). + by apply: cvg_at_right_filter; exact: cdF. +- by move=> x _; exact: cdF. +- by move=> x y _ _; exact: ndF. rewrite -(increasing_ge0_integration_by_substitutionNy _ _ cvgFNy); first last. -- admit. -- admit. -- admit. -- admit. -- admit. -- admit. -- admit. +- by move=> x _; exact: G0. +- exact: continuous_subspaceT. +- exact: FNyNy. +- split=> [x _|]; first apply: dF. +- by apply: cvg_at_left_filter; exact: cF. +- by apply: cvg_at_left_filter; exact: cdF. +- by move=> x _; exact: cdF. +- by move=> x y _ _; exact: ndF. rewrite -integral_itv_obnd_cbnd; last first. - admit. + by apply: measurable_funTS; exact: continuous_measurable_fun. rewrite -ge0_integral_setU//=; first last. -- admit. -- admit. -- admit. +- rewrite disj_set2E; apply/eqP; rewrite -subset0 => x/=. + by rewrite !in_itv/= andbT ltNge => -[? /negP]. +- by move=> x _; rewrite lee_fin; exact: G0. +- apply/measurable_EFinP; apply: measurable_funTS. + exact: continuous_measurable_fun. by rewrite -setCitvr setvU. -Abort. +Qed. End integration_by_substitution. @@ -1982,15 +1962,13 @@ Context {R : realType}. Let mu := @lebesgue_measure R. Local Open Scope ereal_scope. -Lemma ge0_integralT_even (f : R -> R) : (forall x, 0 <= f x)%R -> - continuous f -> - f =1 f \o -%R -> +Lemma ge0_symfun_integralT (f : R -> R) : (forall x, 0 <= f x)%R -> + continuous f -> f =1 f \o -%R -> \int[mu]_x (f x)%:E = 2%:E * \int[mu]_(x in [set x | (0 <= x)%R]) (f x)%:E. Proof. move=> f0 cf evenf. have mf : measurable_fun [set: R] f by exact: continuous_measurable_fun. -have mposnums : measurable [set x : R | 0 <= x]%R. - by rewrite -set_itv_c_infty. +have mposnums : measurable [set x : R | 0 <= x]%R by rewrite -set_itv_c_infty. rewrite -(setUv [set x : R | 0 <= x]%R) ge0_integral_setU//= ; last 4 first. exact: measurableC. by apply/measurable_EFinP; rewrite setUv. @@ -2000,8 +1978,7 @@ rewrite mule_natl mule2n; congr +%E. rewrite -set_itv_c_infty// setCitvr. rewrite integral_itv_bndo_bndc; last exact: measurable_funTS. rewrite -{1}oppr0 ge0_integration_by_substitutionNy//. -- apply: eq_integral => /= x. - rewrite inE/= in_itv/= andbT => x0. +- apply: eq_integral => /= x; rewrite inE/= in_itv/= andbT => x0. by rewrite (evenf x). - exact: continuous_subspaceT. Qed. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 2346a39fc..e96ffd65c 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -3486,7 +3486,7 @@ apply/eqP; rewrite eq_le; apply/andP; split; last first. - by apply/measurable_EFinP; exact: measurable_funS mf. - by move=> ? _; rewrite lee_fin f0. - exact: subset_itvl. -rewrite itv_bnd_infty_bigcup0S. +rewrite itv0y_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. @@ -4420,11 +4420,11 @@ have ? : \int[mu]_(x in \bigcup_i F i) g x \is a fin_num. exact: measurable_int fi. transitivity (\int[mu]_(x in \bigcup_i F i) g^\+ x - \int[mu]_(x in \bigcup_i F i) g^\- x)%E. - rewrite -integralB; last 3 first. - - exact: bigcupT_measurable. - - by apply: integrable_funepos => //; exact: bigcupT_measurable. - - by apply: integrable_funeneg => //; exact: bigcupT_measurable. - by apply: eq_integral => t Ft; rewrite [in LHS](funeposneg g). + rewrite -integralB. + - by apply: eq_integral => t Ft; rewrite [in LHS](funeposneg g). + - exact: bigcupT_measurable. + - by apply: integrable_funepos => //; exact: bigcupT_measurable. + - by apply: integrable_funeneg => //; exact: bigcupT_measurable. transitivity (\sum_(i // i; rewrite [RHS]integralE. @@ -4433,8 +4433,7 @@ transitivity ((\sum_(i n _; exact: integral_ge0. rewrite [X in _ - X]nneseries_esum; last by move=> n _; exact: integral_ge0. rewrite set_true -esumB//=; last 4 first. @@ -6882,8 +6881,7 @@ have [xy|yx _|-> _] := ltgtP x y; last 2 first. move=> mf. transitivity (\int[mu]_(z in [set` Interval (BSide b0 x) (BLeft y)]) (f z)%:E). case: b1 => //; rewrite -integral_itv_bndo_bndc//. - case: b0 => //. - exact: measurable_fun_itv_co mf. + by case: b0 => //; exact: measurable_fun_itv_obnd_cbnd. by case: b0 => //; rewrite -integral_itv_obnd_cbnd. Qed. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index a22fbb1a6..2f597c922 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -697,7 +697,7 @@ Proof. by apply/cvg_lim => //; apply/cvgenyP. Qed. Let lebesgue_measure_itv_bnd_infty x (a : R) : lebesgue_measure ([set` Interval (BSide x a) +oo%O] : set R) = +oo%E. Proof. -rewrite itv_bnd_infty_bigcup; transitivity (limn (lebesgue_measure \o +rewrite itv_bndy_bigcup_BRight; transitivity (limn (lebesgue_measure \o (fun k => [set` Interval (BSide x a) (BRight (a + k%:R))] : set R))). apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. + by move=> k; exact: measurable_itv. @@ -713,7 +713,7 @@ Qed. Let lebesgue_measure_itv_infty_bnd y (b : R) : lebesgue_measure ([set` Interval -oo%O (BSide y b)] : set R) = +oo%E. Proof. -rewrite itv_infty_bnd_bigcup; transitivity (limn (lebesgue_measure \o +rewrite itvNy_bnd_bigcup_BLeft; transitivity (limn (lebesgue_measure \o (fun k => [set` Interval (BLeft (b - k%:R)) (BSide y b)] : set R))). apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu. + by move=> k; exact: measurable_itv. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index cf94f71f6..a36e041a9 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -228,50 +228,75 @@ case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge. Qed. #[local] Hint Resolve measurable_itv : core. +Lemma measurable_fun_itv_bndo_bndc (a : itv_bound R) (b : R) + (f : R -> R) : + measurable_fun [set` Interval a (BLeft b)] f -> + measurable_fun [set` Interval a (BRight b)] f. +Proof. +have [ab|ab] := leP a (BLeft b). +- move: a => [a0 a|[|//]] in ab *; + move=> mf; rewrite -setUitv1//; apply/measurable_funU => //; + by split => //; exact: measurable_fun_set1. +- move: a => [[|] a|[|]//] in ab *; rewrite bnd_simp in ab. + + move=> _; rewrite set_itv_ge// ?bnd_simp -?ltNge//. + exact: measurable_fun_set0. + + move=> _; rewrite set_itv_ge// ?bnd_simp -?leNgt//. + exact: measurable_fun_set0. +Qed. + +Lemma measurable_fun_itv_obnd_cbnd (a : R) (b : itv_bound R) + (f : R -> R) : + measurable_fun [set` Interval (BRight a) b] f -> + measurable_fun [set` Interval (BLeft a) b] f. +Proof. +have [ab|ab] := leP (BRight a) b. +- move: b => [[|] b|[//|]] in ab *; + move=> mf; rewrite -setU1itv//; apply/measurable_funU => //; + by split => //; exact: measurable_fun_set1. +- move: b => [[|] b|[|//]] in ab *; rewrite bnd_simp in ab. + + move=> _; rewrite set_itv_ge// ?bnd_simp -?leNgt//. + exact: measurable_fun_set0. + + move=> _; rewrite set_itv_ge// ?bnd_simp -?ltNge//. + exact: measurable_fun_set0. + + by move=> _; rewrite set_itv_ge//=; exact: measurable_fun_set0. +Qed. + +#[deprecated(since="mathcomp-analysis 1.9.0", note="use `measurable_fun_itv_obnd_cbnd` instead")] Lemma measurable_fun_itv_co (x y : R) b0 b1 (f : R -> R) : measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> measurable_fun `[x, y[ f. Proof. -have [xy|yx _] := ltP x y; last first. - by rewrite set_itv_ge -?leNgt ?bnd_simp//; exact: measurable_fun_set0. -move: b0 b1 => [|] [|] // mf. -- apply: measurable_funS mf => //; exact: subset_itv_co_cc. -- rewrite -setU1itv//= measurable_funU//; split => //. - exact: measurable_fun_set1. -- rewrite -setU1itv//= measurable_funU//; split. - exact: measurable_fun_set1. - by apply: measurable_funS mf => //; exact: subset_itv_oo_oc. +move: b0 b1 => [|] [|]//. +- by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp. +- exact: measurable_fun_itv_obnd_cbnd. +- move=> mf. + have : measurable_fun `[x, y] f by exact: measurable_fun_itv_obnd_cbnd. + by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp. Qed. +#[deprecated(since="mathcomp-analysis 1.9.0", note="use `measurable_fun_itv_bndo_bndc` instead")] Lemma measurable_fun_itv_oc (x y : R) b0 b1 (f : R -> R) : measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> measurable_fun `]x, y] f. Proof. -have [xy|yx _] := ltP x y; last first. - by rewrite set_itv_ge -?leNgt ?bnd_simp//; exact: measurable_fun_set0. -move: b0 b1 => [|] [|] // mf. -- rewrite -setUitv1//= measurable_funU//; split. - by apply: measurable_funS mf => //; exact: subset_itv_oo_co. - exact: measurable_fun_set1. -- by apply: measurable_funS mf => //; exact: subset_itv_oc_cc. -- rewrite -setUitv1//= measurable_funU//; split => //. - exact: measurable_fun_set1. +move: b0 b1 => [|] [|]//. +- move=> mf. + have : measurable_fun `[x, y] f by exact: measurable_fun_itv_bndo_bndc. + by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp. +- by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp. +- exact: measurable_fun_itv_bndo_bndc. Qed. Lemma measurable_fun_itv_cc (x y : R) b0 b1 (f : R -> R) : measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> measurable_fun `[x, y] f. Proof. -move=> mf. -have [xy|] := ltP x y; last first. - rewrite le_eqVlt => /predU1P[->|ba]. - by rewrite set_itv1; exact: measurable_fun_set1. - rewrite set_itv_ge//; first exact: measurable_fun_set0. - by rewrite -leNgt bnd_simp. -rewrite -setUitv1//=; last by rewrite bnd_simp ltW. - rewrite measurable_funU//; split => //. - exact: measurable_fun_itv_co mf. -exact: measurable_fun_set1. +move: b0 b1 => [|] [|]//. +- exact: measurable_fun_itv_bndo_bndc. +- move=> mf. + have : measurable_fun `[x, y[ f by exact: measurable_fun_itv_obnd_cbnd. + exact: measurable_fun_itv_bndo_bndc. +- exact: measurable_fun_itv_obnd_cbnd. Qed. HB.instance Definition _ := (ereal_isMeasurable (R.-ocitv.-measurable)). diff --git a/theories/normedtype.v b/theories/normedtype.v index 69e3f53a7..73bd64e1d 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -214,6 +214,11 @@ rewrite predeqE => A; split=> //= -[] e e_gt0 xeA; exists e => //= y /=. by rewrite -opprD normrN => ?; rewrite -[y]opprK; apply: xeA; rewrite /= opprK. Qed. +Lemma cvg_compNP {T : topologicalType} {R : numFieldType} (f : R -> T) (a : R) + (l : T) : + (f \o -%R) x @[x --> a] --> l <-> f x @[x --> (- a)] --> l. +Proof. by rewrite nbhsN. Qed. + Lemma nbhsNimage (R : numFieldType) (x : R) : nbhs (- x) = [set -%R @` A | A in nbhs x]. Proof. @@ -660,6 +665,76 @@ rewrite pmulrn ceil_le_int// [ceil _]intEsign. by rewrite le_gtF ?expr0 ?mul1r ?lez_nat -?ceil_ge0//; near: n; apply: Foo. Unshelve. all: by end_near. Qed. +Section monotonic_itv_bigcup. +Context {R : realType}. +Implicit Types (F : R -> R) (a : R). + +Lemma decreasing_itvNyo_bigcup F a : + {in `[a, +oo[ &, {homo F : x y /~ x < y}} -> + F x @[x --> +oo] --> -oo -> + (`]-oo, F a[ = \bigcup_i `]F (a + i.+1%:R), F a[)%classic. +Proof. +move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split. +- move=> y/= [n _]/=; rewrite in_itv/= => /andP[Fany yFa]. + have [i iFan] : exists i, F (a + i.+1%:R) < F a - n%:R. + move/cvgrNy_lt : nyF. + move/(_ (F a - n%:R)) => [z [zreal zFan]]. + exists `|ceil (z - a)|%N. + rewrite zFan// -ltrBlDl (le_lt_trans (le_ceil _))//. + by rewrite (le_lt_trans (ler_norm _))// -natr1 -intr_norm ltrDl. + by exists i => //=; rewrite in_itv/= yFa (lt_le_trans _ Fany). +- move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa]. + exists `| ceil (F (a + n.+1%:R) - F a)%R |.+1 => //=. + rewrite in_itv/= zFa andbT lerBlDr -lerBlDl (le_trans _ (abs_ceil_ge _))//. + by rewrite ler_normr orbC opprB lerB// ltW. +Qed. + +Lemma decreasing_itvoo_bigcup F a n : + {in `[a, +oo[ &, {homo F : x y /~ x < y}} -> + (`]F (a + n%:R), F a[ = \bigcup_(i < n) `]F (a + i.+1%:R), F a[)%classic. +Proof. +move=> decrF; rewrite eqEsubset; split. +- move: n => [|n]; first by rewrite addr0 set_itvoo0. + by apply: (@bigcup_sup _ _ n) => /=. +- apply: bigcup_sub => k/= kn; apply: subset_itvr; rewrite bnd_simp. + move: kn; rewrite leq_eqVlt => /predU1P[<-//|kn]. + by rewrite ltW// decrF ?in_itv/= ?andbT ?lerDl//= ltrD2l ltr_nat. +Qed. + +Lemma increasing_itvNyo_bigcup F a : + {in `]-oo, a] &, {homo F : x y / x < y}} -> + F x @[x --> -oo] --> -oo -> + (`]-oo, F a] = \bigcup_i `]F (a - i.+1%:R), F a])%classic. +Proof. +move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split. +- move=> y/= [n _]/=; rewrite in_itv/= => /andP[Fany yFa]. + have [i iFan] : exists i, F (a - i.+1%:R) < F a - n%:R. + move/cvgrNy_lt : nyF. + move/(_ (F a - n%:R)) => [z [zreal zFan]]. + exists `|ceil (a - z)|%N. + rewrite zFan// ltrBlDr -ltrBlDl (le_lt_trans (le_ceil _))//. + by rewrite (le_lt_trans (ler_norm _))// -natr1 -intr_norm ltrDl. + by exists i => //=; rewrite in_itv/= yFa andbT (lt_le_trans _ Fany). +- move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa]. + exists `| ceil (F (a - n.+1%:R) - F a)%R |.+1 => //=. + rewrite in_itv/= zFa andbT lerBlDr -lerBlDl (le_trans _ (abs_ceil_ge _))//. + by rewrite ler_normr orbC opprB lerB// ltW. +Qed. + +Lemma increasing_itvoc_bigcup F a n : + {in `]-oo, a] &, {homo F : x y / x < y}} -> + (`]F (a - n%:R), F a] = \bigcup_(i < n) `]F (a - i.+1%:R), F a])%classic. +Proof. +move=> incrF; rewrite eqEsubset; split. +- move: n => [|n]; first by rewrite subr0 set_itvoc0. + by apply: (@bigcup_sup _ _ n) => /=. +- apply: bigcup_sub => k/= kn; apply: subset_itvr; rewrite bnd_simp. + move: kn; rewrite leq_eqVlt => /predU1P[<-//|kn]. + by rewrite ltW// incrF ?in_itv/= ?andbT ?gerBl ?ler_ltB ?ltr_nat. +Qed. + +End monotonic_itv_bigcup. + Section ecvg_infty_numField. Local Open Scope ereal_scope. diff --git a/theories/realfun.v b/theories/realfun.v index f82995936..50ce089fb 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -23,6 +23,10 @@ From mathcomp Require Import sequences real_interval. (* derivable_oo_continuous_bnd f x y == f is derivable in `]x, y[ and *) (* continuous up to the boundary, i.e., *) (* f @ x^'+ --> f x and f @ y^'- --> f y *) +(* derivable_oy_continuous_bnd f x == f is derivable in `]x, +oo[ and *) +(* f @ x^'+ --> f x *) +(* derivable_Nyo_continuous_bnd f x == f is derivable in `]-oo, x[ and *) +(* f @ x^'- --> f x *) (* *) (* itv_partition a b s == s is a partition of the interval `[a, b] *) (* itv_partitionL s c == the left side of splitting a partition at c *) @@ -1129,6 +1133,12 @@ apply/differentiable_continuous; rewrite -derivable1_diffP. by apply: fxy; rewrite in_itv/= xz zy. Qed. +Definition derivable_Nyo_continuous_bnd (f : R -> V) (x : R) := + {in `]-oo, x[, forall x, derivable f x 1} /\ f @ x^'- --> f x. + +Definition derivable_oy_continuous_bnd (f : R -> V) (x : R) := + {in `]x, +oo[, forall x, derivable f x 1} /\ f @ x^'+ --> f x. + End derivable_oo_continuous_bnd. Section real_inverse_functions. diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index 56e85fa81..3921c35aa 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -112,6 +112,23 @@ exists x => // z /=; rewrite sub0r normrN. by apply: le_lt_trans; rewrite ler_norm. Qed. +Lemma nbhs_lt_trans {R : realType} (x a : R) : x < a -> + \forall y \near nbhs x, y < a. +Proof. +move=> xb; exists ((a - x) / 2) => /=; first by rewrite divr_gt0// subr_gt0. +move=> r/=; rewrite ltr_pdivlMr// ltrBrDr; apply: le_lt_trans. +by rewrite -lerBlDr -normrN opprB (le_trans (ler_norm _))// ler_peMr// ler1n. +Qed. + +Lemma nbhs_lt_transN {R : realType} (x a : R) : + - x < a -> \forall y \near nbhs x, - y < a. +Proof. +move=> xb; exists ((a + x) / 2) => /=. + by rewrite divr_gt0// -(opprK x) subr_gt0. +move=> r/=; rewrite ltr_pdivlMr// -ltrBlDr; apply: le_lt_trans. +by rewrite -lerBlDr opprK addrC (le_trans (ler_norm _))// ler_peMr// ler1n. +Qed. + Global Instance Proper_dnbhs_regular_numFieldType (R : numFieldType) (x : R^o) : ProperFilter x^'. Proof. From 7cd52303fa92c12e354d163c89e326020365f085 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 13 Feb 2025 00:18:27 +0900 Subject: [PATCH 06/11] rm deprecated --- CHANGELOG_UNRELEASED.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a93fdb2be..e81bfd2ed 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -486,6 +486,14 @@ `__deprecated__cvg_gt_ge`, `__deprecated__cvg_lt_le`, `__deprecated__linear_bounded0 ` (deprecated since 0.6.0) +- in `normedtype.v`: + + notations `cvg_distP`, `cvg_distW`, `continuous_cvg_dist`, `cvg_dist2P`, + `cvg_gt_ge`, `cvg_lt_le_`, `linear_bounded0` + (were deprecated since 0.6.0) + + lemmas `__deprecated__cvg_distW`, `__deprecated__continuous_cvg_dist`, + `__deprecated__cvg_gt_ge`, `__deprecated__cvg_lt_le`, + `__deprecated__linear_bounded0` + (were deprecated since 0.6.0) - in `interval_inference.v` + reserved notations `[lb of _]`, `[ub of _]`, `[lbe of _]` and `[ube of _]` From 9554a5b960a2a053e2568cd617cb8e708adb6684 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 13 Feb 2025 00:57:32 +0900 Subject: [PATCH 07/11] fix --- theories/normedtype.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index 73bd64e1d..0321c51cf 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -681,10 +681,11 @@ move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split. move/(_ (F a - n%:R)) => [z [zreal zFan]]. exists `|ceil (z - a)|%N. rewrite zFan// -ltrBlDl (le_lt_trans (le_ceil _))//. - by rewrite (le_lt_trans (ler_norm _))// -natr1 -intr_norm ltrDl. + apply: (le_lt_trans (ler_norm _)). + by rewrite -natr1 -intr_norm ltrDl. by exists i => //=; rewrite in_itv/= yFa (lt_le_trans _ Fany). - move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa]. - exists `| ceil (F (a + n.+1%:R) - F a)%R |.+1 => //=. + exists `|ceil (F (a + n.+1%:R) - F a)%R|.+1 => //=. rewrite in_itv/= zFa andbT lerBlDr -lerBlDl (le_trans _ (abs_ceil_ge _))//. by rewrite ler_normr orbC opprB lerB// ltW. Qed. @@ -713,7 +714,8 @@ move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split. move/(_ (F a - n%:R)) => [z [zreal zFan]]. exists `|ceil (a - z)|%N. rewrite zFan// ltrBlDr -ltrBlDl (le_lt_trans (le_ceil _))//. - by rewrite (le_lt_trans (ler_norm _))// -natr1 -intr_norm ltrDl. + apply: (le_lt_trans (ler_norm _)). + by rewrite -natr1 -intr_norm ltrDl. by exists i => //=; rewrite in_itv/= yFa andbT (lt_le_trans _ Fany). - move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa]. exists `| ceil (F (a - n.+1%:R) - F a)%R |.+1 => //=. From 2b39dd59fd7795068d6113b8470b51ec1425cee9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 13 Feb 2025 01:27:55 +0900 Subject: [PATCH 08/11] fix --- theories/normedtype.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index 0321c51cf..3a855335b 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -680,7 +680,8 @@ move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split. move/cvgrNy_lt : nyF. move/(_ (F a - n%:R)) => [z [zreal zFan]]. exists `|ceil (z - a)|%N. - rewrite zFan// -ltrBlDl (le_lt_trans (le_ceil _))//. + rewrite zFan// -ltrBlDl. + apply: (le_lt_trans (le_ceil _)). apply: (le_lt_trans (ler_norm _)). by rewrite -natr1 -intr_norm ltrDl. by exists i => //=; rewrite in_itv/= yFa (lt_le_trans _ Fany). @@ -713,7 +714,8 @@ move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split. move/cvgrNy_lt : nyF. move/(_ (F a - n%:R)) => [z [zreal zFan]]. exists `|ceil (a - z)|%N. - rewrite zFan// ltrBlDr -ltrBlDl (le_lt_trans (le_ceil _))//. + rewrite zFan// ltrBlDr -ltrBlDl. + apply: (le_lt_trans (le_ceil _)). apply: (le_lt_trans (ler_norm _)). by rewrite -natr1 -intr_norm ltrDl. by exists i => //=; rewrite in_itv/= yFa andbT (lt_le_trans _ Fany). From b9d8f5768993bb89856fb53cc4b3f1cfd1019f7a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 13 Feb 2025 02:17:53 +0900 Subject: [PATCH 09/11] fix --- theories/normedtype.v | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index 3a855335b..05b702a40 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -681,9 +681,8 @@ move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split. move/(_ (F a - n%:R)) => [z [zreal zFan]]. exists `|ceil (z - a)|%N. rewrite zFan// -ltrBlDl. - apply: (le_lt_trans (le_ceil _)). - apply: (le_lt_trans (ler_norm _)). - by rewrite -natr1 -intr_norm ltrDl. + rewrite (le_lt_trans (Num.Theory.le_ceil _)) ?num_real//. + by rewrite (le_lt_trans (ler_norm _))// -natr1 -intr_norm ltrDl. by exists i => //=; rewrite in_itv/= yFa (lt_le_trans _ Fany). - move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa]. exists `|ceil (F (a + n.+1%:R) - F a)%R|.+1 => //=. @@ -715,9 +714,8 @@ move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split. move/(_ (F a - n%:R)) => [z [zreal zFan]]. exists `|ceil (a - z)|%N. rewrite zFan// ltrBlDr -ltrBlDl. - apply: (le_lt_trans (le_ceil _)). - apply: (le_lt_trans (ler_norm _)). - by rewrite -natr1 -intr_norm ltrDl. + rewrite (le_lt_trans (Num.Theory.le_ceil _)) ?num_real//. + by rewrite (le_lt_trans (ler_norm _))// -natr1 -intr_norm ltrDl. by exists i => //=; rewrite in_itv/= yFa andbT (lt_le_trans _ Fany). - move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa]. exists `| ceil (F (a - n.+1%:R) - F a)%R |.+1 => //=. From 23aa62e9a649280cd09efc69989a47010b4588d7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 19 Feb 2025 23:50:31 +0900 Subject: [PATCH 10/11] fix --- CHANGELOG_UNRELEASED.md | 16 +++ theories/ftc.v | 2 +- theories/gauss_integral.v | 24 ++++- theories/normedtype.v | 15 +++ theories/probability.v | 210 +++++++++++++++++++++++++++++++++++++- theories/realfun.v | 7 ++ 6 files changed, 269 insertions(+), 5 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e81bfd2ed..867177f96 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -241,6 +241,22 @@ `increasing_ge0_integration_by_substitutionT`, `ge0_symfun_integralT` +- in `gauss_integral`: + + lemmas `integralT_gauss`, `integrableT_gauss` + +- in `probability.v`: + + definition `normal_pdf` + + lemmas `normal_pdf_ge0`, `normal_pdf_gt0`, `measurable_normal_pdf`, + `continuous_normal_pdf`, `normal_pdf_ub` + + definition `normal_prob`, equipped with the structure of probability measure + + lemmas `integral_normal_pdf`, `normal_prob_dom` + +- in `realfun.v`: + + lemma `cvg_addrr_Ny` + +- in `normedtype.v`: + + lemmas `gt0_cvgMlNy`, `gt0_cvgMly` + ### Changed - in `lebesgue_integral.v` diff --git a/theories/ftc.v b/theories/ftc.v index 9fef7ba2c..f68d3bca5 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1893,7 +1893,7 @@ rewrite derive1N; last exact: derivable_id. by rewrite derive1_id mulrN1 opprK. Unshelve. all: end_near. Qed. -Lemma increasing_ge0_integration_by_substitutionT F G a : +Lemma increasing_ge0_integration_by_substitutionT F G : {homo F : x y / (x < y)%R} -> continuous F^`() -> cvg (F^`() x @[x --> -oo%R]) -> diff --git a/theories/gauss_integral.v b/theories/gauss_integral.v index 0abecf461..79b0dfacd 100644 --- a/theories/gauss_integral.v +++ b/theories/gauss_integral.v @@ -393,7 +393,7 @@ Import gauss_integral_proof. Let mu := @lebesgue_measure R. Lemma integral0y_gauss : - \int[mu]_(x in `[0%R, +oo[) gauss_fun x = Num.sqrt pi / 2. + (\int[mu]_(x in `[0%R, +oo[) (gauss_fun x)%:E)%E = (Num.sqrt pi / 2)%:E. Proof. have cvg_Ig : @integral0_gauss R x @[x --> +oo] --> Num.sqrt pi / 2. have : Num.sqrt (@integral0_gauss R x ^+ 2) @[x --> +oo] @@ -407,7 +407,7 @@ have cvg_Ig : @integral0_gauss R x @[x --> +oo] --> Num.sqrt pi / 2. apply/funext => r; rewrite sqrtr_sqr// ger0_norm//. exact: integral0_gauss_ge0. have /cvg_lim := @ge0_cvgn_integral R mu _ gauss_fun_ge0 measurable_gauss_fun. -rewrite /integral0y_gauss /Rintegral => <-//. +rewrite /integral0y_gauss => <-//. suff: limn (fun n => (\int[mu]_(x in `[0%R, n%:R]) (gauss_fun x)%:E)%E) = (Num.sqrt pi / 2)%:E. by move=> ->. @@ -417,4 +417,24 @@ move/neq0_fine_cvgP; apply. by rewrite gt_eqF// divr_gt0// sqrtr_gt0 pi_gt0. Qed. +Theorem integralT_gauss : (\int[mu]_x (gauss_fun x)%:E)%E = (Num.sqrt pi)%:E. +Proof. +rewrite ge0_symfun_integralT//=. +- rewrite (_ : [set x | _] = `[0, +oo[%classic); last first. + by apply/seteqP; split => x/=; rewrite in_itv/= andbT. + by rewrite integral0y_gauss -EFinM mulrCA divff// mulr1. +- by move=> x; exact: gauss_fun_ge0. +- exact: continuous_gauss_fun. +- by move=> x/=; rewrite /gauss_fun sqrrN. +Qed. + +Lemma integrableT_gauss : mu.-integrable setT (EFin \o gauss_fun). +Proof. +apply/integrableP; split. + by apply/measurable_EFinP/measurable_funTS; exact: measurable_gauss_fun. +apply/abse_integralP => //=. + by apply/measurable_EFinP/measurable_funTS; exact: measurable_gauss_fun. +by rewrite integralT_gauss/= ltry. +Qed. + End gauss_integral. diff --git a/theories/normedtype.v b/theories/normedtype.v index 05b702a40..e1c7bc7c7 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -895,6 +895,21 @@ Lemma cvgenyP {R : realType} {T} {F : set_system T} {FF : Filter F} (f : T -> na (((f n)%:R : R)%:E @[n --> F] --> +oo%E) <-> (f @ F --> \oo). Proof. by rewrite cvgeryP cvgrnyP. Qed. +Lemma gt0_cvgMlNy {R : realFieldType} (M : R) (f : R -> R) : (0 < M)%R -> + (f r) @[r --> -oo] --> -oo -> (f r * M)%R @[r --> -oo] --> -oo. +Proof. +move=> M0 /cvgrNyPle fy; apply/cvgrNyPle => A. +by apply: filterS (fy (A / M)) => x; rewrite ler_pdivlMr. +Qed. + +Lemma gt0_cvgMly {R : realFieldType} (M : R) (f : R -> R) : (0 < M)%R -> + f r @[r --> +oo] --> +oo -> (f r * M)%R @[r --> +oo] --> +oo. +Proof. +move=> M0 /cvgryPge fy; apply/cvgryPge => A. +apply: filterS (fy (A / M)) => x. +by rewrite ler_pdivrMr. +Qed. + (** Modules with a norm depending on a numDomain*) HB.mixin Record PseudoMetricNormedZmod_Tvs_isNormedModule K V diff --git a/theories/probability.v b/theories/probability.v index b26f34573..c00367e51 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -6,8 +6,9 @@ From mathcomp Require Import cardinality fsbigop. From HB Require Import structures. From mathcomp Require Import exp numfun lebesgue_measure lebesgue_integral. From mathcomp Require Import reals interval_inference ereal topology normedtype. -From mathcomp Require Import sequences esum measure exp numfun lebesgue_measure. -From mathcomp Require Import lebesgue_integral kernel. +From mathcomp Require Import sequences derive esum measure exp trigo realfun. +From mathcomp Require Import numfun lebesgue_measure lebesgue_integral kernel. +From mathcomp Require Import ftc gauss_integral. (**md**************************************************************************) (* # Probability *) @@ -1369,3 +1370,208 @@ apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=. Qed. End uniform_probability. + +Section normal_density. +Context {R : realType}. +Local Open Scope ring_scope. +Local Import Num.ExtraDef. + +Definition normal_pdf (m s x : R) : R := + if s == 0 then \1_`[0, 1] x else (* TODO: need the dirac delta function *) + (sqrtr (s ^+2 * pi *+ 2))^-1 * expR (- (x - m) ^+ 2 / (s ^+ 2*+ 2)). + +Lemma normal_pdf_ge0 m s x : 0 <= normal_pdf m s x. +Proof. +rewrite /normal_pdf; case: ifP => // _. +by rewrite mulr_ge0 ?expR_ge0// invr_ge0 mulr_ge0. +Qed. + +Lemma normal_pdf_gt0 m s x : s != 0 -> 0 < normal_pdf m s x. +Proof. +rewrite /normal_pdf; case: ifP => //. +move/negP/negP => s0 _. +set sigma := s ^+ 2. +have sigma0 : 0 < sigma by rewrite exprn_even_gt0/=. +rewrite mulr_gt0 ?expR_gt0// invr_gt0//. +by rewrite sqrtr_gt0 pmulrn_rgt0// pmulr_rgt0// pi_gt0. +Qed. + +Lemma measurable_normal_pdf m s : measurable_fun setT (normal_pdf m s). +Proof. +rewrite /normal_pdf. +have [_|s0] := eqVneq s 0; first exact: measurable_indic. +apply: measurable_funM => //=; apply: measurableT_comp => //=. +apply: measurable_funM => //=; apply: measurableT_comp => //=. +apply: measurableT_comp (exprn_measurable _) _ => /=. +exact: measurable_funD. +Qed. + +Lemma continuous_normal_pdf m s x : s != 0 -> + {for x, continuous (normal_pdf m s)}. +Proof. +rewrite /normal_pdf. +have [|s0 _] := eqVneq s 0; first by []. +apply: continuousM => //=; first exact: cvg_cst. +apply: continuous_comp => /=; last exact: continuous_expR. +apply: continuousM => //=; last exact: cvg_cst. +apply: continuous_comp => //=; last exact: (@continuousN _ R^o). +apply: (@continuous_comp _ _ _ _ (fun x : R => x ^+ 2)%R). + by apply: (@continuousD _ R^o) => //=; exact: cvg_cst. +exact: exprn_continuous. +Qed. + +Lemma normal_pdf_ub m s x : s != 0 -> + normal_pdf m s x <= (sqrtr (s ^+ 2 * pi *+ 2))^-1. +Proof. +rewrite /normal_pdf. +have [|s0 _] := eqVneq s 0; first by []. +rewrite -[leRHS]mulr1. +rewrite ler_wpM2l ?invr_ge0// ?sqrtr_ge0. +rewrite -[leRHS]expR0 ler_expR mulNr oppr_le0 mulr_ge0// ?sqr_ge0//. +by rewrite invr_ge0 mulrn_wge0// sqr_ge0. +Qed. + +End normal_density. + +Definition normal_prob {R : realType} (m : R) (s : R) : set _ -> \bar R := + fun V => (\int[lebesgue_measure]_(x in V) (normal_pdf m s x)%:E)%E. + +Section normal_probability. +Variables (R : realType) (m sigma : R). +Local Open Scope ring_scope. +Notation mu := lebesgue_measure. + +Let integral_normal_pdf' : sigma != 0 -> + (\int[mu]_x (expR (- (x - m) ^+ 2 / (sigma ^+ 2 *+ 2)))%:E = + (Num.sqrt (sigma ^+ 2 * pi *+ 2))%:E)%E. +Proof. +move=> sigma_gt0. +pose F (x : R^o) := (x - m) / (`|sigma| * Num.sqrt 2). +have F'E : F^`()%classic = cst (`|sigma| * Num.sqrt 2)^-1. + apply/funext => x; rewrite /F derive1E deriveM// deriveD// derive_cst scaler0. + by rewrite add0r derive_id derive_cst addr0 scaler1. +have := @integralT_gauss R. +rewrite (@increasing_ge0_integration_by_substitutionT _ F gauss_fun)//=; first last. +- by move=> x; rewrite gauss_fun_ge0. +- exact: continuous_gauss_fun. +- apply/gt0_cvgMly; last exact: cvg_addrr. + by rewrite invr_gt0// mulr_gt0// normr_gt0. +- apply/gt0_cvgMlNy; last exact: cvg_addrr_Ny. + by rewrite invr_gt0// mulr_gt0// normr_gt0. +- by rewrite F'E; exact: is_cvg_cst. +- by rewrite F'E; exact: is_cvg_cst. +- by rewrite F'E => ?; exact: cvg_cst. +- by move=> x y; rewrite /F ltr_pM2r ?invr_gt0 ?mulr_gt0 ?normr_gt0// ltrBlDr subrK. +move=> /(congr1 (fun x => x * (`|sigma| * Num.sqrt 2)%:E)%E). +rewrite -ge0_integralZr//=; last first. + by move=> x _; rewrite lee_fin mulr_ge0//= ?gauss_fun_ge0// F'E/= invr_ge0. + rewrite F'E; apply/measurable_EFinP/measurable_funM => //. + apply/measurableT_comp => //; first exact: measurable_gauss_fun. + by apply: measurable_funM => //; exact: measurable_funD. +move=> int_gauss. +apply: eq_trans. + apply: eq_trans; last exact: int_gauss. + apply: eq_integral => /= x _. + rewrite F'E !fctE/= EFinM -muleA -EFinM mulVf ?mulr1; last first. + by rewrite gt_eqF ?mulr_gt0 ?normr_gt0. + rewrite /gauss_fun /F exprMn exprVn -[in RHS]mulNr. + by rewrite exprMn real_normK ?num_real// sqr_sqrtr// mulr_natr. +rewrite -mulrnAl sqrtrM ?mulrn_wge0 ?sqr_ge0//. +by rewrite -[in RHS]mulr_natr sqrtrM ?sqr_ge0// sqrtr_sqr !EFinM muleC. +Qed. + +Lemma integral_normal_pdf : (\int[mu]_x (normal_pdf m sigma x)%:E = 1%E)%E. +Proof. +rewrite /normal_pdf. +have [_|s0] := eqVneq sigma 0. + by rewrite integral_indic//= setIT lebesgue_measure_itv/= lte01 oppr0 adde0. +under eq_integral do rewrite EFinM. +rewrite integralZl//=; last first. + apply/integrableP; split. + apply/measurable_EFinP => /=. + apply: measurableT_comp => //=. + apply: measurable_funM => //=. + apply: measurableT_comp => //=. + apply: measurable_funX => //=. + exact: measurable_funD. + under eq_integral. + move=> /= x _. + rewrite ger0_norm ?expR_ge0//. + over. + by rewrite /= integral_normal_pdf'// ltry. +rewrite integral_normal_pdf'// -EFinM mulVf// sqrtr_eq0 -ltNge. +by rewrite mulrn_wgt0// mulr_gt0 ?pi_gt0// exprn_even_gt0. +Qed. + +Local Notation normal_pdf := (normal_pdf m sigma). +Local Notation normal_prob := (normal_prob m sigma). + +Let normal0 : normal_prob set0 = 0%E. +Proof. by rewrite /normal_prob integral_set0. Qed. + +Let normal_ge0 A : (0 <= normal_prob A)%E. +Proof. +rewrite /normal_prob integral_ge0//= => x _. +by rewrite lee_fin normal_pdf_ge0 ?ltW. +Qed. + +Let normal_sigma_additive : semi_sigma_additive normal_prob. +Proof. +move=> /= F mF tF mUF. +rewrite /normal_prob/= integral_bigcup//=; last first. + apply/integrableP; split. + apply/measurable_funTS/measurableT_comp => //. + exact: measurable_normal_pdf. + rewrite (_ : (fun x => _) = EFin \o normal_pdf); last first. + by apply/funext => x; rewrite gee0_abs// lee_fin normal_pdf_ge0 ?ltW. + apply: le_lt_trans. + apply: (@ge0_subset_integral _ _ _ _ _ setT) => //=. + by apply/measurable_EFinP; exact: measurable_normal_pdf. + by move=> ? _; rewrite lee_fin normal_pdf_ge0 ?ltW. + by rewrite integral_normal_pdf // ltey. +apply: is_cvg_ereal_nneg_natsum_cond => n _ _. +by apply: integral_ge0 => /= x ?; rewrite lee_fin normal_pdf_ge0 ?ltW. +Qed. + +HB.instance Definition _ := isMeasure.Build _ _ _ + normal_prob normal0 normal_ge0 normal_sigma_additive. + +Let normal_setT : normal_prob [set: _] = 1%E. +Proof. by rewrite /normal_prob integral_normal_pdf. Qed. + +HB.instance Definition _ := + @Measure_isProbability.Build _ _ R normal_prob normal_setT. + +Lemma normal_prob_dom : normal_prob `<< mu. +Proof. +move=> A mA muA0; rewrite /normal_prob /normal_pdf. +have [s0|s0] := eqVneq sigma 0. + apply: null_set_integral => //=; apply: (integrableS measurableT) => //=. + apply/integrableP; split. + by apply/measurable_EFinP; exact: measurable_indic. + apply/abse_integralP => //. + by apply/measurable_EFinP; exact: measurable_indic. + rewrite integral_indic// setIT/= lebesgue_measure_itv/=. + by rewrite lte_fin ltr01 oppr0 addr0 abse1 ltry. +apply/eqP; rewrite eq_le; apply/andP; split; last first. + apply: integral_ge0 => x _; rewrite lee_fin. + have := normal_pdf_ge0 m sigma x. + by rewrite /normal_pdf ifF//; apply/negP/negP. +apply: (@le_trans _ _ + (\int[mu]_(x in A) (Num.sqrt (sigma ^+ 2 * pi *+ 2))^-1%:E))%E; last first. + by rewrite integral_cst//= muA0 mule0. +apply: ge0_le_integral => //=. +- move=> x _; rewrite lee_fin. + have := normal_pdf_ge0 m sigma x. + by rewrite /normal_pdf ifF//; exact/negP/negP. +- apply/measurable_funTS/measurableT_comp => //. + apply: measurable_funM => //; apply: measurableT_comp => //. + apply: measurable_funM => //; apply: measurableT_comp => //. + apply: measurableT_comp (exprn_measurable _) _ => /=. + exact: measurable_funD. +- move=> x _; rewrite lee_fin -[leRHS]mulr1 ler_wpM2l ?invr_ge0// ?sqrtr_ge0. + rewrite -[leRHS]expR0 ler_expR mulNr oppr_le0 mulr_ge0// ?sqr_ge0//. + by rewrite invr_ge0 mulrn_wge0// sqr_ge0. +Qed. + +End normal_probability. diff --git a/theories/realfun.v b/theories/realfun.v index 50ce089fb..786a120ff 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -106,6 +106,13 @@ Qed. Lemma cvg_addrr (M : R) : (r + M) @[r --> +oo] --> +oo. Proof. by under [X in X @ _]funext => n do rewrite addrC; exact: cvg_addrl. Qed. +Lemma cvg_addrr_Ny (M : R) : r + M @[r --> -oo] --> -oo. +Proof. +move=> P [r [rreal rP]]; exists (r - M); split. + by rewrite realB// num_real. +by move=> m/=; rewrite ltrBrDr => /rP. +Qed. + (* NB: see cvg_centern in sequences.v *) Lemma cvg_centerr (M : R) (T : topologicalType) (f : R -> T) (l : T) : (f (n - M) @[n --> +oo] --> l) = (f r @[r --> +oo] --> l). From 7ed1432cf9e7adf0695f980bfff9730620b988e1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 20 Feb 2025 00:06:08 +0900 Subject: [PATCH 11/11] fix --- CHANGELOG_UNRELEASED.md | 2 +- theories/ftc.v | 4 ++-- theories/topology_theory/num_topology.v | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 867177f96..8edaaf6e9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -221,7 +221,7 @@ `increasing_itvNyo_bigcup`, `increasing_itvoc_bigcup` - in `num_topology.v`: - + lemmas `nbhs_lt_trans`, `nbhs_lt_transN` + + lemmas `lt_nbhsl`, `Nlt_nbhsl` - in `measurable_realfun.v`: + lemmas `measurable_fun_itv_bndo_bndc`, `measurable_fun_itv_obnd_cbnd` diff --git a/theories/ftc.v b/theories/ftc.v index f68d3bca5..bdaebbcec 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1750,11 +1750,11 @@ rewrite (@increasing_ge0_integration_by_substitutiony (\- (F \o -%R))%R); last 8 apply: near_eq_cvg; rewrite near_simpl; near=> z. rewrite derive1N; last first. apply: dFcompN. - by near: z; exact: nbhs_lt_transN. + by near: z; exact: Nlt_nbhsl. rewrite [in RHS]derive1_comp; last 2 first. exact: derivable_opp. apply: dFN. - by near: z; exact: nbhs_lt_transN. + by near: z; exact: Nlt_nbhsl. rewrite derive1N; last exact: derivable_id. by rewrite derive1_id mulrN1 opprK. - move: cvgFb => /cvg_at_leftNP cvgFbl. diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index 3921c35aa..7a27da5b0 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -112,7 +112,7 @@ exists x => // z /=; rewrite sub0r normrN. by apply: le_lt_trans; rewrite ler_norm. Qed. -Lemma nbhs_lt_trans {R : realType} (x a : R) : x < a -> +Lemma lt_nbhsl {R : realType} (x a : R) : x < a -> \forall y \near nbhs x, y < a. Proof. move=> xb; exists ((a - x) / 2) => /=; first by rewrite divr_gt0// subr_gt0. @@ -120,7 +120,7 @@ move=> r/=; rewrite ltr_pdivlMr// ltrBrDr; apply: le_lt_trans. by rewrite -lerBlDr -normrN opprB (le_trans (ler_norm _))// ler_peMr// ler1n. Qed. -Lemma nbhs_lt_transN {R : realType} (x a : R) : +Lemma Nlt_nbhsl {R : realType} (x a : R) : - x < a -> \forall y \near nbhs x, - y < a. Proof. move=> xb; exists ((a + x) / 2) => /=.