From 8dc8034c5c6f1edae0f9c3ac3851a86e0d253f3b Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Fri, 18 Apr 2025 17:01:54 +0900 Subject: [PATCH 1/4] ge0_nondecreasing_set_seq_cvg_integral --- CHANGELOG_UNRELEASED.md | 6 + .../lebesgue_integral_nonneg.v | 105 ++++++++++++++++++ 2 files changed, 111 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e4099bc37d..d8fb7670ad 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -80,6 +80,12 @@ + lemma `measurable_cons` + lemma `measurable_behead` +- in `lebesgue_integral_theory/lebesgue_integral_nonneg.v`: + + lemmas `ge0_nondecreasing_set_seq_nondecreasing_integral_seq`, + `ge0_nondecreasing_set_seq_cvg_integral`, + `le0_nondecreasing_set_seq_nonincreasing_integral_seq`, + `le0_nondecreasing_set_seq_cvg_integral` + ### Changed - in `convex.v`: diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index bcfc9eb16e..e2a67a17d3 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -1558,3 +1558,108 @@ Qed. End lebesgue_measure_integral. Arguments integral_Sset1 {R f A} r. + +Section ge0_nondecreasing_set_seq_cvg_integral. +Context {R : realType}. +Variables (S : (set R)^nat) (f : R -> \bar R). + +Local Open Scope ereal_scope. + +Hypotheses (nndS : nondecreasing_seq S) (mS : (forall i, measurable (S i))). +Hypothesis (mf : (forall i, measurable_fun (S i) f)). +Hypothesis (f0 : forall i x, S i x -> 0 <= f x). + +Notation mu := lebesgue_measure. + +Lemma ge0_nondecreasing_set_seq_nondecreasing_integral_seq : + nondecreasing_seq (fun i => \int[mu]_(x in S i) f x). +Proof. +apply/nondecreasing_seqP => n. +apply: ge0_subset_integral => //=; [exact: mS|exact: mS|exact: mf| |]. +- by move=> ?; exact: f0. +- by rewrite -subsetEset; exact: nndS. +Qed. + +Lemma ge0_nondecreasing_set_seq_cvg_integral : + \int[mu]_(x in (S i)) f x @[i --> \oo] --> + \int[mu]_(x in \bigcup_i S i) f x. +Proof. +apply: cvg_toP. + apply: ereal_nondecreasing_is_cvgn. + exact: ge0_nondecreasing_set_seq_nondecreasing_integral_seq. +under eq_fun do rewrite integral_mkcond/=. +rewrite -monotone_convergence//=; last 3 first. +- by move=> n; apply/(measurable_restrictT f). +- by move=> n x _; apply: erestrict_ge0 => {}x Snx; apply: f0 Snx. +- move=> x _; apply/nondecreasing_seqP => n; apply: restrict_lee => //. + by move=> {}x Snx; apply: f0 Snx. + by rewrite -subsetEset; exact: nndS. +rewrite [RHS]integral_mkcond/=. +apply: eq_integral => /=; rewrite /g_sigma_algebraType/ocitv_type => x _. +transitivity (ereal_sup (range (fun n => (f \_ (S n)) x))). + apply/cvg_lim => //. + apply/ereal_nondecreasing_cvgn/nondecreasing_seqP => n; apply: restrict_lee. + by move=> {}x Snx; apply: f0 Snx. + by rewrite -subsetEset; exact: nndS. +apply/eqP; rewrite eq_le; apply/andP; split. +- apply: ub_ereal_sup => _/= [n _ <-]. + apply: restrict_lee => //; last exact: bigcup_sup. + by move=> ? [? _ Smy]; apply: f0 Smy. +- rewrite patchE; case: ifPn=> [|/negP]. + rewrite inE => -[n _ Snx]. + apply: ereal_sup_le; exists (f \_ (S n) x) => //. + by rewrite patchE mem_set. + rewrite inE -[X in X -> _]/((~` _) x) setC_bigcup => nSx. + apply/ereal_sup_le; exists point => //=; exists 0%R => //. + by rewrite patchE memNset//; exact: nSx. +Qed. + +End ge0_nondecreasing_set_seq_cvg_integral. + +Section le0_nondecreasing_set_seq_cvg_integral. +Context {R : realType}. +Variables (S : (set R)^nat) (f : R -> \bar R). + +Local Open Scope ereal_scope. + +Hypotheses (nndS : nondecreasing_seq S) (mS : (forall i, measurable (S i))). +Hypothesis (mf : (forall i, measurable_fun (S i) f)). +Hypothesis (f0 : forall i x, S i x -> f x <= 0). + +Notation mu := lebesgue_measure. + +Let intNS n : (- \int[mu]_(x in S n) f x) = \int[mu]_(x in S n) - f x. +Proof. +apply/esym; apply: integralN => /=. +apply: fin_num_adde_defr. +rewrite integral0_eq// => x Snx. +by rewrite (@le0_funeposE _ _ (S n))// ?inE//; apply: f0. +Qed. + +Let mNf i : measurable_fun (S i) (\- f). +Proof. by apply: measurableT_comp => //; exact: mf. Qed. + +Let Nf_ge0 i x: S i x -> 0%R <= - f x. +Proof. by move=> Six; rewrite leeNr oppe0; exact: f0 Six. Qed. + +Lemma le0_nondecreasing_set_seq_nonincreasing_integral_seq : + nonincreasing_seq (fun i => \int[mu]_(x in S i) f x). +Proof. +move=> m n mn; rewrite -leeN2 2!intNS. +exact: ge0_nondecreasing_set_seq_nondecreasing_integral_seq. +Qed. + +Lemma le0_nondecreasing_set_seq_cvg_integral : + \int[mu]_(x in (S i)) f x @[i --> \oo] --> + \int[mu]_(x in \bigcup_i S i) f x. +Proof. +apply/cvgeNP. +rewrite -integralN/=; last first. + apply: fin_num_adde_defr. + rewrite integral0_eq// => x [n _ Snx]. + by rewrite (le0_funeposE (@f0 n))// inE. +under eq_cvg do rewrite intNS. +exact: ge0_nondecreasing_set_seq_cvg_integral. +Qed. + +End le0_nondecreasing_set_seq_cvg_integral. From 678b20883ea367bfc1bbf6a33b8a875eef627c32 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Fri, 18 Apr 2025 17:23:53 +0900 Subject: [PATCH 2/4] generalize --- .../lebesgue_integral_nonneg.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index e2a67a17d3..c146ce2300 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -1560,8 +1560,9 @@ End lebesgue_measure_integral. Arguments integral_Sset1 {R f A} r. Section ge0_nondecreasing_set_seq_cvg_integral. -Context {R : realType}. -Variables (S : (set R)^nat) (f : R -> \bar R). +Context {d : measure_display} {T : measurableType d} {R : realType}. +Variables (S : (set T)^nat) (f : T -> \bar R). +Variable (mu : measure T R). Local Open Scope ereal_scope. @@ -1569,13 +1570,11 @@ Hypotheses (nndS : nondecreasing_seq S) (mS : (forall i, measurable (S i))). Hypothesis (mf : (forall i, measurable_fun (S i) f)). Hypothesis (f0 : forall i x, S i x -> 0 <= f x). -Notation mu := lebesgue_measure. - Lemma ge0_nondecreasing_set_seq_nondecreasing_integral_seq : nondecreasing_seq (fun i => \int[mu]_(x in S i) f x). Proof. apply/nondecreasing_seqP => n. -apply: ge0_subset_integral => //=; [exact: mS|exact: mS|exact: mf| |]. +apply: ge0_subset_integral => //=. - by move=> ?; exact: f0. - by rewrite -subsetEset; exact: nndS. Qed. @@ -1617,8 +1616,9 @@ Qed. End ge0_nondecreasing_set_seq_cvg_integral. Section le0_nondecreasing_set_seq_cvg_integral. -Context {R : realType}. -Variables (S : (set R)^nat) (f : R -> \bar R). +Context {d : measure_display} {T : measurableType d} {R : realType}. +Variables (S : (set T)^nat) (f : T -> \bar R). +Variable (mu : measure T R). Local Open Scope ereal_scope. From dd84d27f6c8f9921778b6c204e6cd72c0509c37b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 17 Jun 2025 16:50:05 +0900 Subject: [PATCH 3/4] nitpicking --- CHANGELOG_UNRELEASED.md | 2 +- .../lebesgue_integral_nonneg.v | 107 ++++++++---------- 2 files changed, 47 insertions(+), 62 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d8fb7670ad..45830acd72 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -81,7 +81,7 @@ + lemma `measurable_behead` - in `lebesgue_integral_theory/lebesgue_integral_nonneg.v`: - + lemmas `ge0_nondecreasing_set_seq_nondecreasing_integral_seq`, + + lemmas `ge0_nondecreasing_set_nondecreasing_integral`, `ge0_nondecreasing_set_seq_cvg_integral`, `le0_nondecreasing_set_seq_nonincreasing_integral_seq`, `le0_nondecreasing_set_seq_cvg_integral` diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index c146ce2300..329bdb0e69 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -1559,107 +1559,92 @@ Qed. End lebesgue_measure_integral. Arguments integral_Sset1 {R f A} r. -Section ge0_nondecreasing_set_seq_cvg_integral. +Section ge0_nondecreasing_set_cvg_integral. Context {d : measure_display} {T : measurableType d} {R : realType}. -Variables (S : (set T)^nat) (f : T -> \bar R). -Variable (mu : measure T R). - +Variables (F : (set T)^nat) (f : T -> \bar R) (mu : measure T R). Local Open Scope ereal_scope. +Hypotheses (nndF : nondecreasing_seq F) (mF : forall i, measurable (F i)). +Hypothesis mf : forall i, measurable_fun (F i) f. +Hypothesis f0 : forall i x, F i x -> 0 <= f x. -Hypotheses (nndS : nondecreasing_seq S) (mS : (forall i, measurable (S i))). -Hypothesis (mf : (forall i, measurable_fun (S i) f)). -Hypothesis (f0 : forall i x, S i x -> 0 <= f x). - -Lemma ge0_nondecreasing_set_seq_nondecreasing_integral_seq : - nondecreasing_seq (fun i => \int[mu]_(x in S i) f x). +Lemma ge0_nondecreasing_set_nondecreasing_integral : + nondecreasing_seq (fun i => \int[mu]_(x in F i) f x). Proof. -apply/nondecreasing_seqP => n. -apply: ge0_subset_integral => //=. +apply/nondecreasing_seqP => n; apply: ge0_subset_integral => //=. - by move=> ?; exact: f0. -- by rewrite -subsetEset; exact: nndS. +- by rewrite -subsetEset; exact: nndF. Qed. -Lemma ge0_nondecreasing_set_seq_cvg_integral : - \int[mu]_(x in (S i)) f x @[i --> \oo] --> - \int[mu]_(x in \bigcup_i S i) f x. +Lemma ge0_nondecreasing_set_cvg_integral : + \int[mu]_(x in F i) f x @[i --> \oo] --> \int[mu]_(x in \bigcup_i F i) f x. Proof. apply: cvg_toP. apply: ereal_nondecreasing_is_cvgn. - exact: ge0_nondecreasing_set_seq_nondecreasing_integral_seq. + exact: ge0_nondecreasing_set_nondecreasing_integral. under eq_fun do rewrite integral_mkcond/=. rewrite -monotone_convergence//=; last 3 first. - by move=> n; apply/(measurable_restrictT f). -- by move=> n x _; apply: erestrict_ge0 => {}x Snx; apply: f0 Snx. +- by move=> n x _; apply: erestrict_ge0 => {}x; exact: f0. - move=> x _; apply/nondecreasing_seqP => n; apply: restrict_lee => //. - by move=> {}x Snx; apply: f0 Snx. - by rewrite -subsetEset; exact: nndS. + by move=> {}x; exact: f0. + by rewrite -subsetEset; exact: nndF. rewrite [RHS]integral_mkcond/=. apply: eq_integral => /=; rewrite /g_sigma_algebraType/ocitv_type => x _. -transitivity (ereal_sup (range (fun n => (f \_ (S n)) x))). +transitivity (ereal_sup (range (fun n => (f \_ (F n)) x))). apply/cvg_lim => //. apply/ereal_nondecreasing_cvgn/nondecreasing_seqP => n; apply: restrict_lee. - by move=> {}x Snx; apply: f0 Snx. - by rewrite -subsetEset; exact: nndS. + by move=> {}x; exact: f0. + by rewrite -subsetEset; exact: nndF. apply/eqP; rewrite eq_le; apply/andP; split. - apply: ub_ereal_sup => _/= [n _ <-]. - apply: restrict_lee => //; last exact: bigcup_sup. - by move=> ? [? _ Smy]; apply: f0 Smy. + apply: restrict_lee; last exact: bigcup_sup. + by move=> ? [? _]; exact: f0. - rewrite patchE; case: ifPn=> [|/negP]. - rewrite inE => -[n _ Snx]. - apply: ereal_sup_le; exists (f \_ (S n) x) => //. - by rewrite patchE mem_set. - rewrite inE -[X in X -> _]/((~` _) x) setC_bigcup => nSx. - apply/ereal_sup_le; exists point => //=; exists 0%R => //. - by rewrite patchE memNset//; exact: nSx. + rewrite inE => -[n _ Fnx]. + by apply: ereal_sup_ge; exists (f \_ (F n) x) => //; rewrite patchE mem_set. + rewrite inE -[X in X -> _]/((~` _) x) setC_bigcup => nFx. + apply/ereal_sup_ge; exists point => //=; exists 0%R => //. + by rewrite patchE memNset//; exact: nFx. Qed. -End ge0_nondecreasing_set_seq_cvg_integral. +End ge0_nondecreasing_set_cvg_integral. -Section le0_nondecreasing_set_seq_cvg_integral. +Section le0_nondecreasing_set_cvg_integral. Context {d : measure_display} {T : measurableType d} {R : realType}. -Variables (S : (set T)^nat) (f : T -> \bar R). -Variable (mu : measure T R). - +Variables (F : (set T)^nat) (f : T -> \bar R) (mu : measure T R). Local Open Scope ereal_scope. +Hypotheses (nndF : nondecreasing_seq F) (mF : forall i, measurable (F i)). +Hypothesis mf : forall i, measurable_fun (F i) f. +Hypothesis f0 : forall i x, F i x -> f x <= 0. -Hypotheses (nndS : nondecreasing_seq S) (mS : (forall i, measurable (S i))). -Hypothesis (mf : (forall i, measurable_fun (S i) f)). -Hypothesis (f0 : forall i x, S i x -> f x <= 0). - -Notation mu := lebesgue_measure. - -Let intNS n : (- \int[mu]_(x in S n) f x) = \int[mu]_(x in S n) - f x. +Let intNS n : (- \int[mu]_(x in F n) f x) = \int[mu]_(x in F n) - f x. Proof. -apply/esym; apply: integralN => /=. -apply: fin_num_adde_defr. -rewrite integral0_eq// => x Snx. -by rewrite (@le0_funeposE _ _ (S n))// ?inE//; apply: f0. +apply/esym; apply: integralN => /=; apply: fin_num_adde_defr. +rewrite integral0_eq// => x Fnx. +by rewrite (@le0_funeposE _ _ (F n)) ?inE//; exact: f0. Qed. -Let mNf i : measurable_fun (S i) (\- f). +Let mNf i : measurable_fun (F i) (\- f). Proof. by apply: measurableT_comp => //; exact: mf. Qed. -Let Nf_ge0 i x: S i x -> 0%R <= - f x. +Let Nf_ge0 i x: F i x -> 0%R <= - f x. Proof. by move=> Six; rewrite leeNr oppe0; exact: f0 Six. Qed. -Lemma le0_nondecreasing_set_seq_nonincreasing_integral_seq : - nonincreasing_seq (fun i => \int[mu]_(x in S i) f x). +Lemma le0_nondecreasing_set_nonincreasing_integral : + nonincreasing_seq (fun i => \int[mu]_(x in F i) f x). Proof. move=> m n mn; rewrite -leeN2 2!intNS. -exact: ge0_nondecreasing_set_seq_nondecreasing_integral_seq. +exact: ge0_nondecreasing_set_nondecreasing_integral. Qed. -Lemma le0_nondecreasing_set_seq_cvg_integral : - \int[mu]_(x in (S i)) f x @[i --> \oo] --> - \int[mu]_(x in \bigcup_i S i) f x. +Lemma le0_nondecreasing_set_cvg_integral : + \int[mu]_(x in F i) f x @[i --> \oo] --> \int[mu]_(x in \bigcup_i F i) f x. Proof. -apply/cvgeNP. -rewrite -integralN/=; last first. - apply: fin_num_adde_defr. - rewrite integral0_eq// => x [n _ Snx]. +apply/cvgeNP; rewrite -integralN/=; last first. + apply: fin_num_adde_defr; rewrite integral0_eq// => x [n _ Fnx]. by rewrite (le0_funeposE (@f0 n))// inE. under eq_cvg do rewrite intNS. -exact: ge0_nondecreasing_set_seq_cvg_integral. +exact: ge0_nondecreasing_set_cvg_integral. Qed. -End le0_nondecreasing_set_seq_cvg_integral. +End le0_nondecreasing_set_cvg_integral. From 42a64e229c62d3c594f0bf4da5e571e9c01414df Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 17 Jun 2025 16:51:27 +0900 Subject: [PATCH 4/4] fix --- CHANGELOG_UNRELEASED.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 45830acd72..49d39f878a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -82,9 +82,9 @@ - in `lebesgue_integral_theory/lebesgue_integral_nonneg.v`: + lemmas `ge0_nondecreasing_set_nondecreasing_integral`, - `ge0_nondecreasing_set_seq_cvg_integral`, - `le0_nondecreasing_set_seq_nonincreasing_integral_seq`, - `le0_nondecreasing_set_seq_cvg_integral` + `ge0_nondecreasing_set_cvg_integral`, + `le0_nondecreasing_set_nonincreasing_integral`, + `le0_nondecreasing_set_cvg_integral` ### Changed