From 949b179386d1f2038dd7eb57adb23de8ee442316 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Fri, 4 Jul 2025 16:58:11 +0900 Subject: [PATCH] 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 bb6f83da8..b5e8815d7 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -102,6 +102,12 @@ - in `lebesgue_integral_nonneg.v`: + lemma `ge0_integral_ereal_sup` (was a `Let`) +- 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 `convex.v`: diff --git a/theories/ftc.v b/theories/ftc.v index 89676f684..8d046e7c0 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.