From b2536f85b330d5f12c7e66fdc57d3fafbbaa9d40 Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 13:09:48 +0200 Subject: [PATCH 1/8] Utility lemmas in filter.v --- CHANGELOG_UNRELEASED.md | 2 ++ classical/filter.v | 53 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 55 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2d85fdc0a5..9522855b6e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -126,6 +126,8 @@ - in `filter.v`: + mixin `isSubNbhs`, structure `SubNbhs`, notation `subNbhsType` + + new lemmas `near_eq_cvgE`, `near_eq_is_cvg`, `near_eq_lim`, + `cvg_to_eq`, `cvg_to_withinP`, and `within_cvg_to_within`. - in `topology_structure.v`: + structure `SubTopological`, notation `subTopologicalType` diff --git a/classical/filter.v b/classical/filter.v index b26d00d72f..073ef58fdc 100644 --- a/classical/filter.v +++ b/classical/filter.v @@ -925,10 +925,23 @@ Lemma near_eq_cvg {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) : {near F, f =1 g} -> g @ F `=>` f @ F. Proof. by move=> eq_fg P /=; apply: filterS2 eq_fg => x /= <-. Qed. +Lemma near_eq_cvgE {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) : + {near F, f =1 g} -> f @ F = g @ F. +Proof. +move=> eq_fg. +apply/seteqP; split; apply: near_eq_cvg => //. +by near do symmetry. +Unshelve. all: by end_near. +Qed. + Lemma eq_cvg (T T' : Type) (F : set_system T) (f g : T -> T') (x : set_system T') : f =1 g -> (f @ F --> x) = (g @ F --> x). Proof. by move=> /funext->. Qed. +Lemma near_eq_is_cvg (T : Type) (T' : pnbhsType) (F : set_system T) (f g : T -> T') : + Filter F -> {near F, g =1 f} -> cvg (f x @[x --> F]) -> cvg(g x @[x --> F]). +Proof. by move=> /@near_eq_cvgE /[apply] ->. Qed. + Lemma eq_is_cvg_in (T T' : Type) (fT : pfilteredType T') (F : set_system T) (f g : T -> T') : f =1 g -> [cvg (f @ F) in fT] = [cvg (g @ F) in fT]. Proof. by move=> /funext->. Qed. @@ -937,6 +950,14 @@ Lemma eq_is_cvg (T : Type) (T' : pnbhsType) (F : set_system T) (f g : T -> T') : f =1 g -> cvg (f @ F) = cvg (g @ F). Proof. by move=> /funext->. Qed. +Lemma near_eq_lim (T : Type) (T' : pnbhsType) {F : set_system T} {FF : Filter F} (f g : T -> T') : + {near F, f =1 g} -> lim (f @ F) = lim (g @ F). +Proof. by move=> /near_eq_cvgE ->. Qed. + +Lemma cvg_to_eq {T : nbhsType} {F : set_system T} (l l' : T) : + F --> l' -> l = l' -> F --> l. +Proof. by move=> + ->. Qed. + Lemma neari_eq_loc {T U} {F : set_system T} {FF : Filter F} (f g : T -> set U) : {near F, f =2 g} -> g `@ F `=>` f `@ F. Proof. @@ -1197,6 +1218,26 @@ Qed. End within. +Lemma cvg_to_withinP (T U : Type) {F : set_system T} {FF : Filter F} {G : set_system U} {FG : Filter G} + (f : T -> U) (A : set U) : + (f @ F --> within A G) <-> (f @ F --> G /\ \forall x \near F, A (f x)). +Proof. + split. + move=> cvg_w; split. + - apply: (cvg_trans cvg_w). + exact: cvg_within. + - apply: cvg_w. + exact: withinT. + move=> [cvgT nearfA] P. + rewrite !nbhs_nearE near_withinE. + move: cvgT => /[apply]. + rewrite near_map appfilter nbhs_nearE => nearF_AP. + near=> x. + suff : A (f x) by near: x. + by near: x. + Unshelve. all: by end_near. +Qed. + Global Instance within_filter T D F : Filter F -> Filter (@within T D F). Proof. move=> FF; rewrite /within; constructor => /=. @@ -1210,6 +1251,18 @@ Qed. Canonical within_filter_on T D (F : filter_on T) := FilterType (within D F) (within_filter _ _). +Lemma within_cvg_to_within (T U : Type) {F : set_system T} {FF : Filter F} {G : set_system U} {FG : Filter G} + (f : T -> U) (A : set T) (B : set U) : + (\forall x \near F, A x -> B (f x)) -> f @ F --> G -> f @ within A F --> within B G. +Proof. + move=> near_hom cvgT. + apply/cvg_to_withinP; split. + - apply: cvg_trans cvgT. + apply: cvg_app. + exact: cvg_within. + - by rewrite near_withinE. +Qed. + Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T) (F : set_system T) (P : set T) : Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) -> From f11fbdaa38d7d6f98c7c613f9f2090a97607c8d9 Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 13:40:51 +0200 Subject: [PATCH 2/8] Fix indentation --- classical/filter.v | 41 ++++++++++++++++++++--------------------- 1 file changed, 20 insertions(+), 21 deletions(-) diff --git a/classical/filter.v b/classical/filter.v index 073ef58fdc..4233a6d9bc 100644 --- a/classical/filter.v +++ b/classical/filter.v @@ -1222,21 +1222,20 @@ Lemma cvg_to_withinP (T U : Type) {F : set_system T} {FF : Filter F} {G : set_sy (f : T -> U) (A : set U) : (f @ F --> within A G) <-> (f @ F --> G /\ \forall x \near F, A (f x)). Proof. - split. - move=> cvg_w; split. - - apply: (cvg_trans cvg_w). - exact: cvg_within. - - apply: cvg_w. - exact: withinT. - move=> [cvgT nearfA] P. - rewrite !nbhs_nearE near_withinE. - move: cvgT => /[apply]. - rewrite near_map appfilter nbhs_nearE => nearF_AP. - near=> x. - suff : A (f x) by near: x. - by near: x. - Unshelve. all: by end_near. -Qed. +split. + move=> cvg_w; split. + - apply: (cvg_trans cvg_w). + exact: cvg_within. + - apply: cvg_w. + exact: withinT. +move=> [cvgT nearfA] P. +rewrite !nbhs_nearE near_withinE. +move: cvgT => /[apply]. +rewrite near_map appfilter nbhs_nearE => nearF_AP. +near=> x. +suff : A (f x) by near: x. +by near: x. +Unshelve. all: by end_near. Qed. Global Instance within_filter T D F : Filter F -> Filter (@within T D F). Proof. @@ -1255,12 +1254,12 @@ Lemma within_cvg_to_within (T U : Type) {F : set_system T} {FF : Filter F} {G : (f : T -> U) (A : set T) (B : set U) : (\forall x \near F, A x -> B (f x)) -> f @ F --> G -> f @ within A F --> within B G. Proof. - move=> near_hom cvgT. - apply/cvg_to_withinP; split. - - apply: cvg_trans cvgT. - apply: cvg_app. - exact: cvg_within. - - by rewrite near_withinE. +move=> near_hom cvgT. +apply/cvg_to_withinP; split. +- apply: cvg_trans cvgT. + apply: cvg_app. + exact: cvg_within. +- by rewrite near_withinE. Qed. Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T) From 75a094838ef79bf40182e28f9915d37c82a637fa Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 15:43:21 +0200 Subject: [PATCH 3/8] normed module identity convergence lemmas --- theories/normedtype_theory/normed_module.v | 24 ++++++++++++ .../pseudometric_normed_Zmodule.v | 39 +++++++++++++++++++ 2 files changed, 63 insertions(+) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 1252178b3f..94a72d0f8e 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -642,6 +642,30 @@ Proof. exact: cvgZr_tmp. Qed. Lemma cvgMl_tmp g a b : g @ F --> b -> a * g x @[x --> F] --> a * b. Proof. exact: cvgZl_tmp. Qed. +Lemma cvg1MC f a : f @ F --> (1 :> K) -> f x * a @[x --> F] --> a. +Proof. by move/(cvgMr_tmp (b := a)); rewrite mul1r. Qed. + +Lemma cvg1M f g a : f @ F --> (1 :> K) -> g @ F --> a -> f \* g @ F --> a. +Proof. by move=> /cvgM /[apply]; rewrite mul1r. Qed. + +Lemma cvgCM1 f a : f @ F --> (1 :> K) -> a * f x @[x --> F] --> a. +Proof. by move/(cvgMl_tmp (a := a)); rewrite mulr1. Qed. + +Lemma cvgM1 f g a : f @ F --> a -> g @ F --> (1 :> K) -> f \* g @ F --> a. +Proof. by move=> /cvgM /[apply]; rewrite mulr1. Qed. + +Lemma cvg0MC f a : f @ F --> 0 -> f x * a @[x --> F] --> 0. +Proof. by move/(cvgMr_tmp (b := a)); rewrite mul0r. Qed. + +Lemma cvg0M f g a : f @ F --> 0 -> g @ F --> a -> f \* g @ F --> 0. +Proof. by move=> /cvgM /[apply]; rewrite mul0r. Qed. + +Lemma cvgCM0 f a : f @ F --> 0 -> a * f x @[x --> F] --> 0. +Proof. by move/(cvgMl_tmp (a := a)); rewrite mulr0. Qed. + +Lemma cvgM0 f g a : f @ F --> a -> g @ F --> 0 -> f \* g @ F --> 0. +Proof. by move=> /cvgM /[apply]; rewrite mulr0. Qed. + Lemma is_cvgM f g : cvg (f @ F) -> cvg (g @ F) -> cvg (f \* g @ F). Proof. exact: is_cvgZ. Qed. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 9f945624de..82c259cf1f 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -1098,6 +1098,45 @@ Qed. Lemma is_cvgDrE f g : cvg (f @ F) -> cvg ((f + g) @ F) = cvg (g @ F). Proof. by rewrite addrC; apply: is_cvgDlE. Qed. +Lemma cvgDl f a b : f @ F --> b -> a + f x @[x --> F] --> a + b. +Proof. apply: cvgD; exact: cvg_cst. Qed. + +Lemma cvgDr f a b : f @ F --> a -> f x + b @[x --> F] --> a + b. +Proof. move/cvgD; apply; exact: cvg_cst. Qed. + +Lemma cvgBl f a b : f @ F --> b -> a - f x @[x --> F] --> a - b. +Proof. by move/cvgN; apply: cvgDl. Qed. + +Lemma cvgBr f a b : f @ F --> a -> f x - b @[x --> F] --> a - b. +Proof. exact: cvgDr. Qed. + +Lemma cvg0D f g a : f @ F --> 0 -> g @ F --> a -> f x + g x @[x --> F] --> a. +Proof. by move=> /cvgD /[apply]; rewrite add0r. Qed. + +Lemma cvg0DC f a : f @ F --> 0 -> f x + a @[x --> F] --> a. +Proof. by move=> /(cvgDr (b := a)); rewrite add0r. Qed. + +Lemma cvgD0 f g a : f @ F --> a -> g @ F --> 0 -> f x + g x @[x --> F] --> a. +Proof. by move=> /cvgD /[apply]; rewrite addr0. Qed. + +Lemma cvgCD0 f a : f @ F --> 0 -> a + f x @[x --> F] --> a. +Proof. by move/(@cvgDl _ a); rewrite addr0. Qed. + +Lemma cvg0B f g a : f @ F --> 0 -> g @ F --> a -> f x - g x @[x --> F] --> -a. +Proof. by move=> /cvgB /[apply]; rewrite add0r. Qed. + +Lemma cvg0BC f a : f @ F --> 0 -> f x - a @[x --> F] --> -a. +Proof. by move=> /(cvgBr (b := a)); rewrite add0r. Qed. + +Lemma cvgB0 f g a : f @ F --> a -> g @ F --> 0 -> f x - g x @[x --> F] --> a. +Proof. by move=> /cvgB /[apply]; rewrite subr0. Qed. + +Lemma cvgCB0 f a : f @ F --> 0 -> a - f x @[x --> F] --> a. +Proof. by move/(@cvgBl _ a); rewrite subr0. Qed. + +Lemma cvgN0 f : f @ F --> 0 -> - f @ F --> 0. +Proof. by rewrite -{2}oppr0; exact: cvgN. Qed. + Lemma cvg_sub0 f g a : (f - g) @ F --> (0 : V) -> g @ F --> a -> f @ F --> a. Proof. by move=> Cfg Cg; have := cvgD Cfg Cg; rewrite subrK add0r; apply. From 7607dd53424ebb74098d5e3299408d8f5e0a33c0 Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 15:44:31 +0200 Subject: [PATCH 4/8] Update changelog --- CHANGELOG_UNRELEASED.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2d85fdc0a5..ee32fdf6d9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -234,6 +234,13 @@ - in `measurable_structure.v`: + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable` +- in file `normed_module.v`, + + new lemmas `cvg1MC`, `cvg1M`, `cvgCM1`, `cvgM1`, `cvg0MC`, `cvg0M`, + `cvgCM0`, and `cvgM0`. +- in file `pseudometric_normed_Zmodule.v`, + + new lemmas `cvgDl`, `cvgDr`, `cvgBl`, `cvgBr`, `cvg0D`, `cvg0DC`, + `cvgD0`, `cvgCD0`, `cvg0B`, `cvg0BC`, `cvgB0`, `cvgCB0`, and `cvgN0`. + ### Changed - in `realsum.v`: From 8e41cb239fb51246334650b04e83a169571d10f8 Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 18:23:27 +0200 Subject: [PATCH 5/8] Rintegral manipulation lemmas --- CHANGELOG_UNRELEASED.md | 6 + .../lebesgue_Rintegral.v | 178 ++++++++++++++++++ 2 files changed, 184 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2d85fdc0a5..a3ef16de4c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -234,6 +234,12 @@ - in `measurable_structure.v`: + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable` +- in file `lebesgue_Rintegral.v`, + + new lemmas `Rintegral_patch_negligible`, `Rintegral_itvbb_itvoo`, + `Rintegral_itvby_itvoy`, `Rintegral_itvbb_itvbb`, `Rintegral_itvby_itvby`, + `Rintegral_itv0`, `Rintegral_itvD`, `Rintegral_itvDy`, and + `Rintegral_patch_finite`. + ### Changed - in `realsum.v`: diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v index 82c8feb1e5..1d87837d7c 100644 --- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v +++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v @@ -188,6 +188,41 @@ move=> mD if1 if2. by rewrite /Rintegral integralB_EFin// fineB//; exact: integrable_fin_num. Qed. +Lemma Rintegral_patch_negligible (f g : T -> R) (A D : set T) : + d.-measurable A -> d.-measurable D -> mu D = 0 -> measurable_fun A f -> measurable_fun D g -> Rintegral mu A (patch f D g) = Rintegral mu A f. +Proof. +move=> mA mD muD0 mf mg. +wlog D_sub_A : D A mA mD muD0 mf mg / D `<=` A. + move=> sub_case. + transitivity (Rintegral mu A (patch f (D `&` A) g)). + apply: eq_Rintegral => x. + by rewrite in_setI andbC => ->. + apply: sub_case => //. + - by apply: measurableI. + - apply: subset_measure0 muD0 => //. + by apply: measurableI. + - by apply: measurable_funS mg. +congr (fine _). +apply: ae_eq_integral => //; [| exact/measurable_EFinP |]. + change (measurable_fun A (EFin \o patch f D g)). + rewrite comp_patch /patch/=. + rewrite -(setDUK D_sub_A). + apply/measurable_funU => //; first by apply: measurableD. + split. + - apply: (eq_measurable_fun (EFin \o g)). + + by move=> ? ->. + + by apply/measurable_EFinP. + - apply: (eq_measurable_fun (EFin \o f)). + + move=> x. + by rewrite in_setD => /andP[_ /negbTE ->]. + + apply/measurable_EFinP. + by apply: measurable_funS mf. +rewrite /ae_eq /prop_near1 /nbhs/= /almost_everywhere/=. +exists D; split=> //. +apply: subsetCl => x /= nDx Ax. +by rewrite /patch ifN// notin_setE. +Qed. + End Rintegral. #[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `le_normr_Rintegral`")] Notation le_normr_integral := le_normr_Rintegral (only parsing). @@ -242,6 +277,149 @@ rewrite addrC addKr Rintegral_itvob_itvcb//. by apply: integrableS itf => //; exact/subset_itvr/ltW. Qed. +Lemma Rintegral_itvbb_itvoo (x y : R) f (b1 b2 : bool) : + measurable_fun `]x, y[ (EFin \o f) -> + \int[mu]_(z in [set` Interval (BSide b1 x) (BSide b2 y)]) f z = + \int[mu]_(z in `]x, y[) f z. +Proof. by move=> mf /=; congr fine; rewrite integral_itvbb_itvoo. Qed. + +Lemma Rintegral_itvby_itvoy (x : R) f (b1 : bool) : + measurable_fun `]x, +oo[ (EFin \o f) -> + \int[mu]_(z in [set` Interval (BSide b1 x) +oo%O]) f z = + \int[mu]_(z in `]x, +oo[) f z. +Proof. +move=> mf /=; congr fine. +case: b1 => [|//]; symmetry. +by apply: integral_itvob_itvcb. +Qed. + +Lemma Rintegral_itvbb_itvbb (x y : R) (f g : R -> R) (b1 b2 b1' b2' : bool) : + measurable_fun `]x, y[ f -> + {in `]x, y[%R, f =1 g} -> + \int[mu]_(z in [set` Interval (BSide b1 x) (BSide b2 y)]) f z = + \int[mu]_(z in [set` Interval (BSide b1' x) (BSide b2' y)]) g z. +Proof. +move=> mf eqfg. +transitivity (\int[mu]_(z in `]x, y[) f z). + apply: Rintegral_itvbb_itvoo. + by apply/measurable_EFinP. +transitivity (\int[mu]_(z in `]x, y[) g z). + by apply: eq_Rintegral; move=> + /set_mem. +symmetry; apply: Rintegral_itvbb_itvoo. +apply/measurable_EFinP. +by apply: (eq_measurable_fun f); first by move=> + /set_mem. +Qed. + +Lemma Rintegral_itvby_itvby (x : R) (f g : R -> R) (b1 b1' : bool) : + measurable_fun `]x, +oo[ f -> + {in `]x, +oo[, f =1 g} -> + \int[mu]_(z in [set` Interval (BSide b1 x) +oo%O]) f z = + \int[mu]_(z in [set` Interval (BSide b1' x) +oo%O]) g z. +Proof. +move=> mf eqfg. +transitivity (\int[mu]_(z in `]x, +oo[) f z). + apply: Rintegral_itvby_itvoy. + by apply/measurable_EFinP. +transitivity (\int[mu]_(z in `]x, +oo[) g z). + by apply: eq_Rintegral; move=> + /set_mem. +symmetry; apply: Rintegral_itvby_itvoy. +apply/measurable_EFinP. +by apply: (eq_measurable_fun f); first by move=> + /set_mem. +Qed. + +Lemma Rintegral_itv0 f (a b : R) (b1 b2 : bool) : + a >= b -> Rintegral mu [set` Interval (BSide b1 a) (BSide b2 b)] f = 0. +Proof. +rewrite le_eqVlt => /predU1P[->|b_lt_a]. +- case: b1 b2 => [] []; rewrite set_itvE ?Rintegral_set0//. + exact: Rintegral_set1. +- rewrite set_itv_ge -?leNgt; first by apply: lteifS. + exact: Rintegral_set0. +Qed. + +Lemma Rintegral_itvD f (a c : R) (b1 b2 b1' b2' : bool) (b : itv_bound R) : + (BLeft a <= b <= BRight c)%O -> + mu.-integrable `]a, c[ (EFin \o f) -> + Rintegral mu [set` Interval (BSide b1 a) (BSide b2 c)] f = Rintegral mu [set` Interval (BSide b1' a) b] f + Rintegral mu [set` Interval b (BSide b2' c)] f. +Proof. +case: b => [b3 b|[] //]. +rewrite !bnd_simp => /andP[a_le_b b_le_c] f_int. +have mf : measurable_fun `]a, c[ f. + apply/measurable_EFinP. + by apply: (measurable_int mu). +move: a_le_b; rewrite le_eqVlt => /predU1P[<-|a_lt_b]. + rewrite [X in _ = X + _]Rintegral_itv0// add0r. + by apply: Rintegral_itvbb_itvbb. +move: b_le_c; rewrite le_eqVlt => /predU1P[->|b_lt_c]. + rewrite [X in _ = _ + X]Rintegral_itv0// addr0. + by apply: Rintegral_itvbb_itvbb. +transitivity (Rintegral mu `]a, c[ f); first by apply: Rintegral_itvbb_itvbb. +rewrite (itv_bndbnd_setU (x := BSide b3 b)); [ by apply: lteifS .. |]. +rewrite [LHS]Rintegral_setU; [ exact: measurable_itv .. | | |]. +- by rewrite -itv_bndbnd_setU//; apply: lteifS. +- apply/disj_setPS => x /=[/andP[_ +] /andP[+ _]]. + move/le_trans/[apply]. + by rewrite bnd_simp ltxx. +congr (_ + _); apply: Rintegral_itvbb_itvbb => //. +- apply: (measurable_funS (E := `]a, c[)) => //. + by apply: subset_itvl; rewrite bnd_simp ltW. +- apply: (measurable_funS (E := `]a, c[)) => //. + by apply: subset_itvr; rewrite bnd_simp ltW. +Qed. + +Lemma Rintegral_itvDy f (a : R) (b : itv_bound R) (b1 b1' : bool) : + (BLeft a <= b)%O -> + mu.-integrable `]a, +oo[ (EFin \o f) -> + Rintegral mu [set` Interval (BSide b1 a) +oo%O] f + = Rintegral mu [set` Interval (BSide b1' a) b] f + Rintegral mu [set` Interval b +oo%O] f. +Proof. +move=> /[swap] int_f. +case: b => [b2 b|[] // _]; last first. + rewrite set_itvxx Rintegral_set0 addr0. + apply: Rintegral_itvby_itvby => //. + apply/measurable_EFinP. + exact: measurable_int int_f. +rewrite !bnd_simp => a_le_b. +have mf : measurable_fun `]a, +oo[ f. + apply/measurable_EFinP. + by apply: (measurable_int mu). +move: a_le_b; rewrite le_eqVlt => /predU1P[<-|a_lt_b]. + rewrite [X in _ = X + _]Rintegral_itv0// add0r. + by apply: Rintegral_itvby_itvby. +transitivity (Rintegral mu `]a, +oo[ f); first by apply: Rintegral_itvby_itvby. +rewrite (itv_bndbnd_setU (x := BSide b2 b))//; [by apply: lteifS .. |]. +rewrite [LHS]Rintegral_setU; [ exact: measurable_itv .. | | |]. +- by rewrite -itv_bndbnd_setU//; apply: lteifS. +- apply/disj_setPS => x /=[/andP[_ +] /andP[+ _]]. + move/le_trans/[apply]. + by rewrite bnd_simp ltxx. +congr (_ + _); apply: Rintegral_itvbb_itvbb => //. +apply: measurable_funS mf => //. +by apply: subset_itvl. +Qed. + +Lemma Rintegral_patch_finite (f g : R -> R) (A D : set R) : + lebesgue_display.-measurable A -> finite_set D -> measurable_fun A f -> Rintegral mu A (patch f D g) = Rintegral mu A f. +Proof. +move=> mA finD mf. +case: (finD) => n; rewrite card_eq_sym => /pcard_eqP[indexD]. +have bij_indexD := bij (f := indexD). +have D_bigcup : D = \bigcup_(i < n) [set indexD i]. + by rewrite -{1}(fsbig_setU_set1 finD) (reindex_fsbig indexD _ _ _ bij_indexD)/= fsbig_setU. +have mfD (h : R -> R) : measurable_fun D h. + rewrite D_bigcup bigcup_mkcond. + apply/measurable_fun_bigcup => i; first by case: ifP. + case: ifP => // _. + - exact: measurable_fun_set1. + - exact: measurable_fun_set0. +apply: Rintegral_patch_negligible => //. +- rewrite D_bigcup bigcup_mkcond. + apply: bigcup_measurable => k _. + by case: ifP. +- apply: countable_lebesgue_measure0. + exact: finite_set_countable finD. +Qed. + End Rintegral_lebesgue_measure. #[deprecated(since="mathcomp-analysis 1.17.0", use=Rintegral_itvbo_itvbc)] Notation Rintegral_itv_bndo_bndc := Rintegral_itvbo_itvbc (only parsing). From f01d1be9f7c8a6b77a51e1808500240d14b051c3 Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 19:07:58 +0200 Subject: [PATCH 6/8] Rintegral bound continuity --- .../lebesgue_Rintegral.v | 202 ++++++++++++++++++ 1 file changed, 202 insertions(+) diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v index 1d87837d7c..c004c2630c 100644 --- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v +++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v @@ -425,3 +425,205 @@ End Rintegral_lebesgue_measure. Notation Rintegral_itv_bndo_bndc := Rintegral_itvbo_itvbc (only parsing). #[deprecated(since="mathcomp-analysis 1.17.0", use=Rintegral_itvob_itvcb)] Notation Rintegral_itv_obnd_cbnd := Rintegral_itvob_itvcb (only parsing). + +Section Rintegral_bound_continuity. +Context (R : realType) (mu := @lebesgue_measure R) (f : R -> R). +Context (a b x y : R) (x_ y_ : R -> R) (b1 b2 b1' b2' : bool). + +Hypothesis a_lt_b : a < b. +Hypothesis f_int : + mu.-integrable [set` Interval (BSide b1 a) (BSide b2 b)] (EFin \o f). +Hypotheses (a_le_x : a <= x) (y_le_b : y <= b). +Hypothesis near_x_ge_a : \forall e \near 0^'+, a <= x_ e. +Hypothesis near_y_le_b : \forall e \near 0^'+, y_ e <= b. +Hypotheses (cvg_x : x_ @ 0^'+ --> x) (cvg_y : y_ @ 0^'+ --> y). + +Lemma Rintegral_bound_continuous : + \int[mu]_(z in [set` Interval (BSide b1 (x_ e)) (BSide b2 (y_ e))]) (f z) + @[e --> 0^'+] --> + \int[mu]_(z in [set` Interval (BSide b1' x) (BSide b2' y)]) (f z). +Proof. +have mf_oo x' y' : a <= x' -> y' <= b -> measurable_fun `]x', y'[ f. + move=> a_le_x' y'_le_b. + apply: measurable_funS; last first. + - apply/measurable_EFinP. + apply: (measurable_int mu). + exact: f_int. + - by apply: subset_itvW. + - exact: measurable_itv. +wlog suff oo_cvg : / \int[mu]_(z in `]x_ e, y_ e[) f z + @[e --> 0^'+] --> \int[mu]_(z in `]x, y[) f z. +apply: cvg_trans; last apply: (cvg_to_eq oo_cvg). +- apply: near_eq_cvg. + near=> e. + apply: Rintegral_itvbb_itvbb => //. + by apply: mf_oo; near: e. +- apply: Rintegral_itvbb_itvbb => //. + by apply: mf_oo. +apply: cvg_trans. + apply: near_eq_cvg. + near=> e. + by rewrite Rintegral_mkcond. +apply/cvg_at_rightP => u [u_gt0 u_to0]. +wlog x_u_gea : u u_gt0 u_to0 / forall n, a <= x_ (u n). + move=> gea_case. + have [/= r r0 br_gea] := near_x_ge_a. + have [/= N _ geN_Nr] := u_to0 _ (nbhsx_ballx 0 r r0). + rewrite -(cvg_shiftn N). + apply: gea_case. + - by move=> ?; exact: u_gt0. + - by rewrite cvg_shiftn. + - move=> n. + apply: br_gea => //. + apply: geN_Nr => /=. + exact: leq_addl. +wlog y_u_leb : u u_gt0 u_to0 x_u_gea / forall n, y_ (u n) <= b. + move=> leb_case. + have [/= r r0 br_leb] := near_y_le_b. + have [/= N _ geN_Nr] := u_to0 _ (nbhsx_ballx 0 r r0). + rewrite -(cvg_shiftn N). + apply: leb_case. + - by move=> ?; exact: u_gt0. + - by rewrite cvg_shiftn. + - by move=> ?; exact: x_u_gea. + - move=> n. + apply: br_leb => //. + apply: geN_Nr => /=. + exact: leq_addl. +rewrite Rintegral_mkcond. +wlog suff patch_cvg : / + \int[mu]_z patch (f \_ `]x_ (u n), y_ (u n)[) [set x; y] 0 z + @[n --> \oo] --> \int[mu]_z patch (f \_ `]x, y[) [set x; y] 0 z. + apply: cvg_trans; last apply: (cvg_to_eq patch_cvg). + - apply: near_eq_cvg. + near=> n. + apply: Rintegral_patch_finite => //. + apply: (iffLR (measurable_restrictT _ _)) => //. + by apply: mf_oo. + - apply: Rintegral_patch_finite => //. + apply: (iffLR (measurable_restrictT _ _)) => //. + by apply: mf_oo. +unshelve apply: Rdominated_cvg => /=. +- exact: (fun z => `|(f \_ `]a, b[) z|). +- by []. +- move=> n. + apply: (eq_measurable_fun ((f \_ `]x_ (u n), y_ (u n)[) \_ ~` [set x; y])). + move=> z _ /=. + by rewrite /patch /= /in_mem/= /in_set/= asbool_neg if_neg. + have mxy : measurable (~` [set x; y]). + apply: measurableC. + by apply/measurableU. + apply: (iffLR (measurable_restrictT _ _)) => //. + apply/measurable_restrict => //. + rewrite setIC -setDE. + apply/measurable_EFinP. + apply: (measurable_int mu). + apply: integrableS f_int => //. + + by apply: measurableI. + + apply: subset_trans; first exact: subDsetl. + by apply: subset_itvW. +- move=> z _ /=. + apply/cvgrPdist_lt => /= eps eps0. + under eq_near => ?. + rewrite /patch in_setU !in_set1 !set_itvE /in_mem/= /in_set/= !asboolb. + over. + case: (ltgtP x z) => [x_lt_z|z_lt_x|_] /=; last first. + + by apply: nearW; rewrite subrr normr0. + + near=> n. + case: (eqVneq z y) => _; first by rewrite subrr normr0. + rewrite ifN ?subrr ?normr0// negb_and -leNgt. + apply/orP; left. + near: n. + apply: (cvgr_ge x) => //. + move: u {u_gt0 u_to0 x_u_gea y_u_leb} (conj u_gt0 u_to0). + by apply/cvg_at_rightP. + case: (ltgtP z y) => [z_lt_y|y_lt_z|_]; last first. + + by apply: nearW; rewrite subrr normr0. + + near=> n. + rewrite ifN ?subrr ?normr0// negb_and -!leNgt. + apply/orP; right. + near: n. + apply: (cvgr_le y) => //. + move: u {u_gt0 u_to0 x_u_gea y_u_leb} (conj u_gt0 u_to0). + by apply/cvg_at_rightP. + + near=> n. + rewrite ifT ?subrr ?normr0//. + apply/andP; split; near: n. + * apply: (cvgr_lt x) => //. + move: u {u_gt0 u_to0 x_u_gea y_u_leb} (conj u_gt0 u_to0). + by apply/cvg_at_rightP. + * apply: (cvgr_gt y) => //. + move: u {u_gt0 u_to0 x_u_gea y_u_leb} (conj u_gt0 u_to0). + by apply/cvg_at_rightP. +- apply: eq_integrable; first by []. + move=> z _ /=. + rewrite -abse_EFin. + transitivity (`|((EFin \o f) \_ `]a, b[) z|%E) => //. + by rewrite restrict_EFin. + apply: integrable_abse. + apply: (iffLR (integrable_mkcond _ _)) => //. + apply: integrableS; last exact: f_int; [ exact: measurable_itv .. |]. + by apply: subset_itvW. +- move=> n z _ /=. + rewrite /patch /point/=. + case: (ifP (z \in `]a, b[%classic)) => [_|/negbT z_not_itv]. + + by repeat (case: ifP => _); rewrite ?normr0. + + rewrite normr0 normr_le0; apply/eqP. + case: ifP => // /negbT z_not_xy. + rewrite ifN// notin_setE set_itvE/= => /andP[xu_lt_z z_lt_yu]. + move: z_not_itv => /negP; apply. + rewrite inE/= in_itv/=. + apply/andP; split. + * by apply: le_lt_trans; last exact: xu_lt_z. + * by apply: lt_le_trans; first exact: z_lt_yu. +Unshelve. all: by end_near. Qed. + +End Rintegral_bound_continuity. + +Section Rintegral_bound_infty_continuity. +Context (R : realType) (f : R -> R) (mu := @lebesgue_measure R). +Context (a x : R) (x_ : R -> R) (b1 b1' : bool). +Hypothesis f_int : + mu.-integrable [set` Interval (BSide b1 a) +oo%O] (EFin \o f). +Hypothesis a_le_x : a <= x. +Hypothesis near_x_ge_a : \forall e \near 0^'+, a <= x_ e. +Hypotheses cvg_x : x_ @ 0^'+ --> x. + +Lemma Rintegral_bound_infty_continuous : + \int[mu]_(z in [set` Interval (BSide b1 (x_ e)) +oo%O]) (f z) + @[e --> 0^'+] --> \int[mu]_(z in [set` Interval (BSide b1' x) +oo%O]) (f z). +Proof. +near +oo_R => M. +apply: cvg_trans. + apply: near_eq_cvg. + near=> e. + rewrite (Rintegral_itvDy (b := BRight M) b1 b1)// ?bnd_simp. + - near: e. + apply: (cvgr_le x) => //. + near: M. + apply: nbhs_pinfty_gt. + exact: num_real. + - apply: integrableS f_int => //. + apply: subset_itvr. + by near: e. +apply: cvg_to_eq. + apply: cvgDr. + apply: (@Rintegral_bound_continuous _ _ a M x M _ _ _ _ b1' false) => //. + - apply: integrableS f_int => //. + by apply: subset_itvl. + - by near=> y. + - exact: cvg_cst. +transitivity (\int[mu]_(z in `]x, +oo[) f z). + apply: Rintegral_itvby_itvoy. + apply: (measurable_int mu). + apply: integrableS f_int => //. + by apply: subset_itvr. +rewrite (Rintegral_itvDy (b := BRight M) _ b1')// ?bnd_simp. +- near: M. + apply: nbhs_pinfty_ge. + exact: num_real. +- apply: integrableS f_int => //. + by apply: subset_itvr. +Unshelve. all: by end_near. Qed. + +End Rintegral_bound_infty_continuity. From d9f1acca8e2a008e45c1446bda3982b8e23cff1e Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 19:15:09 +0200 Subject: [PATCH 7/8] Dominated convergence for Rintegral --- CHANGELOG_UNRELEASED.md | 3 ++ .../lebesgue_Rintegral.v | 43 +++++++++++++++++++ 2 files changed, 46 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2d85fdc0a5..2a9790a104 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -234,6 +234,9 @@ - in `measurable_structure.v`: + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable` +- in file `lebesgue_Rintegral.v`, + + new lemma `Rdominated_cvg`. + ### Changed - in `realsum.v`: diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v index 82c8feb1e5..4e9b1dc145 100644 --- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v +++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v @@ -247,3 +247,46 @@ End Rintegral_lebesgue_measure. Notation Rintegral_itv_bndo_bndc := Rintegral_itvbo_itvbc (only parsing). #[deprecated(since="mathcomp-analysis 1.17.0", use=Rintegral_itvob_itvcb)] Notation Rintegral_itv_obnd_cbnd := Rintegral_itvob_itvcb (only parsing). + +Section Rdominated_convergence. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D). +Variables (f_ : (T -> R)^nat) (f g : T -> R). +Hypothesis mf_ : forall n, measurable_fun D (f_ n). +Hypothesis f_f : forall x, D x -> f_ ^~ x @ \oo --> f x. +Hypothesis ig : integrable.body mu D (EFin \o g). +Hypothesis absfg : forall n x, D x -> `|f_ n x| <= g x. + +Let mf_e n : measurable_fun D (EFin \o f_ n). +Proof. by apply/measurable_EFinP. Qed. + +Let f_fe (x : T) : D x -> (f_ n x)%:E @[n --> \oo] --> (f x)%:E. +Proof. +move=> Dx. +apply/fine_cvgP; split; first by apply: nearW. +by apply: f_f. +Qed. + +Let egi (x : T) : (g x)%:E \is a fin_num. +Proof. by []. Qed. + +Let absfge (n : nat) (x : T) : D x -> (`|(f_ n x)%:E| <= (g x)%:E)%E. +Proof. +move=> Dx. +rewrite abse_EFin lee_fin. +by apply: absfg. +Qed. + +Let mf : measurable_fun D (EFin \o f). +Proof. by apply: emeasurable_fun_cvg; first by exact: mf_e. Qed. + +Lemma Rdominated_cvg : \int[mu]_(x in D) f_ n x @[n \oo] --> \int[mu]_(x in D) f x. +Proof. +rewrite /Rintegral. +have := dominated_convergence mD mf_e mf (aeW _ f_fe) ig (aeW _ (fun x n Dx => absfge n Dx)). +move=> /= [i_f _ +]. +rewrite -[X in _ --> X]fineK; first by apply: integrable_fin_num. +by move/fine_cvg. +Qed. + +End Rdominated_convergence. \ No newline at end of file From 0889efa54ee430658fde91d67ad1c476d2143d9f Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 20:21:30 +0200 Subject: [PATCH 8/8] Fix unintended nesting --- .../lebesgue_Rintegral.v | 26 +++++++++---------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v index e70cea39b0..b4511aaf10 100644 --- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v +++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v @@ -426,20 +426,6 @@ Notation Rintegral_itv_bndo_bndc := Rintegral_itvbo_itvbc (only parsing). #[deprecated(since="mathcomp-analysis 1.17.0", use=Rintegral_itvob_itvcb)] Notation Rintegral_itv_obnd_cbnd := Rintegral_itvob_itvcb (only parsing). -Section Rintegral_bound_continuity. -Context (R : realType) (mu := @lebesgue_measure R) (f : R -> R). -Context (a b x y : R) (x_ y_ : R -> R) (b1 b2 b1' b2' : bool). - -Hypothesis a_lt_b : a < b. -Hypothesis f_int : - mu.-integrable [set` Interval (BSide b1 a) (BSide b2 b)] (EFin \o f). -Hypotheses (a_le_x : a <= x) (y_le_b : y <= b). -Hypothesis near_x_ge_a : \forall e \near 0^'+, a <= x_ e. -Hypothesis near_y_le_b : \forall e \near 0^'+, y_ e <= b. -Hypotheses (cvg_x : x_ @ 0^'+ --> x) (cvg_y : y_ @ 0^'+ --> y). - - - Section Rdominated_convergence. Context d (T : measurableType d) (R : realType). Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D). @@ -483,6 +469,18 @@ Qed. End Rdominated_convergence. +Section Rintegral_bound_continuity. +Context (R : realType) (mu := @lebesgue_measure R) (f : R -> R). +Context (a b x y : R) (x_ y_ : R -> R) (b1 b2 b1' b2' : bool). + +Hypothesis a_lt_b : a < b. +Hypothesis f_int : + mu.-integrable [set` Interval (BSide b1 a) (BSide b2 b)] (EFin \o f). +Hypotheses (a_le_x : a <= x) (y_le_b : y <= b). +Hypothesis near_x_ge_a : \forall e \near 0^'+, a <= x_ e. +Hypothesis near_y_le_b : \forall e \near 0^'+, y_ e <= b. +Hypotheses (cvg_x : x_ @ 0^'+ --> x) (cvg_y : y_ @ 0^'+ --> y). + Lemma Rintegral_bound_continuous : \int[mu]_(z in [set` Interval (BSide b1 (x_ e)) (BSide b2 (y_ e))]) (f z) @[e --> 0^'+] -->