From aa5c927f88f7b84a7e4d442702847404d5472bcf Mon Sep 17 00:00:00 2001 From: Yosuke-Ito-345 Date: Mon, 15 Dec 2025 20:57:05 +0900 Subject: [PATCH 1/3] generalize lemma null_set_integral --- CHANGELOG_UNRELEASED.md | 3 +++ .../lebesgue_integrable.v | 15 +++++++++++++++ 2 files changed, 18 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 606bd3a17c..456de89994 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -44,6 +44,9 @@ + definition `product_subprobability` + lemma `product_subprobability_setC` +- in `lebesgue_integral_theory/lebesgue_integrable.v` + + lemmas `null_set_integrable`, `null_set_integral_gen` + - new file `lebesgue_integral_theory/giry.v` + definition `measure_eq` + definition `giry` diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index 816623aa8d..585768a6b9 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -818,6 +818,21 @@ Proof. by move=> mN intf ?; rewrite (negligible_integral mN mN)// setDv integral_set0. Qed. +Lemma null_set_integrable (N : set T) (f : T -> \bar R) : + measurable N -> measurable_fun N f -> mu N = 0 -> mu.-integrable N f. +Proof. +move=> mN mf muN0. +rewrite (negligible_integrable(N:=N)) ?setDv //=. +by apply: (eq_integrable measurable0 (cst 0%R)) + => [x|]; [rewrite inE | exact: integrable0]. +Qed. + +Lemma null_set_integral_gen (N : set T) (f : T -> \bar R) : + measurable N -> measurable_fun N f -> mu N = 0 -> \int[mu]_(x in N) f x = 0. +Proof. +by move=> *; apply: null_set_integral; [| exact: null_set_integrable |]. +Qed. + End negligible_integral. Add Search Blacklist "ge0_negligible_integral". From 6f4560138aac93a890c759b4c2db68c6b625c5b4 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 16 Dec 2025 14:24:14 +0900 Subject: [PATCH 2/3] replace lemma by its generalization --- CHANGELOG_UNRELEASED.md | 4 +++- theories/charge.v | 3 ++- .../lebesgue_integral_theory/lebesgue_integrable.v | 13 ++++--------- theories/probability.v | 4 ++-- 4 files changed, 11 insertions(+), 13 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 456de89994..b659bedde2 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -45,7 +45,7 @@ + lemma `product_subprobability_setC` - in `lebesgue_integral_theory/lebesgue_integrable.v` - + lemmas `null_set_integrable`, `null_set_integral_gen` + + lemma `null_set_integrable` - new file `lebesgue_integral_theory/giry.v` + definition `measure_eq` @@ -121,6 +121,8 @@ `integration_by_substitution_onem`, `Rintegration_by_substitution_onem` +- in `lebesgue_integral_theory/lebesgue_integrable.v` + + lemma `null_set_integral` ### Deprecated diff --git a/theories/charge.v b/theories/charge.v index 9a0794264f..2b4c9a09cc 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1260,7 +1260,8 @@ rewrite (le_trans (le_abse_integral _ _ _))//=. by case/integrableP : intnf => /= + _; exact: measurable_funTS. rewrite le_eqVlt; apply/orP; left; apply/eqP. under eq_integral do rewrite abse_id. -by apply: null_set_integral => //=; exact: integrableS intnf. +apply: null_set_integral => //=. +by apply: measurable_funTS; apply: measurable_int intnf. Qed. End dominates_induced. diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index 585768a6b9..aef6bc3d0a 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -811,13 +811,6 @@ congr (_ - _); apply: ge0_negligible_integral => //; apply: (measurable_int mu). exact: integrable_funeneg. Qed. -Lemma null_set_integral (N : set T) (f : T -> \bar R) : - measurable N -> mu.-integrable N f -> - mu N = 0 -> \int[mu]_(x in N) f x = 0. -Proof. -by move=> mN intf ?; rewrite (negligible_integral mN mN)// setDv integral_set0. -Qed. - Lemma null_set_integrable (N : set T) (f : T -> \bar R) : measurable N -> measurable_fun N f -> mu N = 0 -> mu.-integrable N f. Proof. @@ -827,10 +820,12 @@ by apply: (eq_integrable measurable0 (cst 0%R)) => [x|]; [rewrite inE | exact: integrable0]. Qed. -Lemma null_set_integral_gen (N : set T) (f : T -> \bar R) : +Lemma null_set_integral (N : set T) (f : T -> \bar R) : measurable N -> measurable_fun N f -> mu N = 0 -> \int[mu]_(x in N) f x = 0. Proof. -by move=> *; apply: null_set_integral; [| exact: null_set_integrable |]. +move=> mN mf N0. +rewrite (negligible_integral mN mN) ?setDv ?integral_set0//. +exact: null_set_integrable. Qed. End negligible_integral. diff --git a/theories/probability.v b/theories/probability.v index 1f9c02b6e7..0c87621819 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -1876,8 +1876,8 @@ Lemma normal_prob_dominates : normal_prob `<< mu. Proof. apply/null_content_dominatesP=> A mA muA0; rewrite /normal_prob /normal_pdf. have [s0|s0] := eqVneq sigma 0. - apply: null_set_integral => //=; apply: (integrableS measurableT) => //=. - exact: integrable_indic_itv. + apply: null_set_integral => //=; apply: measurable_funTS => /=. + exact/measurable_EFinP/measurable_indic. apply/eqP; rewrite eq_le; apply/andP; split; last first. apply: integral_ge0 => x _. by rewrite lee_fin mulr_ge0 ?normal_peak_ge0 ?normal_fun_ge0. From 99a8910d9f8a302511006eae454caf66a2ee104a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 16 Dec 2025 14:37:26 +0900 Subject: [PATCH 3/3] integrable_set0 --- CHANGELOG_UNRELEASED.md | 3 +++ .../lebesgue_integral_theory/lebesgue_integrable.v | 10 +++++++--- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b659bedde2..3cd6b6edc3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -75,6 +75,9 @@ - in `subspace_topology.v`: + definition `from_subspace` +- in `lebesgue_integrable.v`: + + lemma `integrable_set0` + ### Changed - in `charge.v`: diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index aef6bc3d0a..5db7d85fbe 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -135,6 +135,12 @@ apply/integrableP; split=> //; under eq_integral do rewrite (gee0_abs (lexx 0)). by rewrite integral0. Qed. +Lemma integrable_set0 f : mu.-integrable set0 f. +Proof. +apply/integrableP; split; first exact: measurable_fun_set0. +by rewrite integral_set0. +Qed. + Lemma eq_integrable f g : {in D, f =1 g} -> mu_int f -> mu_int g. Proof. move=> fg /integrableP[mf fi]; apply/integrableP; split. @@ -815,9 +821,7 @@ Lemma null_set_integrable (N : set T) (f : T -> \bar R) : measurable N -> measurable_fun N f -> mu N = 0 -> mu.-integrable N f. Proof. move=> mN mf muN0. -rewrite (negligible_integrable(N:=N)) ?setDv //=. -by apply: (eq_integrable measurable0 (cst 0%R)) - => [x|]; [rewrite inE | exact: integrable0]. +by rewrite (negligible_integrable mN) ?setDv//; exact: integrable_set0. Qed. Lemma null_set_integral (N : set T) (f : T -> \bar R) :