From 785d6fa45470728b7295cc01c205abbaed648c87 Mon Sep 17 00:00:00 2001 From: ScreenL <915402966@qq.com> Date: Wed, 2 Jul 2025 17:46:28 -0700 Subject: [PATCH 1/2] added monotonicity for nonnegative lebesgue integrals w.r.t. measures --- CHANGELOG_UNRELEASED.md | 1 + .../lebesgue_integral_nonneg.v | 32 +++++++++++++++++++ 2 files changed, 33 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index bb6f83da8d..9516b1347c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -85,6 +85,7 @@ `ge0_nondecreasing_set_cvg_integral`, `le0_nondecreasing_set_nonincreasing_integral`, `le0_nondecreasing_set_cvg_integral` + + lemmas `sintegral_le_measure`, `ge0_integral_le_measure` - in `set_interval.v`: + lemma `memB_itv`, `memB_itv0` diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index 65dabf3217..4c36d34243 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -1648,3 +1648,35 @@ exact: ge0_nondecreasing_set_cvg_integral. Qed. End le0_nondecreasing_set_cvg_integral. + +Section ge0_integral_le_measure. +Local Open Scope ereal_scope. +Local Open Scope classical_set_scope. +Context {d} {T : measurableType d} [R : realType]. +Variables (mu1 mu2 : measure T R). +Hypothesis (Hml : (forall S, measurable S -> mu1 S <= mu2 S)). + +Import HBNNSimple. + +Lemma sintegral_le_measure (h : {nnsfun T >-> R}): + sintegral mu1 h <= sintegral mu2 h. +Proof. +rewrite !sintegralE /=. +apply/ lee_fsum => // i [a Ha <-]. +apply: lee_pmul => //; first by apply/ lee_tofin. +by apply: Hml. +Qed. + +Lemma ge0_integral_le_measure (f : T -> \bar R) S (Hms: measurable S): + (forall x, 0 <= f x) -> + measurable_fun setT f -> + (\int[mu1]_(x in S) f x <= \int[mu2]_(x in S) f x). +Proof. +move=> Hf0 Hfm. +rewrite !ge0_integralE //=. +apply: ub_ereal_sup => x [h Hh] /= <-. +apply: ereal_sup_ge; exists (sintegral mu2 h) => //=; first by eexists. +by apply: sintegral_le_measure. +Qed. + +End ge0_integral_le_measure. \ No newline at end of file From bddeb97f9873bd8d73cba45de92291ed43db8a3f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 3 Jul 2025 14:34:52 +0900 Subject: [PATCH 2/2] nitpick --- CHANGELOG_UNRELEASED.md | 4 ++- .../lebesgue_integral_definition.v | 35 +++++++++++++++++++ .../lebesgue_integral_nonneg.v | 32 ----------------- 3 files changed, 38 insertions(+), 33 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9516b1347c..55e7b7c4a6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -85,7 +85,6 @@ `ge0_nondecreasing_set_cvg_integral`, `le0_nondecreasing_set_nonincreasing_integral`, `le0_nondecreasing_set_cvg_integral` - + lemmas `sintegral_le_measure`, `ge0_integral_le_measure` - in `set_interval.v`: + lemma `memB_itv`, `memB_itv0` @@ -103,6 +102,9 @@ - in `lebesgue_integral_nonneg.v`: + lemma `ge0_integral_ereal_sup` (was a `Let`) +- in `lebesgue_integral_definition.v`: + + lemmas `le_measure_sintegral`, `ge0_le_measure_integral` + ### Changed - in `convex.v`: diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index 67b72ae860..ce39a63106 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v @@ -119,6 +119,22 @@ Lemma eq_sintegral d (T : sigmaRingType d) (R : numDomainType) Proof. by move=> /funext->. Qed. Arguments eq_sintegral {d T R mu} g. +Section le_measure_sintegral. +Local Open Scope ereal_scope. +Context {d} {T : measurableType d} {R : realType}. +Variables m1 m2 : {measure set T -> \bar R}. +Hypothesis m12 : forall S, measurable S -> m1 S <= m2 S. + +Import HBNNSimple. + +Lemma le_measure_sintegral (f : {nnsfun T >-> R}) : + sintegral m1 f <= sintegral m2 f. +Proof. +by rewrite !sintegralE lee_fsum// => r [t _ <-]; rewrite lee_pmul ?lee_fin ?m12. +Qed. + +End le_measure_sintegral. + Section sintegralrM. Local Open Scope ereal_scope. Context d (T : sigmaRingType d) (R : realType). @@ -451,6 +467,25 @@ Notation "\int [ mu ]_ x f" := ((integral mu setT (fun x => f)%E))%E : ereal_scope. Arguments eq_integral {d T R mu D} g. +Section ge0_le_measure_integral. +Local Open Scope ereal_scope. +Context {d} {T : measurableType d} {R : realType}. +Variables m1 m2 : {measure set T -> \bar R}. +Hypothesis m12 : forall S, measurable S -> m1 S <= m2 S. + +Import HBNNSimple. + +Lemma ge0_le_measure_integral (f : T -> \bar R) S : measurable S -> + (forall x, 0 <= f x) -> measurable_fun [set: T] f -> + \int[m1]_(x in S) f x <= \int[m2]_(x in S) f x. +Proof. +move=> ms f0 mf; rewrite !ge0_integralE //= ub_ereal_sup// => _ [h/= hfS] <-. +by apply: ereal_sup_ge; exists (sintegral m2 h); + [exists h|exact: le_measure_sintegral]. +Qed. + +End ge0_le_measure_integral. + Section integral_indic. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index 4c36d34243..65dabf3217 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -1648,35 +1648,3 @@ exact: ge0_nondecreasing_set_cvg_integral. Qed. End le0_nondecreasing_set_cvg_integral. - -Section ge0_integral_le_measure. -Local Open Scope ereal_scope. -Local Open Scope classical_set_scope. -Context {d} {T : measurableType d} [R : realType]. -Variables (mu1 mu2 : measure T R). -Hypothesis (Hml : (forall S, measurable S -> mu1 S <= mu2 S)). - -Import HBNNSimple. - -Lemma sintegral_le_measure (h : {nnsfun T >-> R}): - sintegral mu1 h <= sintegral mu2 h. -Proof. -rewrite !sintegralE /=. -apply/ lee_fsum => // i [a Ha <-]. -apply: lee_pmul => //; first by apply/ lee_tofin. -by apply: Hml. -Qed. - -Lemma ge0_integral_le_measure (f : T -> \bar R) S (Hms: measurable S): - (forall x, 0 <= f x) -> - measurable_fun setT f -> - (\int[mu1]_(x in S) f x <= \int[mu2]_(x in S) f x). -Proof. -move=> Hf0 Hfm. -rewrite !ge0_integralE //=. -apply: ub_ereal_sup => x [h Hh] /= <-. -apply: ereal_sup_ge; exists (sintegral mu2 h) => //=; first by eexists. -by apply: sintegral_le_measure. -Qed. - -End ge0_integral_le_measure. \ No newline at end of file