From cdc9e90c5c5dc378002d33689fe4086ebc866390 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Fri, 4 Jul 2025 16:58:11 +0900 Subject: [PATCH 01/22] integration_by_party --- CHANGELOG_UNRELEASED.md | 6 + theories/ftc.v | 320 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 326 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 344dcb5ba2..fa45db4560 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -72,6 +72,12 @@ `derivable_Nyo_continuousWoo`, `derivable_Nyo_continuousW` +- in `ftc.v`: + + lemmas `integration_by_partsy_ge0_ge0`, + `integration_by_partsy_le0_ge0`, + `integration_by_partsy_le0_le0`, + `integration_by_partsy_ge0_le0` + ### Changed - in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`: diff --git a/theories/ftc.v b/theories/ftc.v index 157a707d58..6d3eda8e99 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -836,6 +836,326 @@ Qed. End integration_by_parts. +(* PR#1656 *) +Lemma derivable_oy_continuous_within_itvcy {R : numFieldType} + {V : normedModType R} (f : R -> V) (x : R) : + derivable_oy_continuous_bnd f x -> {within `[x, +oo[, continuous f}. +Proof. +Admitted. + +(* #PR1656 *) +Lemma derivable_oy_continuous_bndW_oo {R : numFieldType} {V : normedModType R} + (a c d : R) (f : R -> V) : + (c < d) -> + (a <= c) -> + derivable_oy_continuous_bnd f a -> + derivable_oo_continuous_bnd f c d. +Proof. +Admitted. + +(* PR#1662 *) +Lemma measurable_fun_itv_bndo_bndcP {R : realType} (a : itv_bound R) (b : R) + (f : R -> R) : + measurable_fun [set` Interval a (BLeft b)] f <-> + measurable_fun [set` Interval a (BRight b)] f. +Proof. +Admitted. + +(* PR#1662 *) +Lemma measurable_fun_itv_obnd_cbndP {R : realType} (a : R) (b : itv_bound R) + (f : R -> R) : + measurable_fun [set` Interval (BRight a) b] f <-> + measurable_fun [set` Interval (BLeft a) b] f. +Proof. +Admitted. + +Section integration_by_partsy_ge0. +Context {R : realType}. +Notation mu := lebesgue_measure. +Local Open Scope ereal_scope. +Local Open Scope classical_set_scope. + +Let itvSay {a : R} {n m} {b0 b1 : bool} : + [set` Interval (BSide b0 (a + n%:R)) (BSide b1 (a + m%:R))] `<=` + [set` Interval (BSide b0 a) (BInfty _ false)]. +Proof. +move=> x/=; rewrite 2!in_itv/= andbT => /andP[+ _]. +by case: b0 => /= H; [apply: le_trans H|apply: le_lt_trans H]; rewrite lerDl. +Qed. + +Variables (F G f g : R -> R^o) (a FGoo : R). +Hypothesis cf : {within `[a, +oo[, continuous f}. +Hypothesis Foy : derivable_oy_continuous_bnd F a. +Hypothesis Ff : {in `]a, +oo[%R, F^`() =1 f}. +Hypothesis cg : {within `[a, +oo[, continuous g}. +Hypothesis Goy : derivable_oy_continuous_bnd G a. +Hypothesis Gg : {in `]a, +oo[%R, G^`() =1 g}. +Hypothesis cvgFG : (F \* G)%R x @[x --> +oo%R] --> FGoo. + +Let mFg : measurable_fun `]a, +oo[ (fun x => (F x * g x)%R). +Proof. +apply: (@measurable_funS _ _ _ _ `[a, +oo[) => //. + by apply: subset_itvr; rewrite bnd_simp. +apply: measurable_funM; apply: subspace_continuous_measurable_fun => //. +exact: (@derivable_oy_continuous_within_itvcy _ R^o). +Qed. + +Let cfG : {within `[a, +oo[, continuous (fun x => (f x * G x)%R)}. +Proof. +have/continuous_within_itvcyP[aycf cfa] := cf. +have/derivable_oy_continuous_within_itvcy/continuous_within_itvcyP[] := Goy. +move=> aycG cGa. +apply/continuous_within_itvcyP; split; last exact: cvgM. +move=> x ax; apply: continuousM; first exact: aycf. +exact: aycG. +Qed. + +Let mfG : measurable_fun `]a, +oo[ (fun x => (f x * G x)%R). +Proof. +apply/measurable_fun_itv_obnd_cbndP. +exact: subspace_continuous_measurable_fun. +Qed. + +Let Ffai i : {in `]a + i%:R, a + i.+1%:R[%R, F^`() =1 f}. +Proof. exact/(in1_subset_itv _ Ff)/itvSay. Qed. + +Let Ggai i : {in `]a + i%:R, a + i.+1%:R[%R, G^`() =1 g}. +Proof. exact/(in1_subset_itv _ Gg)/itvSay. Qed. + +Let integral_sum_lim : + \big[+%R/0%R]_(0 <= i `]a, (a + k%:R)]) i) (F x * g x)%:E + = (limn (fun n => ((F (a + n.-1%:R) * G (a + n.-1%:R) - F a * G a)%:E + + \big[+%R/0%R]_(0 <= i < n) - \int[mu]_(x in + seqDU (fun k : nat => `]a, (a + k%:R)]) i) (f x * G x)%:E))). +Proof. +apply: congr_lim. +apply/funext => n. +case: n. + by rewrite big_nat_cond [in RHS]big_nat_cond 2?big_pred0//= 2!addr0 subrr. +case. + rewrite 2!big_nat1 seqDUE -pred_Sn addr0 subrr add0r. + by rewrite set_itvoc0 2!integral_set0 oppe0. +move=> n. +rewrite big_nat_recl// [in RHS]big_nat_recl//=. +rewrite seqDUE/= addr0 set_itvoc0 2!integral_set0 oppe0 2!add0r. +have subset_ai_ay (b b' : bool) i : + [set` Interval (BSide b (a + i%:R)) (BSide b' (a + i.+1%:R))] `<=` + [set` Interval (BSide b a) (BInfty _ false)]. + by apply/subitvP; rewrite subitvE bnd_simp; rewrite ?ler_wpDr. +under eq_bigr => i _. + rewrite seqDUE/= integral_itv_obnd_cbnd; last first. + exact: (@measurable_funS _ _ _ _ `]a, +oo[). + rewrite (integration_by_parts _ _ _ (@Ffai i) _ _ (@Ggai i)); last 5 first. + - by rewrite ltrD2l ltr_nat. + - exact: continuous_subspaceW cf. + - apply: derivable_oy_continuous_bndW_oo Foy. + + by rewrite ltrD2l ltr_nat. + + by rewrite lerDl. + - exact: continuous_subspaceW cg. + - apply: derivable_oy_continuous_bndW_oo Goy. + + by rewrite ltrD2l ltr_nat. + + by rewrite lerDl. + over. +rewrite big_split/=. +under eq_bigr do rewrite EFinB. +rewrite telescope_sume// addr0; congr +%E. +apply: eq_bigr => k _; rewrite seqDUE/= integral_itv_obnd_cbnd//. +exact: measurable_funS mfG. +Qed. + +Let FGaoo : + (F (a + x.-1%:R)%E * G (a + x.-1%:R)%E - F a * G a)%:E @[x --> \oo] --> + (FGoo - F a * G a)%:E. +Proof. +apply: cvg_EFin; first exact: nearW; apply: (@cvgB _ R^o); last exact: cvg_cst. +rewrite -cvg_shiftS/=. +apply: (@cvg_comp _ _ _ _ (F \* G)%R _ +oo%R); last exact: cvgFG; apply/cvgeryP. +apply: (@cvge_pinftyP R (fun x => (a + x)%:E) +oo).1; last exact: cvgr_idn. +by apply/cvgeryP; exact: cvg_addrl. +Qed. + +Let sumN_Nsum_fG n : + (\sum_(0 <= i < n) + (- (\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i) + (f x * G x)%:E))%E)%R = + - (\sum_(0 <= i < n) + (\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i) + (f x * G x)%:E)%E)%R. +Proof. +rewrite big_nat_cond fin_num_sumeN; rewrite -?big_nat_cond//; move=> m _. +rewrite seqDUE integral_itv_obnd_cbnd; last exact: measurable_funS mfG. +apply: integral_fune_fin_num => //=. +apply: continuous_compact_integrable; first exact: segment_compact. +exact: continuous_subspaceW cfG. +Qed. + +Let sumNint_sumintN_fG n : + (\sum_(0 <= i < n) + (- (\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i) + (f x * G x)%:E))%E)%R = + \sum_(0 <= i < n) + (\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i) + (- (f x * G x))%:E)%E. +Proof. +rewrite big_nat_cond [RHS]big_nat_cond. +apply: eq_bigr => i. +rewrite seqDUE andbT => i0n. +rewrite 2?integral_itv_obnd_cbnd; last exact: measurable_funS mfG; last first. + apply: measurableT_comp => //. + exact: measurable_funS mfG. +rewrite -integralN ?integrable_add_def ?continuous_compact_integrable//. + exact: segment_compact. +exact: continuous_subspaceW cfG. +Qed. + +Lemma integration_by_partsy_ge0_ge0 : + {in `]a, +oo[, forall x, 0 <= (f x * G x)%:E} -> + {in `]a, +oo[, forall x, 0 <= (F x * g x)%:E} -> + \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E - + \int[mu]_(x in `[a, +oo[) (f x * G x)%:E. +Proof. +move=> fG0 Fg0. +rewrite -integral_itv_obnd_cbnd// -[in RHS]integral_itv_obnd_cbnd//. +rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq. +rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight; + last 6 first. +- by move=> k; apply: measurableD => //; apply: bigsetU_measurable. +- exact/measurable_EFinP. +- by move=> ? ?; rewrite fG0// inE. +- by move=> k; apply: measurableD => //; apply: bigsetU_measurable. +- exact/measurable_EFinP. +- by move=> ? ?; rewrite Fg0// inE. +rewrite integral_sum_lim; apply/cvg_lim => //. +apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo. +under eq_cvg do rewrite sumN_Nsum_fG; apply: cvgeN. +apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x. +by rewrite seqDUE => anx; apply: fG0; rewrite inE/=; exact/itvSay/anx. +Qed. + +Lemma integration_by_partsy_le0_ge0 : + {in `]a, +oo[, forall x, (f x * G x)%:E <= 0} -> + {in `]a, +oo[, forall x, 0 <= (F x * g x)%:E} -> + \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E + + \int[mu]_(x in `[a, +oo[) (- (f x * G x)%:E). +Proof. +move=> fG0 Fg0. +have mMfG : measurable_fun `]a, +oo[ (fun x => (- (f x * G x))%R). + exact: measurableT_comp. +rewrite -integral_itv_obnd_cbnd// -[in RHS]integral_itv_obnd_cbnd//. +rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq. +rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight; + last 6 first. +- by move=> k; apply: measurableD => //; apply: bigsetU_measurable. +- by apply/measurable_EFinP; exact: measurableT_comp. +- by move=> ? ?; rewrite EFinN oppe_ge0 fG0// inE. +- by move=> k; apply: measurableD => //; apply: bigsetU_measurable. +- exact/measurable_EFinP. +- by move=> ? ?; rewrite Fg0// inE. +rewrite integral_sum_lim; apply/cvg_lim => //. +apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo. +under eq_cvg do rewrite sumNint_sumintN_fG. +apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x. +rewrite seqDUE => anx; rewrite EFinN oppe_ge0. +apply: fG0; rewrite inE/=; exact/itvSay/anx. +Qed. + +End integration_by_partsy_ge0. + +Section integration_by_partsy_le0. +Context {R: realType}. +Notation mu := lebesgue_measure. +Local Open Scope ereal_scope. +Local Open Scope classical_set_scope. + +Lemma derivable_oy_continuous_bndN (F : R -> R^o) (a : R) : + derivable_oy_continuous_bnd F a -> + derivable_oy_continuous_bnd (- F)%R a. +Proof. +Admitted. + +Variables (F G f g : R -> R^o) (a FGoo : R). +Hypothesis cf : {within `[a, +oo[, continuous f}. +Hypothesis Foy : derivable_oy_continuous_bnd F a. +Hypothesis Ff : {in `]a, +oo[%R, F^`() =1 f}. +Hypothesis cg : {within `[a, +oo[, continuous g}. +Hypothesis Goy : derivable_oy_continuous_bnd G a. +Hypothesis Gg : {in `]a, +oo[%R, G^`() =1 g}. +Hypothesis cvgFG : (F \* G)%R x @[x --> +oo%R] --> FGoo. + +Let mFg : measurable_fun `]a, +oo[ (fun x : R => (F x * g x)%R). +Proof. +apply: subspace_continuous_measurable_fun => //. +rewrite continuous_open_subspace// => x ax. +apply: cvgM. + have [+ _]:= Foy; move/derivable_within_continuous. + by rewrite continuous_open_subspace//; apply. +have /continuous_within_itvcyP[+ _] := cg. +by apply; rewrite inE/= in ax. +Qed. + +Let NintNFg : + {in `]a, +oo[, forall x, (F x * g x)%:E <= 0} -> + \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = + - \int[mu]_(x in `[a, +oo[) (- F x * g x)%:E. +Proof. +move=> Fg0. +rewrite -integral_itv_obnd_cbnd//. +under eq_integral => x do rewrite -(opprK (F x)) mulNr EFinN. +rewrite integralN/=; last first. + apply: fin_num_adde_defl. + apply/EFin_fin_numP; exists 0%R. + apply/eqe_oppLRP; rewrite oppe0. + apply:integral0_eq => /= x ax. + apply: (@ge0_funenegE _ _ `]a, +oo[); last by rewrite inE/=. + move=> ?/= ?; rewrite mulNr EFinN oppe_ge0 Fg0//=. + by rewrite inE/=. +rewrite integral_itv_obnd_cbnd//. +under [X in _ _ X]eq_fun do rewrite mulNr; exact: measurableT_comp. +Qed. + +Lemma integration_by_partsy_le0_le0 : + {in `]a, +oo[, forall x, (f x * G x)%:E <= 0} -> + {in `]a, +oo[, forall x, (F x * g x)%:E <= 0} -> + \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E + + \int[mu]_(x in `[a, +oo[) (- (f x * G x)%:E). +Proof. +move=> fG0 Fg0. +rewrite NintNFg//. +rewrite (@integration_by_partsy_ge0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//; last 6 first. +- by move=> ?; apply: cvgN; exact: cf. +- exact: derivable_oy_continuous_bndN. +- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply. +- by under eq_cvg do rewrite fctE/= mulNr; apply: cvgN. +- by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: fG0. +- by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: Fg0. +rewrite oppeB; last exact: fin_num_adde_defr. +rewrite -EFinN opprD 2!opprK mulNr. +by under eq_integral do rewrite mulNr EFinN. +Qed. + +Lemma integration_by_partsy_ge0_le0 : + {in `]a, +oo[, forall x, 0 <= (f x * G x)%:E} -> + {in `]a, +oo[, forall x, (F x * g x)%:E <= 0} -> + \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E - + \int[mu]_(x in `[a, +oo[) (f x * G x)%:E. +Proof. +move=> fG0 Fg0. +rewrite NintNFg//. +rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//; last 6 first. +- by move=> ?; apply: cvgN; exact: cf. +- exact: derivable_oy_continuous_bndN. +- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply. +- by under eq_cvg do rewrite fctE/= mulNr; apply: cvgN. +- by move=> ? ?; rewrite mulNr EFinN oppe_le0; apply: fG0. +- by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: Fg0. +rewrite oppeD; last exact: fin_num_adde_defr. +rewrite -EFinN opprD 2!opprK mulNr. +by under eq_integral do rewrite mulNr EFinN oppeK. +Qed. + +End integration_by_partsy_le0. + Section Rintegration_by_parts. Context {R : realType}. Notation mu := lebesgue_measure. From 0802b9c4dea2fc23f215ca86bab319a9652c8d15 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 30 Oct 2025 16:07:04 +0900 Subject: [PATCH 02/22] upd and rebase --- theories/ftc.v | 47 ++++++++--------------------------------------- 1 file changed, 8 insertions(+), 39 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 6d3eda8e99..4dfd265383 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -836,39 +836,6 @@ Qed. End integration_by_parts. -(* PR#1656 *) -Lemma derivable_oy_continuous_within_itvcy {R : numFieldType} - {V : normedModType R} (f : R -> V) (x : R) : - derivable_oy_continuous_bnd f x -> {within `[x, +oo[, continuous f}. -Proof. -Admitted. - -(* #PR1656 *) -Lemma derivable_oy_continuous_bndW_oo {R : numFieldType} {V : normedModType R} - (a c d : R) (f : R -> V) : - (c < d) -> - (a <= c) -> - derivable_oy_continuous_bnd f a -> - derivable_oo_continuous_bnd f c d. -Proof. -Admitted. - -(* PR#1662 *) -Lemma measurable_fun_itv_bndo_bndcP {R : realType} (a : itv_bound R) (b : R) - (f : R -> R) : - measurable_fun [set` Interval a (BLeft b)] f <-> - measurable_fun [set` Interval a (BRight b)] f. -Proof. -Admitted. - -(* PR#1662 *) -Lemma measurable_fun_itv_obnd_cbndP {R : realType} (a : R) (b : itv_bound R) - (f : R -> R) : - measurable_fun [set` Interval (BRight a) b] f <-> - measurable_fun [set` Interval (BLeft a) b] f. -Proof. -Admitted. - Section integration_by_partsy_ge0. Context {R : realType}. Notation mu := lebesgue_measure. @@ -949,11 +916,11 @@ under eq_bigr => i _. rewrite (integration_by_parts _ _ _ (@Ffai i) _ _ (@Ggai i)); last 5 first. - by rewrite ltrD2l ltr_nat. - exact: continuous_subspaceW cf. - - apply: derivable_oy_continuous_bndW_oo Foy. + - apply: derivable_oy_continuousWoo Foy. + by rewrite ltrD2l ltr_nat. + by rewrite lerDl. - exact: continuous_subspaceW cg. - - apply: derivable_oy_continuous_bndW_oo Goy. + - apply: derivable_oy_continuousWoo Goy. + by rewrite ltrD2l ltr_nat. + by rewrite lerDl. over. @@ -985,7 +952,7 @@ Let sumN_Nsum_fG n : Proof. rewrite big_nat_cond fin_num_sumeN; rewrite -?big_nat_cond//; move=> m _. rewrite seqDUE integral_itv_obnd_cbnd; last exact: measurable_funS mfG. -apply: integral_fune_fin_num => //=. +apply: integrable_fin_num => //=. apply: continuous_compact_integrable; first exact: segment_compact. exact: continuous_subspaceW cfG. Qed. @@ -1068,11 +1035,13 @@ Notation mu := lebesgue_measure. Local Open Scope ereal_scope. Local Open Scope classical_set_scope. +(* TODO: move *) Lemma derivable_oy_continuous_bndN (F : R -> R^o) (a : R) : - derivable_oy_continuous_bnd F a -> - derivable_oy_continuous_bnd (- F)%R a. + derivable_oy_continuous_bnd F a -> derivable_oy_continuous_bnd (- F)%R a. Proof. -Admitted. +move=> [/= derF Fa]; split; last exact: cvgN. +by move=> /= x xa; exact/derivableN/derF. +Qed. Variables (F G f g : R -> R^o) (a FGoo : R). Hypothesis cf : {within `[a, +oo[, continuous f}. From 675d017703001b46262894f156a586c9aa954e41 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 30 Oct 2025 18:32:26 +0900 Subject: [PATCH 03/22] lint --- CHANGELOG_UNRELEASED.md | 6 + theories/charge.v | 4 +- theories/ftc.v | 246 +++++++++--------- theories/kernel.v | 3 +- .../lebesgue_integral_differentiation.v | 13 +- .../lebesgue_integral_dominated_convergence.v | 4 +- .../measurable_fun_approximation.v | 8 +- theories/measurable_realfun.v | 2 +- theories/measure_theory/measurable_function.v | 1 + theories/realfun.v | 7 + 10 files changed, 149 insertions(+), 145 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index fa45db4560..7a3b003646 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -72,6 +72,9 @@ `derivable_Nyo_continuousWoo`, `derivable_Nyo_continuousW` +- in `realfun.v`: + + lemma `derivable_oy_continuous_bndN` + - in `ftc.v`: + lemmas `integration_by_partsy_ge0_ge0`, `integration_by_partsy_le0_ge0`, @@ -330,6 +333,9 @@ + definition `poisson_pmf`, lemmas `poisson_pmf_ge0`, `measurable_poisson_pmf`, + definition `poisson_prob` +- in `measurable_function.v`: + + lemma `measurable_funS`: implicits changed + ### Renamed - in `reals.v`: diff --git a/theories/charge.v b/theories/charge.v index 8e80aee8ca..63046f3609 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1845,7 +1845,7 @@ have int_f_E j S : measurable S -> \int[mu]_(x in S) f_ j x = nu (S `&` E j). have mSIEj := measurableI _ _ mS (mE j). have mSDEj := measurableD mS (mE j). rewrite -{1}(setUIDK S (E j)) (ge0_integral_setU _ mSIEj mSDEj)//; last 2 first. - - by rewrite setUIDK; exact: (measurable_funS measurableT). + - by rewrite setUIDK; exact: measurable_funTS. - by apply/disj_set2P; rewrite setDE setIACA setICr setI0. rewrite /f_ -(eq_integral _ (g_ j)); last first. by move=> x /[!inE] SIEjx; rewrite /f_ ifT// inE; exact: (@subIsetr _ S). @@ -1957,7 +1957,7 @@ have -> : \int[nu]_(x in E) f x = under eq_integral => x /[!inE] /fE -> //. apply: monotone_convergence => //. - move=> n; apply/measurable_EFinP. - by apply: (measurable_funS measurableT) => //; exact/measurable_funP. + by apply: measurable_funTS => //; exact/measurable_funP. - by move=> n x Ex //=; rewrite lee_fin. - by move=> x Ex a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. have -> : \int[mu]_(x in E) (f \* g) x = diff --git a/theories/ftc.v b/theories/ftc.v index 4dfd265383..b5ed70d5a3 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -842,100 +842,52 @@ Notation mu := lebesgue_measure. Local Open Scope ereal_scope. Local Open Scope classical_set_scope. -Let itvSay {a : R} {n m} {b0 b1 : bool} : - [set` Interval (BSide b0 (a + n%:R)) (BSide b1 (a + m%:R))] `<=` - [set` Interval (BSide b0 a) (BInfty _ false)]. -Proof. -move=> x/=; rewrite 2!in_itv/= andbT => /andP[+ _]. -by case: b0 => /= H; [apply: le_trans H|apply: le_lt_trans H]; rewrite lerDl. -Qed. - -Variables (F G f g : R -> R^o) (a FGoo : R). +Variables (F G f g : R -> R) (a FGoo : R). Hypothesis cf : {within `[a, +oo[, continuous f}. Hypothesis Foy : derivable_oy_continuous_bnd F a. Hypothesis Ff : {in `]a, +oo[%R, F^`() =1 f}. Hypothesis cg : {within `[a, +oo[, continuous g}. Hypothesis Goy : derivable_oy_continuous_bnd G a. Hypothesis Gg : {in `]a, +oo[%R, G^`() =1 g}. -Hypothesis cvgFG : (F \* G)%R x @[x --> +oo%R] --> FGoo. +Hypothesis cvgFG : (F * G)%R x @[x --> +oo%R] --> FGoo. -Let mFg : measurable_fun `]a, +oo[ (fun x => (F x * g x)%R). +Let mFg : measurable_fun `]a, +oo[ (F * g)%R. Proof. -apply: (@measurable_funS _ _ _ _ `[a, +oo[) => //. +apply: (measurable_funS `[a, +oo[) => //. by apply: subset_itvr; rewrite bnd_simp. apply: measurable_funM; apply: subspace_continuous_measurable_fun => //. -exact: (@derivable_oy_continuous_within_itvcy _ R^o). +exact: derivable_oy_continuous_within_itvcy. Qed. -Let cfG : {within `[a, +oo[, continuous (fun x => (f x * G x)%R)}. +Let cfG : {within `[a, +oo[, continuous (f * G)%R}. Proof. -have/continuous_within_itvcyP[aycf cfa] := cf. -have/derivable_oy_continuous_within_itvcy/continuous_within_itvcyP[] := Goy. -move=> aycG cGa. -apply/continuous_within_itvcyP; split; last exact: cvgM. -move=> x ax; apply: continuousM; first exact: aycf. -exact: aycG. +have /continuous_within_itvcyP[aycf cfa] := cf. +have /derivable_oy_continuous_within_itvcy/continuous_within_itvcyP[] := Goy. +move=> aycG cGa; apply/continuous_within_itvcyP; split; last exact: cvgM. +by move=> x ax; apply: continuousM; [exact: aycf|exact: aycG]. Qed. -Let mfG : measurable_fun `]a, +oo[ (fun x => (f x * G x)%R). +Let mfG : measurable_fun `]a, +oo[ (f * G)%R. Proof. apply/measurable_fun_itv_obnd_cbndP. exact: subspace_continuous_measurable_fun. Qed. Let Ffai i : {in `]a + i%:R, a + i.+1%:R[%R, F^`() =1 f}. -Proof. exact/(in1_subset_itv _ Ff)/itvSay. Qed. +Proof. +by apply/(in1_subset_itv _ Ff)/subset_itv => //; rewrite bnd_simp lerDl. +Qed. Let Ggai i : {in `]a + i%:R, a + i.+1%:R[%R, G^`() =1 g}. -Proof. exact/(in1_subset_itv _ Gg)/itvSay. Qed. - -Let integral_sum_lim : - \big[+%R/0%R]_(0 <= i `]a, (a + k%:R)]) i) (F x * g x)%:E - = (limn (fun n => ((F (a + n.-1%:R) * G (a + n.-1%:R) - F a * G a)%:E - + \big[+%R/0%R]_(0 <= i < n) - \int[mu]_(x in - seqDU (fun k : nat => `]a, (a + k%:R)]) i) (f x * G x)%:E))). Proof. -apply: congr_lim. -apply/funext => n. -case: n. - by rewrite big_nat_cond [in RHS]big_nat_cond 2?big_pred0//= 2!addr0 subrr. -case. - rewrite 2!big_nat1 seqDUE -pred_Sn addr0 subrr add0r. - by rewrite set_itvoc0 2!integral_set0 oppe0. -move=> n. -rewrite big_nat_recl// [in RHS]big_nat_recl//=. -rewrite seqDUE/= addr0 set_itvoc0 2!integral_set0 oppe0 2!add0r. -have subset_ai_ay (b b' : bool) i : - [set` Interval (BSide b (a + i%:R)) (BSide b' (a + i.+1%:R))] `<=` - [set` Interval (BSide b a) (BInfty _ false)]. - by apply/subitvP; rewrite subitvE bnd_simp; rewrite ?ler_wpDr. -under eq_bigr => i _. - rewrite seqDUE/= integral_itv_obnd_cbnd; last first. - exact: (@measurable_funS _ _ _ _ `]a, +oo[). - rewrite (integration_by_parts _ _ _ (@Ffai i) _ _ (@Ggai i)); last 5 first. - - by rewrite ltrD2l ltr_nat. - - exact: continuous_subspaceW cf. - - apply: derivable_oy_continuousWoo Foy. - + by rewrite ltrD2l ltr_nat. - + by rewrite lerDl. - - exact: continuous_subspaceW cg. - - apply: derivable_oy_continuousWoo Goy. - + by rewrite ltrD2l ltr_nat. - + by rewrite lerDl. - over. -rewrite big_split/=. -under eq_bigr do rewrite EFinB. -rewrite telescope_sume// addr0; congr +%E. -apply: eq_bigr => k _; rewrite seqDUE/= integral_itv_obnd_cbnd//. -exact: measurable_funS mfG. +by apply/(in1_subset_itv _ Gg)/subset_itv => //; rewrite bnd_simp lerDl. Qed. Let FGaoo : - (F (a + x.-1%:R)%E * G (a + x.-1%:R)%E - F a * G a)%:E @[x --> \oo] --> - (FGoo - F a * G a)%:E. + (F (a + x.-1%:R) * G (a + x.-1%:R) - F a * G a)%:E @[x --> \oo] --> + (FGoo - F a * G a)%:E. Proof. -apply: cvg_EFin; first exact: nearW; apply: (@cvgB _ R^o); last exact: cvg_cst. +apply: cvg_EFin; first exact: nearW; apply: cvgB; last exact: cvg_cst. rewrite -cvg_shiftS/=. apply: (@cvg_comp _ _ _ _ (F \* G)%R _ +oo%R); last exact: cvgFG; apply/cvgeryP. apply: (@cvge_pinftyP R (fun x => (a + x)%:E) +oo).1; last exact: cvgr_idn. @@ -943,41 +895,89 @@ by apply/cvgeryP; exact: cvg_addrl. Qed. Let sumN_Nsum_fG n : - (\sum_(0 <= i < n) - (- (\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i) - (f x * G x)%:E))%E)%R = - - (\sum_(0 <= i < n) - (\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i) - (f x * G x)%:E)%E)%R. + \sum_(0 <= i < n) + (- (\int[mu]_(x in seqDU (fun k => `]a, a + k%:R]) i) + (f x * G x)%:E))%E = + - (\sum_(0 <= i < n) + (\int[mu]_(x in seqDU (fun k => `]a, a + k%:R]) i) + (f x * G x)%:E)%E). Proof. rewrite big_nat_cond fin_num_sumeN; rewrite -?big_nat_cond//; move=> m _. -rewrite seqDUE integral_itv_obnd_cbnd; last exact: measurable_funS mfG. +rewrite seqDUE integral_itv_obnd_cbnd; last first. + apply: measurable_funS mfG => //. + by apply/subset_itv => //; rewrite bnd_simp// lerDl. apply: integrable_fin_num => //=. apply: continuous_compact_integrable; first exact: segment_compact. -exact: continuous_subspaceW cfG. +apply: continuous_subspaceW cfG. +by apply/subset_itv => //; rewrite bnd_simp// lerDl. Qed. Let sumNint_sumintN_fG n : - (\sum_(0 <= i < n) - (- (\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i) - (f x * G x)%:E))%E)%R = \sum_(0 <= i < n) - (\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i) - (- (f x * G x))%:E)%E. + (- (\int[mu]_(x in seqDU (fun k => `]a, a + k%:R]) i) + (f x * G x)%:E))%E = + \sum_(0 <= i < n) + (\int[mu]_(x in seqDU (fun k => `]a, a + k%:R]) i) + (- (f x * G x))%:E)%E. Proof. rewrite big_nat_cond [RHS]big_nat_cond. apply: eq_bigr => i. rewrite seqDUE andbT => i0n. -rewrite 2?integral_itv_obnd_cbnd; last exact: measurable_funS mfG; last first. +rewrite 2?integral_itv_obnd_cbnd; last 2 first. apply: measurableT_comp => //. - exact: measurable_funS mfG. + apply: measurable_funS mfG => //. + by apply/subset_itv; rewrite bnd_simp// lerDl. + apply: measurable_funS mfG => //. + by apply/subset_itv; rewrite bnd_simp// lerDl. rewrite -integralN ?integrable_add_def ?continuous_compact_integrable//. exact: segment_compact. -exact: continuous_subspaceW cfG. +apply: continuous_subspaceW cfG. +by apply/subset_itv; rewrite bnd_simp// lerDl. +Qed. + +Let sum_integral_limn : + \sum_(0 <= i `]a, a + k%:R]) i) (F x * g x)%:E + = limn (fun n => (F (a + n.-1%:R) * G (a + n.-1%:R) - F a * G a)%:E + + \sum_(0 <= i < n) + - \int[mu]_(x in seqDU (fun k => `]a, (a + k%:R)]) i) + (f x * G x)%:E). +Proof. +apply: congr_lim; apply/funext => n. +case: n. + by rewrite big_nat_cond [in RHS]big_nat_cond 2?big_pred0//= 2!addr0 subrr. +case => [|n]. + rewrite 2!big_nat1 seqDUE -pred_Sn addr0 subrr add0r. + by rewrite set_itvoc0 2!integral_set0 oppe0. +rewrite big_nat_recl// [in RHS]big_nat_recl//=. +rewrite seqDUE/= addr0 set_itvoc0 2!integral_set0 oppe0 2!add0r. +under eq_bigr => i _. + rewrite seqDUE/= integral_itv_obnd_cbnd; last first. + apply: (measurable_funS `]a, +oo[) => //. + by apply/subset_itv => //; rewrite bnd_simp lerDl. + rewrite (integration_by_parts _ _ _ (@Ffai i) _ _ (@Ggai i)); last 5 first. + - by rewrite ltrD2l ltr_nat. + - apply: continuous_subspaceW cf. + by apply/subset_itv => //; rewrite bnd_simp lerDl. + - apply: derivable_oy_continuousWoo Foy. + + by rewrite ltrD2l ltr_nat. + + by rewrite lerDl. + - apply: continuous_subspaceW cg. + by apply/subset_itv => //; rewrite bnd_simp lerDl. + - apply: derivable_oy_continuousWoo Goy. + + by rewrite ltrD2l ltr_nat. + + by rewrite lerDl. + over. +rewrite big_split/=. +under eq_bigr do rewrite EFinB. +rewrite telescope_sume// addr0; congr +%E. +apply: eq_bigr => k _; rewrite seqDUE/= integral_itv_obnd_cbnd//. +apply: measurable_funS mfG => //. +by apply/subset_itv => //; rewrite bnd_simp lerDl. Qed. Lemma integration_by_partsy_ge0_ge0 : - {in `]a, +oo[, forall x, 0 <= (f x * G x)%:E} -> + {in `]a, +oo[, forall x, 0 <= (f x * G x)%:E} -> {in `]a, +oo[, forall x, 0 <= (F x * g x)%:E} -> \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E - \int[mu]_(x in `[a, +oo[) (f x * G x)%:E. @@ -985,19 +985,19 @@ Proof. move=> fG0 Fg0. rewrite -integral_itv_obnd_cbnd// -[in RHS]integral_itv_obnd_cbnd//. rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq. -rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight; - last 6 first. +rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight. +- rewrite sum_integral_limn; apply/cvg_lim => //. + apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo. + under eq_cvg do rewrite sumN_Nsum_fG; apply: cvgeN. + apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x. + rewrite seqDUE => anx; apply: fG0; rewrite inE/=. + by apply: subset_itv anx; rewrite bnd_simp// lerDl. - by move=> k; apply: measurableD => //; apply: bigsetU_measurable. - exact/measurable_EFinP. - by move=> ? ?; rewrite fG0// inE. - by move=> k; apply: measurableD => //; apply: bigsetU_measurable. - exact/measurable_EFinP. - by move=> ? ?; rewrite Fg0// inE. -rewrite integral_sum_lim; apply/cvg_lim => //. -apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo. -under eq_cvg do rewrite sumN_Nsum_fG; apply: cvgeN. -apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x. -by rewrite seqDUE => anx; apply: fG0; rewrite inE/=; exact/itvSay/anx. Qed. Lemma integration_by_partsy_le0_ge0 : @@ -1011,20 +1011,20 @@ have mMfG : measurable_fun `]a, +oo[ (fun x => (- (f x * G x))%R). exact: measurableT_comp. rewrite -integral_itv_obnd_cbnd// -[in RHS]integral_itv_obnd_cbnd//. rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq. -rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight; - last 6 first. +rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight. +- rewrite sum_integral_limn; apply/cvg_lim => //. + apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo. + under eq_cvg do rewrite sumNint_sumintN_fG. + apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x. + rewrite seqDUE => anx; rewrite EFinN oppe_ge0. + apply: fG0; rewrite inE/=. + by apply: subset_itv anx; rewrite bnd_simp// lerDl. - by move=> k; apply: measurableD => //; apply: bigsetU_measurable. - by apply/measurable_EFinP; exact: measurableT_comp. - by move=> ? ?; rewrite EFinN oppe_ge0 fG0// inE. - by move=> k; apply: measurableD => //; apply: bigsetU_measurable. - exact/measurable_EFinP. - by move=> ? ?; rewrite Fg0// inE. -rewrite integral_sum_lim; apply/cvg_lim => //. -apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo. -under eq_cvg do rewrite sumNint_sumintN_fG. -apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x. -rewrite seqDUE => anx; rewrite EFinN oppe_ge0. -apply: fG0; rewrite inE/=; exact/itvSay/anx. Qed. End integration_by_partsy_ge0. @@ -1035,15 +1035,7 @@ Notation mu := lebesgue_measure. Local Open Scope ereal_scope. Local Open Scope classical_set_scope. -(* TODO: move *) -Lemma derivable_oy_continuous_bndN (F : R -> R^o) (a : R) : - derivable_oy_continuous_bnd F a -> derivable_oy_continuous_bnd (- F)%R a. -Proof. -move=> [/= derF Fa]; split; last exact: cvgN. -by move=> /= x xa; exact/derivableN/derF. -Qed. - -Variables (F G f g : R -> R^o) (a FGoo : R). +Variables (F G f g : R -> R) (a FGoo : R). Hypothesis cf : {within `[a, +oo[, continuous f}. Hypothesis Foy : derivable_oy_continuous_bnd F a. Hypothesis Ff : {in `]a, +oo[%R, F^`() =1 f}. @@ -1052,7 +1044,7 @@ Hypothesis Goy : derivable_oy_continuous_bnd G a. Hypothesis Gg : {in `]a, +oo[%R, G^`() =1 g}. Hypothesis cvgFG : (F \* G)%R x @[x --> +oo%R] --> FGoo. -Let mFg : measurable_fun `]a, +oo[ (fun x : R => (F x * g x)%R). +Let mFg : measurable_fun `]a, +oo[ (F * g)%R. Proof. apply: subspace_continuous_measurable_fun => //. rewrite continuous_open_subspace// => x ax. @@ -1063,8 +1055,7 @@ have /continuous_within_itvcyP[+ _] := cg. by apply; rewrite inE/= in ax. Qed. -Let NintNFg : - {in `]a, +oo[, forall x, (F x * g x)%:E <= 0} -> +Let NintNFg : {in `]a, +oo[, forall x, (F x * g x)%:E <= 0} -> \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = - \int[mu]_(x in `[a, +oo[) (- F x * g x)%:E. Proof. @@ -1075,52 +1066,52 @@ rewrite integralN/=; last first. apply: fin_num_adde_defl. apply/EFin_fin_numP; exists 0%R. apply/eqe_oppLRP; rewrite oppe0. - apply:integral0_eq => /= x ax. + apply: integral0_eq => /= x ax. apply: (@ge0_funenegE _ _ `]a, +oo[); last by rewrite inE/=. move=> ?/= ?; rewrite mulNr EFinN oppe_ge0 Fg0//=. - by rewrite inE/=. + by rewrite inE. rewrite integral_itv_obnd_cbnd//. under [X in _ _ X]eq_fun do rewrite mulNr; exact: measurableT_comp. Qed. Lemma integration_by_partsy_le0_le0 : - {in `]a, +oo[, forall x, (f x * G x)%:E <= 0} -> + {in `]a, +oo[, forall x, (f x * G x)%:E <= 0} -> {in `]a, +oo[, forall x, (F x * g x)%:E <= 0} -> \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E + \int[mu]_(x in `[a, +oo[) (- (f x * G x)%:E). Proof. move=> fG0 Fg0. rewrite NintNFg//. -rewrite (@integration_by_partsy_ge0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//; last 6 first. +rewrite (@integration_by_partsy_ge0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//. +- rewrite oppeB; last exact: fin_num_adde_defr. + rewrite -EFinN opprD 2!opprK mulNr. + by under eq_integral do rewrite mulNr EFinN. - by move=> ?; apply: cvgN; exact: cf. - exact: derivable_oy_continuous_bndN. - by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply. - by under eq_cvg do rewrite fctE/= mulNr; apply: cvgN. - by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: fG0. - by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: Fg0. -rewrite oppeB; last exact: fin_num_adde_defr. -rewrite -EFinN opprD 2!opprK mulNr. -by under eq_integral do rewrite mulNr EFinN. Qed. Lemma integration_by_partsy_ge0_le0 : - {in `]a, +oo[, forall x, 0 <= (f x * G x)%:E} -> + {in `]a, +oo[, forall x, 0 <= (f x * G x)%:E} -> {in `]a, +oo[, forall x, (F x * g x)%:E <= 0} -> \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E - \int[mu]_(x in `[a, +oo[) (f x * G x)%:E. Proof. move=> fG0 Fg0. rewrite NintNFg//. -rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//; last 6 first. +rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//. +- rewrite oppeD; last exact: fin_num_adde_defr. + rewrite -EFinN opprD 2!opprK mulNr. + by under eq_integral do rewrite mulNr EFinN oppeK. - by move=> ?; apply: cvgN; exact: cf. - exact: derivable_oy_continuous_bndN. - by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply. - by under eq_cvg do rewrite fctE/= mulNr; apply: cvgN. -- by move=> ? ?; rewrite mulNr EFinN oppe_le0; apply: fG0. -- by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: Fg0. -rewrite oppeD; last exact: fin_num_adde_defr. -rewrite -EFinN opprD 2!opprK mulNr. -by under eq_integral do rewrite mulNr EFinN oppeK. +- by move=> ? ?; rewrite mulNr EFinN oppe_le0; exact: fG0. +- by move=> ? ?; rewrite mulNr EFinN oppe_ge0; exact: Fg0. Qed. End integration_by_partsy_le0. @@ -1582,8 +1573,7 @@ have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)[ ((G \o F) * - F^`())%R. apply: open_continuous_measurable_fun; first exact: interval_open. move=> x; rewrite inE/= in_itv/= => /andP[ax _]. apply: continuousM; last first. - apply: continuousN. - by apply: cdF; rewrite in_itv/= andbT. + by apply: continuousN; apply: cdF; rewrite in_itv/= andbT. apply: continuous_comp. have := derivable_within_continuous dF. rewrite continuous_open_subspace; last exact: interval_open. @@ -1610,7 +1600,7 @@ transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a[) (G x)%:E)). exact: (@sub_trivIset _ _ _ [set: nat]). apply/measurable_EFinP. rewrite big_mkord -bigsetU_seqDU. - apply: (measurable_funS _ + apply: (measurable_funS _ _ (@bigsetU_bigcup _ (fun k =>`]F (a + k.+1%:R)%R, _[%classic) _)). exact: bigcup_measurable. apply/measurable_fun_bigcup => //. @@ -1663,7 +1653,7 @@ transitivity (limn (fun n => - exact: iota_uniq. - exact: (@sub_trivIset _ _ _ [set: nat]). - apply/measurable_EFinP. - apply: (measurable_funS (measurable_itv `]a, (a + n.+1%:R)[)). + apply: (measurable_funS `]a, (a + n.+1%:R)[) => //. rewrite big_mkord -bigsetU_seqDU. rewrite -(bigcup_mkord _ (fun k => `]a, (a + k.+1%:R)[%classic)). apply: bigcup_sub => k/= kn. diff --git a/theories/kernel.v b/theories/kernel.v index d5df49fa3f..9094cff8e5 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -899,8 +899,7 @@ apply: measurable_fun_if => //. - rewrite setTI [X in measurable X](_ : _ = [set t | f t setT != 0]). exact: kernel_measurable_neq_cst. by apply/seteqP; split => [x /negbT//|x /negbTE]. -- apply: (@measurable_funS _ _ _ _ setT) => //. - exact: kernel_measurable_fun_eq_cst. +- by apply: measurable_funTS => //; exact: kernel_measurable_fun_eq_cst. - apply: emeasurable_funM. exact: measurable_funS (measurable_kernel f U mU). apply/measurable_EFinP. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v index d83e7c0d77..694ff77778 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v @@ -142,11 +142,11 @@ have intg : mu.-integrable E (EFin \o h). exists h; split => //; rewrite [eps%:num]splitr; apply: le_lt_trans. pose fgh x := `|(f x - g x)%:E| + `|(g x - h x)%:E|. apply: (@ge0_le_integral _ _ _ mu _ mE _ fgh) => //. - - apply: (measurable_funS mE) => //; do 2 apply: measurableT_comp => //. + - apply: (measurable_funS E) => //; do 2 apply: measurableT_comp => //. exact: measurable_funB. - by move=> z _; rewrite adde_ge0. - apply: measurableT_comp => //; apply: measurable_funD; - apply: (measurable_funS mE (@subset_refl _ E)); + apply: (measurable_funS _ mE (@subset_refl _ E)); (apply: measurableT_comp => //); exact: measurable_funB. - move=> x _; rewrite -(subrK (g x) (f x)) -(addrA (_ + _)%R) lee_fin. @@ -161,12 +161,12 @@ rewrite EFinD lteD// -(setDKU AE) ge0_integral_setU => //; first last. - exact: measurableD. rewrite (@ae_eq_integral _ _ _ mu A (cst 0)) //; first last. - by apply: aeW => z Az; rewrite (gh z) ?inE// subrr abse0. -- apply: (measurable_funS mE) => //; do 2 apply: measurableT_comp => //. +- apply: (measurable_funS E) => //; do 2 apply: measurableT_comp => //. exact: measurable_funB. rewrite integral0 adde0. apply: (le_lt_trans (integral_le_bound (M *+ 2)%:E _ _ _ _)) => //. - exact: measurableD. -- apply: (measurable_funS mE) => //; apply: measurableT_comp => //. +- apply: (measurable_funS E) => //; apply: measurableT_comp => //. exact: measurable_funB. - by rewrite lee_fin mulrn_wge0// ltW. - apply: aeW => z [Ez _]; rewrite /= lee_fin mulr2n. @@ -331,7 +331,8 @@ Lemma locally_integrableS (A B : set R) f : Proof. move=> mA mB AB [mfB oT ifB]. have ? : measurable_fun [set: R] (f \_ A). - apply/(measurable_restrictT _ _).1 => //; apply: (measurable_funS _ AB) => //. + apply/(measurable_restrictT _ _).1 => //. + apply: (measurable_funS _ _ AB) => //. exact/(measurable_restrictT _ _).2. split => // K KT cK; apply: le_lt_trans (ifB _ KT cK). apply: ge0_le_integral => //=; first exact: compact_measurable. @@ -1043,7 +1044,7 @@ rewrite -invfM lef_pV2 ?posrE ?divr_gt0// -(@natr1 _ n) -lerBlDr. by near: n; exact: nbhs_infty_ger. Unshelve. all: by end_near. Qed. -Lemma lebesgue_differentiation f : locally_integrable setT f -> +Lemma lebesgue_differentiation f : locally_integrable [set: R] f -> {ae mu, forall x, lebesgue_pt f x}. Proof. move=> locf. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v index 4efad18f7f..2aa43358ef 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v @@ -229,7 +229,7 @@ split. apply/funext => n; apply: ae_eq_integral => //. + apply: measurableT_comp => //; apply: emeasurable_funB => //. apply/measurable_restrict => //; first exact: measurableD. - exact: (measurable_funS mD). + exact: (measurable_funS D). + by rewrite /g_; apply: measurableT_comp => //; exact: emeasurable_funB. + exists N; split => //; rewrite -(setCK N); apply: subsetC => x /= Nx Dx. by rewrite /f_' /f' /restrict mem_set. @@ -242,7 +242,7 @@ split. set Y := (X in _ -> _ --> X); rewrite [X in _ --> X -> _](_ : _ = Y) //. apply: ae_eq_integral => //. apply/measurable_restrict => //; first exact: measurableD. - exact: (measurable_funS mD). + exact: (measurable_funS D). exists N; split => //; rewrite -(setCK N); apply: subsetC => x /= Nx Dx. by rewrite /f' /restrict mem_set. Qed. diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v index 2cf18dca4d..84b9c28722 100644 --- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v +++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v @@ -456,8 +456,8 @@ have-> : D `&` (f \+ g) @^-1` A = by case: (f x) (g x) Afgx => [rf||] [rg||]. have Dfg : D `&` [set x | f x +? g x] `<=` D by apply: subIset; left. apply: hwlogD => //. -- by apply: (measurable_funS mD) => //; do ?exact: measurableI. -- by apply: (measurable_funS mD) => //; do ?exact: measurableI. +- by apply: (measurable_funS _ mD) => //; do ?exact: measurableI. +- by apply: (measurable_funS _ mD) => //; do ?exact: measurableI. - by rewrite -setIA setIid. - by move=> ? []. Qed. @@ -552,8 +552,8 @@ have-> : D `&` (fun x => f x * g x) @^-1` A = by apply: contra_notT NA0; rewrite negbK => /eqP <-. have Dfg : D `&` [set x | f x *? g x] `<=` D by apply: subIset; left. apply: hwlogM => //. -- by apply: (measurable_funS mD) => //; do ?exact: measurableI. -- by apply: (measurable_funS mD) => //; do ?exact: measurableI. +- by apply: (measurable_funS _ mD) => //; do ?exact: measurableI. +- by apply: (measurable_funS _ mD) => //; do ?exact: measurableI. - by rewrite -setIA setIid. - by move=> ? []. Qed. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index fb680408d1..f305e2527d 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -1708,7 +1708,7 @@ move=> mf mg mA Afin [C [mC C0 nC] epspos]. have [B [mB Beps Bunif]] : exists B, [/\ d.-measurable B, mu B < eps%:E & {uniform (A `\` C) `\` B, f @\oo --> g}]. apply: pointwise_almost_uniform => //. - - by move=> n; apply : (measurable_funS mA _ (mf n)) => ? []. + - by move=> n; apply : (measurable_funS _ mA _ (mf n)) => ? []. - by apply: measurableI => //; exact: measurableC. - by rewrite (le_lt_trans _ Afin)// le_measure// inE//; exact: measurableD. - by move=> x; rewrite setDE; case => Ax /(subsetC nC); rewrite setCK; exact. diff --git a/theories/measure_theory/measurable_function.v b/theories/measure_theory/measurable_function.v index c43a271cbf..54e7060f32 100644 --- a/theories/measure_theory/measurable_function.v +++ b/theories/measure_theory/measurable_function.v @@ -174,6 +174,7 @@ End measurable_fun. solve [apply: measurable_id] : core. Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}. Arguments measurable_fun_eqP {d1 d2 T1 T2 D} f {g}. +Arguments measurable_funS {d1 d2 T1 T2} E {D f}. Section mfun. Context {d d'} {aT : sigmaRingType d} {rT : sigmaRingType d'}. diff --git a/theories/realfun.v b/theories/realfun.v index 8d430961be..ed2af1071c 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1192,6 +1192,13 @@ Definition derivable_Nyo_continuous_bnd (f : R -> V) (x : R) := Definition derivable_oy_continuous_bnd (f : R -> V) (x : R) := {in `]x, +oo[, forall x, derivable f x 1} /\ f @ x^'+ --> f x. +Lemma derivable_oy_continuous_bndN (f : R -> V) (x : R) : + derivable_oy_continuous_bnd f x -> derivable_oy_continuous_bnd (- f) x. +Proof. +move=> [/= derF Fa]; split; last exact: cvgN. +by move=> /= ? ?; exact/derivableN/derF. +Qed. + Lemma derivable_oy_continuous_within_itvcy (f : R -> V) (x : R) : derivable_oy_continuous_bnd f x -> {within `[x, +oo[, continuous f}. Proof. From 51221f87da1c51e341969993194446ea323a8dc5 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:01:39 +0900 Subject: [PATCH 04/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index b5ed70d5a3..66b6556aca 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -889,9 +889,8 @@ Let FGaoo : Proof. apply: cvg_EFin; first exact: nearW; apply: cvgB; last exact: cvg_cst. rewrite -cvg_shiftS/=. -apply: (@cvg_comp _ _ _ _ (F \* G)%R _ +oo%R); last exact: cvgFG; apply/cvgeryP. -apply: (@cvge_pinftyP R (fun x => (a + x)%:E) +oo).1; last exact: cvgr_idn. -by apply/cvgeryP; exact: cvg_addrl. +apply: (@cvg_comp _ _ _ _ (F \* G)%R _ +oo%R); last exact: cvgFG. +by apply: cvg_comp; [apply: cvgr_idn|apply: cvg_addrl]. Qed. Let sumN_Nsum_fG n : From 416f04e3d2907e8dbffd1f6246fa1aaefe0878a8 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:01:55 +0900 Subject: [PATCH 05/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/ftc.v b/theories/ftc.v index 66b6556aca..502ebb4dcf 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -901,7 +901,7 @@ Let sumN_Nsum_fG n : (\int[mu]_(x in seqDU (fun k => `]a, a + k%:R]) i) (f x * G x)%:E)%E). Proof. -rewrite big_nat_cond fin_num_sumeN; rewrite -?big_nat_cond//; move=> m _. +rewrite big_nat_cond fin_num_sumeN -?big_nat_cond// => m _. rewrite seqDUE integral_itv_obnd_cbnd; last first. apply: measurable_funS mfG => //. by apply/subset_itv => //; rewrite bnd_simp// lerDl. From ee10e62a4939f96e91e57cd4938e4cf53d5198b2 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:02:11 +0900 Subject: [PATCH 06/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/ftc.v b/theories/ftc.v index 502ebb4dcf..a60bd202f6 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -908,7 +908,7 @@ rewrite seqDUE integral_itv_obnd_cbnd; last first. apply: integrable_fin_num => //=. apply: continuous_compact_integrable; first exact: segment_compact. apply: continuous_subspaceW cfG. -by apply/subset_itv => //; rewrite bnd_simp// lerDl. +by apply: subset_itv; rewrite // bnd_simp// lerDl. Qed. Let sumNint_sumintN_fG n : From 1d4fad1911a92e967f787741b76665b18e6a2e98 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:02:26 +0900 Subject: [PATCH 07/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index a60bd202f6..b9dc69ca56 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -923,10 +923,9 @@ rewrite big_nat_cond [RHS]big_nat_cond. apply: eq_bigr => i. rewrite seqDUE andbT => i0n. rewrite 2?integral_itv_obnd_cbnd; last 2 first. - apply: measurableT_comp => //. - apply: measurable_funS mfG => //. +- apply: measurableT_comp => //; apply: measurable_funS mfG => //. by apply/subset_itv; rewrite bnd_simp// lerDl. - apply: measurable_funS mfG => //. +- apply: measurable_funS mfG => //. by apply/subset_itv; rewrite bnd_simp// lerDl. rewrite -integralN ?integrable_add_def ?continuous_compact_integrable//. exact: segment_compact. From e1f402de4311b5a3e865a31ec050d7afa5c8ddc9 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:02:41 +0900 Subject: [PATCH 08/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index b9dc69ca56..1783b65037 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -929,8 +929,7 @@ rewrite 2?integral_itv_obnd_cbnd; last 2 first. by apply/subset_itv; rewrite bnd_simp// lerDl. rewrite -integralN ?integrable_add_def ?continuous_compact_integrable//. exact: segment_compact. -apply: continuous_subspaceW cfG. -by apply/subset_itv; rewrite bnd_simp// lerDl. +by apply: continuous_subspaceW cfG; apply/subset_itv; rewrite bnd_simp// lerDl. Qed. Let sum_integral_limn : From 56962a5dea6463f70b98800d97d21090aed6bfd7 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:03:03 +0900 Subject: [PATCH 09/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 1783b65037..7810b20bd9 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -940,10 +940,9 @@ Let sum_integral_limn : - \int[mu]_(x in seqDU (fun k => `]a, (a + k%:R)]) i) (f x * G x)%:E). Proof. -apply: congr_lim; apply/funext => n. -case: n. +apply/congr_lim/funext; case. by rewrite big_nat_cond [in RHS]big_nat_cond 2?big_pred0//= 2!addr0 subrr. -case => [|n]. +case=> [|n]. rewrite 2!big_nat1 seqDUE -pred_Sn addr0 subrr add0r. by rewrite set_itvoc0 2!integral_set0 oppe0. rewrite big_nat_recl// [in RHS]big_nat_recl//=. From 29e41af8870671165424de5e1c68f9fd145ee1fb Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:03:22 +0900 Subject: [PATCH 10/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/ftc.v b/theories/ftc.v index 7810b20bd9..17fba766d1 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -966,7 +966,7 @@ under eq_bigr => i _. over. rewrite big_split/=. under eq_bigr do rewrite EFinB. -rewrite telescope_sume// addr0; congr +%E. +rewrite telescope_sume => [|//|//]; rewrite addr0; congr +%E. apply: eq_bigr => k _; rewrite seqDUE/= integral_itv_obnd_cbnd//. apply: measurable_funS mfG => //. by apply/subset_itv => //; rewrite bnd_simp lerDl. From bbfb61168d6280bf10a304a10c65bde4b57f5594 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:03:43 +0900 Subject: [PATCH 11/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/ftc.v b/theories/ftc.v index 17fba766d1..c2b327f311 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -982,7 +982,7 @@ move=> fG0 Fg0. rewrite -integral_itv_obnd_cbnd// -[in RHS]integral_itv_obnd_cbnd//. rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq. rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight. -- rewrite sum_integral_limn; apply/cvg_lim => //. +- rewrite [LHS]sum_integral_limn; apply: cvg_lim => //. apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo. under eq_cvg do rewrite sumN_Nsum_fG; apply: cvgeN. apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x. From 1c8a7bd787be9ec3e00c6996b943b422c5d538b1 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:03:57 +0900 Subject: [PATCH 12/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/ftc.v b/theories/ftc.v index c2b327f311..9e692896e6 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1008,7 +1008,7 @@ have mMfG : measurable_fun `]a, +oo[ (fun x => (- (f x * G x))%R). rewrite -integral_itv_obnd_cbnd// -[in RHS]integral_itv_obnd_cbnd//. rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq. rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight. -- rewrite sum_integral_limn; apply/cvg_lim => //. +- rewrite [LHS]sum_integral_limn; apply: cvg_lim => //. apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo. under eq_cvg do rewrite sumNint_sumintN_fG. apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x. From 6d646847081423186bfadae3fda1ff6ee030625b Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:04:12 +0900 Subject: [PATCH 13/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/ftc.v b/theories/ftc.v index 9e692896e6..8886c6604e 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1016,7 +1016,7 @@ rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight. apply: fG0; rewrite inE/=. by apply: subset_itv anx; rewrite bnd_simp// lerDl. - by move=> k; apply: measurableD => //; apply: bigsetU_measurable. -- by apply/measurable_EFinP; exact: measurableT_comp. +- exact/measurable_EFinP/measurableT_comp. - by move=> ? ?; rewrite EFinN oppe_ge0 fG0// inE. - by move=> k; apply: measurableD => //; apply: bigsetU_measurable. - exact/measurable_EFinP. From 13d160aae8a5b5c858128941f1de65e6472fe910 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:04:33 +0900 Subject: [PATCH 14/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 8886c6604e..b1b3275894 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1045,8 +1045,8 @@ Proof. apply: subspace_continuous_measurable_fun => //. rewrite continuous_open_subspace// => x ax. apply: cvgM. - have [+ _]:= Foy; move/derivable_within_continuous. - by rewrite continuous_open_subspace//; apply. + have [/derivable_within_continuous + _] := Foy. + by rewrite continuous_open_subspace => [|//]; apply. have /continuous_within_itvcyP[+ _] := cg. by apply; rewrite inE/= in ax. Qed. From d3ae24187d4011851bbfefa5219abe722ddd1bec Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:04:50 +0900 Subject: [PATCH 15/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index b1b3275894..3630ba9842 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1059,8 +1059,7 @@ move=> Fg0. rewrite -integral_itv_obnd_cbnd//. under eq_integral => x do rewrite -(opprK (F x)) mulNr EFinN. rewrite integralN/=; last first. - apply: fin_num_adde_defl. - apply/EFin_fin_numP; exists 0%R. + apply/fin_num_adde_defl/EFin_fin_numP; exists 0%R. apply/eqe_oppLRP; rewrite oppe0. apply: integral0_eq => /= x ax. apply: (@ge0_funenegE _ _ `]a, +oo[); last by rewrite inE/=. From 2cc1eafb16bc40bfaa6ab9b159666ebff191a151 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:05:05 +0900 Subject: [PATCH 16/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 3630ba9842..62e24903dd 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1063,8 +1063,7 @@ rewrite integralN/=; last first. apply/eqe_oppLRP; rewrite oppe0. apply: integral0_eq => /= x ax. apply: (@ge0_funenegE _ _ `]a, +oo[); last by rewrite inE/=. - move=> ?/= ?; rewrite mulNr EFinN oppe_ge0 Fg0//=. - by rewrite inE. + by move=> ?/= ?; rewrite mulNr EFinN oppe_ge0 Fg0//= inE. rewrite integral_itv_obnd_cbnd//. under [X in _ _ X]eq_fun do rewrite mulNr; exact: measurableT_comp. Qed. From 8132f6b7d63fd8d7f7f7e48d2ed51ce66138e365 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:05:29 +0900 Subject: [PATCH 17/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/theories/ftc.v b/theories/ftc.v index 62e24903dd..b750242340 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1076,13 +1076,16 @@ Lemma integration_by_partsy_le0_le0 : Proof. move=> fG0 Fg0. rewrite NintNFg//. -rewrite (@integration_by_partsy_ge0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//. +rewrite (@integration_by_partsy_ge0_ge0 R (- F)%R G (- f)%R g a (- FGoo)). - rewrite oppeB; last exact: fin_num_adde_defr. rewrite -EFinN opprD 2!opprK mulNr. by under eq_integral do rewrite mulNr EFinN. - by move=> ?; apply: cvgN; exact: cf. - exact: derivable_oy_continuous_bndN. - by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply. +- by []. +- by []. +- by []. - by under eq_cvg do rewrite fctE/= mulNr; apply: cvgN. - by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: fG0. - by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: Fg0. From 2b869ba7072783c96e039aca10dc7e5d6d4aca13 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:07:28 +0900 Subject: [PATCH 18/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index b750242340..30ecc7275b 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1074,8 +1074,7 @@ Lemma integration_by_partsy_le0_le0 : \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E + \int[mu]_(x in `[a, +oo[) (- (f x * G x)%:E). Proof. -move=> fG0 Fg0. -rewrite NintNFg//. +move=> fG0 Fg0; rewrite NintNFg//. rewrite (@integration_by_partsy_ge0_ge0 R (- F)%R G (- f)%R g a (- FGoo)). - rewrite oppeB; last exact: fin_num_adde_defr. rewrite -EFinN opprD 2!opprK mulNr. From 42b28b4f31ea60572f4343d5bfbee5a7c262fe6e Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:07:49 +0900 Subject: [PATCH 19/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 30ecc7275b..a06edae36e 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1096,8 +1096,7 @@ Lemma integration_by_partsy_ge0_le0 : \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E - \int[mu]_(x in `[a, +oo[) (f x * G x)%:E. Proof. -move=> fG0 Fg0. -rewrite NintNFg//. +move=> fG0 Fg0; rewrite NintNFg//. rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//. - rewrite oppeD; last exact: fin_num_adde_defr. rewrite -EFinN opprD 2!opprK mulNr. From 2f5767f1fe2af529792b1583b80f9de110004f43 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:08:05 +0900 Subject: [PATCH 20/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/ftc.v b/theories/ftc.v index a06edae36e..42177b1344 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1081,7 +1081,7 @@ rewrite (@integration_by_partsy_ge0_ge0 R (- F)%R G (- f)%R g a (- FGoo)). by under eq_integral do rewrite mulNr EFinN. - by move=> ?; apply: cvgN; exact: cf. - exact: derivable_oy_continuous_bndN. -- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply. +- by move=> ? ?; rewrite fctE derive1N ?Ff => [//|//|]; apply: Foy.1. - by []. - by []. - by []. From 7facd275e40f1345f3a7738403b3fcf82094b84c Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:08:31 +0900 Subject: [PATCH 21/22] Update theories/ftc.v Co-authored-by: Quentin VERMANDE --- theories/ftc.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/theories/ftc.v b/theories/ftc.v index 42177b1344..69f6926e80 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1097,13 +1097,16 @@ Lemma integration_by_partsy_ge0_le0 : \int[mu]_(x in `[a, +oo[) (f x * G x)%:E. Proof. move=> fG0 Fg0; rewrite NintNFg//. -rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//. +rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo)). - rewrite oppeD; last exact: fin_num_adde_defr. rewrite -EFinN opprD 2!opprK mulNr. by under eq_integral do rewrite mulNr EFinN oppeK. - by move=> ?; apply: cvgN; exact: cf. - exact: derivable_oy_continuous_bndN. - by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply. +- by []. +- by []. +- by []. - by under eq_cvg do rewrite fctE/= mulNr; apply: cvgN. - by move=> ? ?; rewrite mulNr EFinN oppe_le0; exact: fG0. - by move=> ? ?; rewrite mulNr EFinN oppe_ge0; exact: Fg0. From 66bb713d2450eb15230aabd2abec04138d4cbe3f Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 18 Nov 2025 11:08:57 +0900 Subject: [PATCH 22/22] Update theories/realfun.v Co-authored-by: Quentin VERMANDE --- theories/realfun.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/realfun.v b/theories/realfun.v index ed2af1071c..6b278c1ef2 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1195,7 +1195,7 @@ Definition derivable_oy_continuous_bnd (f : R -> V) (x : R) := Lemma derivable_oy_continuous_bndN (f : R -> V) (x : R) : derivable_oy_continuous_bnd f x -> derivable_oy_continuous_bnd (- f) x. Proof. -move=> [/= derF Fa]; split; last exact: cvgN. +case=> /= derF Fa; split; last exact: cvgN. by move=> /= ? ?; exact/derivableN/derF. Qed.