From baacc9099f28ac4035f7a7c4d13052ca1390dc99 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Fri, 16 Jan 2026 15:41:41 +0900 Subject: [PATCH 01/30] rename and boolify some predicates for open intervals --- CHANGELOG_UNRELEASED.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 318217cd5..597a5e4e7 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -20,6 +20,8 @@ - in probability.v + lemma `pmf_ge0` + lemmas `pmf_gt0_countable`, `pmf_measurable` +- in set_interval.v + + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends` ### Changed - in set_interval.v @@ -135,6 +137,8 @@ * definition `pmf` * lemmas `pmf_ge0`, `pmf_gt0_countable`, `pmf_measurable`, `dRV_expectation`, `expectation_pmf` +- in set_interval.v + + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool) ### Renamed - in `set_interval.v`: @@ -162,6 +166,9 @@ + `weak_sep_nbhsE` -> `initial_sep_nbhsE` + `weak_sep_openE` -> `initial_sep_openE` + `join_product_weak` -> `join_product_initial` +- in set_interval.v + + `itv_is_ray` -> `itv_is_open_unbounded`, + + `itv_is_bd_open` -> `itv_is_oo`, ### Generalized From 0f54bc5dc2e443f55ffe857866ac31ab4c48bd68 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Sat, 17 Jan 2026 15:30:08 +0900 Subject: [PATCH 02/30] address review comments --- CHANGELOG_UNRELEASED.md | 4 ++-- classical/set_interval.v | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 597a5e4e7..d4a80802b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -167,8 +167,8 @@ + `weak_sep_openE` -> `initial_sep_openE` + `join_product_weak` -> `join_product_initial` - in set_interval.v - + `itv_is_ray` -> `itv_is_open_unbounded`, - + `itv_is_bd_open` -> `itv_is_oo`, + + `itv_is_ray` -> `itv_is_open_unbounded` + + `itv_is_bd_open` -> `itv_is_oo` ### Generalized diff --git a/classical/set_interval.v b/classical/set_interval.v index e0d26aaa6..1395bd594 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -860,6 +860,7 @@ Definition itv_closed_ends i : bool := itv_is_closed_unbounded i || itv_is_cc i. End closed_endpoints. +Arguments itv_open_ends {d T} !i /. Lemma itv_open_endsI {d} {T : orderType d} (i j : interval T) : itv_open_ends i -> itv_open_ends j -> itv_open_ends (i `&` j)%O. Proof. From 4f05af60760f10e6cb81e226ebb2017f53289f5e Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Sun, 18 Jan 2026 02:22:49 +0900 Subject: [PATCH 03/30] revert experimental Arguments declaration --- classical/set_interval.v | 1 - 1 file changed, 1 deletion(-) diff --git a/classical/set_interval.v b/classical/set_interval.v index 1395bd594..e0d26aaa6 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -860,7 +860,6 @@ Definition itv_closed_ends i : bool := itv_is_closed_unbounded i || itv_is_cc i. End closed_endpoints. -Arguments itv_open_ends {d T} !i /. Lemma itv_open_endsI {d} {T : orderType d} (i j : interval T) : itv_open_ends i -> itv_open_ends j -> itv_open_ends (i `&` j)%O. Proof. From 18b1844b770f50bdf0b14f3a6e2ab04303ecc9f5 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Fri, 4 Jul 2025 16:58:11 +0900 Subject: [PATCH 04/30] integration_by_party --- CHANGELOG_UNRELEASED.md | 74 ++++++++++ theories/ftc.v | 320 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 394 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d4a80802b..7b97c5fec 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -23,6 +23,80 @@ - in set_interval.v + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends` +- in `set_interval.v`: + + lemmas `itv_setU_setT`, `disjoint_rays` + +- in `constructive_ereal.v`: + + lemma `ltgte_fin_num` + +- in `probability.v`: + + definition `ccdf` + + lemmas `lebesgue_stieltjes_cdf_id`, `cdf_ccdf_1`, `ccdf_nonincreasing`, `cvg_ccdfy0`, `cvg_ccdfNy1`, `ccdf_right_continuous`, `ge0_expectation_ccdf` + + corollaries `ccdf_cdf_1`, `ccdf_1_cdf`, `cdf_1_ccdf` + +- in `num_normedtype.v`: + + lemma `nbhs_infty_gtr` +- in `function_spaces.v`: + + lemmas `cvg_big`, `continuous_big` + +- in `realfun.v`: + + lemma `cvg_addrl_Ny` + +- in `constructive_ereal.v`: + + lemmas `mule_natr`, `dmule_natr` + + lemmas `inve_eqy`, `inve_eqNy` + +- in `uniform_structure.v`: + + lemma `continuous_injective_withinNx` + +- in `constructive_ereal.v`: + + variants `Ione`, `Idummy_placeholder` + + inductives `Inatmul`, `IEFin` + + definition `parse`, `print` + + number notations in scopes `ereal_dual_scope` and `ereal_scope` + + notation `- 1` in scopes `ereal_dual_scope` and `ereal_scope` +- in `pseudometric_normed_Zmodule.v`: + + lemma `le0_ball0` +- in `theories/landau.v`: + + lemma `littleoE0` + +- in `constructive_ereal.v`: + + lemma `lt0_adde` + +- in `unstable.v` + + lemmas `coprime_prodr`, `Gauss_dvd_prod`, `expn_prod`, `mono_leq_infl`, + `card_big_setU` + +- file `pnt.v` + + definitions `next_prime`, `prime_seq` + + lemmas `leq_prime_seq`, `mem_prime_seq` + + theorem `dvg_sum_inv_prime_seq` +- new directory `theories/measure_theory` with new files: + + `measurable_structure.v` + + `measure_function.v` + + `counting_measure.v` + + `dirac_measure.v` + + `probability_measure.v` + + `measure_negligible.v` + + `measure_extension.v` + + `measurable_function.v` + + `measure.v` + +- in `realfun.v`: + + lemmas `derivable_oy_continuous_within_itvcy`, + `derivable_oy_continuous_within_itvNyc` + + lemmas `derivable_oo_continuousW`, + `derivable_oy_continuousWoo`, + `derivable_oy_continuousW`, + `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 set_interval.v + `itv_is_closed_unbounded` (fix the definition) diff --git a/theories/ftc.v b/theories/ftc.v index b83b6a397..164af8f2a 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -839,6 +839,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 d26a12064bd4c9727d527e2d12da9542f6b556eb Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 30 Oct 2025 16:07:04 +0900 Subject: [PATCH 05/30] 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 164af8f2a..b2e719016 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -839,39 +839,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. @@ -952,11 +919,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. @@ -988,7 +955,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. @@ -1071,11 +1038,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 40a6ae7a3509700588f940e18570a1accbb86c9f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 30 Oct 2025 18:32:26 +0900 Subject: [PATCH 06/30] lint --- CHANGELOG_UNRELEASED.md | 256 ++++++++++++++++++ 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 | 8 + 10 files changed, 400 insertions(+), 145 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 7b97c5fec..a613ec1c2 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -91,6 +91,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`, @@ -214,6 +217,259 @@ - in set_interval.v + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool) +- in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`: + + lemma `nondecreasing_right_continuousP` + + definition `CumulativeBounded` + +- in `lebesgue_stieltjes_measure.v`, according to generalization of `Cumulative`, modified: + + lemmas `wlength_ge0`, `cumulative_content_sub_fsum`, `wlength_sigma_subadditive`, `lebesgue_stieltjes_measure_unique` + + definitions `lebesgue_stieltjes_measure`, `completed_lebesgue_stieltjes_measure` + +- moved from `vitali_lemma.v` to `pseudometric_normed_Zmodule.v` and renamed: + + `closure_ball` -> `closure_ballE` + +- moved from `theories/measure.v` (now removed) + + to `sequences.v`: + * lemmas `epsilon_trick`, `epsilon_trick0` + + to `measure_theory/measurable_structure.v`: + * definitions `setC_closed`, `setI_closed`, `setU_closed`, `setSD_closed`, + `setD_closed`, `setY_closed`, `fin_bigcap_closed`, `finN0_bigcap_closed`, + `fin_bigcup_closed`, `semi_setD_closed` + * lemma `setD_semi_setD_closed` + * definitions `ndseq_closed`, `niseq_closed`, `trivIset_closed`, `fin_trivIset_closed`, + `setring`, `sigma_ring`, `sigma_algebra`, `dynkin`, `lambda_system`, + `monotone` + * lemmas `powerset_sigma_ring`, `powerset_lambda_system` + * notations `<>`, `<>`, `<>`, `<>`, `<>`, + `<>`, `<>`, `<>` + * lemmas `lambda_system_smallest`, `fin_bigcup_closedP`, `finN0_bigcap_closedP`, + `setD_closedP`, `sigma_algebra_bigcap`, `sigma_algebraP`, `smallest_sigma_algebra`, + `sub_sigma_algebra2`, `sigma_algebra_id`, `sub_sigma_algebra`, + `sigma_algebra0`, `sigma_algebraCD`, `sigma_algebra_bigcup`, + `smallest_setring`, `sub_setring2`, `setring_id`, `sub_setring`, + `setring0`, `setringD`, `setringU`, `setring_fin_bigcup`, `g_sigma_algebra_lambda_system`, + `smallest_sigma_ring`, `sigma_ring_monotone`, `g_sigma_ring_monotone`, + `sub_g_sigma_ring`, `setring_monotone_sigma_ring`, `g_monotone_monotone`, + `g_monotone_setring`, `g_monotone_g_sigma_ring`, `monotone_setring_sub_g_sigma_ring`, + `smallest_lambda_system`, `lambda_system_subset`, `dynkinT`, `dynkinC`, + `dynkinU`, `dynkin_lambda_system`, `g_dynkin_dynkin`, `sigma_algebra_dynkin`, + `dynkin_setI_sigma_algebra`, `setI_closed_g_dynkin_g_sigma_algebra` + * definition `strace` + * lemmas `subset_strace`, `g_sigma_ring_strace`, `strace_sigma_ring`, + `setI_g_sigma_ring`, `sigma_algebra_strace` + * mixin `isSemiRingOfSets`, structure `SemiRingOfSets`, + notation `semiRingOfSetsType` + * lemma `measurable_curry` + * notations `.-measurable`, `'measurable` + * mixin `SemiRingOfSets_isRingOfSets`, structure `RingOfSets`, + notation `ringOfSetsType` + * mixin `RingOfSets_isAlgebraOfSets`, structure `AlgebraOfSets`, + notation `algebraOfSetsType` + * mixin `hasMeasurableCountableUnion` + * structure `SigmaRing`, structure `SigmaRing`, notation `sigmaRingType` + * factory `isSigmaRing` + * structure `Measurable`, notation `measurableType` + * factories `isRingOfSets`, `isRingOfSets_setY`, `isAlgebraOfSets`, + `isAlgebraOfSets_setD`, `isMeasurable` + * lemmas `bigsetU_measurable`, `fin_bigcup_measurable`, `measurableD`, + `seqDU_measurable`, ` measurableC`, `bigsetI_measurable`, `fin_bigcap_measurable`, + `measurableID`, `bigcup_measurable`, `bigcap_measurable`, `bigcapT_measurable`, + `countable_measurable`, `sigmaRingType_lambda_system`, `countable_bigcupT_measurable`, + `bigcupT_measurable_rat`, `sigma_algebra_measurable`, `bigcap_measurableType` + * definition `discrete_measurable` + * lemmas `discrete_measurable0`, `discrete_measurableC`, `discrete_measurableU` + * definitions `sigma_display`, `g_sigma_algebraType` + * lemmas `sigma_algebraC` + * notations `.-sigma`, `.-sigma.-measurable` + * lemma `measurable_g_measurableTypeE` + * definition `preimage_set_system` + * lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, + `preimage_set_system_id`, `sigma_algebra_preimage` + * definition `image_set_system` + * lemmas `sigma_algebra_image`, `g_sigma_preimageE` + * definition `subset_sigma_subadditive` + * lemmas `big_trivIset` + * definition `covered_by` + * lemmas `covered_bySr`, `covered_byP`, `covered_by_finite`, `covered_by_countable`, + `measurable_uncurry` + * definition `g_sigma_preimageU` + * lemmas `g_sigma_preimageU_comp` + * definition `measure_prod_display` + * notation `.-prod`, `.-prod.-measurable` + * lemmas `measurableX`, `measurable_prod_measurableType`, + `measurable_prod_g_measurableTypeR`, `measurable_prod_g_measurableType` + * definition `g_sigma_preimage` + * lemma `g_sigma_preimage_comp` + * definition `measure_tuple_display` + * definition `measure_dominates`, notation ``` `<< ``` + * lemma `measure_dominates_trans` + + to `measure_theory/measure_function.v`: + * definitions `semi_additive2`, `semi_additive`, `semi_sigma_additive`, + `additive2`, `additive`, `sigma_additive`, `subadditive`, + `measurable_subset_sigma_subadditive` + * lemma `semi_additiveW` + * lemmas `semi_additiveE`, `semi_additive2E`, `additive2P` + * lemmas `semi_sigma_additive_is_additive`, `semi_sigma_additiveE`, + `sigma_additive_is_additive` + * mixin `isContent`, structure `Content`, notation `{content set _ -> \bar _}` + * lemma `content_inum_subproof` + * lemmas `measure0`, `measure_gt0`, `measure_semi_additive_ord`, + `measure_semi_additive_ord_I`, `content_fin_bigcup`, `measure_semi_additive2` + * lemmas `measureU`, `measure_bigsetU`, `measure_fin_bigcup`, + `measure_bigsetU_ord_cond`, `measure_bigsetU_ord`, `measure_fbigsetU` + * mixin `Content_isMeasure` + * structure `Measure`, notations `measure`, + `{measure set _ -> \bar _}` + * lemma `measure_inum_subproof` + * factory `isMeasure`, lemma `eq_measure` + * lemmma `measure_semi_bigcup` + * lemmas `measure_sigma_additive`, `measure_bigcup` + * definition `msum` + * definition `mzero`, lemma `msum_mzero` + * definition `measure_add`, `measure_addE` + * definition `mscale` + * definition `mseries` + * definition `pushforward` + * module `SetRing` + * notations `.-ring`, `.-ring.-measurable` + * lemmas `le_measure`, `measure_le0` + * lemmas `content_subadditive`, `content_sub_fsum` + * lemmas `content_ring_sup_sigma_additive`, `content_ring_sigma_additive` + * lemmas `ring_sigma_subadditive`, `ring_semi_sigma_additive`, + `semiring_sigma_additive` + * factory `Content_SigmaSubAdditive_isMeasure` + * lemma `measure_sigma_subadditive` + * lemma `measure_sigma_subadditive_tail` + * definition `fin_num_fun` + * lemmas `fin_num_fun_lty`, `lty_fin_num_fun` + * definitions `sfinite_measure`, `sigma_finite` + * lemma `fin_num_fun_sigma_finite` + * definition `mrestr` + * lemma `sfinite_measure_sigma_finite` + * mixin `isSFinite`, structure `SFiniteMeasure`, + notation `{sfinite_measure set _ -> \bar _}` + * mixin `isSigmaFinite`, structure `SigmaFiniteContent`, + notation `sigma_finite_content`, `{sigma_finite_content set _ -> \bar _}` + * structure `SigmaFiniteMeasure`, notations `sigma_finite_measure`, + `{sigma_finite_measure set _ -> \bar _}` + * factory `Measure_isSigmaFinite` + * lemmas `sigma_finite_mzero`, `sfinite_mzero` + * mixin `isFinite`, structures `FinNumFun`, `FiniteMeasure`, + notation `{finite_measure set _ -> \bar _}` + * factories `Measure_isFinite`, `Measure_isSFinite` + * definition `sfinite_measure_seq` + * lemma `sfinite_measure_seqP` + * definition `mfrestr` + * lemmas `measureIl`, `measureIr`, `subset_measure0` + * lemmas `measureDI`, `measureD`, `measureU2` + * lemmas `measureUfinr`, `measureUfinl`, `null_set_setU`, `measureU0` + * lemma `eq_measureU` + * lemma `g_sigma_algebra_measure_unique_trace` + * lemmas `nondecreasing_cvg_mu`, `nonincreasing_cvg_mu` + * definition `lim_sup_set` + * lemmas `lim_sup_set_ub`, `lim_sup_set_cvg` + * lemma `lim_sup_set_cvg0` + * theorem `Boole_inequality` + * lemma `sigma_finiteP` + * theorem `generalized_Boole_inequality` + * lemmas `g_sigma_algebra_measure_unique_cover`, `g_sigma_algebra_measure_unique` + * lemma `measure_unique` + + to `measure_theory/counting_measure.v`: + * definition `counting` + * lemma `sigma_finite_counting` + + to `measure_theory/dirac_measure.v`: + * definition `dirac`, notation `\d_` + * lemmas `finite_card_sum`, `finite_card_dirac`, `infinite_card_dirac ` + + to `measure_theory/probability_measure.v`: + * mixin `isSubProbability`, structure `SubProbability`, notation `subprobability` + * factory `Measure_isSubProbability` + * mixin `isProbability`, structure `Probability`, notation `probability` + * lemmas `probability_le1`, `probability_setC` + * factory `Measure_isProbability` + * definition `mnormalize` + * lemmas `mnormalize_id` + * definitions `mset`, `pset`, `pprobability` + * lemmas `lt0_mset`, `gt1_mset` + + to `measure_theory/measure_negligible.v`: + * definition `negligible`, notation `.-negligible` + * lemmas `negligibleP`, `negligible_set0`, `measure_negligible`, `negligibleS`, + `negligibleI` + * definition `measure_is_complete` + * lemmas `negligibleU`, `negligible_bigsetU`, `negligible_bigcup` + * definition `almost_everywhere`, `ae_filter_ringOfSetsType`, + `ae_properfilter_algebraOfSetsType` + * definition `ae_eq`, notations `{ae _, _}`, `\forall _ \ae _, _`, + `_ = _ [%ae _ in _]`, `_ = _ %[ae _]` + * lemmas `measure0_ae`, `aeW` + * instance `ae_eq_equiv` + * instances `comp_ae_eq`, `comp_ae_eq2`, `comp_ae_eq2'`, `sub_ae_eq2` + * lemmas `ae_eq0`, `ae_eq_refl`, `ae_eq_comp`, `ae_eq_comp2`, + `ae_eq_funeposneg`, `ae_eq_sym`, `ae_eq_trans`, `ae_eq_sub`, + `ae_eq_mul2r`, `ae_eq_mul2l`, `ae_eq_mul1l`, `ae_eq_abse`, `ae_foralln` + * lemmas `ae_eq_subset`, `ae_eqe_mul2l` + * lemma `measure_dominates_ae_eq` + + to `measure_theory/measure_extension.v`: + * definitions `sigma_subadditive`, `subset_sigma_subadditive` + * mixin `isOuterMeasure`, structure `OuterMeasure` + * notation `{outer_measure set _ -> \bar _}` + * factory `isSubsetOuterMeasure` + * lemmas `outer_measure_sigma_subadditive_tail`, `outer_measure_subadditive`, + `outer_measureU2`, `le_outer_measureIC` + * definition `caratheodory_measurable`, notation `.-caratheodory` + * lemma `le_caratheodory_measurable` + * lemmas `outer_measure_bigcup_lim`, `caratheodory_measurable_set0`, + `caratheodory_measurable_setC`, `caratheodory_measurable_setU_le`, + `caratheodory_measurable_setU`, `caratheodory_measurable_bigsetU`, + `caratheodory_measurable_setI`, `caratheodory_measurable_setD`, + `disjoint_caratheodoryIU`, `caratheodory_additive`, `caratheodory_lime_le`, + `caratheodory_measurable_trivIset_bigcup`, `caratheodory_measurable_bigcup` + * definition `caratheodory_type`, notation `.-cara.-measurable` + * definition `caratheodory_display`, notation `.-cara` + * lemmas `caratheodory_measure0`, `caratheodory_measure_ge0`, + `caratheodory_measure_sigma_additive`, `measure_is_complete_caratheodory` + * definition `measurable_cover`, lemmas `cover_measurable`, `cover_subset` + * definition `mu_ext`, notation `^*` + * lemmas `le_mu_ext`, `mu_ext_ge0`, `mu_ext0`, `mu_ext_sigma_subadditive` + * lemmas `Rmu_ext`, `measurable_mu_extE`, `measurable_Rmu_extE` + * lemma `sub_caratheodory` + * definition `measure_extension` + * lemmas `measure_extension_sigma_finite`, `measure_extension_unique` + * lemma `caratheodory_measurable_mu_ext` + * definition `completed_measure_extension` + * lemma `completed_measure_extension_sigma_finite` + + to `measure_theory/measurable_function.v`: + * mixin `isMeasurableFun`, structure `MeasurableFun`, notations `{mfun _ >-> _}`, + `[mfun of _]` + * lemmas `measurable_funP`, `measurable_funPTI` + * definitions `mfun`, `mfun_key`, canonical `mfun_keyed` + * lemmas `measurable_id`, `measurable_comp`, `eq_measurable_fun`, + `measurable_fun_eqP`, `measurable_cst`, `measurable_fun_bigcup`, + `measurable_funU`, `measurable_funS`, `measurable_fun_if`, + `measurable_fun_set0`, `measurable_fun_set1` + * definitions `mfun_Sub_subproof`, `mfun_Sub` + * lemmas `mfun_rect`, `mfun_val`, `mfuneqP` + * lemmas `measurableT_comp`, `measurable_funTS`, `measurable_restrict`, + `measurable_restrictT`, `measurable_fun_ifT`, `measurable_fun_bool`, + `measurable_and`, `measurable_neg`, `measurable_or` + * lemmas `preimage_set_system_measurable_fun`, `measurability` + * lemmas `measurable_fun_pairP`, `measurable_fun_pair` + * lemmas `measurable_fst`, `measurable_snd`, `measurable_swap` + * lemmas `measurable_tnth`, `measurable_fun_tnthP`, `measurable_cons` + * lemmas `measurable_behead`, `measurable_fun_if_pair` + * lemmas `pair1_measurable`, `pair2_measurable` + * lemmas `measurable_xsection`, `measurable_ysection`, + `measurable_fun_pair1`, `measurable_fun_pair2` + +- in `constructive_ereal.v`: + + instance of `Monoid.isLaw` for `mine` + +- in `probability.v`: + + definition `poisson_pmf`, lemmas `poisson_pmf_ge0`, `measurable_poisson_pmf`, + + definition `poisson_prob` + +- in `measurable_function.v`: + + lemma `measurable_funS`: implicits changed + ### Renamed - in `set_interval.v`: + `itv_is_ray` -> `itv_is_open_unbounded` diff --git a/theories/charge.v b/theories/charge.v index 7f1a4f6b1..698584f58 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1890,7 +1890,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). @@ -2002,7 +2002,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 b2e719016..422d1c606 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -845,100 +845,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. @@ -946,41 +898,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. @@ -988,19 +988,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 : @@ -1014,20 +1014,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. @@ -1038,15 +1038,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}. @@ -1055,7 +1047,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. @@ -1066,8 +1058,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. @@ -1078,52 +1069,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. @@ -1587,8 +1578,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. @@ -1615,7 +1605,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 => //. @@ -1668,7 +1658,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 2eaa9643c..12c84bf58 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -898,8 +898,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 a7a232c7e..a72be77ab 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v @@ -142,10 +142,10 @@ 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. - 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. @@ -160,12 +160,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. @@ -328,7 +328,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. @@ -1036,7 +1037,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 3622ce6a1..faae353ad 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 14da12b36..6fbe6fc19 100644 --- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v +++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v @@ -458,8 +458,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. @@ -554,8 +554,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 422a97b53..4696383d3 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 56c294b87..b5291dbe4 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 1acb9d7af..e9842b8f6 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1124,6 +1124,14 @@ Definition derivable_Nyo_Lcontinuous (f : R -> V) (x : R) := Definition derivable_oy_Rcontinuous (f : R -> V) (x : R) := {in `]x, +oo[, forall x, derivable f x 1} /\ f @ x^'+ --> f x. +(* TODO rename to derivable_oy_Rcontinuous_bndN *) +Lemma derivable_oy_continuous_bndN (f : R -> V) (x : R) : + derivable_oy_Rcontinuous f x -> derivable_oy_Rcontinuous (- f) x. +Proof. +move=> [/= derF Fa]; split; last exact: cvgN. +by move=> /= ? ?; exact/derivableN/derF. +Qed. + Lemma derivable_oy_Rcontinuous_within_itvcy (f : R -> V) (x : R) : derivable_oy_Rcontinuous f x -> {within `[x, +oo[, continuous f}. Proof. From efdaef9b0958d71d4e9b8bbfb231848fd1736bef 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 07/30] 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 422d1c606..619982094 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -892,9 +892,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 54169c747f4062f92fc057a1299a94c09235e615 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 08/30] 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 619982094..78ee8ae3d 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -904,7 +904,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 cab4c34efcd8401b0d46af0080498562b7f10ce2 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 09/30] 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 78ee8ae3d..876bdb950 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -911,7 +911,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 19691fc0b49a6e3c2d1ef27923813438ae096b91 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 10/30] 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 876bdb950..b404bd7ff 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -926,10 +926,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 2aceefae47f14871de824ce4031fb9726c683aaa 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 11/30] 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 b404bd7ff..f21a048c2 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -932,8 +932,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 3dd463d6a045b0b49729a7a120a4cc87c0cf4f4b 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 12/30] 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 f21a048c2..14d9e6098 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -943,10 +943,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 7a7219edf3aad3181eb6836d8bac2886c7a9ce32 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 13/30] 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 14d9e6098..87b81290f 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -969,7 +969,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 eee575228fe93efe3f74e84cbb29dd25e0817e0c 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 14/30] 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 87b81290f..ff3f48246 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -985,7 +985,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 2b184ddaceed9da8a1a6a2dfb3730c1b1b1c89de 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 15/30] 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 ff3f48246..45cc6a997 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1011,7 +1011,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 dfffa609b38b7fe568e89da767b4807cd6ce71f0 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 16/30] 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 45cc6a997..7640ba65a 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1019,7 +1019,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 e8112c2fb22fb1db10dfa364881989c333d1de5e 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 17/30] 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 7640ba65a..be5d6396b 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1048,8 +1048,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 87a0c2577347ec92c51244918be5cfffb8e6a2ed 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 18/30] 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 be5d6396b..d31a271e7 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1062,8 +1062,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 a331e6f723dcd548948666dbc9b5bad63eb986ed 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 19/30] 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 d31a271e7..5e7f6c5f8 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1066,8 +1066,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 12ea4b15a476cac6c0a18dc7316077f3e35990c8 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 20/30] 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 5e7f6c5f8..d2b2fcd0c 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1079,13 +1079,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 7e72396e4e9e9697e3b2646ea624e03696a0ba37 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 21/30] 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 d2b2fcd0c..b0bfdbbda 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1077,8 +1077,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 680dde42e094602d3f7817a5087b485bc2267aae 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 22/30] 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 b0bfdbbda..6ba22b964 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1099,8 +1099,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 5421a879ea794562016b85e2fbd8d49054005b0c 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 23/30] 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 6ba22b964..903dbfae1 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1084,7 +1084,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 6fbca0b18ac651637ac23a9de2d0a9c3fc596d93 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 24/30] 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 903dbfae1..cbb28dcec 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1100,13 +1100,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 243a8baaea9548695b2144f4ac6155d874ed0462 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 25/30] 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 e9842b8f6..25d9efaa6 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1128,7 +1128,7 @@ Definition derivable_oy_Rcontinuous (f : R -> V) (x : R) := Lemma derivable_oy_continuous_bndN (f : R -> V) (x : R) : derivable_oy_Rcontinuous f x -> derivable_oy_Rcontinuous (- f) x. Proof. -move=> [/= derF Fa]; split; last exact: cvgN. +case=> /= derF Fa; split; last exact: cvgN. by move=> /= ? ?; exact/derivableN/derF. Qed. From bb9c30e5decf538ebd859df8caa4dc75c370bee0 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Fri, 9 Jan 2026 12:12:05 +0900 Subject: [PATCH 26/30] fix --- theories/ftc.v | 49 +++++++++++++++++++++++-------------------------- 1 file changed, 23 insertions(+), 26 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index cbb28dcec..5c08e6a71 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -978,14 +978,14 @@ 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 = (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. -- rewrite [LHS]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. @@ -1002,13 +1002,17 @@ 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). + \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 -integralN; last first. + rewrite fin_num_adde_defr//. + under eq_integral do rewrite (le0_funeposE fG0) 1?inE//. + by rewrite integral_cst// mul0e. rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq. rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight. - rewrite [LHS]sum_integral_limn; apply: cvg_lim => //. @@ -1054,6 +1058,17 @@ have /continuous_within_itvcyP[+ _] := cg. by apply; rewrite inE/= in ax. Qed. +Let mfG : measurable_fun `]a, +oo[ (f * G)%R. +Proof. +apply: subspace_continuous_measurable_fun => //. +rewrite continuous_open_subspace// => x ax. +apply: cvgM. + have /continuous_within_itvcyP[+ _] := cf. + by apply; rewrite inE/= in ax. +have [/derivable_within_continuous + _] := Goy. +by rewrite continuous_open_subspace => [|//]; apply. +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. @@ -1096,14 +1111,14 @@ 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. + \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)). - rewrite oppeD; last exact: fin_num_adde_defr. - rewrite -EFinN opprD 2!opprK mulNr. - by under eq_integral do rewrite mulNr EFinN oppeK. + rewrite -EFinN opprD 2!opprK mulNr oppeK. + 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. @@ -1306,24 +1321,6 @@ Unshelve. all: end_near. Qed. End integration_by_substitution_preliminaries. -(* PR in progress *) -Lemma cvgNy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T) - (l : set_system T) : - f x @[x --> -oo] --> l <-> (f \o -%R) x @[x --> +oo] --> l. -Proof. -have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK. -by rewrite (eq_cvg -oo _ f_opp) [in X in X <-> _]fmap_comp ninftyN. -Qed. - -(* PR in progress *) -Lemma cvgy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T) - (l : set_system T) : - f x @[x --> +oo] --> l <-> (f \o -%R) x @[x --> -oo] --> l. -Proof. -have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK. -by rewrite (eq_cvg +oo _ f_opp) [in X in X <-> _]fmap_comp ninfty. -Qed. - Section integration_by_substitution. Local Open Scope ereal_scope. Context {R : realType}. From efcc45d32e9550b7019d99b39b188f9df1e08a79 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Fri, 9 Jan 2026 12:30:03 +0900 Subject: [PATCH 27/30] minor fix --- theories/ftc.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/ftc.v b/theories/ftc.v index 5c08e6a71..2be1660f4 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -978,7 +978,7 @@ 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 = (FGoo - F a * G a)%:E - \int[mu]_(x in `[a, +oo[) (f x * G x)%:E. Proof. move=> fG0 Fg0. From f69b03ae0769c3e3440d2fb5bcdeed44da28bbd2 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Tue, 13 Jan 2026 10:14:11 +0900 Subject: [PATCH 28/30] wip cleaning Let --- theories/ftc.v | 88 ++++++++++++++++++++++++++++++++------------------ 1 file changed, 56 insertions(+), 32 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 2be1660f4..cbf2305db 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -839,6 +839,18 @@ Qed. End integration_by_parts. +Section subset_itv_lemmas. +Context {R : realType}. + +Lemma subset_itv_cbnd (a c d : R) : + c < d -> + `]c, d] `<=` `]a, +oo[ -> + `[c, d] `<=` `[a, +oo[. +Proof. +Admitted. + +End subset_itv_lemmas. + Section integration_by_partsy_ge0. Context {R : realType}. Notation mu := lebesgue_measure. @@ -896,44 +908,41 @@ 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 : - \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). +Let fin_num_intfG (c d : R) : + `]c, d] `<=` `]a, +oo[ -> + \int[mu]_(x in `]c, d]) (f x * G x)%:E + \is a fin_num. Proof. -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. +have [dc|cd] := leP d c. + admit. +move=> cda. +rewrite integral_itv_obnd_cbnd; last first. + exact: measurable_funS mfG => //. apply: integrable_fin_num => //=. apply: continuous_compact_integrable; first exact: segment_compact. apply: continuous_subspaceW cfG. -by apply: subset_itv; rewrite // bnd_simp// lerDl. -Qed. +exact: subset_itv_cbnd cda. +Admitted. -Let sumNint_sumintN_fG n : - \sum_(0 <= i < n) - (- (\int[mu]_(x in seqDU (fun k => `]a, a + k%:R]) i) +Let sumNint_sumintN_fG (c d : R) : + `]c, d] `<=` `]a, +oo[ -> + (- (\int[mu]_(x in `]c, d]) (f x * G x)%:E))%E = - \sum_(0 <= i < n) - (\int[mu]_(x in seqDU (fun k => `]a, a + k%:R]) i) + (\int[mu]_(x in `]c, d]) (- (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 2 first. -- apply: measurableT_comp => //; 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. -by apply: continuous_subspaceW cfG; apply/subset_itv; rewrite bnd_simp// lerDl. -Qed. +have [dc|cd] := ltP d c. + admit. +move=> ja. +rewrite -integralN//=. +apply: fin_num_adde_defr. +apply: integrable_pos_fin_num => //=. +apply/integrableP; split. + apply/measurable_EFinP. + exact: measurable_funS mfG. +rewrite integral_fin_num_abs//; last exact: measurable_funS mfG. +exact: fin_num_intfG. +Admitted. Let sum_integral_limn : \sum_(0 <= i //. apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo. - under eq_cvg do rewrite sumN_Nsum_fG; apply: cvgeN. + under eq_cvg. + move=> n. + rewrite big_nat_cond fin_num_sumeN -?big_nat_cond//; last first. + move=> m _; rewrite seqDUE. + case: m => //; first by rewrite set_itvxx integral_set0. + move=> m/=; apply: fin_num_intfG. + + by apply: subset_itv; rewrite bnd_simp// lerDl. + over. + 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. @@ -1017,7 +1034,14 @@ rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq. rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight. - 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. + rewrite [X in X --> _](_ : _ = \sum_(0 <= i < x) + \int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]) i) (- (f x * G x))%:E + @[x --> \oo]); last first. + congr (_ @[x --> \oo]); apply: funext => n. + apply: eq_bigr; case. + by move=> _; rewrite seqDUE addr0 set_itvxx 2!integral_set0 oppe0. + move=> m _; rewrite seqDUE sumNint_sumintN_fG//. + by apply: subset_itv; rewrite bnd_simp// lerDl. apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x. rewrite seqDUE => anx; rewrite EFinN oppe_ge0. apply: fG0; rewrite inE/=. From 21e23f2a1aa1b83b69520d1efc91931695f5f8c3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 13 Jan 2026 16:08:55 +0900 Subject: [PATCH 29/30] prove admit --- CHANGELOG_UNRELEASED.md | 3 + reals/real_interval.v | 34 +++++++++ theories/ftc.v | 155 +++++++++++++++++----------------------- 3 files changed, 102 insertions(+), 90 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a613ec1c2..3444a2ec9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -100,6 +100,9 @@ `integration_by_partsy_le0_le0`, `integration_by_partsy_ge0_le0` +- in `real_interval.v`: + + lemma `subset_itvoSo_cSc` + ### Changed - in set_interval.v + `itv_is_closed_unbounded` (fix the definition) diff --git a/reals/real_interval.v b/reals/real_interval.v index 4beab5562..3aa9ddb3a 100644 --- a/reals/real_interval.v +++ b/reals/real_interval.v @@ -249,6 +249,40 @@ Qed. End itv_realDomainType. +(* generalization of + a < b -> `]a, b] `<=` `]r, +oo[ -> `[a, b] `<=` `[r, +oo[. *) +Lemma subset_itvoSo_cSc {R : realFieldType} (r a : R) (b x : itv_bound R) : + (BRight a < b)%O -> + (b <= x)%O -> + [set` Interval (BRight a)(*open*) b] + `<=` [set` Interval (BRight r)(*open*) x] -> + [set` Interval (BLeft a)(*closed*) b] + `<=` [set` Interval (BLeft r)(*closed*) x]. +Proof. +move: b => [[|]b ab bx abrx|[//|/= _]]; rewrite ?bnd_simp. +- apply: subset_itv => //=; rewrite bnd_simp leNgt; apply/negP => ar. + have rb : (r <= b)%O. + rewrite leNgt; apply/negP => br; have /= := abrx ((a + b) / 2). + rewrite !in_itv/= !midf_lt//= => /(_ isT). + by rewrite ltNge (le_trans _ (ltW br))//= midf_le// ltW. + have /abrx /= : (a + r) / 2 \in `]a, b[. + by rewrite in_itv/= midf_lt//= (lt_le_trans _ rb)// midf_lt. + by rewrite in_itv/= ltNge midf_le// ltW. +- apply: subset_itv => //=; rewrite bnd_simp leNgt; apply/negP => ar. + have rb : r <= b. + rewrite leNgt; apply/negP => br; have /= := abrx ((a + b) / 2). + rewrite !in_itv/= midf_lt// (midf_le (ltW _))// => /(_ isT). + by rewrite ltNge (le_trans _ (ltW br))//= midf_le// ltW. + have /abrx /= : (a + r) / 2 \in `]a, b]. + by rewrite in_itv/= midf_lt//= (le_trans _ rb)// (midf_le (ltW _)). + by rewrite in_itv/= ltNge midf_le// ltW. +- move/eqP => ->{x} ar. + apply/subset_itvr; rewrite bnd_simp leNgt; apply/negP => ra. + have /= := ar ((a + r) / 2). + rewrite !in_itv/= !andbT midf_lt// => /(_ isT). + by rewrite ltNge midf_le// ltW. +Qed. + Section set_ereal. Context (R : realType) T (f g : T -> \bar R). Local Open Scope ereal_scope. diff --git a/theories/ftc.v b/theories/ftc.v index cbf2305db..20007a2b3 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -839,18 +839,6 @@ Qed. End integration_by_parts. -Section subset_itv_lemmas. -Context {R : realType}. - -Lemma subset_itv_cbnd (a c d : R) : - c < d -> - `]c, d] `<=` `]a, +oo[ -> - `[c, d] `<=` `[a, +oo[. -Proof. -Admitted. - -End subset_itv_lemmas. - Section integration_by_partsy_ge0. Context {R : realType}. Notation mu := lebesgue_measure. @@ -908,80 +896,59 @@ apply: (@cvg_comp _ _ _ _ (F \* G)%R _ +oo%R); last exact: cvgFG. by apply: cvg_comp; [apply: cvgr_idn|apply: cvg_addrl]. Qed. -Let fin_num_intfG (c d : R) : - `]c, d] `<=` `]a, +oo[ -> - \int[mu]_(x in `]c, d]) (f x * G x)%:E - \is a fin_num. +Let fin_num_intfG (c d : R) : `]c, d] `<=` `]a, +oo[ -> + \int[mu]_(x in `]c, d]) (f x * G x)%:E \is a fin_num. Proof. -have [dc|cd] := leP d c. - admit. -move=> cda. -rewrite integral_itv_obnd_cbnd; last first. - exact: measurable_funS mfG => //. +have [dc _|cd cday] := leP d c. + by rewrite set_itv_ge ?bnd_simp -?leNgt// integral_set0. +rewrite integral_itv_obnd_cbnd; last exact: measurable_funS mfG. apply: integrable_fin_num => //=. apply: continuous_compact_integrable; first exact: segment_compact. -apply: continuous_subspaceW cfG. -exact: subset_itv_cbnd cda. -Admitted. - -Let sumNint_sumintN_fG (c d : R) : - `]c, d] `<=` `]a, +oo[ -> - (- (\int[mu]_(x in `]c, d]) - (f x * G x)%:E))%E = - (\int[mu]_(x in `]c, d]) - (- (f x * G x))%:E)%E. -Proof. -have [dc|cd] := ltP d c. - admit. -move=> ja. -rewrite -integralN//=. -apply: fin_num_adde_defr. -apply: integrable_pos_fin_num => //=. -apply/integrableP; split. - apply/measurable_EFinP. - exact: measurable_funS mfG. -rewrite integral_fin_num_abs//; last exact: measurable_funS mfG. -exact: fin_num_intfG. -Admitted. +by apply: continuous_subspaceW cfG; exact: subset_itvoSo_cSc. +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) + \int[mu]_(x in `](a + i.-1%:R), (a + i%:R)]) (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 `](a + i.-1%:R), (a + i%:R)]) (f x * G x)%:E). Proof. -apply/congr_lim/funext; case. - 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. +apply/congr_lim/funext => -[|[|n]]. + by rewrite !big_nil/= oppr0 !addr0 subrr. + by rewrite 2!big_nat1/= addr0 subrr add0r 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. +rewrite addr0 set_itvoc0 2!integral_set0 2!add0r. +have mFg' i : measurable_fun `](a + i%:R), (a + i.+1%:R)] + (fun x => F x * g x)%R. + apply: measurable_funS mFg => //. + by apply/subset_itv => //; rewrite bnd_simp lerDl. +have mfG' i : measurable_fun `](a + i%:R), (a + i.+1%:R)] + (fun x => f x * G x)%R. + apply: measurable_funS mfG => //. + by apply/subset_itv => //; rewrite bnd_simp lerDl. 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 integral_itv_obnd_cbnd//. 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: derivable_oy_continuousWoo Foy; last by rewrite lerDl. + by rewrite ltrD2l ltr_nat. - 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. + - apply: derivable_oy_continuousWoo Goy; last by rewrite lerDl. + by rewrite ltrD2l ltr_nat. over. rewrite big_split/=. under eq_bigr do rewrite EFinB. 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. +rewrite sumeN//. +- congr (- _). + by apply: eq_bigr => k _; rewrite integral_itv_obnd_cbnd. +- move=> x y _ _; rewrite fin_num_adde_defl//. + rewrite -integral_itv_obnd_cbnd//= fin_num_intfG//. + by apply/subset_itv; rewrite bnd_simp//= lerDl. Qed. Lemma integration_by_partsy_ge0_ge0 : @@ -992,21 +959,16 @@ Lemma integration_by_partsy_ge0_ge0 : Proof. move=> fG0 Fg0. rewrite -integral_itv_obnd_cbnd// -[in RHS]integral_itv_obnd_cbnd//. -rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq. +rewrite itv_bndy_bigcup_BRight. +rewrite seqDU_bigcup_eq. rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight. -- rewrite [LHS]sum_integral_limn; apply: cvg_lim => //. +- under eq_eseriesr do rewrite seqDUE. + under [in RHS]eq_eseriesr do rewrite seqDUE. + rewrite [LHS]sum_integral_limn; apply: cvg_lim => //. apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo. - under eq_cvg. - move=> n. - rewrite big_nat_cond fin_num_sumeN -?big_nat_cond//; last first. - move=> m _; rewrite seqDUE. - case: m => //; first by rewrite set_itvxx integral_set0. - move=> m/=; apply: fin_num_intfG. - + by apply: subset_itv; rewrite bnd_simp// lerDl. - over. apply: cvgeN. apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x. - rewrite seqDUE => anx; apply: fG0; rewrite inE/=. + move=> 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. @@ -1026,30 +988,43 @@ 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 -integralN; last first. +rewrite -integralN/=; last first. rewrite fin_num_adde_defr//. under eq_integral do rewrite (le0_funeposE fG0) 1?inE//. by rewrite integral_cst// mul0e. rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq. rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight. -- rewrite [LHS]sum_integral_limn; apply: cvg_lim => //. +- under eq_eseriesr do rewrite seqDUE. + under [in RHS]eq_eseriesr do rewrite seqDUE. + rewrite [LHS]sum_integral_limn; apply: cvg_lim => //. apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo. - rewrite [X in X --> _](_ : _ = \sum_(0 <= i < x) - \int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]) i) (- (f x * G x))%:E - @[x --> \oo]); last first. - congr (_ @[x --> \oo]); apply: funext => n. - apply: eq_bigr; case. - by move=> _; rewrite seqDUE addr0 set_itvxx 2!integral_set0 oppe0. - move=> m _; rewrite seqDUE sumNint_sumintN_fG//. - by apply: subset_itv; rewrite bnd_simp// lerDl. + rewrite [X in X x @[x --> _] --> _](_ : _ = fun x => \sum_(0 <= i < x) + \int[mu]_(x in `](a + i.-1%:R), (a + i%:R)]) (- (f x * G x))%:E); + last first. + apply: funext => n; rewrite -sumeN; last first. + move=> x y _ _; rewrite fin_num_adde_defl//. + apply: fin_num_intfG => //. + by apply/subset_itv; rewrite bnd_simp//= lerDl. + apply: eq_bigr => -[_|m _]. + by rewrite addr0 set_itvxx 2!integral_set0 oppe0. + have ? : + measurable_fun `](a + m%:R), (a + m.+1%:R)] (fun x => (f x * G x)%R). + apply: measurable_funS mfG => //. + by apply: subset_itv => //; rewrite bnd_simp lerDl. + under [RHS]eq_integral do rewrite EFinN. + rewrite [in RHS]integralN//. + apply: fin_num_adde_defr => /=; apply: integrable_pos_fin_num => //=. + apply/integrableP; split; first exact/measurable_EFinP. + rewrite integral_fin_num_abs// fin_num_intfG//. + by apply: subset_itv => //; rewrite bnd_simp lerDl. apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x. - rewrite seqDUE => anx; rewrite EFinN oppe_ge0. + move=> 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 move=> k; apply: measurableD => //; exact: bigsetU_measurable. - exact/measurable_EFinP/measurableT_comp. - by move=> ? ?; rewrite EFinN oppe_ge0 fG0// inE. -- by move=> k; apply: measurableD => //; apply: bigsetU_measurable. +- by move=> k; apply: measurableD => //; exact: bigsetU_measurable. - exact/measurable_EFinP. - by move=> ? ?; rewrite Fg0// inE. Qed. From 3a69bded7fb57c3ff542bf83c419e0dd2c23c1f3 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Sun, 18 Jan 2026 01:51:49 +0900 Subject: [PATCH 30/30] rename: derivable_oy_continuous_bndN -> derivable_oy_RcontinuousN --- CHANGELOG_UNRELEASED.md | 2 +- theories/ftc.v | 4 ++-- theories/realfun.v | 3 +-- 3 files changed, 4 insertions(+), 5 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3444a2ec9..b0212288f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -92,7 +92,7 @@ `derivable_Nyo_continuousW` - in `realfun.v`: - + lemma `derivable_oy_continuous_bndN` + + lemma `derivable_oy_RcontinuousN` - in `ftc.v`: + lemmas `integration_by_partsy_ge0_ge0`, diff --git a/theories/ftc.v b/theories/ftc.v index 20007a2b3..4cf211786 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1097,7 +1097,7 @@ rewrite (@integration_by_partsy_ge0_ge0 R (- F)%R G (- f)%R g a (- FGoo)). 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. +- exact: derivable_oy_RcontinuousN. - by move=> ? ?; rewrite fctE derive1N ?Ff => [//|//|]; apply: Foy.1. - by []. - by []. @@ -1119,7 +1119,7 @@ rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo)). rewrite -EFinN opprD 2!opprK mulNr oppeK. by under eq_integral do rewrite mulNr EFinN. - by move=> ?; apply: cvgN; exact: cf. -- exact: derivable_oy_continuous_bndN. +- exact: derivable_oy_RcontinuousN. - by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply. - by []. - by []. diff --git a/theories/realfun.v b/theories/realfun.v index 25d9efaa6..2978e5397 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1124,8 +1124,7 @@ Definition derivable_Nyo_Lcontinuous (f : R -> V) (x : R) := Definition derivable_oy_Rcontinuous (f : R -> V) (x : R) := {in `]x, +oo[, forall x, derivable f x 1} /\ f @ x^'+ --> f x. -(* TODO rename to derivable_oy_Rcontinuous_bndN *) -Lemma derivable_oy_continuous_bndN (f : R -> V) (x : R) : +Lemma derivable_oy_RcontinuousN (f : R -> V) (x : R) : derivable_oy_Rcontinuous f x -> derivable_oy_Rcontinuous (- f) x. Proof. case=> /= derF Fa; split; last exact: cvgN.