From 285aaaf779b81f59e0fcb32dee47adef541d24a7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 23 Jul 2024 15:21:59 +0900 Subject: [PATCH 01/16] rebase --- CHANGELOG_UNRELEASED.md | 93 +++++++++++++++++++++++++++++++++++++++++ theories/ftc.v | 2 +- 2 files changed, 94 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5724ef64c8..5c58a75f1e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -9,12 +9,105 @@ - in `mathcomp_extra.v`: + lemma `bij_forall` +- in `normedtype.v`: + + lemma `ninftyN` + +- in `derive.v`: + + lemma `derive_id` + + lemmas `exp_derive`, `exp_derive1` + + lemma `derive_cst` + + lemma `deriveMr`, `deriveMl` + +- in `functions.v`: + + lemmas `mul_funC` +- in `sequences.v`: + + lemma `cvg_geometric_eseries_half` + +- in `lebesgue_measure.v`: + + definitions `is_open_itv`, `open_itv_cover` + + lemmas `outer_measure_open_itv_cover`, `outer_measure_open_le`, + `outer_measure_open`, `outer_measure_Gdelta`, `negligible_outer_measure` +- in `ftc.v`: + + lemmas `integration_by_parts`, `Rintegration_by_parts` + + lemma `continuous_integration_by_parts` + +- in `classical_sets.v`: + + scope `relation_scope` with delimiter `relation` + + notation `^-1` in `relation_scope` (use to be a local notation) + + lemma `set_prod_invK` (was a local lemma in `normedtype.v`) + + definition `diagonal`, lemma `diagonalP` +- in `mathcomp_extra.v`: + + lemmas `invf_ple`, `invf_lep` + +- in `lebesgue_integral.v`: + + lemma `integralZr` + +- in `normedtype.v`: + + lemma `le_closed_ball` +- in `sequences.v`: + + theorem `Baire` + + definition `bounded_fun_norm` + + lemma `bounded_landau` + + definition `pointwise_bounded` + + definition `uniform_bounded` + + theorem `Banach_Steinhauss` + +- in `topology.v`: + + Structures `PointedFiltered`, `PointedNbhs`, `PointedUniform`, + `PseudoPointedMetric` +- in `measure.v`: + + lemma `measurable_neg`, `measurable_or` +- in `continuous_FTC1_closed`: + + corollary `continuous_FTC1_closed` + +- in `lebesgue_integral.v`: + + lemma `locally_integrableS` + +- in `normedtype.v`: + + lemmas `nbhs_right_ltW`, `cvg_patch` + +- in `set_interval.v`: + + lemma `subset_itvSoo` + +### Changed + +- in `lebesgue_measure.v`: + + lemmas `measurable_fun_eqr`, `measurable_fun_indic`, `measurable_fun_dirac`, + `measurable_fun_addn`, `measurable_fun_maxn`, `measurable_fun_subn`, `measurable_fun_ltn`, + `measurable_fun_leq`, `measurable_fun_eqn` + + module `NGenCInfty` + * definition `G` + * lemmas `measurable_itv_bounded`, `measurableE` +- in `continuous_FTC1_closed`: + + corollary `continuous_FTC1_closed` + +- in `lebesgue_integral.v`: + + lemma `locally_integrableS` - in `normedtype.v`: + lemma `cvgyNP` - in `realfun.v`: + lemmas `cvg_pinftyP`, `cvg_ninftyP` +- in `set_interval.v`: + + lemma `subset_itvSoo` + +- in `lebesgue_integral.v`: + + lemma `locally_integrableS` + +- in `normedtype.v`: + + lemmas `nbhs_right_ltW`, `cvg_patch` + +- in `set_interval.v`: + + lemma `subset_itvSoo` + +- in `lebesgue_integral.v`: + + lemma `integrable_locally_restrict` + + lemma `near_davg` + + lemma `lebesgue_pt_restrict` + + lemma `integrable_locally_restrict` + + lemma `near_davg` + + lemma `lebesgue_pt_restrict` - in `filter.v` (new file): + lemma `in_nearW` diff --git a/theories/ftc.v b/theories/ftc.v index 938408668f..a7c59c369a 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -51,7 +51,7 @@ apply: cvg_at_right_left_dnbhs. by rewrite -EFinD addrAC subrr add0r. have nice_E y : nicely_shrinking y (E y). split=> [n|]; first exact: measurable_itv. - exists (2, (fun n => PosNum (d_gt0 n))); split => //= [n z|n]. + exists (2, fun n => PosNum (d_gt0 n)); split => //= [n z|n]. rewrite /E/= in_itv/= /ball/= ltr_distlC => /andP[yz ->]. by rewrite (lt_le_trans _ yz)// ltrBlDr ltrDl. rewrite (lebesgue_measure_ball _ (ltW _))// -/mu muE -EFinM lee_fin. From 62d542afeb3dc0505812848cef052d64b485c92e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 29 Aug 2024 09:28:42 +0900 Subject: [PATCH 02/16] change of variables (tentative) Co-authored-by: IshiguroYoshihiro --- theories/ftc.v | 328 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 328 insertions(+) diff --git a/theories/ftc.v b/theories/ftc.v index a7c59c369a..622cfd263e 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -679,3 +679,331 @@ exact: (derivable_oo_continuous_bnd_within Gab). Qed. End Rintegration_by_parts. + +(* TODO: PR *) +Lemma nbhs_left_ltBl {R : numFieldType} (x : R) e : + (0 < e)%R -> \forall y \near x^'-, (x - y < e)%R. +Proof. +move=> e0. +near=> y; rewrite -ltrBrDl ltrNl opprB; near: y. +apply: nbhs_left_gt. +by rewrite ltrBlDr ltrDl. +Unshelve. all: by end_near. Qed. + +Lemma within_continuous_continuous {R : realType} a b (f : R -> R) x : (a < b)%R -> + {within `[a, b], continuous f} -> x \in `]a, b[ -> {for x, continuous f}. +Proof. +move=> ab cG xab; have := cG x. +move=> /cvg_patch => /(_ ab xab). +apply: cvg_trans; apply: near_eq_cvg. +rewrite near_simpl; near=> n. +rewrite patchE/= ifT// inE; apply: subset_itv_oo_cc. +by near: n; exact: near_in_itv. +Unshelve. all: end_near. Qed. + +Section change_of_variables_preliminaries. +Context {R : realType}. +Notation mu := lebesgue_measure. +Implicit Types (F G f : R -> R) (a b : R). + +Lemma increasing_image_oo F (a b : R) : (a < b)%R -> + {in `[a, b] &, {homo F : x y / (x < y)%R}} -> + F @` `]a, b[ `<=` `]F a, F b[. +Proof. +move=> ab iF ? [x /= xab <-]. +move: xab; rewrite !in_itv/= => /andP[ax xb]. +by apply/andP; split; apply: iF; rewrite // in_itv/= ?lexx !ltW. +Qed. + +Lemma decreasing_image_oo F (a b : R) : (a < b)%R -> + {in `[a, b] &, {homo F : x y /~ (x < y)%R}} -> + F @` `]a, b[ `<=` `]F b, F a[. +Proof. +move=> ab iF ? [x /= xab <-]. +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}} -> + F x @[x --> a^'+] --> F a -> + G x @[x --> (F a)^'+] --> l -> + (G \o F) x @[x --> a^'+] --> l. +Proof. +move=> ab incrF cFa GFa. +(* take arbitrary e > 0, find d s.t. `| G (F (a + d))) - G (F a)| < e *) +apply/cvgrPdist_le => /= e e0. +(* for this e, + there exists d s.t. `| G (F a + d) - G (F a)| < e by continuity of G *) +have/cvgrPdist_le /(_ e e0) [d /= d0 {}GFa] := GFa. +(* for this d, + there exists d' s.t. forall r, `| r - a | < d' implies F (a + d') - F a < d + by continuity of F at a *) +(* apply a lemma for take r := (a + d') from `[a, b] *) +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 !ltW. +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}} -> + F x @[x --> b^'-] --> F b -> + G x @[x --> (F b)^'-] --> l -> + (G \o F) x @[x --> b^'-] --> l. +Proof. +move=> ab incrF cFb GFb. +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 !ltW. +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}} -> + F x @[x --> a^'+] --> F a -> + G x @[x --> (F a)^'-] --> l -> + (G \o F) x @[x --> a^'+] --> l. +Proof. +move=> ab decrF cFa GFa. +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 !ltW. +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}} -> + F x @[x --> b^'-] --> F b -> + G x @[x --> (F b)^'+] --> l -> + (G \o F) x @[x --> b^'-] --> l. +Proof. +move=> ab decrF cFb GFb. +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 !ltW. +apply: cFb => //=. +rewrite gtr0_norm// ?subr_gt0//. +by near: t; exact: nbhs_left_ltBl. +Unshelve. all: end_near. Qed. + +End change_of_variables_preliminaries. + +Section change_of_variables. +Local Open Scope ereal_scope. +Context {R : realType}. +Notation mu := lebesgue_measure. +Implicit Types (F G f : R -> R) (a b : R). + +Lemma increasing_change F G a b : (a < b)%R -> + {in `[a, b]&, {homo F : x y / (x < y)%R}} -> + {within `[a, b], continuous F^`()} -> + derivable_oo_continuous_bnd F a b -> + {within `[F a, F b], continuous G} -> + \int[mu]_(x in `[F a, F b]) (G x)%:E = + \int[mu]_(x in `[a, b]) (((G \o F) * F^`()) x)%:E. +Proof. +set f : R -> R := F^`(). +move=> ab incrF cf dcbF cG. +have FaFb : (F a < F b)%R by apply: incrF; rewrite //= in_itv/= (ltW ab) lexx. +pose PG x := parameterized_integral mu (F a) x G. +have intGFb : mu.-integrable `[(F a), (F b)] (EFin \o G). + by apply: continuous_compact_integrable => //; exact: segment_compact. +have locG : locally_integrable setT (G \_`[F a, F b]). + apply: integrable_locally; first exact: openT. + by rewrite -restrict_comp// -integrable_restrict//= setTI. +set H := PG \o F. +set h : R -> R := ((G \o F) * f)%R. +have dcbPG : derivable_oo_continuous_bnd PG (F a) (F b). + have [/= dF rF lF] := dcbF. + split => /=. + - move=> x xFaFb /=. + have xFb : (x < F b)%R by move: xFaFb; rewrite in_itv/= => /andP[]. + have /= := continuous_FTC1 xFb intGFb locG _ + (within_continuous_continuous FaFb cG xFaFb). + rewrite lte_fin. + by move: (xFaFb); rewrite in_itv/= => /andP[-> _] /(_ isT)[]. + - have := parameterized_integral_continuous FaFb intGFb. + by move=> /(continuous_within_itvP _ FaFb)[_ []]. + - exact: parameterized_integral_cvg_at_left. +have dPGE : {in `](F a), (F b)[, PG^`() =1 G}. + move=> x xFaFb. + have xFb : (x < F b)%R by move: xFaFb; rewrite in_itv/= => /andP[]. + have /= := continuous_FTC1 xFb intGFb locG _ + (within_continuous_continuous FaFb cG xFaFb). + rewrite lte_fin. + by move: (xFaFb); rewrite in_itv/= => /andP[-> _] /(_ isT)[]. +move/continuous_within_itvP : (cG) => /(_ FaFb)[incG [GFa GFb]]. +have : {within `[a, b], continuous F} := + derivable_oo_continuous_bnd_within dcbF. +move/continuous_within_itvP => /(_ ab)[incF [cFa cFb]]. +have ch : {within `[a, b], continuous h}. + apply/(continuous_within_itvP _ ab); split; last split. + - move=> /= x xab. + apply: continuousM; last first. + by move/(continuous_within_itvP _ ab) : cf => [+ _]; exact. + apply: continuous_comp; first by exact: incF. + by apply: incG; exact: increasing_image_oo. + - apply: cvgM. + exact: (increasing_cvg_at_right_comp ab). + by move /(continuous_within_itvP _ ab) : cf => [_ []]. + - apply: cvgM. + exact: (increasing_cvg_at_left_comp ab). + by move /(continuous_within_itvP _ ab) : cf => [_ []]. +have dcbH : derivable_oo_continuous_bnd H a b. + have := derivable_oo_continuous_bnd_within dcbPG. + move=> /(continuous_within_itvP _ FaFb)[_ [PGFa PGFb]]. + split => /=. + - move=> x xab. + apply/derivable1_diffP. + apply: differentiable_comp; apply/derivable1_diffP. + by have [+ _ _] := dcbF; apply. + have [+ _ _] := dcbPG. + by apply; exact: increasing_image_oo. + - apply/cvgrPdist_le => /= e e0. + have/cvgrPdist_le /(_ e e0) [d /= d0 {}PGFa] := PGFa. + have := cvg_at_right_within cFa. + move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFa]. + near=> t. + apply: PGFa; last by apply: incrF; rewrite //in_itv/= ?lexx !ltW. + apply: cFa => //=. + rewrite ltr0_norm// ?subr_lt0// opprB. + by near: t; exact: nbhs_right_ltDr. + - apply/cvgrPdist_le => /= e e0. + have/cvgrPdist_le /(_ e e0) [d /= d0 {}PGFb] := PGFb. + have := cvg_at_left_within cFb. + move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFb]. + near=> t. + apply: (PGFb); last by apply: incrF; rewrite //in_itv/= ?lexx !ltW. + apply: cFb => //=. + rewrite gtr0_norm// ?subr_gt0//. + by near: t; exact: nbhs_left_ltBl. +have ? : {in `]a, b[, H^`() =1 h}. + move=> x xab; rewrite derive1_comp. + - by rewrite dPGE//; exact: increasing_image_oo. + - by have [+ _ _] := dcbF; apply. + - by have [+ _ _] := dcbPG; apply; exact: increasing_image_oo. +rewrite (continuous_FTC2 FaFb cG dcbPG dPGE). +by rewrite (continuous_FTC2 ab ch dcbH). +Unshelve. all: end_near. Qed. + +Lemma decreasing_change F G a b : + (a < b)%R -> + {in `[a, b]&, {homo F : x y /~ (x < y)%R}} -> + {within `[a, b], continuous F^`()} -> + derivable_oo_continuous_bnd F a b -> + {within `[F b, F a], continuous G} -> + \int[mu]_(x in `[F b, F a]) (G x)%:E = + \int[mu]_(x in `[a, b]) (((G \o F) * - (F^`() : R -> R)) x)%:E. +Proof. +set f : R -> R := F^`(). +move=> ab decrF cf dcbF cG. +have FbFa : (F b < F a)%R by apply: decrF; rewrite //in_itv/= (ltW ab) lexx. +pose PG x := parameterized_integral mu (F b) x G. +have intGFa : mu.-integrable `[(F b), (F a)] (EFin \o G). + by apply: continuous_compact_integrable => //; exact: segment_compact. +have locG : locally_integrable setT (G \_`[F b, F a]). + apply: integrable_locally; first exact: openT. + by rewrite -restrict_comp// -integrable_restrict//= setTI. +set H := PG \o F. +set h : R -> R := ((G \o F) * (- f))%R. +have dcbPG : derivable_oo_continuous_bnd PG (F b) (F a). + have [dF rF lF] := dcbF. + split. + - move=> x xFbFa /=. + have xFa : (x < F a)%R by move: xFbFa; rewrite in_itv/= => /andP[]. + have /= := continuous_FTC1 xFa intGFa locG _ (within_continuous_continuous FbFa cG xFbFa). + rewrite lte_fin. + by move: (xFbFa); rewrite in_itv/= => /andP[-> _] /(_ isT)[]. + - move: intGFa. + move/(parameterized_integral_continuous FbFa). + by move/(continuous_within_itvP _ FbFa) => [_ [+ _]]. + - exact: parameterized_integral_cvg_at_left. +have dPGE : {in `](F b), (F a)[, PG^`() =1 G}. + move=> x xFbFa. + have xFa : (x < F a)%R by move: xFbFa; rewrite in_itv/= => /andP[]. + have /= := continuous_FTC1 xFa intGFa locG _ (within_continuous_continuous FbFa cG xFbFa). + rewrite lte_fin. + by move: (xFbFa); rewrite in_itv/= => /andP[-> _] /(_ isT)[]. +move/continuous_within_itvP : (cG) => /(_ FbFa)[in_cG [GFb GFa]]. +have := derivable_oo_continuous_bnd_within dcbF. +move=> /continuous_within_itvP => /(_ ab)[in_cF [cFa cFb]]. +have cNh : {within `[a, b], continuous (- h)%R}. + apply/(continuous_within_itvP _ ab); split; last split. + - move=> /= x xab. + apply: continuousN. + apply: continuousM; last first. + apply: continuousN. + move/(continuous_within_itvP _ ab) : cf => [+ _]. + exact. + apply: continuous_comp. + exact: in_cF. + by apply: in_cG; exact: decreasing_image_oo. + - apply: cvgN; apply: cvgM. + exact: (decreasing_cvg_at_right_comp ab). + apply: (@cvgN _ _ _ _ _ f (f a)). + by move /(continuous_within_itvP _ ab) : cf => [_ []]. + - apply: cvgN; apply: cvgM. + exact: (decreasing_cvg_at_left_comp ab). + apply: (@cvgN _ _ _ _ _ f (f b)). + by move /(continuous_within_itvP _ ab) : cf => [_ []]. +have dcbH : derivable_oo_continuous_bnd H a b. + have := derivable_oo_continuous_bnd_within dcbPG. + move=> /(continuous_within_itvP _ FbFa)[_ [PGFb PGFa]]. + split => /=. + - move=> x xab. + apply/derivable1_diffP. + apply: differentiable_comp; apply/derivable1_diffP. + by have [+ _ _] := dcbF; apply. + have [dPG ? ?] := dcbPG. + by apply: dPG; exact: decreasing_image_oo. + - apply/cvgrPdist_le => /= e e0. + have/cvgrPdist_le /(_ e e0) [d' /= d'0 {}PGFa] := PGFa. + have := cvg_at_right_within cFa. + move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFa]. + near=> t. + apply: PGFa; last by apply: decrF; rewrite //in_itv/= ?lexx !ltW. + apply: cFa => //=. + rewrite ltr0_norm// ?subr_lt0// opprB. + by near: t; exact: nbhs_right_ltDr. + - apply/cvgrPdist_le => /= e e0. + have/cvgrPdist_le /(_ e e0) [d' /= d'0 {}PGFb] := PGFb. + have := cvg_at_left_within cFb. + move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFb]. + near=> t. + apply: (PGFb); last by apply: decrF; rewrite //in_itv/= ?lexx !ltW. + apply: cFb => //=. + rewrite gtr0_norm// ?subr_gt0//. + by near: t; exact: nbhs_left_ltBl. +have dHE : {in `]a, b[, H^`() =1 (- h)%R}. (* difference from gt0 version *) + move=> x xab; rewrite derive1_comp. + - rewrite dPGE//; first by rewrite /h mulrN opprK//. + exact: decreasing_image_oo. + - by have [+ _ _] := dcbF; apply. + - by have [+ _ _] := dcbPG; apply; exact: decreasing_image_oo. +rewrite (continuous_FTC2 FbFa cG dcbPG dPGE). +under eq_integral do rewrite -(opprK (h _)) EFinN. +rewrite integralN/=; last first. + apply: integrable_add_def => //. + apply: continuous_compact_integrable => //. + exact: segment_compact. +by rewrite (continuous_FTC2 ab cNh dcbH dHE) oppeB// EFinN addeC. +Unshelve. all: end_near. Qed. + +End change_of_variables. From ef7c784a10041a3e6f69d5504eac899ac3e9f458 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 13 Sep 2024 20:24:23 +0900 Subject: [PATCH 03/16] changelog --- CHANGELOG_UNRELEASED.md | 10 ++++ theories/ftc.v | 100 ++++++++++++++-------------------------- theories/normedtype.v | 12 +++++ theories/topology.v | 2 + 4 files changed, 59 insertions(+), 65 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5c58a75f1e..5f6ec0f505 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -69,6 +69,16 @@ - in `set_interval.v`: + lemma `subset_itvSoo` +- in `normedtype.v`: + + lemma `nbhs_left_ltBl` + + lemma `within_continuous_continuous` + +- in `ftc.v`: + + lemma `increasing_image_oo`, `decreasing_image_oo`, + `increasing_cvg_at_right_comp`, `increasing_cvg_at_left_comp`, + `decreasing_cvg_at_right_comp`, `decreasing_cvg_at_left_comp`, + `increasing_change`, `decreasing_change` + ### Changed - in `lebesgue_measure.v`: diff --git a/theories/ftc.v b/theories/ftc.v index 622cfd263e..77c1658c02 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -680,28 +680,7 @@ Qed. End Rintegration_by_parts. -(* TODO: PR *) -Lemma nbhs_left_ltBl {R : numFieldType} (x : R) e : - (0 < e)%R -> \forall y \near x^'-, (x - y < e)%R. -Proof. -move=> e0. -near=> y; rewrite -ltrBrDl ltrNl opprB; near: y. -apply: nbhs_left_gt. -by rewrite ltrBlDr ltrDl. -Unshelve. all: by end_near. Qed. - -Lemma within_continuous_continuous {R : realType} a b (f : R -> R) x : (a < b)%R -> - {within `[a, b], continuous f} -> x \in `]a, b[ -> {for x, continuous f}. -Proof. -move=> ab cG xab; have := cG x. -move=> /cvg_patch => /(_ ab xab). -apply: cvg_trans; apply: near_eq_cvg. -rewrite near_simpl; near=> n. -rewrite patchE/= ifT// inE; apply: subset_itv_oo_cc. -by near: n; exact: near_in_itv. -Unshelve. all: end_near. Qed. - -Section change_of_variables_preliminaries. +Section integration_by_substitution_preliminaries. Context {R : realType}. Notation mu := lebesgue_measure. Implicit Types (F G f : R -> R) (a b : R). @@ -803,16 +782,16 @@ rewrite gtr0_norm// ?subr_gt0//. by near: t; exact: nbhs_left_ltBl. Unshelve. all: end_near. Qed. -End change_of_variables_preliminaries. +End integration_by_substitution_preliminaries. -Section change_of_variables. +Section integration_by_substitution. Local Open Scope ereal_scope. Context {R : realType}. Notation mu := lebesgue_measure. Implicit Types (F G f : R -> R) (a b : R). Lemma increasing_change F G a b : (a < b)%R -> - {in `[a, b]&, {homo F : x y / (x < y)%R}} -> + {in `[a, b] &, {homo F : x y / (x < y)%R}} -> {within `[a, b], continuous F^`()} -> derivable_oo_continuous_bnd F a b -> {within `[F a, F b], continuous G} -> @@ -825,9 +804,6 @@ have FaFb : (F a < F b)%R by apply: incrF; rewrite //= in_itv/= (ltW ab) lexx. pose PG x := parameterized_integral mu (F a) x G. have intGFb : mu.-integrable `[(F a), (F b)] (EFin \o G). by apply: continuous_compact_integrable => //; exact: segment_compact. -have locG : locally_integrable setT (G \_`[F a, F b]). - apply: integrable_locally; first exact: openT. - by rewrite -restrict_comp// -integrable_restrict//= setTI. set H := PG \o F. set h : R -> R := ((G \o F) * f)%R. have dcbPG : derivable_oo_continuous_bnd PG (F a) (F b). @@ -835,40 +811,38 @@ have dcbPG : derivable_oo_continuous_bnd PG (F a) (F b). split => /=. - move=> x xFaFb /=. have xFb : (x < F b)%R by move: xFaFb; rewrite in_itv/= => /andP[]. - have /= := continuous_FTC1 xFb intGFb locG _ - (within_continuous_continuous FaFb cG xFaFb). - rewrite lte_fin. - by move: (xFaFb); rewrite in_itv/= => /andP[-> _] /(_ isT)[]. + apply: (continuous_FTC1 xFb intGFb _ _).1 => /=. + by move: (xFaFb); rewrite lte_fin in_itv/= => /andP[]. + exact: (within_continuous_continuous _ _ xFaFb). - have := parameterized_integral_continuous FaFb intGFb. - by move=> /(continuous_within_itvP _ FaFb)[_ []]. + by move=> /(continuous_within_itvP _ FaFb)[]. - exact: parameterized_integral_cvg_at_left. have dPGE : {in `](F a), (F b)[, PG^`() =1 G}. move=> x xFaFb. have xFb : (x < F b)%R by move: xFaFb; rewrite in_itv/= => /andP[]. - have /= := continuous_FTC1 xFb intGFb locG _ - (within_continuous_continuous FaFb cG xFaFb). - rewrite lte_fin. - by move: (xFaFb); rewrite in_itv/= => /andP[-> _] /(_ isT)[]. -move/continuous_within_itvP : (cG) => /(_ FaFb)[incG [GFa GFb]]. + apply: (continuous_FTC1 xFb intGFb _ _).2 => //=. + by move: (xFaFb); rewrite lte_fin in_itv/= => /andP[]. + exact: (within_continuous_continuous _ _ xFaFb). +move/continuous_within_itvP : (cG) => /(_ FaFb)[incG GFa GFb]. have : {within `[a, b], continuous F} := derivable_oo_continuous_bnd_within dcbF. -move/continuous_within_itvP => /(_ ab)[incF [cFa cFb]]. +move/continuous_within_itvP => /(_ ab)[incF cFa cFb]. have ch : {within `[a, b], continuous h}. - apply/(continuous_within_itvP _ ab); split; last split. + apply/(continuous_within_itvP _ ab); split. - move=> /= x xab. apply: continuousM; last first. - by move/(continuous_within_itvP _ ab) : cf => [+ _]; exact. - apply: continuous_comp; first by exact: incF. + by move/(continuous_within_itvP _ ab) : cf => [+ _ _]; exact. + apply: continuous_comp; first exact: incF. by apply: incG; exact: increasing_image_oo. - apply: cvgM. exact: (increasing_cvg_at_right_comp ab). - by move /(continuous_within_itvP _ ab) : cf => [_ []]. + by move/(continuous_within_itvP _ ab) : cf => []. - apply: cvgM. exact: (increasing_cvg_at_left_comp ab). - by move /(continuous_within_itvP _ ab) : cf => [_ []]. + by move/(continuous_within_itvP _ ab) : cf => []. have dcbH : derivable_oo_continuous_bnd H a b. have := derivable_oo_continuous_bnd_within dcbPG. - move=> /(continuous_within_itvP _ FaFb)[_ [PGFa PGFb]]. + move=> /(continuous_within_itvP _ FaFb)[_ PGFa PGFb]. split => /=. - move=> x xab. apply/derivable1_diffP. @@ -918,9 +892,6 @@ have FbFa : (F b < F a)%R by apply: decrF; rewrite //in_itv/= (ltW ab) lexx. pose PG x := parameterized_integral mu (F b) x G. have intGFa : mu.-integrable `[(F b), (F a)] (EFin \o G). by apply: continuous_compact_integrable => //; exact: segment_compact. -have locG : locally_integrable setT (G \_`[F b, F a]). - apply: integrable_locally; first exact: openT. - by rewrite -restrict_comp// -integrable_restrict//= setTI. set H := PG \o F. set h : R -> R := ((G \o F) * (- f))%R. have dcbPG : derivable_oo_continuous_bnd PG (F b) (F a). @@ -928,29 +899,28 @@ have dcbPG : derivable_oo_continuous_bnd PG (F b) (F a). split. - move=> x xFbFa /=. have xFa : (x < F a)%R by move: xFbFa; rewrite in_itv/= => /andP[]. - have /= := continuous_FTC1 xFa intGFa locG _ (within_continuous_continuous FbFa cG xFbFa). - rewrite lte_fin. - by move: (xFbFa); rewrite in_itv/= => /andP[-> _] /(_ isT)[]. + apply: (continuous_FTC1 xFa intGFa _ _).1 => //=. + by move: (xFbFa); rewrite lte_fin in_itv/= => /andP[]. + exact: (within_continuous_continuous _ _ xFbFa). - move: intGFa. move/(parameterized_integral_continuous FbFa). - by move/(continuous_within_itvP _ FbFa) => [_ [+ _]]. + by move/(continuous_within_itvP _ FbFa) => [_ + _]. - exact: parameterized_integral_cvg_at_left. have dPGE : {in `](F b), (F a)[, PG^`() =1 G}. move=> x xFbFa. have xFa : (x < F a)%R by move: xFbFa; rewrite in_itv/= => /andP[]. - have /= := continuous_FTC1 xFa intGFa locG _ (within_continuous_continuous FbFa cG xFbFa). - rewrite lte_fin. - by move: (xFbFa); rewrite in_itv/= => /andP[-> _] /(_ isT)[]. -move/continuous_within_itvP : (cG) => /(_ FbFa)[in_cG [GFb GFa]]. + apply: (continuous_FTC1 xFa intGFa _ _).2 => //=. + by move: (xFbFa); rewrite lte_fin in_itv/= => /andP[]. + exact: (within_continuous_continuous _ _ xFbFa). +move/continuous_within_itvP : (cG) => /(_ FbFa)[in_cG GFb GFa]. have := derivable_oo_continuous_bnd_within dcbF. -move=> /continuous_within_itvP => /(_ ab)[in_cF [cFa cFb]]. +move=> /continuous_within_itvP => /(_ ab)[in_cF cFa cFb]. have cNh : {within `[a, b], continuous (- h)%R}. - apply/(continuous_within_itvP _ ab); split; last split. - - move=> /= x xab. - apply: continuousN. + apply/(continuous_within_itvP _ ab); split. + - move=> /= x xab; apply: continuousN. apply: continuousM; last first. apply: continuousN. - move/(continuous_within_itvP _ ab) : cf => [+ _]. + move/(continuous_within_itvP _ ab) : cf => [+ _ _]. exact. apply: continuous_comp. exact: in_cF. @@ -958,14 +928,14 @@ have cNh : {within `[a, b], continuous (- h)%R}. - apply: cvgN; apply: cvgM. exact: (decreasing_cvg_at_right_comp ab). apply: (@cvgN _ _ _ _ _ f (f a)). - by move /(continuous_within_itvP _ ab) : cf => [_ []]. + by move /(continuous_within_itvP _ ab) : cf => []. - apply: cvgN; apply: cvgM. exact: (decreasing_cvg_at_left_comp ab). apply: (@cvgN _ _ _ _ _ f (f b)). - by move /(continuous_within_itvP _ ab) : cf => [_ []]. + by move /(continuous_within_itvP _ ab) : cf => []. have dcbH : derivable_oo_continuous_bnd H a b. have := derivable_oo_continuous_bnd_within dcbPG. - move=> /(continuous_within_itvP _ FbFa)[_ [PGFb PGFa]]. + move=> /(continuous_within_itvP _ FbFa)[_ PGFb PGFa]. split => /=. - move=> x xab. apply/derivable1_diffP. @@ -1006,4 +976,4 @@ rewrite integralN/=; last first. by rewrite (continuous_FTC2 ab cNh dcbH dHE) oppeB// EFinN addeC. Unshelve. all: end_near. Qed. -End change_of_variables. +End integration_by_substitution. diff --git a/theories/normedtype.v b/theories/normedtype.v index 238c5d0a7f..e34d9ec5bb 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -1361,6 +1361,12 @@ Lemma nbhs_left_ge x z : z < x -> \forall y \near x^'-, z <= y. Proof. by move=> xz; near do apply/ltW; apply: nbhs_left_gt. Unshelve. all: by end_near. Qed. +Lemma nbhs_left_ltBl x e : 0 < e -> \forall y \near x^'-, x - y < e. +Proof. +move=> e0; near=> y; rewrite -ltrBrDl ltrNl opprB; near: y. +by apply: nbhs_left_gt; rewrite ltrBlDr ltrDl. +Unshelve. all: by end_near. Qed. + Lemma withinN (A : set R) a : within A (nbhs (- a)) = - x @[x --> within (-%R @` A) (nbhs a)]. Proof. @@ -2181,6 +2187,12 @@ rewrite !bnd_simp/= !le_eqVlt => /predU1P[<-{x}|ax] /predU1P[|]. by rewrite -open_subsetE; [exact: subset_itvW| exact: interval_open]. Qed. +Lemma within_continuous_continuous {R : realType} a b (f : R -> R) x : (a < b)%R -> + {within `[a, b], continuous f} -> x \in `]a, b[ -> {for x, continuous f}. +Proof. +by move=> ab /continuous_within_itvP-/(_ ab)[+ _] /[swap] xab cf; exact. +Qed. + (* TODO: generalize to R : numFieldType *) Section hausdorff. diff --git a/theories/topology.v b/theories/topology.v index 7600e7f760..edc6a806b3 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -4177,6 +4177,8 @@ Proof. by move=> ? ctsF ? ? ?; apply: (@nbhs_subspace_subset A B) => //; exact: ctsF. Qed. + + Lemma nbhs_subspaceT (x : T) : nbhs (x : subspace setT) = nbhs x. Proof. have [_|] := nbhs_subspaceP [set: T]; last by cbn. From d59d691ca357c6604b8ec76eeec81b9116370329 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Sun, 15 Sep 2024 23:07:24 +0900 Subject: [PATCH 04/16] weaken conditions of in/decreasing_cvg_at_right/left_comp --- theories/ftc.v | 32 ++++++++++++++++++-------------- 1 file changed, 18 insertions(+), 14 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 77c1658c02..a63abe3a1f 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -704,7 +704,7 @@ 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}} -> + {in `[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. @@ -722,14 +722,14 @@ 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 !ltW. +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. 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}} -> + {in `]a, 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. @@ -740,14 +740,14 @@ 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 !ltW. +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. 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}} -> + {in `[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. @@ -758,14 +758,14 @@ 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 !ltW. +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. 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}} -> + {in `]a, 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. @@ -776,7 +776,7 @@ 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 !ltW. +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. @@ -835,11 +835,13 @@ have ch : {within `[a, b], continuous h}. apply: continuous_comp; first exact: incF. by apply: incG; exact: increasing_image_oo. - apply: cvgM. - exact: (increasing_cvg_at_right_comp ab). - by move/(continuous_within_itvP _ ab) : cf => []. + apply: (increasing_cvg_at_right_comp ab) => //x y xab yab. + by apply: incrF; apply: subset_itv_co_cc. + by move /(continuous_within_itvP _ ab) : cf => []. - apply: cvgM. - exact: (increasing_cvg_at_left_comp ab). - by move/(continuous_within_itvP _ ab) : cf => []. + apply: (increasing_cvg_at_left_comp ab) => //x y xab yab. + by apply: incrF; apply: subset_itv_oc_cc. + by move /(continuous_within_itvP _ ab) : cf => []. have dcbH : derivable_oo_continuous_bnd H a b. have := derivable_oo_continuous_bnd_within dcbPG. move=> /(continuous_within_itvP _ FaFb)[_ PGFa PGFb]. @@ -926,11 +928,13 @@ have cNh : {within `[a, b], continuous (- h)%R}. exact: in_cF. by apply: in_cG; exact: decreasing_image_oo. - apply: cvgN; apply: cvgM. - exact: (decreasing_cvg_at_right_comp ab). + apply: (decreasing_cvg_at_right_comp ab) => //x y xab yab. + by apply: decrF; apply: subset_itv_co_cc. apply: (@cvgN _ _ _ _ _ f (f a)). by move /(continuous_within_itvP _ ab) : cf => []. - apply: cvgN; apply: cvgM. - exact: (decreasing_cvg_at_left_comp ab). + apply: (decreasing_cvg_at_left_comp ab) => //x y xab yab. + by apply: decrF; apply: subset_itv_oc_cc. apply: (@cvgN _ _ _ _ _ f (f b)). by move /(continuous_within_itvP _ ab) : cf => []. have dcbH : derivable_oo_continuous_bnd H a b. From 9559466b8370f7e75a53b627795bfdbd44bebd3c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 18 Sep 2024 09:10:57 +0900 Subject: [PATCH 05/16] fix changelog --- CHANGELOG_UNRELEASED.md | 45 +++++++++-------------------------------- theories/topology.v | 2 -- 2 files changed, 10 insertions(+), 37 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5f6ec0f505..fc337cbcdf 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -29,7 +29,6 @@ `outer_measure_open`, `outer_measure_Gdelta`, `negligible_outer_measure` - in `ftc.v`: + lemmas `integration_by_parts`, `Rintegration_by_parts` - + lemma `continuous_integration_by_parts` - in `classical_sets.v`: + scope `relation_scope` with delimiter `relation` @@ -57,29 +56,6 @@ `PseudoPointedMetric` - in `measure.v`: + lemma `measurable_neg`, `measurable_or` -- in `continuous_FTC1_closed`: - + corollary `continuous_FTC1_closed` - -- in `lebesgue_integral.v`: - + lemma `locally_integrableS` - -- in `normedtype.v`: - + lemmas `nbhs_right_ltW`, `cvg_patch` - -- in `set_interval.v`: - + lemma `subset_itvSoo` - -- in `normedtype.v`: - + lemma `nbhs_left_ltBl` - + lemma `within_continuous_continuous` - -- in `ftc.v`: - + lemma `increasing_image_oo`, `decreasing_image_oo`, - `increasing_cvg_at_right_comp`, `increasing_cvg_at_left_comp`, - `decreasing_cvg_at_right_comp`, `decreasing_cvg_at_left_comp`, - `increasing_change`, `decreasing_change` - -### Changed - in `lebesgue_measure.v`: + lemmas `measurable_fun_eqr`, `measurable_fun_indic`, `measurable_fun_dirac`, @@ -103,21 +79,20 @@ + lemma `subset_itvSoo` - in `lebesgue_integral.v`: - + lemma `locally_integrableS` + + lemma `integrable_locally_restrict` + + lemma `near_davg` + + lemma `lebesgue_pt_restrict` - in `normedtype.v`: - + lemmas `nbhs_right_ltW`, `cvg_patch` + + lemma `nbhs_left_ltBl` + + lemma `within_continuous_continuous` -- in `set_interval.v`: - + lemma `subset_itvSoo` +- in `ftc.v`: + + lemma `increasing_image_oo`, `decreasing_image_oo`, + `increasing_cvg_at_right_comp`, `increasing_cvg_at_left_comp`, + `decreasing_cvg_at_right_comp`, `decreasing_cvg_at_left_comp`, + `increasing_change`, `decreasing_change` -- in `lebesgue_integral.v`: - + lemma `integrable_locally_restrict` - + lemma `near_davg` - + lemma `lebesgue_pt_restrict` - + lemma `integrable_locally_restrict` - + lemma `near_davg` - + lemma `lebesgue_pt_restrict` - in `filter.v` (new file): + lemma `in_nearW` diff --git a/theories/topology.v b/theories/topology.v index edc6a806b3..7600e7f760 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -4177,8 +4177,6 @@ Proof. by move=> ? ctsF ? ? ?; apply: (@nbhs_subspace_subset A B) => //; exact: ctsF. Qed. - - Lemma nbhs_subspaceT (x : T) : nbhs (x : subspace setT) = nbhs x. Proof. have [_|] := nbhs_subspaceP [set: T]; last by cbn. From fb95fcebc6eef3509c6c12682b5acd7ae2d45e41 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Wed, 25 Sep 2024 02:38:19 +0900 Subject: [PATCH 06/16] weaken hypothesis of integration_by_parts --- theories/ftc.v | 368 +++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 310 insertions(+), 58 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index a63abe3a1f..7919a7efa1 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -784,6 +784,70 @@ Unshelve. all: end_near. Qed. End integration_by_substitution_preliminaries. +Section within_continuous_derive. +Context {R : numFieldType} {V W : normedModType R}. + +Definition right_derive (f : V -> W) a v := + lim ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ 0^'+). +Definition left_derive (f : V -> W) a v := + lim ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ 0^'-). + +End within_continuous_derive. + +(* PR *) +Lemma measurable_fun_set1 d d' (T : measurableType d) (U : measurableType d') + (a : T) (f : T -> U) : +d.-measurable (set1 a) -> measurable_fun (set1 a) f. +Proof. +Admitted. + +(* PR *) +Lemma in_nearW (R : realFieldType) (P : R -> Prop) (S : set R) : + @open R^o S -> + {in S, forall x, P x} -> + forall x, x \in S -> \forall y \near x, P y. +Proof. +move=> oS HP z. +rewrite inE => Sz. +have [e/= e0 He] := (open_subball oS Sz). +exists (e / 2) => //=. + by rewrite -(add0r e) midf_lt. +move=> t/= zte. +apply: HP. +move: He Sz zte. +have [<- |zt He Sz zte] := eqVneq z t; first by rewrite inE. +rewrite inE. +apply: (He (e / 2)) => //=. +rewrite sub0r normrN ger0_norm. + by rewrite -{1}(add0r e) midf_lt. + by rewrite -(add0r e) midf_le// ltW. +by rewrite -(add0r e) midf_lt. +Qed. + +Section integral_itv. +Local Open Scope ereal_scope. +Context {R : realType}. + +Local Notation mu := (@lebesgue_measure R). + +(* PR *) +Lemma integral_itv_bndo_bndc' (a : itv_bound R) (r : R) (f : R -> R) : + measurable_fun [set` Interval a (BLeft r)] f -> + \int[mu]_(x in [set` Interval a (BLeft r)]) (f x)%:E = + \int[mu]_(x in [set` Interval a (BRight r)]) (f x)%:E. +Proof. +Admitted. + +(* PR *) +Lemma integral_itv_obnd_cbnd' (r : R) (b : itv_bound R) (f : R -> R) : + measurable_fun [set` Interval (BRight r) b] f -> + \int[mu]_(x in [set` Interval (BRight r) b]) (f x)%:E = + \int[mu]_(x in [set` Interval (BLeft r) b]) (f x)%:E. +Proof. +Admitted. + +End integral_itv. + Section integration_by_substitution. Local Open Scope ereal_scope. Context {R : realType}. @@ -792,14 +856,17 @@ Implicit Types (F G f : R -> R) (a b : R). Lemma increasing_change F G a b : (a < b)%R -> {in `[a, b] &, {homo F : x y / (x < y)%R}} -> - {within `[a, b], continuous F^`()} -> + {in `]a, b[, continuous F^`()} -> + cvg ((F^`() : R -> R) x @[x --> a^'+]) -> + cvg ((F^`() : R -> R) x @[x --> b^'-]) -> derivable_oo_continuous_bnd F a b -> - {within `[F a, F b], continuous G} -> + {within `[F a, F b], continuous G} -> \int[mu]_(x in `[F a, F b]) (G x)%:E = \int[mu]_(x in `[a, b]) (((G \o F) * F^`()) x)%:E. Proof. -set f : R -> R := F^`(). -move=> ab incrF cf dcbF cG. +move=> ab incrF cf /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] dcbF cG. +set f : R -> R := fun x => if x == a then r else + if x == b then l else F^`() x. have FaFb : (F a < F b)%R by apply: incrF; rewrite //= in_itv/= (ltW ab) lexx. pose PG x := parameterized_integral mu (F a) x G. have intGFb : mu.-integrable `[(F a), (F b)] (EFin \o G). @@ -824,24 +891,54 @@ have dPGE : {in `](F a), (F b)[, PG^`() =1 G}. by move: (xFaFb); rewrite lte_fin in_itv/= => /andP[]. exact: (within_continuous_continuous _ _ xFaFb). move/continuous_within_itvP : (cG) => /(_ FaFb)[incG GFa GFb]. -have : {within `[a, b], continuous F} := +have cF : {within `[a, b], continuous F} := derivable_oo_continuous_bnd_within dcbF. -move/continuous_within_itvP => /(_ ab)[incF cFa cFb]. +move/continuous_within_itvP : (cF) => /(_ ab)[incF cFa cFb]. have ch : {within `[a, b], continuous h}. apply/(continuous_within_itvP _ ab); split. - move=> /= x xab. - apply: continuousM; last first. - by move/(continuous_within_itvP _ ab) : cf => [+ _ _]; exact. + apply: continuousM; last first. + have : F^`() y @[y --> x] --> f x. + rewrite /f. + rewrite ifF; last first. + apply: gt_eqF. + by move: xab; rewrite in_itv/= => /andP[]. + rewrite ifF; last first. + apply: lt_eqF. + by move: xab; rewrite in_itv/= => /andP[]. + exact: cf. + apply: cvg_trans. + apply: near_eq_cvg. + rewrite near_simpl. + apply: (@in_nearW _ _ `]a, b[%classic). + - exact: interval_open. + - move=> z; rewrite inE/= in_itv/= => /andP[az zb]. + rewrite /f ifF; last by rewrite gt_eqF. + by rewrite ifF// lt_eqF. + by rewrite inE. apply: continuous_comp; first exact: incF. by apply: incG; exact: increasing_image_oo. - apply: cvgM. apply: (increasing_cvg_at_right_comp ab) => //x y xab yab. by apply: incrF; apply: subset_itv_co_cc. - by move /(continuous_within_itvP _ ab) : cf => []. + rewrite {2}/f eq_refl. + move: F'ar. + apply: cvg_trans. + apply: near_eq_cvg. + near=> z. + rewrite /f ifF; last by rewrite gt_eqF. + by rewrite ifF// lt_eqF. - apply: cvgM. apply: (increasing_cvg_at_left_comp ab) => //x y xab yab. by apply: incrF; apply: subset_itv_oc_cc. - by move /(continuous_within_itvP _ ab) : cf => []. + rewrite {2}/f ifF; last by rewrite gt_eqF. + rewrite eq_refl. + move: F'bl. + apply: cvg_trans. + apply: near_eq_cvg. + near=> z. + rewrite /f ifF; last by rewrite gt_eqF. + by rewrite ifF// lt_eqF. have dcbH : derivable_oo_continuous_bnd H a b. have := derivable_oo_continuous_bnd_within dcbPG. move=> /(continuous_within_itvP _ FaFb)[_ PGFa PGFb]. @@ -870,43 +967,83 @@ have dcbH : derivable_oo_continuous_bnd H a b. apply: cFb => //=. rewrite gtr0_norm// ?subr_gt0//. by near: t; exact: nbhs_left_ltBl. -have ? : {in `]a, b[, H^`() =1 h}. +have dHE : {in `]a, b[, H^`() =1 h}. move=> x xab; rewrite derive1_comp. - - by rewrite dPGE//; exact: increasing_image_oo. + - rewrite dPGE//; last exact: increasing_image_oo. + rewrite /h/f. + move: xab. + rewrite in_itv/= => /andP[ax xb]. + rewrite mulrfctE ifF; last by rewrite gt_eqF. + by rewrite ifF// lt_eqF. - by have [+ _ _] := dcbF; apply. - by have [+ _ _] := dcbPG; apply; exact: increasing_image_oo. rewrite (continuous_FTC2 FaFb cG dcbPG dPGE). -by rewrite (continuous_FTC2 ab ch dcbH). +rewrite -(continuous_FTC2 ab ch dcbH dHE). +have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R. + apply: measurable_funM. + - apply: (measurable_comp (measurable_itv `]F a, F b[)). + exact: increasing_image_oo. + apply: subspace_continuous_measurable_fun => //. + apply: continuous_in_subspaceT => x; rewrite inE/=. + exact: incG. + - apply: subspace_continuous_measurable_fun => //. + apply: continuous_in_subspaceT => x; rewrite inE/=. + exact: incF. + - apply: subspace_continuous_measurable_fun; first by []. + apply: continuous_in_subspaceT => x. + rewrite inE/=. + exact: cf. +rewrite -!integral_itv_bndo_bndc'; last 2 first. +- rewrite -setU1itv ?bnd_simp//. + by rewrite measurable_funU//; split => //; apply: measurable_fun_set1. +- apply: subspace_continuous_measurable_fun => //. + move: ch; apply: continuous_subspaceW. + exact: subset_itv_co_cc. +rewrite -!integral_itv_obnd_cbnd'; last 2 first. +- exact: mGFF'. +- apply: subspace_continuous_measurable_fun => //. + move: ch; apply: continuous_subspaceW. + exact: subset_itv_oo_cc. +apply: eq_integral => //. +move=> x xab. +rewrite /h/f. +rewrite mulrfctE ifF; last first. + apply: gt_eqF. + by move: xab; rewrite inE/= in_itv/= => /andP[]. +rewrite ifF//. +apply: lt_eqF. +by move: xab; rewrite inE/= in_itv/= => /andP[]. Unshelve. all: end_near. Qed. -Lemma decreasing_change F G a b : - (a < b)%R -> - {in `[a, b]&, {homo F : x y /~ (x < y)%R}} -> - {within `[a, b], continuous F^`()} -> - derivable_oo_continuous_bnd F a b -> - {within `[F b, F a], continuous G} -> +Lemma decreasing_change F G a b : (a < b)%R -> + {in `[a, b] &, {homo F : x y /~ (x < y)%R}} -> + {in `]a, b[, continuous F^`()} -> + cvg ((F^`() : R -> R) x @[x --> a^'+]) -> + cvg ((F^`() : R -> R) x @[x --> b^'-]) -> + derivable_oo_continuous_bnd F a b -> + {within `[F b, F a], continuous G} -> \int[mu]_(x in `[F b, F a]) (G x)%:E = - \int[mu]_(x in `[a, b]) (((G \o F) * - (F^`() : R -> R)) x)%:E. + \int[mu]_(x in `[a, b]) (((G \o F) * (- F^`())) x)%:E. Proof. -set f : R -> R := F^`(). -move=> ab decrF cf dcbF cG. -have FbFa : (F b < F a)%R by apply: decrF; rewrite //in_itv/= (ltW ab) lexx. +move=> ab decrF cf /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] dcbF cG. +set f : R -> R := fun x => if x == a then r else + if x == b then l else F^`() x. +have FbFa : (F b < F a)%R by apply: decrF; rewrite //= in_itv/= (ltW ab) lexx. pose PG x := parameterized_integral mu (F b) x G. have intGFa : mu.-integrable `[(F b), (F a)] (EFin \o G). by apply: continuous_compact_integrable => //; exact: segment_compact. set H := PG \o F. set h : R -> R := ((G \o F) * (- f))%R. have dcbPG : derivable_oo_continuous_bnd PG (F b) (F a). - have [dF rF lF] := dcbF. - split. + have [/= dF rF lF] := dcbF. + split => /=. - move=> x xFbFa /=. have xFa : (x < F a)%R by move: xFbFa; rewrite in_itv/= => /andP[]. - apply: (continuous_FTC1 xFa intGFa _ _).1 => //=. + apply: (continuous_FTC1 xFa intGFa _ _).1 => /=. by move: (xFbFa); rewrite lte_fin in_itv/= => /andP[]. exact: (within_continuous_continuous _ _ xFbFa). - - move: intGFa. - move/(parameterized_integral_continuous FbFa). - by move/(continuous_within_itvP _ FbFa) => [_ + _]. + - have := parameterized_integral_continuous FbFa intGFa. + by move=> /(continuous_within_itvP _ FbFa)[]. - exact: parameterized_integral_cvg_at_left. have dPGE : {in `](F b), (F a)[, PG^`() =1 G}. move=> x xFbFa. @@ -914,29 +1051,60 @@ have dPGE : {in `](F b), (F a)[, PG^`() =1 G}. apply: (continuous_FTC1 xFa intGFa _ _).2 => //=. by move: (xFbFa); rewrite lte_fin in_itv/= => /andP[]. exact: (within_continuous_continuous _ _ xFbFa). -move/continuous_within_itvP : (cG) => /(_ FbFa)[in_cG GFb GFa]. -have := derivable_oo_continuous_bnd_within dcbF. -move=> /continuous_within_itvP => /(_ ab)[in_cF cFa cFb]. +move/continuous_within_itvP : (cG) => /(_ FbFa)[incG GFb GFa]. +have cF : {within `[a, b], continuous F} := + derivable_oo_continuous_bnd_within dcbF. +move/continuous_within_itvP : (cF) => /(_ ab)[incF cFa cFb]. have cNh : {within `[a, b], continuous (- h)%R}. + move=> x; apply: continuousN; move: x. apply/(continuous_within_itvP _ ab); split. - - move=> /= x xab; apply: continuousN. + - move=> /= x xab. apply: continuousM; last first. - apply: continuousN. - move/(continuous_within_itvP _ ab) : cf => [+ _ _]. - exact. - apply: continuous_comp. - exact: in_cF. - by apply: in_cG; exact: decreasing_image_oo. - - apply: cvgN; apply: cvgM. + have : (- F^`())%R y @[y --> x] --> (- f)%R x. + apply: cvgN => //. + rewrite /f. + rewrite ifF; last first. + apply: gt_eqF. + by move: xab; rewrite in_itv/= => /andP[]. + rewrite ifF; last first. + apply: lt_eqF. + by move: xab; rewrite in_itv/= => /andP[]. + exact: cf. + apply: cvg_trans. + apply: near_eq_cvg. + rewrite near_simpl. + apply: (@in_nearW _ _ `]a, b[%classic). + - exact: interval_open. + - move=> z; rewrite inE/= in_itv/= => /andP[az zb]. + rewrite !fctE; congr (- _)%R. + rewrite /f ifF; last by rewrite gt_eqF. + by rewrite ifF// lt_eqF. + by rewrite inE. + apply: continuous_comp; first exact: incF. + by apply: incG; exact: decreasing_image_oo. + - apply: cvgM. apply: (decreasing_cvg_at_right_comp ab) => //x y xab yab. by apply: decrF; apply: subset_itv_co_cc. - apply: (@cvgN _ _ _ _ _ f (f a)). - by move /(continuous_within_itvP _ ab) : cf => []. - - apply: cvgN; apply: cvgM. + apply: cvgN. + rewrite {2}/f eq_refl. + move: F'ar. + apply: cvg_trans. + apply: near_eq_cvg. + near=> z. + rewrite /f ifF; last by rewrite gt_eqF. + by rewrite ifF// lt_eqF. + - apply: cvgM. apply: (decreasing_cvg_at_left_comp ab) => //x y xab yab. by apply: decrF; apply: subset_itv_oc_cc. - apply: (@cvgN _ _ _ _ _ f (f b)). - by move /(continuous_within_itvP _ ab) : cf => []. + apply: cvgN. + rewrite {2}/f ifF; last by rewrite gt_eqF. + rewrite eq_refl. + move: F'bl. + apply: cvg_trans. + apply: near_eq_cvg. + near=> z. + rewrite /f ifF; last by rewrite gt_eqF. + by rewrite ifF// lt_eqF. have dcbH : derivable_oo_continuous_bnd H a b. have := derivable_oo_continuous_bnd_within dcbPG. move=> /(continuous_within_itvP _ FbFa)[_ PGFb PGFa]. @@ -945,39 +1113,123 @@ have dcbH : derivable_oo_continuous_bnd H a b. apply/derivable1_diffP. apply: differentiable_comp; apply/derivable1_diffP. by have [+ _ _] := dcbF; apply. - have [dPG ? ?] := dcbPG. - by apply: dPG; exact: decreasing_image_oo. + have [+ _ _] := dcbPG. + by apply; exact: decreasing_image_oo. - apply/cvgrPdist_le => /= e e0. - have/cvgrPdist_le /(_ e e0) [d' /= d'0 {}PGFa] := PGFa. + have/cvgrPdist_le /(_ e e0) [d /= d0 {}PGFa] := PGFa. have := cvg_at_right_within cFa. - move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFa]. + move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFa]. near=> t. apply: PGFa; last by apply: decrF; rewrite //in_itv/= ?lexx !ltW. apply: cFa => //=. rewrite ltr0_norm// ?subr_lt0// opprB. by near: t; exact: nbhs_right_ltDr. - apply/cvgrPdist_le => /= e e0. - have/cvgrPdist_le /(_ e e0) [d' /= d'0 {}PGFb] := PGFb. + have/cvgrPdist_le /(_ e e0) [d /= d0 {}PGFb] := PGFb. have := cvg_at_left_within cFb. - move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFb]. + move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFb]. near=> t. apply: (PGFb); last by apply: decrF; rewrite //in_itv/= ?lexx !ltW. apply: cFb => //=. rewrite gtr0_norm// ?subr_gt0//. by near: t; exact: nbhs_left_ltBl. -have dHE : {in `]a, b[, H^`() =1 (- h)%R}. (* difference from gt0 version *) +have dHE : {in `]a, b[, H^`() =1 (- h)%R}. move=> x xab; rewrite derive1_comp. - - rewrite dPGE//; first by rewrite /h mulrN opprK//. - exact: decreasing_image_oo. + - rewrite dPGE//; last exact: decreasing_image_oo. + rewrite /h/f. + move: xab. + rewrite in_itv/= => /andP[ax xb]. + rewrite mulrN opprK. + rewrite mulrfctE ifF; last by rewrite gt_eqF. + by rewrite ifF// lt_eqF. - by have [+ _ _] := dcbF; apply. - by have [+ _ _] := dcbPG; apply; exact: decreasing_image_oo. rewrite (continuous_FTC2 FbFa cG dcbPG dPGE). -under eq_integral do rewrite -(opprK (h _)) EFinN. -rewrite integralN/=; last first. - apply: integrable_add_def => //. +apply: oppe_inj. +rewrite oppeB// addeC. +rewrite -(continuous_FTC2 ab cNh dcbH dHE). +have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R. + apply: measurable_funM. + - apply: (measurable_comp (measurable_itv `]F b, F a[)). + exact: decreasing_image_oo. + apply: subspace_continuous_measurable_fun => //. + apply: continuous_in_subspaceT => x; rewrite inE/=. + exact: incG. + - apply: subspace_continuous_measurable_fun => //. + apply: continuous_in_subspaceT => x; rewrite inE/=. + exact: incF. + - apply: subspace_continuous_measurable_fun; first by []. + apply: continuous_in_subspaceT => x. + rewrite inE/=. + exact: cf. +rewrite -!integral_itv_bndo_bndc'; last 2 first. +- rewrite -setU1itv ?bnd_simp//. + rewrite mulrN; apply: measurableT_comp => //. + by rewrite measurable_funU//; split => //; apply: measurable_fun_set1. +- apply: subspace_continuous_measurable_fun => //. + move: cNh; apply: continuous_subspaceW. + exact: subset_itv_co_cc. +rewrite -!integral_itv_obnd_cbnd'; last 2 first. +- rewrite mulrN. + exact: measurableT_comp => //. +- apply: subspace_continuous_measurable_fun => //. + move: cNh; apply: continuous_subspaceW. + exact: subset_itv_oo_cc. +rewrite -[LHS]oppeK -integralN//=; last first. + apply: integrable_add_def => //=. + apply: (@integrableS _ _ _ mu `[a, b]) => //. + exact: subset_itv_oo_cc. apply: continuous_compact_integrable => //. exact: segment_compact. -by rewrite (continuous_FTC2 ab cNh dcbH dHE) oppeB// EFinN addeC. +congr (- _). +apply: eq_integral => //. +move=> x xab. +rewrite mulrN; congr (- _)%:E. +rewrite /h/f. +rewrite mulrN opprK. +rewrite mulrfctE ifF; last first. + apply: gt_eqF. + by move: xab; rewrite inE/= in_itv/= => /andP[]. +rewrite ifF//. +apply: lt_eqF. +by move: xab; rewrite inE/= in_itv/= => /andP[]. Unshelve. all: end_near. Qed. End integration_by_substitution. + +Module old_integration_by_substitution. +Section old_integration_by_substitution. +Local Open Scope ereal_scope. +Context {R : realType}. +Notation mu := lebesgue_measure. +Implicit Types (F G f : R -> R) (a b : R). + +Lemma increasing_change_old F G a b : (a < b)%R -> + {in `[a, b] &, {homo F : x y / (x < y)%R}} -> + {within `[a, b], continuous F^`()} -> + derivable_oo_continuous_bnd F a b -> + {within `[F a, F b], continuous G} -> + \int[mu]_(x in `[F a, F b]) (G x)%:E = + \int[mu]_(x in `[a, b]) (((G \o F) * F^`()) x)%:E. +Proof. +move=> ab incrF. +move/(continuous_within_itvP _ ab) => [+ /cvgP + /cvgP]. +exact: (increasing_change ab incrF). +Qed. + +Lemma decreasing_change_old F G a b : + (a < b)%R -> + {in `[a, b]&, {homo F : x y /~ (x < y)%R}} -> + {within `[a, b], continuous F^`()} -> + derivable_oo_continuous_bnd F a b -> + {within `[F b, F a], continuous G} -> + \int[mu]_(x in `[F b, F a]) (G x)%:E = + \int[mu]_(x in `[a, b]) (((G \o F) * - (F^`() : R -> R)) x)%:E. +Proof. +move=> ab decrF. +move/(continuous_within_itvP _ ab) => [+ /cvgP + /cvgP]. +exact: decreasing_change. +Qed. + +End old_integration_by_substitution. +End old_integration_by_substitution. From 74fdccfe1b30b6cd8678ebc064c405aa7581330a Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Wed, 25 Sep 2024 11:32:08 +0900 Subject: [PATCH 07/16] remove admit --- theories/ftc.v | 38 ++++++++++++++++++++++++++++++++++---- 1 file changed, 34 insertions(+), 4 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 7919a7efa1..a209acad77 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -797,9 +797,11 @@ End within_continuous_derive. (* PR *) Lemma measurable_fun_set1 d d' (T : measurableType d) (U : measurableType d') (a : T) (f : T -> U) : -d.-measurable (set1 a) -> measurable_fun (set1 a) f. +measurable_fun (set1 a) f. Proof. -Admitted. +move=> ma S mS. +by rewrite set1I; case: ifP. +Qed. (* PR *) Lemma in_nearW (R : realFieldType) (P : R -> Prop) (S : set R) : @@ -824,19 +826,44 @@ rewrite sub0r normrN ger0_norm. by rewrite -(add0r e) midf_lt. Qed. +Lemma notin_setD1K (T : Type) (r : T) (D : set T) : r \notin D -> D `\ r = D. +Proof. +rewrite notin_setE => NDr. +apply: setDidl. +apply/disjoints_subset. +apply/subsetCr. +by move=> _ ->. +Qed. + Section integral_itv. Local Open Scope ereal_scope. Context {R : realType}. Local Notation mu := (@lebesgue_measure R). +Lemma integral_setD1_EFin' (f : R -> R) r (D : set R) : + measurable (D `\ r) -> measurable_fun (D `\ r) f -> + \int[mu]_(x in D `\ r) (f x)%:E = \int[mu]_(x in D) (f x)%:E. +Proof. +move=> mD mf. +have [Dr|NDr] := pselect (D r); last by rewrite notin_setD1K// notin_setE. +rewrite -[in RHS](@setD1K _ r D)// integral_setU_EFin//. +- by rewrite integral_set1// ?add0e. +- apply/measurable_funU => //; split => //. + exact: measurable_fun_set1. +- by rewrite disj_set2E; apply/eqP/seteqP; split => // x [? []]. +Qed. + (* PR *) Lemma integral_itv_bndo_bndc' (a : itv_bound R) (r : R) (f : R -> R) : measurable_fun [set` Interval a (BLeft r)] f -> \int[mu]_(x in [set` Interval a (BLeft r)]) (f x)%:E = \int[mu]_(x in [set` Interval a (BRight r)]) (f x)%:E. Proof. -Admitted. +move=> mf; have [ar|ar] := leP a (BLeft r). +- by rewrite -[RHS](@integral_setD1_EFin' _ r) ?setDitv1r. +- by rewrite !set_itv_ge// -leNgt// ltW. +Qed. (* PR *) Lemma integral_itv_obnd_cbnd' (r : R) (b : itv_bound R) (f : R -> R) : @@ -844,7 +871,10 @@ Lemma integral_itv_obnd_cbnd' (r : R) (b : itv_bound R) (f : R -> R) : \int[mu]_(x in [set` Interval (BRight r) b]) (f x)%:E = \int[mu]_(x in [set` Interval (BLeft r) b]) (f x)%:E. Proof. -Admitted. +move=> mf; have [rb|rb] := leP (BRight r) b. +- rewrite -[RHS](@integral_setD1_EFin' _ r) ?setDitv1l//. +- by rewrite !set_itv_ge// -leNgt -?ltBRight_leBLeft// ltW. +Qed. End integral_itv. From 2f0c9bbf64c3558ec430f9048b8764fba48f5f79 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Fri, 27 Sep 2024 10:24:53 +0900 Subject: [PATCH 08/16] wip clean --- theories/ftc.v | 160 +++++++++++++++++++++++++++++++++++-------------- 1 file changed, 115 insertions(+), 45 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index a209acad77..5e4bd60c43 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -784,27 +784,14 @@ Unshelve. all: end_near. Qed. End integration_by_substitution_preliminaries. -Section within_continuous_derive. -Context {R : numFieldType} {V W : normedModType R}. - -Definition right_derive (f : V -> W) a v := - lim ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ 0^'+). -Definition left_derive (f : V -> W) a v := - lim ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ 0^'-). - -End within_continuous_derive. - -(* PR *) +(* PR#1327 *) Lemma measurable_fun_set1 d d' (T : measurableType d) (U : measurableType d') (a : T) (f : T -> U) : measurable_fun (set1 a) f. -Proof. -move=> ma S mS. -by rewrite set1I; case: ifP. -Qed. +Proof. Admitted. (* PR *) -Lemma in_nearW (R : realFieldType) (P : R -> Prop) (S : set R) : +Lemma in_nearW (R : topologicalType) (P : R -> Prop) (S : set R) : @open R^o S -> {in S, forall x, P x} -> forall x, x \in S -> \forall y \near x, P y. @@ -826,14 +813,9 @@ rewrite sub0r normrN ger0_norm. by rewrite -(add0r e) midf_lt. Qed. +(* PR#1327 *) Lemma notin_setD1K (T : Type) (r : T) (D : set T) : r \notin D -> D `\ r = D. -Proof. -rewrite notin_setE => NDr. -apply: setDidl. -apply/disjoints_subset. -apply/subsetCr. -by move=> _ ->. -Qed. +Proof. Admitted. Section integral_itv. Local Open Scope ereal_scope. @@ -841,40 +823,25 @@ Context {R : realType}. Local Notation mu := (@lebesgue_measure R). +(* PR#1327 *) Lemma integral_setD1_EFin' (f : R -> R) r (D : set R) : measurable (D `\ r) -> measurable_fun (D `\ r) f -> \int[mu]_(x in D `\ r) (f x)%:E = \int[mu]_(x in D) (f x)%:E. -Proof. -move=> mD mf. -have [Dr|NDr] := pselect (D r); last by rewrite notin_setD1K// notin_setE. -rewrite -[in RHS](@setD1K _ r D)// integral_setU_EFin//. -- by rewrite integral_set1// ?add0e. -- apply/measurable_funU => //; split => //. - exact: measurable_fun_set1. -- by rewrite disj_set2E; apply/eqP/seteqP; split => // x [? []]. -Qed. +Proof. Admitted. -(* PR *) +(* PR#1327 *) Lemma integral_itv_bndo_bndc' (a : itv_bound R) (r : R) (f : R -> R) : measurable_fun [set` Interval a (BLeft r)] f -> \int[mu]_(x in [set` Interval a (BLeft r)]) (f x)%:E = \int[mu]_(x in [set` Interval a (BRight r)]) (f x)%:E. -Proof. -move=> mf; have [ar|ar] := leP a (BLeft r). -- by rewrite -[RHS](@integral_setD1_EFin' _ r) ?setDitv1r. -- by rewrite !set_itv_ge// -leNgt// ltW. -Qed. +Proof. Admitted. -(* PR *) +(* PR#1327 *) Lemma integral_itv_obnd_cbnd' (r : R) (b : itv_bound R) (f : R -> R) : measurable_fun [set` Interval (BRight r) b] f -> \int[mu]_(x in [set` Interval (BRight r) b]) (f x)%:E = \int[mu]_(x in [set` Interval (BLeft r) b]) (f x)%:E. -Proof. -move=> mf; have [rb|rb] := leP (BRight r) b. -- rewrite -[RHS](@integral_setD1_EFin' _ r) ?setDitv1l//. -- by rewrite !set_itv_ge// -leNgt -?ltBRight_leBLeft// ltW. -Qed. +Proof. Admitted. End integral_itv. @@ -894,7 +861,110 @@ Lemma increasing_change F G a b : (a < b)%R -> \int[mu]_(x in `[F a, F b]) (G x)%:E = \int[mu]_(x in `[a, b]) (((G \o F) * F^`()) x)%:E. Proof. -move=> ab incrF cf /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] dcbF cG. +move=> ab incrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] dcbF cG. +have cF := (derivable_oo_continuous_bnd_within dcbF). +have FaFb : (F a < F b)%R by apply: incrF; rewrite //= in_itv/= (ltW ab) lexx. +have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R. + apply: measurable_funM. + - apply: (measurable_comp (measurable_itv `]F a, F b[)). + exact: increasing_image_oo. + apply: subspace_continuous_measurable_fun => //. + apply: continuous_in_subspaceT => x; rewrite inE/=. + move/(continuous_within_itvP _ FaFb) : cG => [+ _ _]; exact. + - apply: subspace_continuous_measurable_fun => //. + apply: continuous_in_subspaceT => x; rewrite inE/=. + move/(continuous_within_itvP _ ab) : cF => [+ _ _]; exact. + - apply: subspace_continuous_measurable_fun; first by []. + apply: continuous_in_subspaceT => x. + rewrite inE/=. + exact: cF'. +have intGFb : mu.-integrable `[(F a), (F b)] (EFin \o G). + by apply: continuous_compact_integrable => //; exact: segment_compact. +pose PG x := parameterized_integral mu (F a) x G. +rewrite (@continuous_FTC2 _ _ PG _ _ FaFb cG); last 2 first. +- split. + + move=> x /[dup]xFaFb; rewrite in_itv/= => /andP[Fax xFb]. + apply: (continuous_FTC1 xFb intGFb Fax _).1. + have/(continuous_within_itvP _ FaFb)[+ _ _] := cG; exact. + + have := parameterized_integral_continuous FaFb intGFb. + by move=> /(continuous_within_itvP _ FaFb)[]. + + exact: parameterized_integral_cvg_at_left. +- move=> x xFaFb. + have xFb : (x < F b)%R by move: xFaFb; rewrite in_itv/= => /andP[]. + apply: (continuous_FTC1 xFb _ _ _).2 => //=. + by move: (xFaFb); rewrite lte_fin in_itv/= => /andP[]. + exact: (within_continuous_continuous _ _ xFaFb). +set f := fun x => if x == a then r else if x == b then l else F^`() x. +have fE : {in `]a, b[, F^`() =1 f}. + move=> x; rewrite in_itv/= => /andP[ax xb]. + rewrite /f ifF; last by rewrite gt_eqF. + by rewrite ifF// lt_eqF. +rewrite -(@continuous_FTC2 _ ((G \o F) * f)%R (PG \o F) _ _ ab); last 3 first. +- apply/(continuous_within_itvP _ ab); split. + + move=> x xab. + apply: continuousM; first apply: continuous_comp. + * by move/(continuous_within_itvP _ ab) : cF => [+ _ _]; exact. + * move/(continuous_within_itvP _ FaFb) : cG => [+ _ _]; apply. + exact: increasing_image_oo. + * have : F^`() @ x --> f x by rewrite -fE//; exact: cF'. + apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl. + apply: (@in_nearW _ _ `]a, b[); last by rewrite inE. + exact: interval_open. + move=> z; rewrite inE/=; exact: fE. + + apply: cvgM. + apply: (increasing_cvg_at_right_comp ab) => //. x y. + by apply: incrF; apply: subset_itv_co_cc. + rewrite {2}/f eq_refl. + move: F'ar. + apply: cvg_trans. + apply: near_eq_cvg. + near=> z. + rewrite /f ifF; last by rewrite gt_eqF. + by rewrite ifF// lt_eqF. + - apply: cvgM. + apply: (increasing_cvg_at_left_comp ab) => //x y xab yab. + by apply: incrF; apply: subset_itv_oc_cc. + rewrite {2}/f ifF; last by rewrite gt_eqF. + rewrite eq_refl. + move: F'bl. + apply: cvg_trans. + apply: near_eq_cvg. + near=> z. + rewrite /f ifF; last by rewrite gt_eqF. + by rewrite ifF// lt_eqF. + + + + + + + +move/(continuous_within_itvP _ ab) : + by apply: incG; exact: increasing_image_oo. +- +- +rewrite -integral_itv_bndo_bndc'; last first. + rewrite -setU1itv ?bnd_simp//. + by rewrite measurable_funU//; split => //; apply: measurable_fun_set1. +rewrite -integral_itv_obnd_cbnd'; last exact: mGFF'. +- apply/(continuous_within_itvP _ ab); split. + + move=> x xab. + apply: continuousM; last exact: cf. + apply: continuous_comp. + * have:= derivable_oo_continuous_bnd_within dcbF. + by move/(continuous_within_itvP _ ab) => [+ _ _]; exact. + * move/(continuous_within_itvP _ FaFb): cG => [+ _ _]; apply. + exact: increasing_image_oo. + + apply: cvgM. + +- +- admit. +rewrite -integral_itv_bndo_bndc'; last first. +- rewrite -setU1itv; last by rewrite bnd_simp. + by rewrite measurable_funU//; split => //; exact: measurable_fun_set1. +by rewrite -integral_itv_obnd_cbnd'//. + + +=== + set f : R -> R := fun x => if x == a then r else if x == b then l else F^`() x. have FaFb : (F a < F b)%R by apply: incrF; rewrite //= in_itv/= (ltW ab) lexx. From e4dbf34ecc951cb9f89cc12cbc63c7d507696371 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Tue, 1 Oct 2024 10:26:58 +0900 Subject: [PATCH 09/16] generalize in_nearW --- theories/ftc.v | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 5e4bd60c43..eddcf2afd3 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -798,19 +798,9 @@ Lemma in_nearW (R : topologicalType) (P : R -> Prop) (S : set R) : Proof. move=> oS HP z. rewrite inE => Sz. -have [e/= e0 He] := (open_subball oS Sz). -exists (e / 2) => //=. - by rewrite -(add0r e) midf_lt. -move=> t/= zte. -apply: HP. -move: He Sz zte. -have [<- |zt He Sz zte] := eqVneq z t; first by rewrite inE. -rewrite inE. -apply: (He (e / 2)) => //=. -rewrite sub0r normrN ger0_norm. - by rewrite -{1}(add0r e) midf_lt. - by rewrite -(add0r e) midf_le// ltW. -by rewrite -(add0r e) midf_lt. +rewrite -nbhs_nearE nbhsE/=. +exists S => //. +by move=> x /mem_set/HP. Qed. (* PR#1327 *) From 19dbb01ff79153f3ab703e7c761307496e1d8bfe Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Tue, 1 Oct 2024 16:25:15 +0900 Subject: [PATCH 10/16] cleaning --- theories/ftc.v | 273 ++++++++++--------------------------------------- 1 file changed, 53 insertions(+), 220 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index eddcf2afd3..907d9aa444 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -784,57 +784,6 @@ Unshelve. all: end_near. Qed. End integration_by_substitution_preliminaries. -(* PR#1327 *) -Lemma measurable_fun_set1 d d' (T : measurableType d) (U : measurableType d') - (a : T) (f : T -> U) : -measurable_fun (set1 a) f. -Proof. Admitted. - -(* PR *) -Lemma in_nearW (R : topologicalType) (P : R -> Prop) (S : set R) : - @open R^o S -> - {in S, forall x, P x} -> - forall x, x \in S -> \forall y \near x, P y. -Proof. -move=> oS HP z. -rewrite inE => Sz. -rewrite -nbhs_nearE nbhsE/=. -exists S => //. -by move=> x /mem_set/HP. -Qed. - -(* PR#1327 *) -Lemma notin_setD1K (T : Type) (r : T) (D : set T) : r \notin D -> D `\ r = D. -Proof. Admitted. - -Section integral_itv. -Local Open Scope ereal_scope. -Context {R : realType}. - -Local Notation mu := (@lebesgue_measure R). - -(* PR#1327 *) -Lemma integral_setD1_EFin' (f : R -> R) r (D : set R) : - measurable (D `\ r) -> measurable_fun (D `\ r) f -> - \int[mu]_(x in D `\ r) (f x)%:E = \int[mu]_(x in D) (f x)%:E. -Proof. Admitted. - -(* PR#1327 *) -Lemma integral_itv_bndo_bndc' (a : itv_bound R) (r : R) (f : R -> R) : - measurable_fun [set` Interval a (BLeft r)] f -> - \int[mu]_(x in [set` Interval a (BLeft r)]) (f x)%:E = - \int[mu]_(x in [set` Interval a (BRight r)]) (f x)%:E. -Proof. Admitted. - -(* PR#1327 *) -Lemma integral_itv_obnd_cbnd' (r : R) (b : itv_bound R) (f : R -> R) : - measurable_fun [set` Interval (BRight r) b] f -> - \int[mu]_(x in [set` Interval (BRight r) b]) (f x)%:E = - \int[mu]_(x in [set` Interval (BLeft r) b]) (f x)%:E. -Proof. Admitted. - -End integral_itv. - Section integration_by_substitution. Local Open Scope ereal_scope. Context {R : realType}. @@ -871,6 +820,17 @@ have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R. have intGFb : mu.-integrable `[(F a), (F b)] (EFin \o G). by apply: continuous_compact_integrable => //; exact: segment_compact. pose PG x := parameterized_integral mu (F a) x G. +have dcbPG : derivable_oo_continuous_bnd PG (F a) (F b). + have [/= dF rF lF] := dcbF. + split => /=. + - move=> x xFaFb /=. + have xFb : (x < F b)%R by move: xFaFb; rewrite in_itv/= => /andP[]. + apply: (continuous_FTC1 xFb intGFb _ _).1 => /=. + by move: (xFaFb); rewrite lte_fin in_itv/= => /andP[]. + exact: (within_continuous_continuous _ _ xFaFb). + - have := parameterized_integral_continuous FaFb intGFb. + by move=> /(continuous_within_itvP _ FaFb)[]. + - exact: parameterized_integral_cvg_at_left. rewrite (@continuous_FTC2 _ _ PG _ _ FaFb cG); last 2 first. - split. + move=> x /[dup]xFaFb; rewrite in_itv/= => /andP[Fax xFb]. @@ -898,139 +858,36 @@ rewrite -(@continuous_FTC2 _ ((G \o F) * f)%R (PG \o F) _ _ ab); last 3 first. exact: increasing_image_oo. * have : F^`() @ x --> f x by rewrite -fE//; exact: cF'. apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl. - apply: (@in_nearW _ _ `]a, b[); last by rewrite inE. + apply: (@open_in_nearW _ _ `]a, b[); last by rewrite inE. exact: interval_open. move=> z; rewrite inE/=; exact: fE. + apply: cvgM. - apply: (increasing_cvg_at_right_comp ab) => //. x y. - by apply: incrF; apply: subset_itv_co_cc. + apply: (increasing_cvg_at_right_comp ab) => //. + move=> x y xab yab. + by apply: incrF; apply: subset_itv_co_cc. + by move/continuous_within_itvP : cF => /(_ ab)[]. + by move/continuous_within_itvP : cG => /(_ FaFb)[]. rewrite {2}/f eq_refl. move: F'ar. apply: cvg_trans. apply: near_eq_cvg. near=> z. - rewrite /f ifF; last by rewrite gt_eqF. - by rewrite ifF// lt_eqF. - - apply: cvgM. - apply: (increasing_cvg_at_left_comp ab) => //x y xab yab. - by apply: incrF; apply: subset_itv_oc_cc. - rewrite {2}/f ifF; last by rewrite gt_eqF. - rewrite eq_refl. - move: F'bl. - apply: cvg_trans. - apply: near_eq_cvg. - near=> z. - rewrite /f ifF; last by rewrite gt_eqF. - by rewrite ifF// lt_eqF. - - + - + - - -move/(continuous_within_itvP _ ab) : - by apply: incG; exact: increasing_image_oo. -- -- -rewrite -integral_itv_bndo_bndc'; last first. - rewrite -setU1itv ?bnd_simp//. - by rewrite measurable_funU//; split => //; apply: measurable_fun_set1. -rewrite -integral_itv_obnd_cbnd'; last exact: mGFF'. -- apply/(continuous_within_itvP _ ab); split. - + move=> x xab. - apply: continuousM; last exact: cf. - apply: continuous_comp. - * have:= derivable_oo_continuous_bnd_within dcbF. - by move/(continuous_within_itvP _ ab) => [+ _ _]; exact. - * move/(continuous_within_itvP _ FaFb): cG => [+ _ _]; apply. - exact: increasing_image_oo. + by rewrite fE// in_itv/=; apply/andP; split. + apply: cvgM. - -- -- admit. -rewrite -integral_itv_bndo_bndc'; last first. -- rewrite -setU1itv; last by rewrite bnd_simp. - by rewrite measurable_funU//; split => //; exact: measurable_fun_set1. -by rewrite -integral_itv_obnd_cbnd'//. - - -=== - -set f : R -> R := fun x => if x == a then r else - if x == b then l else F^`() x. -have FaFb : (F a < F b)%R by apply: incrF; rewrite //= in_itv/= (ltW ab) lexx. -pose PG x := parameterized_integral mu (F a) x G. -have intGFb : mu.-integrable `[(F a), (F b)] (EFin \o G). - by apply: continuous_compact_integrable => //; exact: segment_compact. -set H := PG \o F. -set h : R -> R := ((G \o F) * f)%R. -have dcbPG : derivable_oo_continuous_bnd PG (F a) (F b). - have [/= dF rF lF] := dcbF. - split => /=. - - move=> x xFaFb /=. - have xFb : (x < F b)%R by move: xFaFb; rewrite in_itv/= => /andP[]. - apply: (continuous_FTC1 xFb intGFb _ _).1 => /=. - by move: (xFaFb); rewrite lte_fin in_itv/= => /andP[]. - exact: (within_continuous_continuous _ _ xFaFb). - - have := parameterized_integral_continuous FaFb intGFb. - by move=> /(continuous_within_itvP _ FaFb)[]. - - exact: parameterized_integral_cvg_at_left. -have dPGE : {in `](F a), (F b)[, PG^`() =1 G}. - move=> x xFaFb. - have xFb : (x < F b)%R by move: xFaFb; rewrite in_itv/= => /andP[]. - apply: (continuous_FTC1 xFb intGFb _ _).2 => //=. - by move: (xFaFb); rewrite lte_fin in_itv/= => /andP[]. - exact: (within_continuous_continuous _ _ xFaFb). -move/continuous_within_itvP : (cG) => /(_ FaFb)[incG GFa GFb]. -have cF : {within `[a, b], continuous F} := - derivable_oo_continuous_bnd_within dcbF. -move/continuous_within_itvP : (cF) => /(_ ab)[incF cFa cFb]. -have ch : {within `[a, b], continuous h}. - apply/(continuous_within_itvP _ ab); split. - - move=> /= x xab. - apply: continuousM; last first. - have : F^`() y @[y --> x] --> f x. - rewrite /f. - rewrite ifF; last first. - apply: gt_eqF. - by move: xab; rewrite in_itv/= => /andP[]. - rewrite ifF; last first. - apply: lt_eqF. - by move: xab; rewrite in_itv/= => /andP[]. - exact: cf. - apply: cvg_trans. - apply: near_eq_cvg. - rewrite near_simpl. - apply: (@in_nearW _ _ `]a, b[%classic). - - exact: interval_open. - - move=> z; rewrite inE/= in_itv/= => /andP[az zb]. - rewrite /f ifF; last by rewrite gt_eqF. - by rewrite ifF// lt_eqF. - by rewrite inE. - apply: continuous_comp; first exact: incF. - by apply: incG; exact: increasing_image_oo. - - apply: cvgM. - apply: (increasing_cvg_at_right_comp ab) => //x y xab yab. - by apply: incrF; apply: subset_itv_co_cc. - rewrite {2}/f eq_refl. - move: F'ar. - apply: cvg_trans. - apply: near_eq_cvg. - near=> z. - rewrite /f ifF; last by rewrite gt_eqF. - by rewrite ifF// lt_eqF. - - apply: cvgM. - apply: (increasing_cvg_at_left_comp ab) => //x y xab yab. - by apply: incrF; apply: subset_itv_oc_cc. + apply: (increasing_cvg_at_left_comp ab). + move=> //x y xab yab. + by apply: incrF; apply: subset_itv_oc_cc. + by move/continuous_within_itvP : cF => /(_ ab) []. + by move/continuous_within_itvP : cG => /(_ FaFb) []. rewrite {2}/f ifF; last by rewrite gt_eqF. rewrite eq_refl. move: F'bl. apply: cvg_trans. apply: near_eq_cvg. near=> z. - rewrite /f ifF; last by rewrite gt_eqF. - by rewrite ifF// lt_eqF. -have dcbH : derivable_oo_continuous_bnd H a b. - have := derivable_oo_continuous_bnd_within dcbPG. + by rewrite fE// in_itv/=; apply/andP; split. +- have := derivable_oo_continuous_bnd_within dcbPG. + have [/= dF rF lF] := dcbF. move=> /(continuous_within_itvP _ FaFb)[_ PGFa PGFb]. split => /=. - move=> x xab. @@ -1041,7 +898,7 @@ have dcbH : derivable_oo_continuous_bnd H a b. by apply; exact: increasing_image_oo. - apply/cvgrPdist_le => /= e e0. have/cvgrPdist_le /(_ e e0) [d /= d0 {}PGFa] := PGFa. - have := cvg_at_right_within cFa. + have := cvg_at_right_within rF. move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFa]. near=> t. apply: PGFa; last by apply: incrF; rewrite //in_itv/= ?lexx !ltW. @@ -1050,59 +907,35 @@ have dcbH : derivable_oo_continuous_bnd H a b. by near: t; exact: nbhs_right_ltDr. - apply/cvgrPdist_le => /= e e0. have/cvgrPdist_le /(_ e e0) [d /= d0 {}PGFb] := PGFb. - have := cvg_at_left_within cFb. + have := cvg_at_left_within lF. move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFb]. near=> t. apply: (PGFb); last by apply: incrF; rewrite //in_itv/= ?lexx !ltW. apply: cFb => //=. rewrite gtr0_norm// ?subr_gt0//. by near: t; exact: nbhs_left_ltBl. -have dHE : {in `]a, b[, H^`() =1 h}. - move=> x xab; rewrite derive1_comp. - - rewrite dPGE//; last exact: increasing_image_oo. - rewrite /h/f. - move: xab. - rewrite in_itv/= => /andP[ax xb]. - rewrite mulrfctE ifF; last by rewrite gt_eqF. - by rewrite ifF// lt_eqF. - - by have [+ _ _] := dcbF; apply. - - by have [+ _ _] := dcbPG; apply; exact: increasing_image_oo. -rewrite (continuous_FTC2 FaFb cG dcbPG dPGE). -rewrite -(continuous_FTC2 ab ch dcbH dHE). -have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R. - apply: measurable_funM. - - apply: (measurable_comp (measurable_itv `]F a, F b[)). - exact: increasing_image_oo. - apply: subspace_continuous_measurable_fun => //. - apply: continuous_in_subspaceT => x; rewrite inE/=. - exact: incG. - - apply: subspace_continuous_measurable_fun => //. - apply: continuous_in_subspaceT => x; rewrite inE/=. - exact: incF. - - apply: subspace_continuous_measurable_fun; first by []. - apply: continuous_in_subspaceT => x. - rewrite inE/=. - exact: cf. -rewrite -!integral_itv_bndo_bndc'; last 2 first. -- rewrite -setU1itv ?bnd_simp//. - by rewrite measurable_funU//; split => //; apply: measurable_fun_set1. -- apply: subspace_continuous_measurable_fun => //. - move: ch; apply: continuous_subspaceW. - exact: subset_itv_co_cc. -rewrite -!integral_itv_obnd_cbnd'; last 2 first. -- exact: mGFF'. -- apply: subspace_continuous_measurable_fun => //. - move: ch; apply: continuous_subspaceW. - exact: subset_itv_oo_cc. -apply: eq_integral => //. -move=> x xab. -rewrite /h/f. -rewrite mulrfctE ifF; last first. - apply: gt_eqF. - by move: xab; rewrite inE/= in_itv/= => /andP[]. -rewrite ifF//. -apply: lt_eqF. -by move: xab; rewrite inE/= in_itv/= => /andP[]. +- move=> x /[dup]xab /andP[ax xb]; rewrite derive1_comp. + + congr (_ * _)%R. + * have /[dup]FxFaFb : F x \in `]F a, F b[ by exact: increasing_image_oo. + rewrite in_itv/= => /andP[FaFx FxFb]. + apply: (continuous_FTC1 FxFb intGFb FaFx _).2 => //=. + exact: (within_continuous_continuous _ _ FxFaFb). + * by rewrite fE. + + by have [+ _ _] := dcbF; apply. + + by have [+ _ _] := dcbPG; apply; exact: increasing_image_oo. +have mGFf : measurable_fun `]a, b[ ((G \o F) * f)%R. + apply: (eq_measurable_fun ((G \o F) * F^`())%R) => //. + move=> x; rewrite inE/= => xab; congr (_ * _)%R. + by rewrite fE. +rewrite -!integral_itv_bndo_bndc; last 2 first. +- rewrite -setU1itv ?bnd_simp// measurable_funU//; split => //. + exact: measurable_fun_set1. +- rewrite -setU1itv ?bnd_simp// measurable_funU//; split => //. + exact: measurable_fun_set1. +rewrite -!integral_itv_obnd_cbnd//. +apply: eq_integral => x; rewrite inE/= => xab. +congr (EFin (_ * _)%R). +by rewrite fE. Unshelve. all: end_near. Qed. Lemma decreasing_change F G a b : (a < b)%R -> @@ -1163,7 +996,7 @@ have cNh : {within `[a, b], continuous (- h)%R}. apply: cvg_trans. apply: near_eq_cvg. rewrite near_simpl. - apply: (@in_nearW _ _ `]a, b[%classic). + apply: (@open_in_nearW _ _ `]a, b[%classic). - exact: interval_open. - move=> z; rewrite inE/= in_itv/= => /andP[az zb]. rewrite !fctE; congr (- _)%R. @@ -1252,14 +1085,14 @@ have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R. apply: continuous_in_subspaceT => x. rewrite inE/=. exact: cf. -rewrite -!integral_itv_bndo_bndc'; last 2 first. +rewrite -!integral_itv_bndo_bndc; last 2 first. - rewrite -setU1itv ?bnd_simp//. rewrite mulrN; apply: measurableT_comp => //. by rewrite measurable_funU//; split => //; apply: measurable_fun_set1. - apply: subspace_continuous_measurable_fun => //. move: cNh; apply: continuous_subspaceW. exact: subset_itv_co_cc. -rewrite -!integral_itv_obnd_cbnd'; last 2 first. +rewrite -!integral_itv_obnd_cbnd; last 2 first. - rewrite mulrN. exact: measurableT_comp => //. - apply: subspace_continuous_measurable_fun => //. From ed8d3e13941b8bf58b073be33338c612ed32a056 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Wed, 2 Oct 2024 15:52:54 +0900 Subject: [PATCH 11/16] increasing_change2 --- theories/ftc.v | 286 +++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 277 insertions(+), 9 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 907d9aa444..960b4b6e1f 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -784,6 +784,38 @@ Unshelve. all: end_near. Qed. End integration_by_substitution_preliminaries. +Lemma integral_itv_oo (R : realType) (f : R -> R) (b0 b1 : bool) (x y : R) : + measurable_fun `]x, y[ f -> + (\int[lebesgue_measure]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (f z)%:E = + \int[lebesgue_measure]_(z in `]x, y[) (f z)%:E)%E. +Proof. +have [xy|yx _|-> _] := ltgtP x y; last 2 first. + rewrite !set_itv_ge ?integral_set0//=. + by rewrite bnd_simp le_gtF// ltW. + by case b0; case: b1; rewrite bnd_simp ?lt_geF// le_gtF// ltW. + by case: b0; case: b1; rewrite !set_itvE ?integral_set0 ?integral_set1. +move=> mf. +transitivity (\int[lebesgue_measure]_(z in [set` Interval (BSide b0 x) (BLeft y)]) (f z)%:E)%E. + case: b1 => //. + rewrite -integral_itv_bndo_bndc//. + case: b0 => //. + rewrite -setU1itv ?bnd_simp// measurable_funU//; split => //. + exact: measurable_fun_set1. +by case: b0 => //; rewrite -integral_itv_obnd_cbnd. +Qed. + +Lemma eq_integral_itvoo (R : realType) (g f : R -> R) (b0 b1 : bool) (x y : R) : + measurable_fun `]x, y[ f -> + measurable_fun `]x, y[ g -> + {in `]x, y[, f =1 g} -> + (\int[lebesgue_measure]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (f z)%:E = + \int[lebesgue_measure]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (g z)%:E)%E. +Proof. +move=> mf mg fg. +rewrite integral_itv_oo// (@integral_itv_oo _ g)//. +by apply: eq_integral => z; rewrite inE/= => zxy; congr EFin; exact: fg. +Qed. + Section integration_by_substitution. Local Open Scope ereal_scope. Context {R : realType}. @@ -927,14 +959,8 @@ have mGFf : measurable_fun `]a, b[ ((G \o F) * f)%R. apply: (eq_measurable_fun ((G \o F) * F^`())%R) => //. move=> x; rewrite inE/= => xab; congr (_ * _)%R. by rewrite fE. -rewrite -!integral_itv_bndo_bndc; last 2 first. -- rewrite -setU1itv ?bnd_simp// measurable_funU//; split => //. - exact: measurable_fun_set1. -- rewrite -setU1itv ?bnd_simp// measurable_funU//; split => //. - exact: measurable_fun_set1. -rewrite -!integral_itv_obnd_cbnd//. -apply: eq_integral => x; rewrite inE/= => xab. -congr (EFin (_ * _)%R). +apply: eq_integral_itvoo => //x; rewrite inE/= => xab. +congr (_ * _)%R. by rewrite fE. Unshelve. all: end_near. Qed. @@ -1118,6 +1144,248 @@ apply: lt_eqF. by move: xab; rewrite inE/= in_itv/= => /andP[]. Unshelve. all: end_near. Qed. +Lemma oppr_change G a b : (a < b)%R -> + {within `[(- b)%R, (- a)%R], continuous G} -> + \int[mu]_(x in `[(- b)%R, (- a)%R]) (G x)%:E = + \int[mu]_(x in `[a, b]) ((G \o -%R) x)%:E. +Proof. +move=> ab cG. +have Dopp: (@GRing.opp R)^`() = cst (-1)%R :> (R -> R). + apply/funext => z. + rewrite derive1E. + exact: derive_val. +rewrite (@decreasing_change -%R)//. +- apply: eq_integral => //= x; rewrite inE/= => xab. + congr (EFin _). + rewrite !fctE -[RHS]mulr1; congr (_ * _)%R. + rewrite derive1E. + rewrite deriveN//. + rewrite opprK. + exact: derive_val. +- by move=> ? ? _ _; rewrite ltrN2. +- rewrite Dopp. + move=> ? _; exact: cvg_cst. +- rewrite Dopp. + apply: is_cvgN. + exact: is_cvg_cst. +- rewrite Dopp. + apply: is_cvgN. + exact: is_cvg_cst. +- split. + + by move=> x _. + + rewrite -at_leftN. + exact: cvg_at_left_filter. + + rewrite -at_rightN. + exact: cvg_at_right_filter. +Qed. + +Lemma increasing_change2 F G a b : (a < b)%R -> + {in `[a, b] &, {homo F : x y / (x < y)%R}} -> + {in `]a, b[, continuous F^`()} -> + cvg ((F^`() : R -> R) x @[x --> a^'+]) -> + cvg ((F^`() : R -> R) x @[x --> b^'-]) -> + derivable_oo_continuous_bnd F a b -> + {within `[F a, F b], continuous G} -> + \int[mu]_(x in `[F a, F b]) (G x)%:E = + \int[mu]_(x in `[a, b]) (((G \o F) * F^`()) x)%:E. +Proof. +move=> ab incrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] dcbF cG. +have cF := (derivable_oo_continuous_bnd_within dcbF). +have FaFb : (F a < F b)%R by apply: incrF; rewrite //= in_itv/= (ltW ab) lexx. +set f := fun x => if x == a then r else if x == b then l else F^`() x. +have fE : {in `]a, b[, F^`() =1 f}. + move=> x; rewrite in_itv/= => /andP[ax xb]. + rewrite /f ifF; last by rewrite gt_eqF. + by rewrite ifF// lt_eqF. +have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R. + apply: measurable_funM. + - apply: (measurable_comp (measurable_itv `]F a, F b[)). + exact: increasing_image_oo. + apply: subspace_continuous_measurable_fun => //. + apply: continuous_in_subspaceT => x; rewrite inE/=. + move/(continuous_within_itvP _ FaFb) : cG => [+ _ _]; exact. + - apply: subspace_continuous_measurable_fun => //. + apply: continuous_in_subspaceT => x; rewrite inE/=. + move/(continuous_within_itvP _ ab) : cF => [+ _ _]; exact. + - apply: subspace_continuous_measurable_fun; first by []. + apply: continuous_in_subspaceT => x. + rewrite inE/=. + exact: cF'. +have intE : \int[mu]_(x in `[a, b]) (((G \o F) * F^`()) x)%:E = (\int[mu]_(x in `[a, b]) (((G \o F) * f) x)%:E). + apply: eq_integral_itvoo => //. + apply: eq_measurable_fun mGFF'. + by move=> x; rewrite inE/= => xab; congr (_ * _)%R; rewrite fE. + by move=> x xab; congr (_ * _)%R; rewrite fE. +rewrite intE. +have F'N : {in `](- b)%R, (- a)%R[, forall x, (- F^`() (- x) @[x --> x] --> (F \o -%R)^`() x)%R}. + move=> x xNbNa. + rewrite derive1_comp//; last first. + by have [+ _ _] := dcbF; apply; rewrite oppr_itvoo. + have := (@is_deriveNid _ _ x 1%R). + move/(@derive_val _ _ _ _ _ -%R). + rewrite -derive1E => ->. + rewrite mulrN1. + have cNF' : {in `]-%R b, -%R a[, continuous (F^`() \o -%R)}. + move=> z; rewrite -oppr_itvoo => Nzab. + apply: continuous_comp. + exact: opp_continuous. + exact: cF'. + apply: cvgN. + suff : F^`() (- x0) @[x0 --> x] --> F^`() (- x) by []. + rewrite -/(F^`() \o -%R) -/((F^`() \o -%R) x). + exact: cNF'. +rewrite -(opprK a) -(opprK b). +rewrite oppr_change; last 2 first. +- by rewrite ltrN2. +- rewrite !opprK; apply/(continuous_within_itvP _ ab); split. + + move=> x /[dup]xab; rewrite in_itv/= => /andP[ax xb]. + apply: continuousM. + apply: continuous_comp. + by move/(continuous_within_itvP _ ab) : cF => [+ _ _]; exact. + move/(continuous_within_itvP _ FaFb) : cG => [+ _ _]; apply. + exact: increasing_image_oo. + have : F^`() @ x --> f x by rewrite -fE//; exact: cF'. + apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl. + apply: (@open_in_nearW _ _ `]a, b[); last by rewrite inE. + exact: interval_open. + move=> z; rewrite inE/=; exact: fE. + + apply: cvgM. + apply: (increasing_cvg_at_right_comp ab) => //. + move=> x y xab yab. + by apply: incrF; apply: subset_itv_co_cc. + by move/continuous_within_itvP : cF => /(_ ab)[]. + by move/continuous_within_itvP : cG => /(_ FaFb)[]. + rewrite {2}/f eq_refl. + move: F'ar. + apply: cvg_trans. + apply: near_eq_cvg. + near=> z. + by rewrite fE// in_itv/=; apply/andP; split. + + apply: cvgM. + apply: (increasing_cvg_at_left_comp ab). + move=> //x y xab yab. + by apply: incrF; apply: subset_itv_oc_cc. + by move/continuous_within_itvP : cF => /(_ ab) []. + by move/continuous_within_itvP : cG => /(_ FaFb) []. + rewrite {2}/f ifF; last by rewrite gt_eqF. + rewrite eq_refl. + move: F'bl. + apply: cvg_trans. + apply: near_eq_cvg. + near=> z. + by rewrite fE// in_itv/=; apply/andP; split. +rewrite (@decreasing_change (F \o -%R) G (- b)%R (- a)%R); last 7 first. +- by rewrite ltrN2. + move=> x y; rewrite -!oppr_itvcc => Nxab Nyab; rewrite -ltrN2 => NxNy. + exact: incrF. +- move=> x xNbNa. + move: (F'N x xNbNa). + apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl. + apply: (@open_in_nearW _ _ `]-%R b, -%R a[); last by rewrite inE. + exact: interval_open. + move=> z; rewrite inE/= -oppr_itvoo => Nzab. + rewrite [RHS]derive1_comp//; last first. + have [+ _ _] := dcbF; exact. + have := (@is_deriveNid _ _ z 1%R). + move/(@derive_val _ _ _ _ _ -%R). + rewrite -derive1E => ->. + by rewrite mulrN1. +- apply/(cvgP (- l)%R). + have : -%R (F^`() \o -%R) x @[x --> (-b)^'+] --> (- l)%R. + apply: cvgN. + exact/cvg_at_leftNP. + apply: cvg_trans. + apply: near_eq_cvg. + near=> z. + rewrite derive1_comp//; last first. + have [+ _ _] := dcbF; apply; rewrite in_itv/=; apply/andP; split. + rewrite ltrNr//. + near: z. + apply: nbhs_right_lt. + by rewrite ltrN2. + by rewrite ltrNl. + have := (@is_deriveNid _ _ z 1%R). + move/(@derive_val _ _ _ _ _ -%R). + rewrite -derive1E => ->. + by rewrite mulrN1. +- apply/(cvgP (- r)%R). + have : -%R (F^`() \o -%R) x @[x --> (-a)^'-] --> (- r)%R. + apply: cvgN. + exact/cvg_at_rightNP. + apply: cvg_trans. + apply: near_eq_cvg. + near=> z. + rewrite derive1_comp//; last first. + have [+ _ _] := dcbF; apply; rewrite in_itv/=; apply/andP; split. + by rewrite ltrNr. + rewrite ltrNl//. + near: z. + apply: nbhs_left_gt. + by rewrite ltrN2. + have := (@is_deriveNid _ _ z 1%R). + move/(@derive_val _ _ _ _ _ -%R). + rewrite -derive1E => ->. + by rewrite mulrN1. +- split. + + move=> x xNbNa. + apply: diff_derivable. + apply: differentiable_comp => //. + apply/derivable1_diffP. + have [+ _ _] := dcbF; apply. + by rewrite oppr_itvoo. + + apply/cvg_at_leftNP; rewrite fctE opprK. + by have [] := dcbF. + + apply/cvg_at_rightNP; rewrite fctE opprK. + by have [] := dcbF. +- by rewrite fctE !opprK. +have mGFNDFN : measurable_fun `](- b)%R, (- a)%R[ ((G \o (F \o -%R)) * - (F \o -%R)^`())%R. + apply: measurable_funM. + - rewrite compA. + apply: (measurable_comp (measurable_itv `]a, b[)) => //. + by move=> _/=[x + <-]; rewrite oppr_itvoo. + apply: (measurable_comp (measurable_itv `]F a, F b[)). + exact: increasing_image_oo. + apply: subspace_continuous_measurable_fun => //. + move: cG. + apply: continuous_subspaceW. + exact: subset_itv_oo_cc. + apply: subspace_continuous_measurable_fun => //. + move: cF. + apply: continuous_subspaceW. + exact: subset_itv_oo_cc. + - apply: measurableT_comp => //. + apply: (eq_measurable_fun (- (F^`() \o -%R))%R). + move=> x. + rewrite inE/= -oppr_itvoo => Nxab. + rewrite derive1_comp//; last by have [+ _ _] := dcbF; apply. + have := (@is_deriveNid _ _ x 1%R). + move/(@derive_val _ _ _ _ _ -%R). + rewrite -derive1E => ->. + by rewrite mulrN1. + apply: measurableT_comp => //. + apply: (measurable_comp (measurable_itv `]a, b[)) => //. + by move=> _ [x /= + <-]; rewrite -oppr_itvoo. + apply: open_continuous_measurable_fun. + exact: interval_open. + move=> x; rewrite inE/= => xab. + exact: cF'. +apply: (eq_integral_itvoo _ _ mGFNDFN). + apply: (measurable_comp (measurable_itv `]a, b[)) => //. + by move=> _ [x /= + <-]; rewrite oppr_itvoo. + apply: (eq_measurable_fun ((G \o F) * F^`())%R) => //. + move=> x; rewrite inE/= => xab; congr (_ * _)%R. + by rewrite fE. +move=> x; rewrite -oppr_itvoo => Nxab. +rewrite fctE; congr (_ * _)%R. +rewrite -fE// -[RHS]opprK; congr -%R. +rewrite derive1_comp//; last first. + by have [+ _ _] := dcbF; apply. +have := (@is_deriveNid _ _ x 1%R). +move/(@derive_val _ _ _ _ _ -%R). +rewrite -derive1E => ->. +by rewrite mulrN1. +Unshelve. all: end_near. Qed. + End integration_by_substitution. Module old_integration_by_substitution. @@ -1137,7 +1405,7 @@ Lemma increasing_change_old F G a b : (a < b)%R -> Proof. move=> ab incrF. move/(continuous_within_itvP _ ab) => [+ /cvgP + /cvgP]. -exact: (increasing_change ab incrF). +exact: (increasing_change2 ab incrF). Qed. Lemma decreasing_change_old F G a b : From 9264eb20dbc0715aee8fb42725a346786a5fa433 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Thu, 3 Oct 2024 09:24:34 +0900 Subject: [PATCH 12/16] cleaning, increasing_change from decreasing_change --- theories/ftc.v | 237 +++++++++++++++++++++++++------------------------ 1 file changed, 119 insertions(+), 118 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 960b4b6e1f..e9a407d362 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -974,15 +974,31 @@ Lemma decreasing_change F G a b : (a < b)%R -> \int[mu]_(x in `[F b, F a]) (G x)%:E = \int[mu]_(x in `[a, b]) (((G \o F) * (- F^`())) x)%:E. Proof. -move=> ab decrF cf /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] dcbF cG. -set f : R -> R := fun x => if x == a then r else - if x == b then l else F^`() x. +move=> ab decrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] dcbF cG. +have cF := (derivable_oo_continuous_bnd_within dcbF). have FbFa : (F b < F a)%R by apply: decrF; rewrite //= in_itv/= (ltW ab) lexx. -pose PG x := parameterized_integral mu (F b) x G. +have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R. + apply: measurable_funM. + - apply: (measurable_comp (measurable_itv `]F b, F a[)). + exact: decreasing_image_oo. + apply: subspace_continuous_measurable_fun => //. + apply: continuous_in_subspaceT => x; rewrite inE/=. + move/(continuous_within_itvP _ FbFa) : cG => [+ _ _]; exact. + - apply: subspace_continuous_measurable_fun => //. + apply: continuous_in_subspaceT => x; rewrite inE/=. + move/(continuous_within_itvP _ ab) : cF => [+ _ _]; exact. + - apply: subspace_continuous_measurable_fun; first by []. + apply: continuous_in_subspaceT => x. + rewrite inE/=. + exact: cF'. +have {}mGFF' : measurable_fun `[a, b] ((G \o F) * F^`())%R. + rewrite -setU1itv//; last by rewrite bnd_simp ltW. + rewrite measurable_funU//; split; first exact: measurable_fun_set1. + rewrite -setUitv1// measurable_funU//; split => //. + exact: measurable_fun_set1. have intGFa : mu.-integrable `[(F b), (F a)] (EFin \o G). by apply: continuous_compact_integrable => //; exact: segment_compact. -set H := PG \o F. -set h : R -> R := ((G \o F) * (- f))%R. +pose PG x := parameterized_integral mu (F b) x G. have dcbPG : derivable_oo_continuous_bnd PG (F b) (F a). have [/= dF rF lF] := dcbF. split => /=. @@ -994,154 +1010,138 @@ have dcbPG : derivable_oo_continuous_bnd PG (F b) (F a). - have := parameterized_integral_continuous FbFa intGFa. by move=> /(continuous_within_itvP _ FbFa)[]. - exact: parameterized_integral_cvg_at_left. -have dPGE : {in `](F b), (F a)[, PG^`() =1 G}. - move=> x xFbFa. +rewrite (@continuous_FTC2 _ _ PG _ _ FbFa cG); last 2 first. +- split. + + move=> x /[dup]xFbFa; rewrite in_itv/= => /andP[Fbx xFa]. + apply: (continuous_FTC1 xFa intGFa Fbx _).1. + have/(continuous_within_itvP _ FbFa)[+ _ _] := cG; exact. + + have := parameterized_integral_continuous FbFa intGFa. + by move=> /(continuous_within_itvP _ FbFa)[]. + + exact: parameterized_integral_cvg_at_left. +- move=> x xFbFa. have xFa : (x < F a)%R by move: xFbFa; rewrite in_itv/= => /andP[]. - apply: (continuous_FTC1 xFa intGFa _ _).2 => //=. + apply: (continuous_FTC1 xFa _ _ _).2 => //=. by move: (xFbFa); rewrite lte_fin in_itv/= => /andP[]. exact: (within_continuous_continuous _ _ xFbFa). -move/continuous_within_itvP : (cG) => /(_ FbFa)[incG GFb GFa]. -have cF : {within `[a, b], continuous F} := - derivable_oo_continuous_bnd_within dcbF. -move/continuous_within_itvP : (cF) => /(_ ab)[incF cFa cFb]. -have cNh : {within `[a, b], continuous (- h)%R}. - move=> x; apply: continuousN; move: x. - apply/(continuous_within_itvP _ ab); split. - - move=> /= x xab. - apply: continuousM; last first. - have : (- F^`())%R y @[y --> x] --> (- f)%R x. - apply: cvgN => //. - rewrite /f. - rewrite ifF; last first. - apply: gt_eqF. - by move: xab; rewrite in_itv/= => /andP[]. - rewrite ifF; last first. - apply: lt_eqF. - by move: xab; rewrite in_itv/= => /andP[]. - exact: cf. - apply: cvg_trans. - apply: near_eq_cvg. - rewrite near_simpl. - apply: (@open_in_nearW _ _ `]a, b[%classic). - - exact: interval_open. - - move=> z; rewrite inE/= in_itv/= => /andP[az zb]. - rewrite !fctE; congr (- _)%R. - rewrite /f ifF; last by rewrite gt_eqF. - by rewrite ifF// lt_eqF. - by rewrite inE. - apply: continuous_comp; first exact: incF. - by apply: incG; exact: decreasing_image_oo. - - apply: cvgM. - apply: (decreasing_cvg_at_right_comp ab) => //x y xab yab. - by apply: decrF; apply: subset_itv_co_cc. +set f := fun x => if x == a then r else if x == b then l else F^`() x. +have fE : {in `]a, b[, F^`() =1 f}. + move=> x; rewrite in_itv/= => /andP[ax xb]. + rewrite /f ifF; last by rewrite gt_eqF. + by rewrite ifF// lt_eqF. +have DPGFE : {in `]a, b[, (- (PG \o F))%R^`() =1 ((G \o F) * (- f))%R}. + move=> x /[dup]xab /andP[ax xb]; rewrite derive1_comp; last 2 first. + + apply: diff_derivable. + apply: differentiable_comp; apply/derivable1_diffP. + by have [+ _ _] := dcbF; apply. + have [+ _ _] := dcbPG; apply. + exact: decreasing_image_oo. + + exact: ex_derive. + have := (@is_deriveNid _ _ (PG (F x)) 1%R). + move/(@derive_val _ _ _ _ _ -%R). + rewrite fctE -derive1E => ->. + rewrite mulN1r. + rewrite mulrN. + congr -%R. + rewrite derive1_comp; last 2 first. + + by have [+ _ _] := dcbF; apply. + + by have [+ _ _] := dcbPG; apply; exact: decreasing_image_oo. + congr (_ * _)%R. + + have /[dup]FxFbFa : F x \in `]F b, F a[ by exact: decreasing_image_oo. + rewrite in_itv/= => /andP[FbFx FxFa]. + apply: (continuous_FTC1 FxFa intGFa FbFx _).2 => //=. + exact: (within_continuous_continuous _ _ FxFbFa). + + by rewrite fE. +rewrite -[LHS]oppeK oppeB// addrC. +under eq_integral do rewrite mulrN EFinN. +rewrite oppeD//. +rewrite -(continuous_FTC2 ab _ _ DPGFE); last 2 first. +- apply/(continuous_within_itvP _ ab); split. + + move=> x xab. + apply: continuousM; first apply: continuous_comp. + * by move/(continuous_within_itvP _ ab) : cF => [+ _ _]; exact. + * move/(continuous_within_itvP _ FbFa) : cG => [+ _ _]; apply. + exact: decreasing_image_oo. + * have : -%R F^`() @ x --> (- f x)%R. + rewrite -fE//. + apply: cvgN. + exact: cF'. + apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl. + apply: (@open_in_nearW _ _ `]a, b[); last by rewrite inE. + exact: interval_open. + by move=> z; rewrite inE/= => zab; rewrite fctE fE. + + apply: cvgM. + apply: (decreasing_cvg_at_right_comp ab) => //. + move=> x y xab yab. + by apply: decrF; apply: subset_itv_co_cc. + by move/continuous_within_itvP : cF => /(_ ab)[]. + by move/continuous_within_itvP : cG => /(_ FbFa)[]. + rewrite fctE {2}/f eq_refl. apply: cvgN. - rewrite {2}/f eq_refl. move: F'ar. apply: cvg_trans. apply: near_eq_cvg. near=> z. - rewrite /f ifF; last by rewrite gt_eqF. - by rewrite ifF// lt_eqF. - - apply: cvgM. - apply: (decreasing_cvg_at_left_comp ab) => //x y xab yab. - by apply: decrF; apply: subset_itv_oc_cc. - apply: cvgN. - rewrite {2}/f ifF; last by rewrite gt_eqF. + by rewrite fE// in_itv/=; apply/andP; split. + + apply: cvgM. + apply: (decreasing_cvg_at_left_comp ab). + move=> //x y xab yab. + by apply: decrF; apply: subset_itv_oc_cc. + by move/continuous_within_itvP : cF => /(_ ab) []. + by move/continuous_within_itvP : cG => /(_ FbFa) []. + rewrite fctE {2}/f ifF; last by rewrite gt_eqF. rewrite eq_refl. + apply: cvgN. move: F'bl. apply: cvg_trans. apply: near_eq_cvg. near=> z. - rewrite /f ifF; last by rewrite gt_eqF. - by rewrite ifF// lt_eqF. -have dcbH : derivable_oo_continuous_bnd H a b. - have := derivable_oo_continuous_bnd_within dcbPG. + by rewrite fE// in_itv/=; apply/andP; split. +- have := derivable_oo_continuous_bnd_within dcbPG. + have [/= dF rF lF] := dcbF. move=> /(continuous_within_itvP _ FbFa)[_ PGFb PGFa]. split => /=. - move=> x xab. apply/derivable1_diffP. + apply: differentiable_comp => //. apply: differentiable_comp; apply/derivable1_diffP. by have [+ _ _] := dcbF; apply. have [+ _ _] := dcbPG. by apply; exact: decreasing_image_oo. - - apply/cvgrPdist_le => /= e e0. + - apply: cvgN. + apply/cvgrPdist_le => /= e e0. have/cvgrPdist_le /(_ e e0) [d /= d0 {}PGFa] := PGFa. - have := cvg_at_right_within cFa. + have := cvg_at_right_within rF. move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFa]. near=> t. apply: PGFa; last by apply: decrF; rewrite //in_itv/= ?lexx !ltW. apply: cFa => //=. rewrite ltr0_norm// ?subr_lt0// opprB. by near: t; exact: nbhs_right_ltDr. - - apply/cvgrPdist_le => /= e e0. + - apply: cvgN. + apply/cvgrPdist_le => /= e e0. have/cvgrPdist_le /(_ e e0) [d /= d0 {}PGFb] := PGFb. - have := cvg_at_left_within cFb. + have := cvg_at_left_within lF. move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFb]. near=> t. apply: (PGFb); last by apply: decrF; rewrite //in_itv/= ?lexx !ltW. apply: cFb => //=. rewrite gtr0_norm// ?subr_gt0//. by near: t; exact: nbhs_left_ltBl. -have dHE : {in `]a, b[, H^`() =1 (- h)%R}. - move=> x xab; rewrite derive1_comp. - - rewrite dPGE//; last exact: decreasing_image_oo. - rewrite /h/f. - move: xab. - rewrite in_itv/= => /andP[ax xb]. - rewrite mulrN opprK. - rewrite mulrfctE ifF; last by rewrite gt_eqF. - by rewrite ifF// lt_eqF. - - by have [+ _ _] := dcbF; apply. - - by have [+ _ _] := dcbPG; apply; exact: decreasing_image_oo. -rewrite (continuous_FTC2 FbFa cG dcbPG dPGE). -apply: oppe_inj. -rewrite oppeB// addeC. -rewrite -(continuous_FTC2 ab cNh dcbH dHE). -have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R. - apply: measurable_funM. - - apply: (measurable_comp (measurable_itv `]F b, F a[)). - exact: decreasing_image_oo. - apply: subspace_continuous_measurable_fun => //. - apply: continuous_in_subspaceT => x; rewrite inE/=. - exact: incG. - - apply: subspace_continuous_measurable_fun => //. - apply: continuous_in_subspaceT => x; rewrite inE/=. - exact: incF. - - apply: subspace_continuous_measurable_fun; first by []. - apply: continuous_in_subspaceT => x. - rewrite inE/=. - exact: cf. -rewrite -!integral_itv_bndo_bndc; last 2 first. -- rewrite -setU1itv ?bnd_simp//. - rewrite mulrN; apply: measurableT_comp => //. - by rewrite measurable_funU//; split => //; apply: measurable_fun_set1. -- apply: subspace_continuous_measurable_fun => //. - move: cNh; apply: continuous_subspaceW. - exact: subset_itv_co_cc. -rewrite -!integral_itv_obnd_cbnd; last 2 first. -- rewrite mulrN. - exact: measurableT_comp => //. -- apply: subspace_continuous_measurable_fun => //. - move: cNh; apply: continuous_subspaceW. - exact: subset_itv_oo_cc. -rewrite -[LHS]oppeK -integralN//=; last first. - apply: integrable_add_def => //=. - apply: (@integrableS _ _ _ mu `[a, b]) => //. +apply: eq_integral_itvoo. + rewrite mulrN. + apply: measurableT_comp => //. + apply: (eq_measurable_fun ((G \o F) * F^`())%R) => //. + move=> x; rewrite inE/= => xab; congr (_ * _)%R. + by rewrite fE. + move: mGFF'; apply: measurable_funS => //. exact: subset_itv_oo_cc. - apply: continuous_compact_integrable => //. - exact: segment_compact. -congr (- _). -apply: eq_integral => //. -move=> x xab. -rewrite mulrN; congr (- _)%:E. -rewrite /h/f. -rewrite mulrN opprK. -rewrite mulrfctE ifF; last first. - apply: gt_eqF. - by move: xab; rewrite inE/= in_itv/= => /andP[]. -rewrite ifF//. -apply: lt_eqF. -by move: xab; rewrite inE/= in_itv/= => /andP[]. + apply: measurableT_comp => //. + move: mGFF'; apply: measurable_funS => //. + exact: subset_itv_oo_cc. +move=> //x /=; rewrite inE/= => xab. +rewrite mulrN. +congr (- (_ * _))%R. +by rewrite fE. Unshelve. all: end_near. Qed. Lemma oppr_change G a b : (a < b)%R -> @@ -1179,6 +1179,7 @@ rewrite (@decreasing_change -%R)//. exact: cvg_at_right_filter. Qed. +(* proved from decreasing_change *) Lemma increasing_change2 F G a b : (a < b)%R -> {in `[a, b] &, {homo F : x y / (x < y)%R}} -> {in `]a, b[, continuous F^`()} -> From 0ae79995a3732f97b5e092914ead299f17c50e04 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 7 Oct 2024 23:41:27 +0900 Subject: [PATCH 13/16] prove incr with change_oppr + decr --- theories/ftc.v | 571 ++++++++++++------------------------------------- 1 file changed, 131 insertions(+), 440 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index e9a407d362..c9e36387b4 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -822,180 +822,41 @@ Context {R : realType}. Notation mu := lebesgue_measure. Implicit Types (F G f : R -> R) (a b : R). -Lemma increasing_change F G a b : (a < b)%R -> - {in `[a, b] &, {homo F : x y / (x < y)%R}} -> - {in `]a, b[, continuous F^`()} -> - cvg ((F^`() : R -> R) x @[x --> a^'+]) -> - cvg ((F^`() : R -> R) x @[x --> b^'-]) -> - derivable_oo_continuous_bnd F a b -> - {within `[F a, F b], continuous G} -> - \int[mu]_(x in `[F a, F b]) (G x)%:E = - \int[mu]_(x in `[a, b]) (((G \o F) * F^`()) x)%:E. +(* TODO: generalize *) +Lemma measurable_fun_oo_cc a b (f : R -> R) : (a < b)%R -> + measurable_fun `]a, b[ f -> measurable_fun `[a, b] f. Proof. -move=> ab incrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] dcbF cG. -have cF := (derivable_oo_continuous_bnd_within dcbF). -have FaFb : (F a < F b)%R by apply: incrF; rewrite //= in_itv/= (ltW ab) lexx. -have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R. - apply: measurable_funM. - - apply: (measurable_comp (measurable_itv `]F a, F b[)). - exact: increasing_image_oo. - apply: subspace_continuous_measurable_fun => //. - apply: continuous_in_subspaceT => x; rewrite inE/=. - move/(continuous_within_itvP _ FaFb) : cG => [+ _ _]; exact. - - apply: subspace_continuous_measurable_fun => //. - apply: continuous_in_subspaceT => x; rewrite inE/=. - move/(continuous_within_itvP _ ab) : cF => [+ _ _]; exact. - - apply: subspace_continuous_measurable_fun; first by []. - apply: continuous_in_subspaceT => x. - rewrite inE/=. - exact: cF'. -have intGFb : mu.-integrable `[(F a), (F b)] (EFin \o G). - by apply: continuous_compact_integrable => //; exact: segment_compact. -pose PG x := parameterized_integral mu (F a) x G. -have dcbPG : derivable_oo_continuous_bnd PG (F a) (F b). - have [/= dF rF lF] := dcbF. - split => /=. - - move=> x xFaFb /=. - have xFb : (x < F b)%R by move: xFaFb; rewrite in_itv/= => /andP[]. - apply: (continuous_FTC1 xFb intGFb _ _).1 => /=. - by move: (xFaFb); rewrite lte_fin in_itv/= => /andP[]. - exact: (within_continuous_continuous _ _ xFaFb). - - have := parameterized_integral_continuous FaFb intGFb. - by move=> /(continuous_within_itvP _ FaFb)[]. - - exact: parameterized_integral_cvg_at_left. -rewrite (@continuous_FTC2 _ _ PG _ _ FaFb cG); last 2 first. -- split. - + move=> x /[dup]xFaFb; rewrite in_itv/= => /andP[Fax xFb]. - apply: (continuous_FTC1 xFb intGFb Fax _).1. - have/(continuous_within_itvP _ FaFb)[+ _ _] := cG; exact. - + have := parameterized_integral_continuous FaFb intGFb. - by move=> /(continuous_within_itvP _ FaFb)[]. - + exact: parameterized_integral_cvg_at_left. -- move=> x xFaFb. - have xFb : (x < F b)%R by move: xFaFb; rewrite in_itv/= => /andP[]. - apply: (continuous_FTC1 xFb _ _ _).2 => //=. - by move: (xFaFb); rewrite lte_fin in_itv/= => /andP[]. - exact: (within_continuous_continuous _ _ xFaFb). -set f := fun x => if x == a then r else if x == b then l else F^`() x. -have fE : {in `]a, b[, F^`() =1 f}. - move=> x; rewrite in_itv/= => /andP[ax xb]. - rewrite /f ifF; last by rewrite gt_eqF. - by rewrite ifF// lt_eqF. -rewrite -(@continuous_FTC2 _ ((G \o F) * f)%R (PG \o F) _ _ ab); last 3 first. -- apply/(continuous_within_itvP _ ab); split. - + move=> x xab. - apply: continuousM; first apply: continuous_comp. - * by move/(continuous_within_itvP _ ab) : cF => [+ _ _]; exact. - * move/(continuous_within_itvP _ FaFb) : cG => [+ _ _]; apply. - exact: increasing_image_oo. - * have : F^`() @ x --> f x by rewrite -fE//; exact: cF'. - apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl. - apply: (@open_in_nearW _ _ `]a, b[); last by rewrite inE. - exact: interval_open. - move=> z; rewrite inE/=; exact: fE. - + apply: cvgM. - apply: (increasing_cvg_at_right_comp ab) => //. - move=> x y xab yab. - by apply: incrF; apply: subset_itv_co_cc. - by move/continuous_within_itvP : cF => /(_ ab)[]. - by move/continuous_within_itvP : cG => /(_ FaFb)[]. - rewrite {2}/f eq_refl. - move: F'ar. - apply: cvg_trans. - apply: near_eq_cvg. - near=> z. - by rewrite fE// in_itv/=; apply/andP; split. - + apply: cvgM. - apply: (increasing_cvg_at_left_comp ab). - move=> //x y xab yab. - by apply: incrF; apply: subset_itv_oc_cc. - by move/continuous_within_itvP : cF => /(_ ab) []. - by move/continuous_within_itvP : cG => /(_ FaFb) []. - rewrite {2}/f ifF; last by rewrite gt_eqF. - rewrite eq_refl. - move: F'bl. - apply: cvg_trans. - apply: near_eq_cvg. - near=> z. - by rewrite fE// in_itv/=; apply/andP; split. -- have := derivable_oo_continuous_bnd_within dcbPG. - have [/= dF rF lF] := dcbF. - move=> /(continuous_within_itvP _ FaFb)[_ PGFa PGFb]. - split => /=. - - move=> x xab. - apply/derivable1_diffP. - apply: differentiable_comp; apply/derivable1_diffP. - by have [+ _ _] := dcbF; apply. - have [+ _ _] := dcbPG. - by apply; exact: increasing_image_oo. - - apply/cvgrPdist_le => /= e e0. - have/cvgrPdist_le /(_ e e0) [d /= d0 {}PGFa] := PGFa. - have := cvg_at_right_within rF. - move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFa]. - near=> t. - apply: PGFa; last by apply: incrF; rewrite //in_itv/= ?lexx !ltW. - apply: cFa => //=. - rewrite ltr0_norm// ?subr_lt0// opprB. - by near: t; exact: nbhs_right_ltDr. - - apply/cvgrPdist_le => /= e e0. - have/cvgrPdist_le /(_ e e0) [d /= d0 {}PGFb] := PGFb. - have := cvg_at_left_within lF. - move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFb]. - near=> t. - apply: (PGFb); last by apply: incrF; rewrite //in_itv/= ?lexx !ltW. - apply: cFb => //=. - rewrite gtr0_norm// ?subr_gt0//. - by near: t; exact: nbhs_left_ltBl. -- move=> x /[dup]xab /andP[ax xb]; rewrite derive1_comp. - + congr (_ * _)%R. - * have /[dup]FxFaFb : F x \in `]F a, F b[ by exact: increasing_image_oo. - rewrite in_itv/= => /andP[FaFx FxFb]. - apply: (continuous_FTC1 FxFb intGFb FaFx _).2 => //=. - exact: (within_continuous_continuous _ _ FxFaFb). - * by rewrite fE. - + by have [+ _ _] := dcbF; apply. - + by have [+ _ _] := dcbPG; apply; exact: increasing_image_oo. -have mGFf : measurable_fun `]a, b[ ((G \o F) * f)%R. - apply: (eq_measurable_fun ((G \o F) * F^`())%R) => //. - move=> x; rewrite inE/= => xab; congr (_ * _)%R. - by rewrite fE. -apply: eq_integral_itvoo => //x; rewrite inE/= => xab. -congr (_ * _)%R. -by rewrite fE. -Unshelve. all: end_near. Qed. +move=> mf; rewrite -setU1itv//; last by rewrite bnd_simp ltW. +rewrite measurable_funU//; split; first exact: measurable_fun_set1. +rewrite -setUitv1// measurable_funU//; split => //. +exact: measurable_fun_set1. +Qed. Lemma decreasing_change F G a b : (a < b)%R -> {in `[a, b] &, {homo F : x y /~ (x < y)%R}} -> {in `]a, b[, continuous F^`()} -> - cvg ((F^`() : R -> R) x @[x --> a^'+]) -> - cvg ((F^`() : R -> R) x @[x --> b^'-]) -> + cvg (F^`() x @[x --> a^'+]) -> + cvg (F^`() x @[x --> b^'-]) -> derivable_oo_continuous_bnd F a b -> - {within `[F b, F a], continuous G} -> + {within `[F b, F a], continuous G} -> \int[mu]_(x in `[F b, F a]) (G x)%:E = - \int[mu]_(x in `[a, b]) (((G \o F) * (- F^`())) x)%:E. + \int[mu]_(x in `[a, b]) (((G \o F) * - F^`()) x)%:E. Proof. move=> ab decrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] dcbF cG. -have cF := (derivable_oo_continuous_bnd_within dcbF). +have cF := derivable_oo_continuous_bnd_within dcbF. have FbFa : (F b < F a)%R by apply: decrF; rewrite //= in_itv/= (ltW ab) lexx. have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R. apply: measurable_funM. - apply: (measurable_comp (measurable_itv `]F b, F a[)). exact: decreasing_image_oo. apply: subspace_continuous_measurable_fun => //. - apply: continuous_in_subspaceT => x; rewrite inE/=. - move/(continuous_within_itvP _ FbFa) : cG => [+ _ _]; exact. + by apply: continuous_subspaceW cG; exact/subset_itv_oo_cc. - apply: subspace_continuous_measurable_fun => //. - apply: continuous_in_subspaceT => x; rewrite inE/=. - move/(continuous_within_itvP _ ab) : cF => [+ _ _]; exact. + by apply: continuous_subspaceW cF; exact/subset_itv_oo_cc. - apply: subspace_continuous_measurable_fun; first by []. - apply: continuous_in_subspaceT => x. - rewrite inE/=. - exact: cF'. + by apply: continuous_in_subspaceT => x; rewrite inE/= => /cF'. have {}mGFF' : measurable_fun `[a, b] ((G \o F) * F^`())%R. - rewrite -setU1itv//; last by rewrite bnd_simp ltW. - rewrite measurable_funU//; split; first exact: measurable_fun_set1. - rewrite -setUitv1// measurable_funU//; split => //. - exact: measurable_fun_set1. + exact: measurable_fun_oo_cc. have intGFa : mu.-integrable `[(F b), (F a)] (EFin \o G). by apply: continuous_compact_integrable => //; exact: segment_compact. pose PG x := parameterized_integral mu (F b) x G. @@ -1014,7 +875,7 @@ rewrite (@continuous_FTC2 _ _ PG _ _ FbFa cG); last 2 first. - split. + move=> x /[dup]xFbFa; rewrite in_itv/= => /andP[Fbx xFa]. apply: (continuous_FTC1 xFa intGFa Fbx _).1. - have/(continuous_within_itvP _ FbFa)[+ _ _] := cG; exact. + by have/(continuous_within_itvP _ FbFa)[+ _ _] := cG; exact. + have := parameterized_integral_continuous FbFa intGFa. by move=> /(continuous_within_itvP _ FbFa)[]. + exact: parameterized_integral_cvg_at_left. @@ -1025,27 +886,20 @@ rewrite (@continuous_FTC2 _ _ PG _ _ FbFa cG); last 2 first. exact: (within_continuous_continuous _ _ xFbFa). set f := fun x => if x == a then r else if x == b then l else F^`() x. have fE : {in `]a, b[, F^`() =1 f}. - move=> x; rewrite in_itv/= => /andP[ax xb]. - rewrite /f ifF; last by rewrite gt_eqF. - by rewrite ifF// lt_eqF. + by move=> x; rewrite in_itv/= => /andP[ax xb]; rewrite /f gt_eqF// lt_eqF. have DPGFE : {in `]a, b[, (- (PG \o F))%R^`() =1 ((G \o F) * (- f))%R}. move=> x /[dup]xab /andP[ax xb]; rewrite derive1_comp; last 2 first. - + apply: diff_derivable. - apply: differentiable_comp; apply/derivable1_diffP. + - apply: diff_derivable; apply: differentiable_comp; apply/derivable1_diffP. by have [+ _ _] := dcbF; apply. - have [+ _ _] := dcbPG; apply. - exact: decreasing_image_oo. - + exact: ex_derive. - have := (@is_deriveNid _ _ (PG (F x)) 1%R). - move/(@derive_val _ _ _ _ _ -%R). + by have [+ _ _] := dcbPG; apply; exact: decreasing_image_oo. + - by []. + have /(@derive_val _ _ _ _ _ -%R) := @is_deriveNid _ _ (PG (F x)) 1%R. rewrite fctE -derive1E => ->. - rewrite mulN1r. - rewrite mulrN. - congr -%R. + rewrite mulN1r mulrN; congr -%R. rewrite derive1_comp; last 2 first. - + by have [+ _ _] := dcbF; apply. - + by have [+ _ _] := dcbPG; apply; exact: decreasing_image_oo. - congr (_ * _)%R. + - by have [+ _ _] := dcbF; exact. + by have [+ _ _] := dcbPG; apply; exact: decreasing_image_oo. + congr *%R. + have /[dup]FxFbFa : F x \in `]F b, F a[ by exact: decreasing_image_oo. rewrite in_itv/= => /andP[FbFx FxFa]. apply: (continuous_FTC1 FxFa intGFa FbFx _).2 => //=. @@ -1053,65 +907,54 @@ have DPGFE : {in `]a, b[, (- (PG \o F))%R^`() =1 ((G \o F) * (- f))%R}. + by rewrite fE. rewrite -[LHS]oppeK oppeB// addrC. under eq_integral do rewrite mulrN EFinN. -rewrite oppeD//. -rewrite -(continuous_FTC2 ab _ _ DPGFE); last 2 first. +rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first. - apply/(continuous_within_itvP _ ab); split. - + move=> x xab. - apply: continuousM; first apply: continuous_comp. + + move=> x xab; apply: continuousM; first apply: continuous_comp. * by move/(continuous_within_itvP _ ab) : cF => [+ _ _]; exact. * move/(continuous_within_itvP _ FbFa) : cG => [+ _ _]; apply. exact: decreasing_image_oo. * have : -%R F^`() @ x --> (- f x)%R. - rewrite -fE//. - apply: cvgN. - exact: cF'. + by rewrite -fE//; apply: cvgN; exact: cF'. apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl. apply: (@open_in_nearW _ _ `]a, b[); last by rewrite inE. exact: interval_open. by move=> z; rewrite inE/= => zab; rewrite fctE fE. + apply: cvgM. apply: (decreasing_cvg_at_right_comp ab) => //. - move=> x y xab yab. - by apply: decrF; apply: subset_itv_co_cc. - by move/continuous_within_itvP : cF => /(_ ab)[]. - by move/continuous_within_itvP : cG => /(_ FbFa)[]. - rewrite fctE {2}/f eq_refl. - apply: cvgN. - move: F'ar. - apply: cvg_trans. - apply: near_eq_cvg. + * move=> x y xab yab. + by apply: decrF; exact: subset_itv_co_cc. + * 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. near=> z. by rewrite fE// in_itv/=; apply/andP; split. + apply: cvgM. apply: (decreasing_cvg_at_left_comp ab). - move=> //x y xab yab. - by apply: decrF; apply: subset_itv_oc_cc. - by move/continuous_within_itvP : cF => /(_ ab) []. - by move/continuous_within_itvP : cG => /(_ FbFa) []. - rewrite fctE {2}/f ifF; last by rewrite gt_eqF. - rewrite eq_refl. + * move=> //x y xab yab. + by apply: decrF; apply: subset_itv_oc_cc. + * by move/continuous_within_itvP : cF => /(_ ab) []. + * by move/continuous_within_itvP : cG => /(_ FbFa) []. + rewrite fctE {2}/f gt_eqF// eqxx. apply: cvgN. - move: F'bl. - apply: cvg_trans. - apply: near_eq_cvg. + apply: cvg_trans F'bl; apply: near_eq_cvg. near=> z. by rewrite fE// in_itv/=; apply/andP; split. -- have := derivable_oo_continuous_bnd_within dcbPG. - have [/= dF rF lF] := dcbF. +- have [/= dF rF lF] := dcbF. + have := derivable_oo_continuous_bnd_within dcbPG. move=> /(continuous_within_itvP _ FbFa)[_ PGFb PGFa]. split => /=. - move=> x xab. - apply/derivable1_diffP. - apply: differentiable_comp => //. + apply/derivable1_diffP; apply: differentiable_comp => //. apply: differentiable_comp; apply/derivable1_diffP. - by have [+ _ _] := dcbF; apply. + by have [+ _ _] := dcbF; exact. have [+ _ _] := dcbPG. by apply; exact: decreasing_image_oo. - apply: cvgN. apply/cvgrPdist_le => /= e e0. have/cvgrPdist_le /(_ e e0) [d /= d0 {}PGFa] := PGFa. have := cvg_at_right_within rF. - move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFa]. + move/cvgrPdist_lt => /(_ _ d0)[d' /= d'0 {}cFa]. near=> t. apply: PGFa; last by apply: decrF; rewrite //in_itv/= ?lexx !ltW. apply: cFa => //=. @@ -1119,9 +962,9 @@ rewrite -(continuous_FTC2 ab _ _ DPGFE); last 2 first. by near: t; exact: nbhs_right_ltDr. - apply: cvgN. apply/cvgrPdist_le => /= e e0. - have/cvgrPdist_le /(_ e e0) [d /= d0 {}PGFb] := PGFb. + have /cvgrPdist_le/(_ e e0)[d /= d0 {}PGFb] := PGFb. have := cvg_at_left_within lF. - move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFb]. + move/cvgrPdist_lt => /(_ _ d0)[d' /= d'0 {}cFb]. near=> t. apply: (PGFb); last by apply: decrF; rewrite //in_itv/= ?lexx !ltW. apply: cFb => //=. @@ -1131,260 +974,108 @@ apply: eq_integral_itvoo. rewrite mulrN. apply: measurableT_comp => //. apply: (eq_measurable_fun ((G \o F) * F^`())%R) => //. - move=> x; rewrite inE/= => xab; congr (_ * _)%R. - by rewrite fE. - move: mGFF'; apply: measurable_funS => //. - exact: subset_itv_oo_cc. + by move=> x; rewrite inE/= => xab; rewrite !fctE fE. + by move: mGFF'; apply: measurable_funS => //; exact: subset_itv_oo_cc. apply: measurableT_comp => //. - move: mGFF'; apply: measurable_funS => //. + apply: measurable_funS mGFF' => //. exact: subset_itv_oo_cc. move=> //x /=; rewrite inE/= => xab. -rewrite mulrN. -congr (- (_ * _))%R. -by rewrite fE. +by rewrite mulrN !fctE fE. Unshelve. all: end_near. Qed. Lemma oppr_change G a b : (a < b)%R -> - {within `[(- b)%R, (- a)%R], continuous G} -> + {within `[(- b)%R, (- a)%R], continuous G} -> \int[mu]_(x in `[(- b)%R, (- a)%R]) (G x)%:E = \int[mu]_(x in `[a, b]) ((G \o -%R) x)%:E. Proof. move=> ab cG. -have Dopp: (@GRing.opp R)^`() = cst (-1)%R :> (R -> R). - apply/funext => z. - rewrite derive1E. - exact: derive_val. +have Dopp: (@GRing.opp R)^`() = cst (-1)%R. + by apply/funext => z; rewrite derive1E derive_val. rewrite (@decreasing_change -%R)//. -- apply: eq_integral => //= x; rewrite inE/= => xab. - congr (EFin _). - rewrite !fctE -[RHS]mulr1; congr (_ * _)%R. - rewrite derive1E. - rewrite deriveN//. - rewrite opprK. - exact: derive_val. +- apply: eq_integral => //= x; rewrite inE/= => xab; congr (EFin _). + rewrite !fctE -[RHS]mulr1; congr *%R. + by rewrite derive1E deriveN// opprK derive_val. - by move=> ? ? _ _; rewrite ltrN2. -- rewrite Dopp. - move=> ? _; exact: cvg_cst. -- rewrite Dopp. - apply: is_cvgN. - exact: is_cvg_cst. -- rewrite Dopp. - apply: is_cvgN. - exact: is_cvg_cst. -- split. - + by move=> x _. - + rewrite -at_leftN. - exact: cvg_at_left_filter. - + rewrite -at_rightN. - exact: cvg_at_right_filter. +- by rewrite Dopp => ? _; exact: cvg_cst. +- by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst. +- by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst. +- split => //. + + by rewrite -at_leftN; exact: cvg_at_left_filter. + + by rewrite -at_rightN; exact: cvg_at_right_filter. Qed. -(* proved from decreasing_change *) -Lemma increasing_change2 F G a b : (a < b)%R -> +Lemma increasing_change F G a b : (a < b)%R -> {in `[a, b] &, {homo F : x y / (x < y)%R}} -> {in `]a, b[, continuous F^`()} -> - cvg ((F^`() : R -> R) x @[x --> a^'+]) -> - cvg ((F^`() : R -> R) x @[x --> b^'-]) -> + cvg (F^`() x @[x --> a^'+]) -> + cvg (F^`() x @[x --> b^'-]) -> derivable_oo_continuous_bnd F a b -> - {within `[F a, F b], continuous G} -> + {within `[F a, F b], continuous G} -> \int[mu]_(x in `[F a, F b]) (G x)%:E = \int[mu]_(x in `[a, b]) (((G \o F) * F^`()) x)%:E. Proof. -move=> ab incrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] dcbF cG. -have cF := (derivable_oo_continuous_bnd_within dcbF). -have FaFb : (F a < F b)%R by apply: incrF; rewrite //= in_itv/= (ltW ab) lexx. -set f := fun x => if x == a then r else if x == b then l else F^`() x. -have fE : {in `]a, b[, F^`() =1 f}. - move=> x; rewrite in_itv/= => /andP[ax xb]. - rewrite /f ifF; last by rewrite gt_eqF. - by rewrite ifF// lt_eqF. -have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R. - apply: measurable_funM. - - apply: (measurable_comp (measurable_itv `]F a, F b[)). - exact: increasing_image_oo. - apply: subspace_continuous_measurable_fun => //. - apply: continuous_in_subspaceT => x; rewrite inE/=. - move/(continuous_within_itvP _ FaFb) : cG => [+ _ _]; exact. +move=> ab incrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] Fab cG. +transitivity (\int[mu]_(x in `[F a, F b]) (((G \o -%R) \o -%R) x)%:E). + by apply/eq_integral => x ? /=; rewrite opprK. +have FaFb : (F a < F b)%R by rewrite incrF// in_itv/= lexx (ltW ab). +have cGN : {within `[- (F b), - (F a)]%classic%R, continuous (G \o -%R)}. + apply/continuous_within_itvP; [by rewrite ltrN2|split]. + - move=> x /[dup]xab /[!in_itv]/= /andP[ax xb]. + apply: continuous_comp; first exact: continuousN. + - move/(continuous_within_itvP _ FaFb) : cG => [+ _ _]; apply. + by rewrite in_itv/= ltrNr xb ltrNl. + - move/(continuous_within_itvP _ FaFb) : cG => [_ _]. + by rewrite /= opprK => /cvg_at_leftNP. + - move/(continuous_within_itvP _ FaFb) : cG => [_ + _]. + by rewrite /= opprK => /cvg_at_rightNP. +rewrite -oppr_change// (@decreasing_change (- F)%R); first last. +- exact: cGN. +- split; [|by apply: cvgN; case: Fab..]. + by move=> x xab; apply: derivableN; case: Fab => + _ _; exact. +- apply/cvg_ex; exists (- l)%R. + move/cvgN : F'bl; apply: cvg_trans; apply: near_eq_cvg. + near=> z; rewrite fctE !derive1E deriveN//. + have [+ _ _] := Fab. + by apply; rewrite in_itv/=; apply/andP; split. +- apply/cvg_ex; exists (- r)%R. + move/cvgN : F'ar; apply: cvg_trans; apply: near_eq_cvg. + near=> z; rewrite fctE !derive1E deriveN//. + by case: Fab => + _ _; apply; rewrite in_itv/=; apply/andP; split. +- move=> x xab; rewrite /continuous_at derive1E deriveN; last first. + by case: Fab => + _ _; exact. + rewrite -derive1E. + have /cvgN := cF' _ xab; apply: cvg_trans; apply: near_eq_cvg. + rewrite near_simpl; near=> y. + rewrite fctE !derive1E deriveN//. + case: Fab => + _ _; apply. + by near: y; exact: near_in_itv. +- by move=> x y xab yab yx; rewrite ltrN2 incrF. +- by []. +have ? : measurable_fun `]a, b[ (G \o F). + apply: (@measurable_comp _ _ _ _ _ _ `](F a)%R, (F b)%R[%classic) => //. + - move=> /= _ [x] /[!in_itv]/= /andP[ax xb] <-. + by rewrite incrF ?incrF// in_itv/= ?lexx/= ?(ltW ab)//= ?(ltW ax) ?(ltW xb). - apply: subspace_continuous_measurable_fun => //. - apply: continuous_in_subspaceT => x; rewrite inE/=. - move/(continuous_within_itvP _ ab) : cF => [+ _ _]; exact. - - apply: subspace_continuous_measurable_fun; first by []. - apply: continuous_in_subspaceT => x. - rewrite inE/=. - exact: cF'. -have intE : \int[mu]_(x in `[a, b]) (((G \o F) * F^`()) x)%:E = (\int[mu]_(x in `[a, b]) (((G \o F) * f) x)%:E). - apply: eq_integral_itvoo => //. - apply: eq_measurable_fun mGFF'. - by move=> x; rewrite inE/= => xab; congr (_ * _)%R; rewrite fE. - by move=> x xab; congr (_ * _)%R; rewrite fE. -rewrite intE. -have F'N : {in `](- b)%R, (- a)%R[, forall x, (- F^`() (- x) @[x --> x] --> (F \o -%R)^`() x)%R}. - move=> x xNbNa. - rewrite derive1_comp//; last first. - by have [+ _ _] := dcbF; apply; rewrite oppr_itvoo. - have := (@is_deriveNid _ _ x 1%R). - move/(@derive_val _ _ _ _ _ -%R). - rewrite -derive1E => ->. - rewrite mulrN1. - have cNF' : {in `]-%R b, -%R a[, continuous (F^`() \o -%R)}. - move=> z; rewrite -oppr_itvoo => Nzab. - apply: continuous_comp. - exact: opp_continuous. - exact: cF'. - apply: cvgN. - suff : F^`() (- x0) @[x0 --> x] --> F^`() (- x) by []. - rewrite -/(F^`() \o -%R) -/((F^`() \o -%R) x). - exact: cNF'. -rewrite -(opprK a) -(opprK b). -rewrite oppr_change; last 2 first. -- by rewrite ltrN2. -- rewrite !opprK; apply/(continuous_within_itvP _ ab); split. - + move=> x /[dup]xab; rewrite in_itv/= => /andP[ax xb]. - apply: continuousM. - apply: continuous_comp. - by move/(continuous_within_itvP _ ab) : cF => [+ _ _]; exact. - move/(continuous_within_itvP _ FaFb) : cG => [+ _ _]; apply. - exact: increasing_image_oo. - have : F^`() @ x --> f x by rewrite -fE//; exact: cF'. - apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl. - apply: (@open_in_nearW _ _ `]a, b[); last by rewrite inE. - exact: interval_open. - move=> z; rewrite inE/=; exact: fE. - + apply: cvgM. - apply: (increasing_cvg_at_right_comp ab) => //. - move=> x y xab yab. - by apply: incrF; apply: subset_itv_co_cc. - by move/continuous_within_itvP : cF => /(_ ab)[]. - by move/continuous_within_itvP : cG => /(_ FaFb)[]. - rewrite {2}/f eq_refl. - move: F'ar. - apply: cvg_trans. - apply: near_eq_cvg. - near=> z. - by rewrite fE// in_itv/=; apply/andP; split. - + apply: cvgM. - apply: (increasing_cvg_at_left_comp ab). - move=> //x y xab yab. - by apply: incrF; apply: subset_itv_oc_cc. - by move/continuous_within_itvP : cF => /(_ ab) []. - by move/continuous_within_itvP : cG => /(_ FaFb) []. - rewrite {2}/f ifF; last by rewrite gt_eqF. - rewrite eq_refl. - move: F'bl. - apply: cvg_trans. - apply: near_eq_cvg. - near=> z. - by rewrite fE// in_itv/=; apply/andP; split. -rewrite (@decreasing_change (F \o -%R) G (- b)%R (- a)%R); last 7 first. -- by rewrite ltrN2. - move=> x y; rewrite -!oppr_itvcc => Nxab Nyab; rewrite -ltrN2 => NxNy. - exact: incrF. -- move=> x xNbNa. - move: (F'N x xNbNa). - apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl. - apply: (@open_in_nearW _ _ `]-%R b, -%R a[); last by rewrite inE. - exact: interval_open. - move=> z; rewrite inE/= -oppr_itvoo => Nzab. - rewrite [RHS]derive1_comp//; last first. - have [+ _ _] := dcbF; exact. - have := (@is_deriveNid _ _ z 1%R). - move/(@derive_val _ _ _ _ _ -%R). - rewrite -derive1E => ->. - by rewrite mulrN1. -- apply/(cvgP (- l)%R). - have : -%R (F^`() \o -%R) x @[x --> (-b)^'+] --> (- l)%R. - apply: cvgN. - exact/cvg_at_leftNP. - apply: cvg_trans. - apply: near_eq_cvg. - near=> z. - rewrite derive1_comp//; last first. - have [+ _ _] := dcbF; apply; rewrite in_itv/=; apply/andP; split. - rewrite ltrNr//. - near: z. - apply: nbhs_right_lt. - by rewrite ltrN2. - by rewrite ltrNl. - have := (@is_deriveNid _ _ z 1%R). - move/(@derive_val _ _ _ _ _ -%R). - rewrite -derive1E => ->. - by rewrite mulrN1. -- apply/(cvgP (- r)%R). - have : -%R (F^`() \o -%R) x @[x --> (-a)^'-] --> (- r)%R. - apply: cvgN. - exact/cvg_at_rightNP. - apply: cvg_trans. - apply: near_eq_cvg. - near=> z. - rewrite derive1_comp//; last first. - have [+ _ _] := dcbF; apply; rewrite in_itv/=; apply/andP; split. - by rewrite ltrNr. - rewrite ltrNl//. - near: z. - apply: nbhs_left_gt. - by rewrite ltrN2. - have := (@is_deriveNid _ _ z 1%R). - move/(@derive_val _ _ _ _ _ -%R). - rewrite -derive1E => ->. - by rewrite mulrN1. -- split. - + move=> x xNbNa. - apply: diff_derivable. - apply: differentiable_comp => //. - apply/derivable1_diffP. - have [+ _ _] := dcbF; apply. - by rewrite oppr_itvoo. - + apply/cvg_at_leftNP; rewrite fctE opprK. - by have [] := dcbF. - + apply/cvg_at_rightNP; rewrite fctE opprK. - by have [] := dcbF. -- by rewrite fctE !opprK. -have mGFNDFN : measurable_fun `](- b)%R, (- a)%R[ ((G \o (F \o -%R)) * - (F \o -%R)^`())%R. - apply: measurable_funM. - - rewrite compA. - apply: (measurable_comp (measurable_itv `]a, b[)) => //. - by move=> _/=[x + <-]; rewrite oppr_itvoo. - apply: (measurable_comp (measurable_itv `]F a, F b[)). - exact: increasing_image_oo. - apply: subspace_continuous_measurable_fun => //. - move: cG. - apply: continuous_subspaceW. - exact: subset_itv_oo_cc. - apply: subspace_continuous_measurable_fun => //. - move: cF. - apply: continuous_subspaceW. - exact: subset_itv_oo_cc. - - apply: measurableT_comp => //. - apply: (eq_measurable_fun (- (F^`() \o -%R))%R). - move=> x. - rewrite inE/= -oppr_itvoo => Nxab. - rewrite derive1_comp//; last by have [+ _ _] := dcbF; apply. - have := (@is_deriveNid _ _ x 1%R). - move/(@derive_val _ _ _ _ _ -%R). - rewrite -derive1E => ->. - by rewrite mulrN1. - apply: measurableT_comp => //. - apply: (measurable_comp (measurable_itv `]a, b[)) => //. - by move=> _ [x /= + <-]; rewrite -oppr_itvoo. - apply: open_continuous_measurable_fun. - exact: interval_open. - move=> x; rewrite inE/= => xab. - exact: cF'. -apply: (eq_integral_itvoo _ _ mGFNDFN). - apply: (measurable_comp (measurable_itv `]a, b[)) => //. - by move=> _ [x /= + <-]; rewrite oppr_itvoo. - apply: (eq_measurable_fun ((G \o F) * F^`())%R) => //. - move=> x; rewrite inE/= => xab; congr (_ * _)%R. - by rewrite fE. -move=> x; rewrite -oppr_itvoo => Nxab. -rewrite fctE; congr (_ * _)%R. -rewrite -fE// -[RHS]opprK; congr -%R. -rewrite derive1_comp//; last first. - by have [+ _ _] := dcbF; apply. -have := (@is_deriveNid _ _ x 1%R). -move/(@derive_val _ _ _ _ _ -%R). -rewrite -derive1E => ->. -by rewrite mulrN1. + by apply: continuous_subspaceW cG; exact/subset_itv_oo_cc. + - apply: subspace_continuous_measurable_fun => //. + apply: derivable_within_continuous => x xab. + by case: Fab => + _ _; exact. +have ? : measurable_fun `]a, b[ F^`(). + apply: subspace_continuous_measurable_fun => //. + by apply: continuous_in_subspaceT => x /[!inE] xab; exact: cF'. +rewrite integral_itv_oo//; last first. + rewrite compA -(compA G -%R) (_ : -%R \o -%R = id); last first. + by apply/funext => y; rewrite /= opprK. + apply: measurable_funM => //; apply: measurableT_comp => //. + apply: (@eq_measurable_fun _ _ _ _ _ (- F^`())%R). + move=> x /[!inE] xab; rewrite [in RHS]derive1E deriveN -?derive1E//. + by case: Fab => + _ _; apply. + exact: measurableT_comp. +rewrite [in RHS]integral_itv_oo//; last exact: measurable_funM. +apply: eq_integral => x /[!inE] xab. +rewrite !fctE !opprK derive1E deriveN. +- by rewrite opprK -derive1E. +- by case: Fab => + _ _; exact. Unshelve. all: end_near. Qed. End integration_by_substitution. @@ -1406,7 +1097,7 @@ Lemma increasing_change_old F G a b : (a < b)%R -> Proof. move=> ab incrF. move/(continuous_within_itvP _ ab) => [+ /cvgP + /cvgP]. -exact: (increasing_change2 ab incrF). +exact: (increasing_change ab incrF). Qed. Lemma decreasing_change_old F G a b : From bece9f249d6b91b337bad059aa14e7b5cdf942e2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 7 Oct 2024 23:56:24 +0900 Subject: [PATCH 14/16] fix changelog --- CHANGELOG_UNRELEASED.md | 68 ----------------------------------------- theories/ftc.v | 44 -------------------------- 2 files changed, 112 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index fc337cbcdf..6d1d150c7f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -9,79 +9,12 @@ - in `mathcomp_extra.v`: + lemma `bij_forall` -- in `normedtype.v`: - + lemma `ninftyN` - -- in `derive.v`: - + lemma `derive_id` - + lemmas `exp_derive`, `exp_derive1` - + lemma `derive_cst` - + lemma `deriveMr`, `deriveMl` - -- in `functions.v`: - + lemmas `mul_funC` -- in `sequences.v`: - + lemma `cvg_geometric_eseries_half` - -- in `lebesgue_measure.v`: - + definitions `is_open_itv`, `open_itv_cover` - + lemmas `outer_measure_open_itv_cover`, `outer_measure_open_le`, - `outer_measure_open`, `outer_measure_Gdelta`, `negligible_outer_measure` -- in `ftc.v`: - + lemmas `integration_by_parts`, `Rintegration_by_parts` - -- in `classical_sets.v`: - + scope `relation_scope` with delimiter `relation` - + notation `^-1` in `relation_scope` (use to be a local notation) - + lemma `set_prod_invK` (was a local lemma in `normedtype.v`) - + definition `diagonal`, lemma `diagonalP` -- in `mathcomp_extra.v`: - + lemmas `invf_ple`, `invf_lep` - -- in `lebesgue_integral.v`: - + lemma `integralZr` - -- in `normedtype.v`: - + lemma `le_closed_ball` -- in `sequences.v`: - + theorem `Baire` - + definition `bounded_fun_norm` - + lemma `bounded_landau` - + definition `pointwise_bounded` - + definition `uniform_bounded` - + theorem `Banach_Steinhauss` - -- in `topology.v`: - + Structures `PointedFiltered`, `PointedNbhs`, `PointedUniform`, - `PseudoPointedMetric` -- in `measure.v`: - + lemma `measurable_neg`, `measurable_or` - -- in `lebesgue_measure.v`: - + lemmas `measurable_fun_eqr`, `measurable_fun_indic`, `measurable_fun_dirac`, - `measurable_fun_addn`, `measurable_fun_maxn`, `measurable_fun_subn`, `measurable_fun_ltn`, - `measurable_fun_leq`, `measurable_fun_eqn` - + module `NGenCInfty` - * definition `G` - * lemmas `measurable_itv_bounded`, `measurableE` -- in `continuous_FTC1_closed`: - + corollary `continuous_FTC1_closed` - -- in `lebesgue_integral.v`: - + lemma `locally_integrableS` - in `normedtype.v`: + lemma `cvgyNP` - in `realfun.v`: + lemmas `cvg_pinftyP`, `cvg_ninftyP` -- in `set_interval.v`: - + lemma `subset_itvSoo` - -- in `lebesgue_integral.v`: - + lemma `integrable_locally_restrict` - + lemma `near_davg` - + lemma `lebesgue_pt_restrict` - in `normedtype.v`: + lemma `nbhs_left_ltBl` @@ -93,7 +26,6 @@ `decreasing_cvg_at_right_comp`, `decreasing_cvg_at_left_comp`, `increasing_change`, `decreasing_change` - - in `filter.v` (new file): + lemma `in_nearW` diff --git a/theories/ftc.v b/theories/ftc.v index c9e36387b4..b93c644623 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -710,15 +710,8 @@ Lemma increasing_cvg_at_right_comp F G a b (l : R) : (a < b)%R -> (G \o F) x @[x --> a^'+] --> l. Proof. move=> ab incrF cFa GFa. -(* take arbitrary e > 0, find d s.t. `| G (F (a + d))) - G (F a)| < e *) apply/cvgrPdist_le => /= e e0. -(* for this e, - there exists d s.t. `| G (F a + d) - G (F a)| < e by continuity of G *) have/cvgrPdist_le /(_ e e0) [d /= d0 {}GFa] := GFa. -(* for this d, - there exists d' s.t. forall r, `| r - a | < d' implies F (a + d') - F a < d - by continuity of F at a *) -(* apply a lemma for take r := (a + d') from `[a, b] *) have := cvg_at_right_within cFa. move=> /cvgrPdist_lt/(_ _ d0)[d' /= d'0 {}cFa]. near=> t. @@ -1079,40 +1072,3 @@ rewrite !fctE !opprK derive1E deriveN. Unshelve. all: end_near. Qed. End integration_by_substitution. - -Module old_integration_by_substitution. -Section old_integration_by_substitution. -Local Open Scope ereal_scope. -Context {R : realType}. -Notation mu := lebesgue_measure. -Implicit Types (F G f : R -> R) (a b : R). - -Lemma increasing_change_old F G a b : (a < b)%R -> - {in `[a, b] &, {homo F : x y / (x < y)%R}} -> - {within `[a, b], continuous F^`()} -> - derivable_oo_continuous_bnd F a b -> - {within `[F a, F b], continuous G} -> - \int[mu]_(x in `[F a, F b]) (G x)%:E = - \int[mu]_(x in `[a, b]) (((G \o F) * F^`()) x)%:E. -Proof. -move=> ab incrF. -move/(continuous_within_itvP _ ab) => [+ /cvgP + /cvgP]. -exact: (increasing_change ab incrF). -Qed. - -Lemma decreasing_change_old F G a b : - (a < b)%R -> - {in `[a, b]&, {homo F : x y /~ (x < y)%R}} -> - {within `[a, b], continuous F^`()} -> - derivable_oo_continuous_bnd F a b -> - {within `[F b, F a], continuous G} -> - \int[mu]_(x in `[F b, F a]) (G x)%:E = - \int[mu]_(x in `[a, b]) (((G \o F) * - (F^`() : R -> R)) x)%:E. -Proof. -move=> ab decrF. -move/(continuous_within_itvP _ ab) => [+ /cvgP + /cvgP]. -exact: decreasing_change. -Qed. - -End old_integration_by_substitution. -End old_integration_by_substitution. From 411156c9db1b9a95f3236273a98a34829c3f957a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 8 Oct 2024 00:21:53 +0900 Subject: [PATCH 15/16] fix --- CHANGELOG_UNRELEASED.md | 24 ++++++++++++++---------- theories/ftc.v | 37 +++++++++++++++++++++++++------------ theories/measure.v | 6 ++++-- 3 files changed, 43 insertions(+), 24 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6d1d150c7f..1f16b8a3fe 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -16,16 +16,6 @@ - in `realfun.v`: + lemmas `cvg_pinftyP`, `cvg_ninftyP` -- in `normedtype.v`: - + lemma `nbhs_left_ltBl` - + lemma `within_continuous_continuous` - -- in `ftc.v`: - + lemma `increasing_image_oo`, `decreasing_image_oo`, - `increasing_cvg_at_right_comp`, `increasing_cvg_at_left_comp`, - `decreasing_cvg_at_right_comp`, `decreasing_cvg_at_left_comp`, - `increasing_change`, `decreasing_change` - - in `filter.v` (new file): + lemma `in_nearW` @@ -64,6 +54,20 @@ - in `normedtype.v`: + lemma `limf_esup_ge0` +- in `normedtype.v`: + + lemma `nbhs_left_ltBl` + + lemma `within_continuous_continuous` + +- in `ftc.v`: + + lemmas `increasing_image_oo`, `decreasing_image_oo`, + `increasing_cvg_at_right_comp`, `increasing_cvg_at_left_comp`, + `decreasing_cvg_at_right_comp`, `decreasing_cvg_at_left_comp`, + + lemmas `integral_itv_oo`, `eq_integral_itvoo`. + + lemma `measurable_fun_itv_cc` + + lemmas `decreasing_change`, `oppr_change`, `increasing_change` + +- in `measure.v`: + + lemma `measurable_fun_set0` ### Changed diff --git a/theories/ftc.v b/theories/ftc.v index b93c644623..dc2c22371d 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -777,10 +777,11 @@ Unshelve. all: end_near. Qed. End integration_by_substitution_preliminaries. +(* TODO: move? *) Lemma integral_itv_oo (R : realType) (f : R -> R) (b0 b1 : bool) (x y : R) : measurable_fun `]x, y[ f -> (\int[lebesgue_measure]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (f z)%:E = - \int[lebesgue_measure]_(z in `]x, y[) (f z)%:E)%E. + \int[lebesgue_measure]_(z in `]x, y[) (f z)%:E)%E. Proof. have [xy|yx _|-> _] := ltgtP x y; last 2 first. rewrite !set_itv_ge ?integral_set0//=. @@ -797,6 +798,7 @@ transitivity (\int[lebesgue_measure]_(z in [set` Interval (BSide b0 x) (BLeft y) by case: b0 => //; rewrite -integral_itv_obnd_cbnd. Qed. +(* TODO: move? *) Lemma eq_integral_itvoo (R : realType) (g f : R -> R) (b0 b1 : bool) (x y : R) : measurable_fun `]x, y[ f -> measurable_fun `]x, y[ g -> @@ -809,22 +811,33 @@ rewrite integral_itv_oo// (@integral_itv_oo _ g)//. by apply: eq_integral => z; rewrite inE/= => zxy; congr EFin; exact: fg. Qed. +(* TODO: move? *) +Lemma measurable_fun_itv_cc {R : realType} (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|] := 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. +move: b0 b1 => [|] [|] // mf. +- rewrite -setUitv1//=; last by rewrite bnd_simp ltW. + by rewrite measurable_funU//; split => //; exact: measurable_fun_set1. +- rewrite -setU1itv//=; last by rewrite bnd_simp ltW. + rewrite measurable_funU//; split; first exact: measurable_fun_set1. + rewrite -setUitv1// measurable_funU//; split => //. + exact: measurable_fun_set1. +- rewrite -setU1itv//=; last by rewrite bnd_simp ltW. + by rewrite measurable_funU//; split => //; exact: measurable_fun_set1. +Qed. + Section integration_by_substitution. Local Open Scope ereal_scope. Context {R : realType}. Notation mu := lebesgue_measure. Implicit Types (F G f : R -> R) (a b : R). -(* TODO: generalize *) -Lemma measurable_fun_oo_cc a b (f : R -> R) : (a < b)%R -> - measurable_fun `]a, b[ f -> measurable_fun `[a, b] f. -Proof. -move=> mf; rewrite -setU1itv//; last by rewrite bnd_simp ltW. -rewrite measurable_funU//; split; first exact: measurable_fun_set1. -rewrite -setUitv1// measurable_funU//; split => //. -exact: measurable_fun_set1. -Qed. - Lemma decreasing_change F G a b : (a < b)%R -> {in `[a, b] &, {homo F : x y /~ (x < y)%R}} -> {in `]a, b[, continuous F^`()} -> @@ -849,7 +862,7 @@ have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R. - apply: subspace_continuous_measurable_fun; first by []. by apply: continuous_in_subspaceT => x; rewrite inE/= => /cF'. have {}mGFF' : measurable_fun `[a, b] ((G \o F) * F^`())%R. - exact: measurable_fun_oo_cc. + exact: measurable_fun_itv_cc mGFF'. have intGFa : mu.-integrable `[(F b), (F a)] (EFin \o G). by apply: continuous_compact_integrable => //; exact: segment_compact. pose PG x := parameterized_integral mu (F b) x G. diff --git a/theories/measure.v b/theories/measure.v index c9238f6eec..a00237c84e 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1582,8 +1582,10 @@ apply/seteqP; split=> [t /=| t /= [] [] ->//]. by case: ifPn => ft; [left|right]. Qed. -Lemma measurable_fun_set1 a (f : T1 -> T2) : -measurable_fun (set1 a) f. +Lemma measurable_fun_set0 (f : T1 -> T2) : measurable_fun set0 f. +Proof. by move=> A B _; rewrite set0I. Qed. + +Lemma measurable_fun_set1 a (f : T1 -> T2) : measurable_fun [set a] f. Proof. by move=> ? ? ?; rewrite set1I; case: ifP. Qed. End measurable_fun. From 7b511862ad3f67f37cdd991420f45e1cdfc450f2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 8 Oct 2024 08:47:45 +0900 Subject: [PATCH 16/16] mv lemmas --- CHANGELOG_UNRELEASED.md | 19 ++- theories/ftc.v | 229 ++++++++++++----------------------- theories/lebesgue_integral.v | 29 +++++ theories/lebesgue_measure.v | 46 +++++++ 4 files changed, 164 insertions(+), 159 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1f16b8a3fe..1aeb19d666 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -58,16 +58,23 @@ + lemma `nbhs_left_ltBl` + lemma `within_continuous_continuous` +- in `measure.v`: + + lemma `measurable_fun_set0` + +- in `lebesgue_measure.v`: + + lemmas `measurable_fun_itv_co`, `measurable_fun_itv_oc`, `measurable_fun_itv_cc` + +- in `lebesgue_integral.v`: + + lemma `integral_itv_bndoo` + - in `ftc.v`: + lemmas `increasing_image_oo`, `decreasing_image_oo`, `increasing_cvg_at_right_comp`, `increasing_cvg_at_left_comp`, `decreasing_cvg_at_right_comp`, `decreasing_cvg_at_left_comp`, - + lemmas `integral_itv_oo`, `eq_integral_itvoo`. - + lemma `measurable_fun_itv_cc` - + lemmas `decreasing_change`, `oppr_change`, `increasing_change` - -- in `measure.v`: - + lemma `measurable_fun_set0` + + lemma `eq_integral_itv_bounded`. + + lemmas `integration_by_substitution_decreasing`, + `integration_by_substitution_oppr`, + `integration_by_substitution_increasing` ### Changed diff --git a/theories/ftc.v b/theories/ftc.v index dc2c22371d..4e41c0198f 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -680,6 +680,7 @@ Qed. End Rintegration_by_parts. +(* TODO: move to realfun.v? *) Section integration_by_substitution_preliminaries. Context {R : realType}. Notation mu := lebesgue_measure. @@ -777,68 +778,13 @@ Unshelve. all: end_near. Qed. End integration_by_substitution_preliminaries. -(* TODO: move? *) -Lemma integral_itv_oo (R : realType) (f : R -> R) (b0 b1 : bool) (x y : R) : - measurable_fun `]x, y[ f -> - (\int[lebesgue_measure]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (f z)%:E = - \int[lebesgue_measure]_(z in `]x, y[) (f z)%:E)%E. -Proof. -have [xy|yx _|-> _] := ltgtP x y; last 2 first. - rewrite !set_itv_ge ?integral_set0//=. - by rewrite bnd_simp le_gtF// ltW. - by case b0; case: b1; rewrite bnd_simp ?lt_geF// le_gtF// ltW. - by case: b0; case: b1; rewrite !set_itvE ?integral_set0 ?integral_set1. -move=> mf. -transitivity (\int[lebesgue_measure]_(z in [set` Interval (BSide b0 x) (BLeft y)]) (f z)%:E)%E. - case: b1 => //. - rewrite -integral_itv_bndo_bndc//. - case: b0 => //. - rewrite -setU1itv ?bnd_simp// measurable_funU//; split => //. - exact: measurable_fun_set1. -by case: b0 => //; rewrite -integral_itv_obnd_cbnd. -Qed. - -(* TODO: move? *) -Lemma eq_integral_itvoo (R : realType) (g f : R -> R) (b0 b1 : bool) (x y : R) : - measurable_fun `]x, y[ f -> - measurable_fun `]x, y[ g -> - {in `]x, y[, f =1 g} -> - (\int[lebesgue_measure]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (f z)%:E = - \int[lebesgue_measure]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (g z)%:E)%E. -Proof. -move=> mf mg fg. -rewrite integral_itv_oo// (@integral_itv_oo _ g)//. -by apply: eq_integral => z; rewrite inE/= => zxy; congr EFin; exact: fg. -Qed. - -(* TODO: move? *) -Lemma measurable_fun_itv_cc {R : realType} (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|] := 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. -move: b0 b1 => [|] [|] // mf. -- rewrite -setUitv1//=; last by rewrite bnd_simp ltW. - by rewrite measurable_funU//; split => //; exact: measurable_fun_set1. -- rewrite -setU1itv//=; last by rewrite bnd_simp ltW. - rewrite measurable_funU//; split; first exact: measurable_fun_set1. - rewrite -setUitv1// measurable_funU//; split => //. - exact: measurable_fun_set1. -- rewrite -setU1itv//=; last by rewrite bnd_simp ltW. - by rewrite measurable_funU//; split => //; exact: measurable_fun_set1. -Qed. - Section integration_by_substitution. Local Open Scope ereal_scope. Context {R : realType}. Notation mu := lebesgue_measure. Implicit Types (F G f : R -> R) (a b : R). -Lemma decreasing_change F G a b : (a < b)%R -> +Lemma integration_by_substitution_decreasing F G a b : (a < b)%R -> {in `[a, b] &, {homo F : x y /~ (x < y)%R}} -> {in `]a, b[, continuous F^`()} -> cvg (F^`() x @[x --> a^'+]) -> @@ -848,117 +794,104 @@ Lemma decreasing_change F G a b : (a < b)%R -> \int[mu]_(x in `[F b, F a]) (G x)%:E = \int[mu]_(x in `[a, b]) (((G \o F) * - F^`()) x)%:E. Proof. -move=> ab decrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] dcbF cG. -have cF := derivable_oo_continuous_bnd_within dcbF. +move=> ab decrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] Fab cG. +have cF := derivable_oo_continuous_bnd_within Fab. have FbFa : (F b < F a)%R by apply: decrF; rewrite //= in_itv/= (ltW ab) lexx. have mGFF' : measurable_fun `]a, b[ ((G \o F) * F^`())%R. apply: measurable_funM. - apply: (measurable_comp (measurable_itv `]F b, F a[)). - exact: decreasing_image_oo. - apply: subspace_continuous_measurable_fun => //. - by apply: continuous_subspaceW cG; exact/subset_itv_oo_cc. + + exact: decreasing_image_oo. + + apply: subspace_continuous_measurable_fun => //. + by apply: continuous_subspaceW cG; exact/subset_itv_oo_cc. + + apply: subspace_continuous_measurable_fun => //. + by apply: continuous_subspaceW cF; exact/subset_itv_oo_cc. - apply: subspace_continuous_measurable_fun => //. - by apply: continuous_subspaceW cF; exact/subset_itv_oo_cc. - - apply: subspace_continuous_measurable_fun; first by []. by apply: continuous_in_subspaceT => x; rewrite inE/= => /cF'. have {}mGFF' : measurable_fun `[a, b] ((G \o F) * F^`())%R. exact: measurable_fun_itv_cc mGFF'. -have intGFa : mu.-integrable `[(F b), (F a)] (EFin \o G). +have intG : mu.-integrable `[F b, F a] (EFin \o G). by apply: continuous_compact_integrable => //; exact: segment_compact. pose PG x := parameterized_integral mu (F b) x G. -have dcbPG : derivable_oo_continuous_bnd PG (F b) (F a). - have [/= dF rF lF] := dcbF. - split => /=. +have PGFbFa : derivable_oo_continuous_bnd PG (F b) (F a). + have [/= dF rF lF] := Fab; split => /=. - move=> x xFbFa /=. have xFa : (x < F a)%R by move: xFbFa; rewrite in_itv/= => /andP[]. - apply: (continuous_FTC1 xFa intGFa _ _).1 => /=. - by move: (xFbFa); rewrite lte_fin in_itv/= => /andP[]. + apply: (continuous_FTC1 xFa intG _ _).1 => /=. + by move: xFbFa; rewrite lte_fin in_itv/= => /andP[]. exact: (within_continuous_continuous _ _ xFbFa). - - have := parameterized_integral_continuous FbFa intGFa. + - have := parameterized_integral_continuous FbFa intG. by move=> /(continuous_within_itvP _ FbFa)[]. - exact: parameterized_integral_cvg_at_left. rewrite (@continuous_FTC2 _ _ PG _ _ FbFa cG); last 2 first. - split. + move=> x /[dup]xFbFa; rewrite in_itv/= => /andP[Fbx xFa]. - apply: (continuous_FTC1 xFa intGFa Fbx _).1. - by have/(continuous_within_itvP _ FbFa)[+ _ _] := cG; exact. - + have := parameterized_integral_continuous FbFa intGFa. + apply: (continuous_FTC1 xFa intG Fbx _).1. + by move: cG => /(continuous_within_itvP _ FbFa)[+ _ _]; exact. + + have := parameterized_integral_continuous FbFa intG. by move=> /(continuous_within_itvP _ FbFa)[]. + exact: parameterized_integral_cvg_at_left. - move=> x xFbFa. have xFa : (x < F a)%R by move: xFbFa; rewrite in_itv/= => /andP[]. apply: (continuous_FTC1 xFa _ _ _).2 => //=. - by move: (xFbFa); rewrite lte_fin in_itv/= => /andP[]. + by move: xFbFa; rewrite lte_fin in_itv/= => /andP[]. exact: (within_continuous_continuous _ _ xFbFa). set f := fun x => if x == a then r else if x == b then l else F^`() x. have fE : {in `]a, b[, F^`() =1 f}. by move=> x; rewrite in_itv/= => /andP[ax xb]; rewrite /f gt_eqF// lt_eqF. have DPGFE : {in `]a, b[, (- (PG \o F))%R^`() =1 ((G \o F) * (- f))%R}. - move=> x /[dup]xab /andP[ax xb]; rewrite derive1_comp; last 2 first. - - apply: diff_derivable; apply: differentiable_comp; apply/derivable1_diffP. - by have [+ _ _] := dcbF; apply. - by have [+ _ _] := dcbPG; apply; exact: decreasing_image_oo. - - by []. + move=> x /[dup]xab /andP[ax xb]; rewrite derive1_comp //; last first. + apply: diff_derivable; apply: differentiable_comp; apply/derivable1_diffP. + by case: Fab => + _ _; exact. + by case: PGFbFa => + _ _; apply; exact: decreasing_image_oo. have /(@derive_val _ _ _ _ _ -%R) := @is_deriveNid _ _ (PG (F x)) 1%R. - rewrite fctE -derive1E => ->. - rewrite mulN1r mulrN; congr -%R. + rewrite fctE -derive1E => ->; rewrite mulN1r mulrN; congr -%R. rewrite derive1_comp; last 2 first. - - by have [+ _ _] := dcbF; exact. - by have [+ _ _] := dcbPG; apply; exact: decreasing_image_oo. - congr *%R. - + have /[dup]FxFbFa : F x \in `]F b, F a[ by exact: decreasing_image_oo. - rewrite in_itv/= => /andP[FbFx FxFa]. - apply: (continuous_FTC1 FxFa intGFa FbFx _).2 => //=. - exact: (within_continuous_continuous _ _ FxFbFa). - + by rewrite fE. + - by case: Fab => + _ _; exact. + - by case: PGFbFa => [+ _ _]; apply; exact: decreasing_image_oo. + rewrite fE//; congr *%R. + have /[dup]FxFbFa : F x \in `]F b, F a[ by exact: decreasing_image_oo. + rewrite in_itv/= => /andP[FbFx FxFa]. + apply: (continuous_FTC1 FxFa intG FbFx _).2 => //=. + exact: (within_continuous_continuous _ _ FxFbFa). rewrite -[LHS]oppeK oppeB// addrC. under eq_integral do rewrite mulrN EFinN. rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first. - apply/(continuous_within_itvP _ ab); split. + move=> x xab; apply: continuousM; first apply: continuous_comp. - * by move/(continuous_within_itvP _ ab) : cF => [+ _ _]; exact. + * by move: cF => /(continuous_within_itvP _ ab)[+ _ _]; exact. * move/(continuous_within_itvP _ FbFa) : cG => [+ _ _]; apply. exact: decreasing_image_oo. * have : -%R F^`() @ x --> (- f x)%R. by rewrite -fE//; apply: cvgN; exact: cF'. apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl. - apply: (@open_in_nearW _ _ `]a, b[); last by rewrite inE. + apply: (@open_in_nearW _ _ `]a, b[) ; last by rewrite inE. exact: interval_open. by move=> z; rewrite inE/= => zab; rewrite fctE fE. + apply: cvgM. apply: (decreasing_cvg_at_right_comp ab) => //. - * move=> x y xab yab. - by apply: decrF; exact: subset_itv_co_cc. + * by move=> x y xab yab; apply: decrF; exact: subset_itv_co_cc. * 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. - near=> z. - by rewrite fE// in_itv/=; apply/andP; split. + by near=> z; rewrite fE// in_itv/=; apply/andP; split. + apply: cvgM. apply: (decreasing_cvg_at_left_comp ab). - * move=> //x y xab yab. - by apply: decrF; apply: subset_itv_oc_cc. - * by move/continuous_within_itvP : cF => /(_ ab) []. - * by move/continuous_within_itvP : cG => /(_ FbFa) []. + * by move=> //x y xab yab; apply: decrF; apply: subset_itv_oc_cc. + * by move/continuous_within_itvP : cF => /(_ ab)[]. + * by move/continuous_within_itvP : cG => /(_ FbFa)[]. rewrite fctE {2}/f gt_eqF// eqxx. - apply: cvgN. - apply: cvg_trans F'bl; apply: near_eq_cvg. - near=> z. - by rewrite fE// in_itv/=; apply/andP; split. -- have [/= dF rF lF] := dcbF. - have := derivable_oo_continuous_bnd_within dcbPG. - move=> /(continuous_within_itvP _ FbFa)[_ PGFb PGFa]. - split => /=. - - move=> x xab. - apply/derivable1_diffP; apply: differentiable_comp => //. + apply: cvgN; apply: cvg_trans F'bl; apply: near_eq_cvg. + by near=> z; rewrite fE// in_itv/=; apply/andP; split. +- have [/= dF rF lF] := Fab. + have := derivable_oo_continuous_bnd_within PGFbFa. + move=> /(continuous_within_itvP _ FbFa)[_ PGFb PGFa]; split => /=. + - move=> x xab; apply/derivable1_diffP; apply: differentiable_comp => //. apply: differentiable_comp; apply/derivable1_diffP. - by have [+ _ _] := dcbF; exact. - have [+ _ _] := dcbPG. - by apply; exact: decreasing_image_oo. - - apply: cvgN. - apply/cvgrPdist_le => /= e e0. - have/cvgrPdist_le /(_ e e0) [d /= d0 {}PGFa] := PGFa. + by case: Fab => + _ _; exact. + by case: PGFbFa => + _ _; apply; exact: decreasing_image_oo. + - apply: cvgN; apply/cvgrPdist_le => /= e e0. + have /cvgrPdist_le/(_ e e0)[d /= d0 {}PGFa] := PGFa. have := cvg_at_right_within rF. move/cvgrPdist_lt => /(_ _ d0)[d' /= d'0 {}cFa]. near=> t. @@ -966,41 +899,35 @@ rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first. apply: cFa => //=. rewrite ltr0_norm// ?subr_lt0// opprB. by near: t; exact: nbhs_right_ltDr. - - apply: cvgN. - apply/cvgrPdist_le => /= e e0. + - apply: cvgN; apply/cvgrPdist_le => /= e e0. have /cvgrPdist_le/(_ e e0)[d /= d0 {}PGFb] := PGFb. have := cvg_at_left_within lF. move/cvgrPdist_lt => /(_ _ d0)[d' /= d'0 {}cFb]. near=> t. - apply: (PGFb); last by apply: decrF; rewrite //in_itv/= ?lexx !ltW. + apply: PGFb; last by apply: decrF; rewrite //in_itv/= ?lexx !ltW. apply: cFb => //=. rewrite gtr0_norm// ?subr_gt0//. by near: t; exact: nbhs_left_ltBl. -apply: eq_integral_itvoo. - rewrite mulrN. - apply: measurableT_comp => //. - apply: (eq_measurable_fun ((G \o F) * F^`())%R) => //. - by move=> x; rewrite inE/= => xab; rewrite !fctE fE. - by move: mGFF'; apply: measurable_funS => //; exact: subset_itv_oo_cc. - apply: measurableT_comp => //. - apply: measurable_funS mGFF' => //. +apply: eq_integral_itv_bounded. +- rewrite mulrN; apply: measurableT_comp => //. + apply: (eq_measurable_fun ((G \o F) * F^`())%R) => //. + by move=> x; rewrite inE/= => xab; rewrite !fctE fE. + by move: mGFF'; apply: measurable_funS => //; exact: subset_itv_oo_cc. +- apply: measurableT_comp => //; apply: measurable_funS mGFF' => //. exact: subset_itv_oo_cc. -move=> //x /=; rewrite inE/= => xab. -by rewrite mulrN !fctE fE. +- by move=> x /[!inE] xab; rewrite mulrN !fctE fE. Unshelve. all: end_near. Qed. -Lemma oppr_change G a b : (a < b)%R -> +Lemma integration_by_substitution_oppr G a b : (a < b)%R -> {within `[(- b)%R, (- a)%R], continuous G} -> \int[mu]_(x in `[(- b)%R, (- a)%R]) (G x)%:E = \int[mu]_(x in `[a, b]) ((G \o -%R) x)%:E. Proof. -move=> ab cG. -have Dopp: (@GRing.opp R)^`() = cst (-1)%R. +move=> ab cG; have Dopp: (@GRing.opp R)^`() = cst (-1)%R. by apply/funext => z; rewrite derive1E derive_val. -rewrite (@decreasing_change -%R)//. -- apply: eq_integral => //= x; rewrite inE/= => xab; congr (EFin _). - rewrite !fctE -[RHS]mulr1; congr *%R. - by rewrite derive1E deriveN// opprK derive_val. +rewrite (@integration_by_substitution_decreasing -%R)//. +- apply: eq_integral => //= x /[!inE] xab; congr (EFin _). + by rewrite !fctE -[RHS]mulr1 derive1E deriveN// opprK derive_val. - by move=> ? ? _ _; rewrite ltrN2. - by rewrite Dopp => ? _; exact: cvg_cst. - by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst. @@ -1010,7 +937,7 @@ rewrite (@decreasing_change -%R)//. + by rewrite -at_rightN; exact: cvg_at_right_filter. Qed. -Lemma increasing_change F G a b : (a < b)%R -> +Lemma integration_by_substitution_increasing F G a b : (a < b)%R -> {in `[a, b] &, {homo F : x y / (x < y)%R}} -> {in `]a, b[, continuous F^`()} -> cvg (F^`() x @[x --> a^'+]) -> @@ -1024,7 +951,7 @@ move=> ab incrF cF' /cvg_ex[/= r F'ar] /cvg_ex[/= l F'bl] Fab cG. transitivity (\int[mu]_(x in `[F a, F b]) (((G \o -%R) \o -%R) x)%:E). by apply/eq_integral => x ? /=; rewrite opprK. have FaFb : (F a < F b)%R by rewrite incrF// in_itv/= lexx (ltW ab). -have cGN : {within `[- (F b), - (F a)]%classic%R, continuous (G \o -%R)}. +have cGN : {within `[- F b, - F a]%classic%R, continuous (G \o -%R)}. apply/continuous_within_itvP; [by rewrite ltrN2|split]. - move=> x /[dup]xab /[!in_itv]/= /andP[ax xb]. apply: continuous_comp; first exact: continuousN. @@ -1034,15 +961,15 @@ have cGN : {within `[- (F b), - (F a)]%classic%R, continuous (G \o -%R)}. by rewrite /= opprK => /cvg_at_leftNP. - move/(continuous_within_itvP _ FaFb) : cG => [_ + _]. by rewrite /= opprK => /cvg_at_rightNP. -rewrite -oppr_change// (@decreasing_change (- F)%R); first last. +rewrite -integration_by_substitution_oppr//. +rewrite (@integration_by_substitution_decreasing (- F)%R); first last. - exact: cGN. - split; [|by apply: cvgN; case: Fab..]. by move=> x xab; apply: derivableN; case: Fab => + _ _; exact. - apply/cvg_ex; exists (- l)%R. move/cvgN : F'bl; apply: cvg_trans; apply: near_eq_cvg. near=> z; rewrite fctE !derive1E deriveN//. - have [+ _ _] := Fab. - by apply; rewrite in_itv/=; apply/andP; split. + by case: Fab => + _ _; apply; rewrite in_itv/=; apply/andP; split. - apply/cvg_ex; exists (- r)%R. move/cvgN : F'ar; apply: cvg_trans; apply: near_eq_cvg. near=> z; rewrite fctE !derive1E deriveN//. @@ -1051,25 +978,22 @@ rewrite -oppr_change// (@decreasing_change (- F)%R); first last. by case: Fab => + _ _; exact. rewrite -derive1E. have /cvgN := cF' _ xab; apply: cvg_trans; apply: near_eq_cvg. - rewrite near_simpl; near=> y. - rewrite fctE !derive1E deriveN//. - case: Fab => + _ _; apply. - by near: y; exact: near_in_itv. + rewrite near_simpl; near=> y; rewrite fctE !derive1E deriveN//. + by case: Fab => + _ _; apply; near: y; exact: near_in_itv. - by move=> x y xab yab yx; rewrite ltrN2 incrF. - by []. -have ? : measurable_fun `]a, b[ (G \o F). - apply: (@measurable_comp _ _ _ _ _ _ `](F a)%R, (F b)%R[%classic) => //. +have mGF : measurable_fun `]a, b[ (G \o F). + apply: (@measurable_comp _ _ _ _ _ _ `]F a, F b[%classic) => //. - move=> /= _ [x] /[!in_itv]/= /andP[ax xb] <-. by rewrite incrF ?incrF// in_itv/= ?lexx/= ?(ltW ab)//= ?(ltW ax) ?(ltW xb). - apply: subspace_continuous_measurable_fun => //. by apply: continuous_subspaceW cG; exact/subset_itv_oo_cc. - apply: subspace_continuous_measurable_fun => //. - apply: derivable_within_continuous => x xab. - by case: Fab => + _ _; exact. -have ? : measurable_fun `]a, b[ F^`(). + by apply: derivable_within_continuous => x xab; case: Fab => + _ _; exact. +have mF' : measurable_fun `]a, b[ F^`(). apply: subspace_continuous_measurable_fun => //. by apply: continuous_in_subspaceT => x /[!inE] xab; exact: cF'. -rewrite integral_itv_oo//; last first. +rewrite integral_itv_bndoo//; last first. rewrite compA -(compA G -%R) (_ : -%R \o -%R = id); last first. by apply/funext => y; rewrite /= opprK. apply: measurable_funM => //; apply: measurableT_comp => //. @@ -1077,9 +1001,8 @@ rewrite integral_itv_oo//; last first. move=> x /[!inE] xab; rewrite [in RHS]derive1E deriveN -?derive1E//. by case: Fab => + _ _; apply. exact: measurableT_comp. -rewrite [in RHS]integral_itv_oo//; last exact: measurable_funM. -apply: eq_integral => x /[!inE] xab. -rewrite !fctE !opprK derive1E deriveN. +rewrite [in RHS]integral_itv_bndoo//; last exact: measurable_funM. +apply: eq_integral => x /[!inE] xab; rewrite !fctE !opprK derive1E deriveN. - by rewrite opprK -derive1E. - by case: Fab => + _ _; exact. Unshelve. all: end_near. Qed. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 2f38b17082..bb0fda01b6 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -6480,6 +6480,35 @@ move=> mf; have [rb|rb] := leP (BRight r) b. - by rewrite !set_itv_ge// -leNgt -?ltBRight_leBLeft// ltW. Qed. +Lemma integral_itv_bndoo (x y : R) (f : R -> R) (b0 b1 : bool) : + measurable_fun `]x, y[ f -> + \int[mu]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (f z)%:E = + \int[mu]_(z in `]x, y[) (f z)%:E. +Proof. +have [xy|yx _|-> _] := ltgtP x y; last 2 first. +- rewrite !set_itv_ge ?integral_set0//=. + + by rewrite bnd_simp le_gtF// ltW. + + by move: b0 b1 => [|] [|]; rewrite bnd_simp ?lt_geF// le_gtF// ltW. +- by move: b0 b1 => [|] [|]; rewrite !set_itvE ?integral_set0 ?integral_set1. +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 => //; rewrite -integral_itv_obnd_cbnd. +Qed. + +Lemma eq_integral_itv_bounded (x y : R) (g f : R -> R) (b0 b1 : bool) : + measurable_fun `]x, y[ f -> measurable_fun `]x, y[ g -> + {in `]x, y[, f =1 g} -> + \int[mu]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (f z)%:E = + \int[mu]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (g z)%:E. +Proof. +move=> mf mg fg. +rewrite integral_itv_bndoo// (@integral_itv_bndoo _ _ g)//. +by apply: eq_integral => z; rewrite inE/= => zxy; congr EFin; exact: fg. +Qed. + End lebesgue_measure_integral. Arguments integral_Sset1 {R f A} r. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 7c79837eea..8689a25297 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -243,6 +243,52 @@ case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge. Qed. #[local] Hint Resolve measurable_itv : core. +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. +Qed. + +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. +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. +Qed. + HB.instance Definition _ := (ereal_isMeasurable (R.-ocitv.-measurable)). (* NB: Until we dropped support for Coq 8.12, we were using HB.instance (\bar (Real.sort R))