From 017af921f7aae1e38546dadceaaf8ac402fd61be Mon Sep 17 00:00:00 2001 From: Yosuke-Ito-345 Date: Sun, 15 Feb 2026 15:15:43 +0900 Subject: [PATCH 1/9] add lemma le0_expectation_cdf --- CHANGELOG_UNRELEASED_new.md | 19 ++ .../lebesgue_integral_nonneg.v | 32 +++ theories/measurable_realfun.v | 7 + theories/probability_theory/random_variable.v | 248 +++++++++++++----- 4 files changed, 241 insertions(+), 65 deletions(-) create mode 100644 CHANGELOG_UNRELEASED_new.md diff --git a/CHANGELOG_UNRELEASED_new.md b/CHANGELOG_UNRELEASED_new.md new file mode 100644 index 0000000000..7b2c00c7a9 --- /dev/null +++ b/CHANGELOG_UNRELEASED_new.md @@ -0,0 +1,19 @@ +# Changelog (unreleased) + +## [Unreleased] + +### Added + +- in lebesgue_integral_nonneg.v + + lemmas `lebesgue_measure_oppr`, `ge0_integral_oppr` + +- in measurable_realfun.v + + lemma `min_mfun_subproof` + + definition `min_mfun` + +- in random_variable.v + + lemmas `lebesgue_integral_pmf`, `cdf_measurable`, `ccdf_measurable`, `ge0_expectation_prob_ge`, `le0_expectation_cdf` + + + + diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index a6ad41e9fb..0a3abe4a63 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -568,6 +568,38 @@ Qed. End ge0_transfer. +Section change_of_variable. +Open Scope ereal_scope. +Context {R : realType}. + +Let mu : {measure set _ -> \bar R} := @lebesgue_measure R. + +Lemma lebesgue_measure_oppr A (mA : measurable A) : + pushforward(T2 := measurableTypeR R) mu -%R A = mu A. +Proof. +apply /esym/lebesgue_stieltjes_measure_unique => //= _ [[a b]] _ <-. +rewrite /lebesgue_stieltjes_measure/measure_extension. +rewrite measurable_mu_extE /pushforward/preimage/=; last exact: is_ocitv. +have ->: [set r | (-r)%R \in `]a, b]] = `[(-b)%R, (-a)%R[%classic. + by apply: eq_set => r; rewrite oppr_itvoc. +rewrite lebesgue_measure_itv/= lte_fin ltrN2. +have [ab | ba] := (ltP a b). +- by rewrite wlength_itv_bnd ?ltW// opprK EFinD addeC. +- by rewrite set_itv_ge ?wlength0// bnd_simp -leNgt. +Qed. + +Lemma ge0_integral_oppr (f : R -> \bar R) + (mf : measurable_fun setT f) (ge0 : forall r, 0 <= f r) : + \int[mu]_(r in `[0%R, +oo[) f r = \int[mu]_(r in `]-oo, 0%R]) f (- r)%R. +Proof. +rewrite (eq_measure_integral (pushforward(T2 := measurableTypeR R) mu -%R)) + => [| A mA /=]; rewrite ?lebesgue_measure_oppr//. +rewrite ge0_integral_pushforward //; last exact: measurable_funS mf. +by congr integral; apply: eq_set => r/=; rewrite !in_itv/= oppr_ge0 andbT. +Qed. + +End change_of_variable. + Section integral_dirac. Local Open Scope ereal_scope. Context d (T : measurableType d) (a : T) (R : realType). diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 7f0d773d3b..771278d1b3 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -1182,6 +1182,13 @@ HB.instance Definition _ f g := max_mfun_subproof f g. Definition max_mfun f g : {mfun aT >-> _} := f \max g. +Lemma min_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \min g). +Proof. by split; apply: measurable_minr. Qed. + +HB.instance Definition _ f g := min_mfun_subproof f g. + +Definition min_mfun f g : {mfun aT >-> _} := f \min g. + End ring. Arguments indic_mfun {d aT rT} _. (* TODO: move earlier?*) diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index 992f0e1272..ba487747cc 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -136,6 +136,107 @@ Proof. by move=> mf intf; rewrite integral_pushforward. Qed. End transfer_probability. +Section pmf_definition. +Context {d} {T : measurableType d} {R : realType}. +Variables (P : probability T R). + +Definition pmf (X : {RV P >-> R}) (r : R) : R := fine (P (X @^-1` [set r])). + +Lemma pmf_ge0 (X : {RV P >-> R}) (r : R) : 0 <= pmf X r. +Proof. by rewrite fine_ge0. Qed. + +End pmf_definition. + +Section pmf_measurable. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) + (P : probability T R) (X : {RV P >-> R}). + +Lemma pmf_gt0_countable : countable [set r | 0 < pmf X r]%R. +Proof. +rewrite [X in countable X](_ : _ = + \bigcup_n [set r | n.+1%:R^-1 < pmf X r]%R); last first. + by apply/seteqP; split=> [r/= /ltr_add_invr[k /[!add0r] kXr]|r/= [k _]]; + [exists k|exact: lt_trans]. +apply: bigcup_countable => // n _; apply: finite_set_countable. +apply: contrapT => /infiniteP/pcard_leP/injfunPex[/= q q_fun q_inj]. +have /(probability_le1 P) : measurable (\bigcup_k X @^-1` [set q k]). + by apply: bigcup_measurable => k _; exact: measurable_funPTI. +rewrite leNgt => /negP; apply. +rewrite [ltRHS](_ : _ = \sum_(0 <= k // i; rewrite in_setT. + rewrite (trivIset_comp (fun r => X@^-1` [set r]))//. + exact: trivIset_preimage1. +apply: (lt_le_trans _ (nneseries_lim_ge n.+1 _)) => //. +rewrite -EFin_sum_fine//; last by move=> ? _; rewrite fin_num_measure. +under eq_bigr do rewrite -/(pmf X (q _)). +rewrite lte_fin (_ : 1%R = (\sum_(0 <= k < n.+1) n.+1%:R^-1:R)%R); last first. + by rewrite sumr_const_nat subn0 -[RHS]mulr_natr mulVf. +by apply: ltr_sum => // k _; exact: q_fun. +Qed. + +Lemma pmf_measurable : measurable_fun [set: R] (pmf X). +Proof. +have /countable_bijP[S] := pmf_gt0_countable. +rewrite card_eq_sym => /pcard_eqP/bijPex[/= h h_bij]. +have pmf1_ge0 k s : 0 <= (pmf X (h k) * \1_[set h k] s)%:E. + by rewrite EFinM mule_ge0// lee_fin pmf_ge0. +pose sfun r := \sum_(0 <= k [r _|]; last first. + by apply: ge0_emeasurable_sum => // *; exact/measurable_EFinP/measurable_funM. +have [rS|nrS] := boolP (r \in [set h k | k in S]). +- pose kr := pinv S h r. + have neqh k : k \in S /\ k != kr -> r != h k. + move=> [Sk]; apply: contra_neq. + by rewrite /kr => ->; rewrite pinvKV//; exact: (set_bij_inj h_bij). + rewrite /sfun (@nneseriesD1 _ _ kr)//; last by rewrite inE; exact/invS/set_mem. + by rewrite eseries0 => [| k k_ge0 /andP/neqh]; rewrite indicE in_set1_eq; + [rewrite pinvK// eqxx mulr1 addr0|move/negPf => ->; rewrite mulr0]. +- rewrite /sfun eseries0 => [|k k_ge0 Sk]/=. + apply: le_anti; rewrite !lee_fin pmf_ge0/= leNgt; apply: contraNN nrS. + by rewrite (surj_image_eq _ (set_bij_surj h_bij)) ?inE//; exact:set_bij_sub. + rewrite indicE in_set1_eq (_ : (r == h k) = false) ?mulr0//. + by apply: contraNF nrS => /eqP ->; exact/image_f. +Qed. + +End pmf_measurable. + +Section lebesgue_integral_pmf. +Context d (T : measurableType d) (R : realType) + (P : probability T R) (X : {RV P >-> R}). +Local Open Scope ereal_scope. + +Lemma lebesgue_integral_pmf : + \int[lebesgue_measure]_r (pmf X r)%:E = 0. +Proof. +pose mu := @lebesgue_measure R. +pose pmfP := [set r | (0 < pmf X r)%R]. +pose pmf0 := [set r | (0 = pmf X r)%R]. +have Upmf : pmfP `|` pmf0 = setT. + rewrite -subTset => r /= _. + by case: (ltrgt0P (pmf X r)); [left | rewrite ltNge fine_ge0 | right]. +have Ipmf : [disjoint pmfP & pmf0]. + rewrite disj_set2E; apply/eqP. + by rewrite -subset0 setIC /pmfP/pmf0 => r /= [] ->; rewrite ltxx. +have pmf0NP : pmf0 = ~`pmfP. + rewrite /pmf0 /pmfP seteqP; split=> r /= => [-> | /negP]; rewrite ?ltxx//. + by rewrite -real_leNgt//= => pmfN; apply: le_anti; rewrite pmfN fine_ge0. +have cpmfP : countable pmfP by exact: pmf_gt0_countable. +have mpmfP : measurable pmfP by exact: countable_measurable. +have mupmfP : mu pmfP = 0 by exact: countable_lebesgue_measure0. +have mpmf : measurable_fun setT (fun r => (pmf X r)%:E). + by apply/measurable_EFinP; exact: pmf_measurable. +transitivity + (\int[mu]_(r in pmfP) (pmf X r)%:E + \int[mu]_(r in pmf0) (pmf X r)%:E). + by rewrite -ge0_integral_setU ?Upmf// ?pmf0NP => [| r _]; + [exact: measurableC | exact: fine_ge0]. +rewrite (_ : \int[mu]_(r in pmf0) (pmf X r)%:E = 0) ?addr0; + last by apply: integral0_eq => r <-. +by apply: null_set_integral; [| exact: (measurable_funS(E:=setT)) |]. +Qed. + +End lebesgue_integral_pmf. + Definition cdf d (T : measurableType d) (R : realType) (P : probability T R) (X : {RV P >-> R}) (r : R) := distribution P X `]-oo, r]. @@ -151,6 +252,15 @@ Lemma cdf_le1 r : cdf X r <= 1. Proof. exact: probability_le1. Qed. Lemma cdf_nondecreasing : nondecreasing_fun (cdf X). Proof. by move=> r s rs; rewrite le_measure ?inE//; exact: subitvPr. Qed. +Lemma cdf_measurable : measurable_fun setT (cdf X). +Proof. +suff : measurable_fun setT (fine \o (cdf X)) => [/measurable_EFinP |]. + apply: eq_measurable_fun => r _. + by rewrite /comp fineK; last exact: fin_num_measure. +apply: nondecreasing_measurable => // r s rs. +by apply: fine_le; [rewrite fin_num_measure .. | exact: cdf_nondecreasing]. +Qed. + Lemma cvg_cdfy1 : cdf X @ +oo%R --> 1. Proof. pose s : \bar R := ereal_sup (range (cdf X)). @@ -341,6 +451,13 @@ Proof. by rewrite -(cdf_ccdf_1 r) addeK ?fin_num_measure. Qed. Lemma ccdf_nonincreasing : nonincreasing_fun (ccdf X). Proof. by move=> r s rs; rewrite le_measure ?inE//; exact: subitvPl. Qed. +Lemma ccdf_measurable : measurable_fun setT (ccdf X). +Proof. +apply: (eq_measurable_fun (fun r => 1 - cdf X r)) => [r _|]. + by rewrite ccdf_1_cdf. +by apply: emeasurable_funB; last exact: cdf_measurable. +Qed. + Lemma cvg_ccdfy0 : ccdf X @ +oo%R --> 0. Proof. have : 1 - cdf X r @[r --> +oo%R] --> 1 - 1. @@ -519,6 +636,72 @@ rewrite [X in measurable X](_ : _ = fgts @^-1` [set true]). by apply: eq_set => r; rewrite in_itv/= s_ge0. Qed. +Lemma ge0_expectation_prob_ge (X : {RV P >-> R}) : (forall x, 0 <= X x)%R -> + 'E_P[X] = \int[mu]_(r in `[0%R, +oo[) P [set x | (r <= X x)%R]. +Proof. +have gtpre r : [set x | (r < X x)%R] = X @^-1` `]r, +oo[. + by apply: eq_set => x/=; rewrite in_itv andbT. +have mPeqr : measurable_fun setT (fun r => P [set x | X x = r]). + apply: (eq_measurable_fun (EFin \o (pmf X))) => [r |]. + by rewrite /comp fineK ?fin_num_measure. + by apply/measurable_EFinP; exact: pmf_measurable. +have mPgtr : measurable_fun setT (fun r:R => P [set x | (r < X x)%R]). + apply: (eq_measurable_fun (ccdf X)) => [r _|]; rewrite ?gtpre//. + exact: ccdf_measurable. +move=> X_ge0; rewrite ge0_expectation_ccdf//. +transitivity + (\int[mu]_(r in `[0%R, +oo[) (P [set x | X x = r] + P [set x | (r < X x)%R])). + rewrite ge0_integralD//=; [| exact: measurable_funTS ..]. + rewrite (_ : \int[mu]_(r in `[0%R, +oo[) P [set x | X x = r] = 0). + by rewrite add0e; apply: eq_integral => r; rewrite gtpre. + rewrite -(lebesgue_integral_pmf X) integral_mkcond; apply: eq_integral => r _. + rewrite patchE; case/asboolP: (r \in `[0%R, +oo[) => [r_ge0 | r_lt0]. + - by rewrite ifT ?inE// fineK ?fin_num_measure. + - rewrite ifF; [rewrite fineK ?fin_num_measure// | exact: asboolF]. + suff ->: X @^-1` [set r] = set0; first by rewrite measure0. + rewrite -nonemptyPn; apply: contra_not r_lt0. + by case=> x <-; rewrite in_itv/= andbT. +apply: eq_integral =>/= r _; rewrite -measureU. +- congr (P _); rewrite seteqP; split=> x/=; first by case=> [->//|]; exact: ltW. + by rewrite le_eqVlt; case/orP => [/eqP|]; [left | right]. +- by rewrite (_ : [set x | X x = r] = X @^-1` [set r]). +- by rewrite gtpre; exact: (measurable_funPTI X). +- by rewrite -subset0 => x []/= ->; rewrite ltxx. +Qed. + +Lemma le0_expectation_cdf (X : {RV P >-> R}) : (forall x, X x <= 0)%R -> + 'E_P[X] = - \int[mu]_(r in `]-oo, 0%R[) cdf X r. +Proof. +pose Y : {RV P >-> R} := (- X)%R. +pose fPleY r := fine (P [set x | (r <= Y x)%R]). +have mgeY r : d.-measurable [set x | (r <= Y x)%R]. + by rewrite -(setTI (mkset _)); exact: measurable_fun_le. +have mfPleY : measurable_fun setT fPleY. + apply: nonincreasing_measurable => // r s rs. + apply: fine_le; rewrite ?fin_num_measure//. + by apply: le_measure; rewrite ?inE// => x /=; exact: (le_trans rs). +move=> X_le0. +have Y_ge0 x : (0 <= Y x)%R by rewrite oppr_ge0/=. +transitivity (- 'E_P[Y]). + rewrite !expectation_def -integral_ge0N/= => [| x]. + by apply: eq_integral => x _; rewrite opprK. + by rewrite lee_tofin//; exact: Y_ge0. +transitivity (- \int[mu]_(s in `]-oo, 0%R]) P [set x | (- s <= Y x)%R]). + rewrite ge0_expectation_prob_ge ?ge0_integral_oppr//. + by apply: (eq_measurable_fun (fun r:R => (fine (P [set x | (r <= Y x)%R]))%:E)) + => [r _|]; [rewrite fineK ?fin_num_measure | apply/measurable_EFinP]. +transitivity (- \int[mu]_(s in `]-oo, 0%R] `\ 0%R) P [set x | (- s <= Y x)%R]). + congr oppe. + under[LHS] eq_integral => s _ do + rewrite -(@fineK _ (P [set x | (- s <= Y x)%R])) ?fin_num_measure//. + under[RHS] eq_integral => s _ do + rewrite -(@fineK _ (P [set x | (- s <= Y x)%R])) ?fin_num_measure//. + rewrite integral_setD1_EFin//; first exact: measurableD. + by apply: measurable_funTS; exact: (measurableT_comp mfPleY). +rewrite setDitv1r; congr oppe; apply: eq_integral => r _. +by congr (P _); apply: eq_set => x; rewrite lerN2. +Qed. + End tail_expectation_formula. HB.lock Definition covariance {d} {T : measurableType d} {R : realType} @@ -1039,71 +1222,6 @@ Qed. End distribution_dRV. -Section pmf_definition. -Context {d} {T : measurableType d} {R : realType}. -Variables (P : probability T R). - -Definition pmf (X : {RV P >-> R}) (r : R) : R := fine (P (X @^-1` [set r])). - -Lemma pmf_ge0 (X : {RV P >-> R}) (r : R) : 0 <= pmf X r. -Proof. by rewrite fine_ge0. Qed. - -End pmf_definition. - -Section pmf_measurable. -Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) - (P : probability T R) (X : {RV P >-> R}). - -Lemma pmf_gt0_countable : countable [set r | 0 < pmf X r]%R. -Proof. -rewrite [X in countable X](_ : _ = - \bigcup_n [set r | n.+1%:R^-1 < pmf X r]%R); last first. - by apply/seteqP; split=> [r/= /ltr_add_invr[k /[!add0r] kXr]|r/= [k _]]; - [exists k|exact: lt_trans]. -apply: bigcup_countable => // n _; apply: finite_set_countable. -apply: contrapT => /infiniteP/pcard_leP/injfunPex[/= q q_fun q_inj]. -have /(probability_le1 P) : measurable (\bigcup_k X @^-1` [set q k]). - by apply: bigcup_measurable => k _; exact: measurable_funPTI. -rewrite leNgt => /negP; apply. -rewrite [ltRHS](_ : _ = \sum_(0 <= k // i; rewrite in_setT. - rewrite (trivIset_comp (fun r => X@^-1` [set r]))//. - exact: trivIset_preimage1. -apply: (lt_le_trans _ (nneseries_lim_ge n.+1 _)) => //. -rewrite -EFin_sum_fine//; last by move=> ? _; rewrite fin_num_measure. -under eq_bigr do rewrite -/(pmf X (q _)). -rewrite lte_fin (_ : 1%R = (\sum_(0 <= k < n.+1) n.+1%:R^-1:R)%R); last first. - by rewrite sumr_const_nat subn0 -[RHS]mulr_natr mulVf. -by apply: ltr_sum => // k _; exact: q_fun. -Qed. - -Lemma pmf_measurable : measurable_fun [set: R] (pmf X). -Proof. -have /countable_bijP[S] := pmf_gt0_countable. -rewrite card_eq_sym => /pcard_eqP/bijPex[/= h h_bij]. -have pmf1_ge0 k s : 0 <= (pmf X (h k) * \1_[set h k] s)%:E. - by rewrite EFinM mule_ge0// lee_fin pmf_ge0. -pose sfun r := \sum_(0 <= k [r _|]; last first. - by apply: ge0_emeasurable_sum => // *; exact/measurable_EFinP/measurable_funM. -have [rS|nrS] := boolP (r \in [set h k | k in S]). -- pose kr := pinv S h r. - have neqh k : k \in S /\ k != kr -> r != h k. - move=> [Sk]; apply: contra_neq. - by rewrite /kr => ->; rewrite pinvKV//; exact: (set_bij_inj h_bij). - rewrite /sfun (@nneseriesD1 _ _ kr)//; last by rewrite inE; exact/invS/set_mem. - by rewrite eseries0 => [| k k_ge0 /andP/neqh]; rewrite indicE in_set1_eq; - [rewrite pinvK// eqxx mulr1 addr0|move/negPf => ->; rewrite mulr0]. -- rewrite /sfun eseries0 => [|k k_ge0 Sk]/=. - apply: le_anti; rewrite !lee_fin pmf_ge0/= leNgt; apply: contraNN nrS. - by rewrite (surj_image_eq _ (set_bij_surj h_bij)) ?inE//; exact:set_bij_sub. - rewrite indicE in_set1_eq (_ : (r == h k) = false) ?mulr0//. - by apply: contraNF nrS => /eqP ->; exact/image_f. -Qed. - -End pmf_measurable. - Section discrete_distribution. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). From e5092bb0a960c43dff4902c27993d1a8b5c83230 Mon Sep 17 00:00:00 2001 From: Yosuke-Ito-345 Date: Wed, 18 Feb 2026 20:52:21 +0900 Subject: [PATCH 2/9] rename lemmas / add doc --- .../lebesgue_integral_theory/lebesgue_integral_nonneg.v | 6 +++--- theories/measurable_realfun.v | 1 + theories/probability_theory/random_variable.v | 2 +- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index 0a3abe4a63..a84ca5fc48 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -574,7 +574,7 @@ Context {R : realType}. Let mu : {measure set _ -> \bar R} := @lebesgue_measure R. -Lemma lebesgue_measure_oppr A (mA : measurable A) : +Lemma lebesgue_measureN A (mA : measurable A) : pushforward(T2 := measurableTypeR R) mu -%R A = mu A. Proof. apply /esym/lebesgue_stieltjes_measure_unique => //= _ [[a b]] _ <-. @@ -588,12 +588,12 @@ have [ab | ba] := (ltP a b). - by rewrite set_itv_ge ?wlength0// bnd_simp -leNgt. Qed. -Lemma ge0_integral_oppr (f : R -> \bar R) +Lemma ge0_integral_pushforwardN (f : R -> \bar R) (mf : measurable_fun setT f) (ge0 : forall r, 0 <= f r) : \int[mu]_(r in `[0%R, +oo[) f r = \int[mu]_(r in `]-oo, 0%R]) f (- r)%R. Proof. rewrite (eq_measure_integral (pushforward(T2 := measurableTypeR R) mu -%R)) - => [| A mA /=]; rewrite ?lebesgue_measure_oppr//. + => [| A mA /=]; rewrite ?lebesgue_measureN//. rewrite ge0_integral_pushforward //; last exact: measurable_funS mf. by congr integral; apply: eq_set => r/=; rewrite !in_itv/= oppr_ge0 andbT. Qed. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 771278d1b3..ede44a2caa 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -46,6 +46,7 @@ From mathcomp Require Export lebesgue_stieltjes_measure. (* indic_mfun mD := mindic mD *) (* scale_mfun k f := k \o* f *) (* max_mfun f g := f \max g *) +(* min_mfun f g := f \min g *) (* ``` *) (******************************************************************************) diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index ba487747cc..1f326672dc 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -687,7 +687,7 @@ transitivity (- 'E_P[Y]). by apply: eq_integral => x _; rewrite opprK. by rewrite lee_tofin//; exact: Y_ge0. transitivity (- \int[mu]_(s in `]-oo, 0%R]) P [set x | (- s <= Y x)%R]). - rewrite ge0_expectation_prob_ge ?ge0_integral_oppr//. + rewrite ge0_expectation_prob_ge ?ge0_integral_pushforwardN//. by apply: (eq_measurable_fun (fun r:R => (fine (P [set x | (r <= Y x)%R]))%:E)) => [r _|]; [rewrite fineK ?fin_num_measure | apply/measurable_EFinP]. transitivity (- \int[mu]_(s in `]-oo, 0%R] `\ 0%R) P [set x | (- s <= Y x)%R]). From 08065f69aad52545ec60c164f7cb38cb26f83065 Mon Sep 17 00:00:00 2001 From: Yosuke-Ito-345 Date: Thu, 19 Feb 2026 09:01:25 +0900 Subject: [PATCH 3/9] change Lemma to Let --- theories/probability_theory/random_variable.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index 1f326672dc..a6cb2ad54e 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -636,7 +636,7 @@ rewrite [X in measurable X](_ : _ = fgts @^-1` [set true]). by apply: eq_set => r; rewrite in_itv/= s_ge0. Qed. -Lemma ge0_expectation_prob_ge (X : {RV P >-> R}) : (forall x, 0 <= X x)%R -> +Let ge0_expectation_prob_ge (X : {RV P >-> R}) : (forall x, 0 <= X x)%R -> 'E_P[X] = \int[mu]_(r in `[0%R, +oo[) P [set x | (r <= X x)%R]. Proof. have gtpre r : [set x | (r < X x)%R] = X @^-1` `]r, +oo[. From 66397bc6a053c4804fadf0b3cd5cf069f5a9af15 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 21 Feb 2026 20:06:13 +0900 Subject: [PATCH 4/9] linting --- CHANGELOG_UNRELEASED_new.md | 28 +++- classical/set_interval.v | 10 ++ classical/unstable.v | 21 +++ .../lebesgue_integral_nonneg.v | 31 ++--- .../simple_functions.v | 5 - theories/lebesgue_measure.v | 6 + theories/lebesgue_stieltjes_measure.v | 11 +- theories/measurable_realfun.v | 4 +- theories/probability_theory/random_variable.v | 121 ++++++++---------- 9 files changed, 136 insertions(+), 101 deletions(-) diff --git a/CHANGELOG_UNRELEASED_new.md b/CHANGELOG_UNRELEASED_new.md index 7b2c00c7a9..2ff47e896a 100644 --- a/CHANGELOG_UNRELEASED_new.md +++ b/CHANGELOG_UNRELEASED_new.md @@ -4,15 +4,31 @@ ### Added -- in lebesgue_integral_nonneg.v - + lemmas `lebesgue_measure_oppr`, `ge0_integral_oppr` +- in `unstable.v`: + + lemmas `oppr_itvNy`, `oppr_itvy` -- in measurable_realfun.v - + lemma `min_mfun_subproof` +- in `set_interval.v`: + + lemmas `opp_preimage_itvbndy`, `opp_preimage_itvbndbnd` + +- in `lebesgue_measure.v`: + + lemma `lebesgue_measure_unique` + +- in `lebesgue_integral_nonneg.v`: + + lemmas `lebesgue_measureN`, `ge0_integral_pushforwardN` + +- in `measurable_realfun.v`: + definition `min_mfun` -- in random_variable.v - + lemmas `lebesgue_integral_pmf`, `cdf_measurable`, `ccdf_measurable`, `ge0_expectation_prob_ge`, `le0_expectation_cdf` +- in `random_variable.v` + + lemmas `lebesgue_integral_pmf`, `cdf_measurable`, `ccdf_measurable`, + `le0_expectation_cdf` + +### Removed + +- in `measurable_realfun.v`: + + lemma `max_mfun_subproof` (has become a `Let`) +- in `simple_functions.v`: + + definition `max_sfun` diff --git a/classical/set_interval.v b/classical/set_interval.v index 7008aadd0f..3d1c4da994 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -505,6 +505,16 @@ rewrite predeqE => /= r; split => [[{}r + <-]|]. by exists (- r); rewrite ?opprK// !in_itv/= ltrNl ltrNr andbC. Qed. +Lemma opp_preimage_itvbndy (R : numDomainType) ba (a : R) (bb : bool): + -%R @^-1` [set` Interval (BSide ba a) (BInfty _ bb)] = + [set` Interval (BInfty _ (~~ bb)) (BSide (~~ ba) (- a))]. +Proof. by apply/seteqP; split => [x/=|x/=]; rewrite oppr_itvy. Qed. + +Lemma opp_preimage_itvbndbnd (R : numDomainType) ba (a : R) bb (b : R) : + -%R @^-1` [set` Interval (BSide ba a) (BSide bb b)] = + [set` Interval (BSide (~~ bb) (- b)) (BSide (~~ ba) (- a))]. +Proof. by apply/seteqP; split => [x/=|x/=]; rewrite oppr_itv. Qed. + (** lemmas between itv and set-theoretic operations *) Section set_itv_porderType. Variables (d : Order.disp_t) (T : porderType d). diff --git a/classical/unstable.v b/classical/unstable.v index da4e0b8087..a18a730d09 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -37,6 +37,27 @@ Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope ring_scope. +Section IntervalNumDomain. +Variable R : numDomainType. +Implicit Types x : R. + +(* TODO: PR to num_domain.v *) +Lemma oppr_itvNy ba bb (xa xb x : R) : + (- x \in Interval (BInfty _ ba) (BSide bb xb)) = + (x \in Interval (BSide (~~ bb) (- xb)) (BInfty _ (~~ ba))). +Proof. +by rewrite !itv_boundlr /<=%O /= !implybF if_neg lteifNl andbC. +Qed. + +Lemma oppr_itvy ba bb (xa x : R) : + (- x \in Interval (BSide ba xa) (BInfty _ bb)) = + (x \in Interval (BInfty _ (~~ bb)) (BSide (~~ ba) (- xa))). +Proof. +by rewrite !itv_boundlr /<=%O /= !implybF if_neg lteifNr negbK andbC. +Qed. + +End IntervalNumDomain. + Lemma coprime_prodr (I : Type) (r : seq I) (P : {pred I}) (F : I -> nat) (a : I) (l : seq I) : all (coprime (F a)) [seq F i | i <- [seq i <- l | P i]] -> diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index a84ca5fc48..2e2ee36ed9 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -572,30 +572,25 @@ Section change_of_variable. Open Scope ereal_scope. Context {R : realType}. -Let mu : {measure set _ -> \bar R} := @lebesgue_measure R. +Local Notation mu := lebesgue_measure. -Lemma lebesgue_measureN A (mA : measurable A) : - pushforward(T2 := measurableTypeR R) mu -%R A = mu A. +Lemma lebesgue_measureN (A : set R) : measurable A -> + pushforward mu (-%R : _ -> measurableTypeR R) A = mu A. Proof. -apply /esym/lebesgue_stieltjes_measure_unique => //= _ [[a b]] _ <-. -rewrite /lebesgue_stieltjes_measure/measure_extension. -rewrite measurable_mu_extE /pushforward/preimage/=; last exact: is_ocitv. -have ->: [set r | (-r)%R \in `]a, b]] = `[(-b)%R, (-a)%R[%classic. - by apply: eq_set => r; rewrite oppr_itvoc. -rewrite lebesgue_measure_itv/= lte_fin ltrN2. -have [ab | ba] := (ltP a b). -- by rewrite wlength_itv_bnd ?ltW// opprK EFinD addeC. -- by rewrite set_itv_ge ?wlength0// bnd_simp -leNgt. +move=> mA; apply/esym/lebesgue_measure_unique => //= _ [[a b]] _ <-. +rewrite /pushforward opp_preimage_itvbndbnd/= !lebesgue_measure_itv/=. +by rewrite !lte_fin ltrN2 opprK addrC. Qed. -Lemma ge0_integral_pushforwardN (f : R -> \bar R) - (mf : measurable_fun setT f) (ge0 : forall r, 0 <= f r) : +Lemma ge0_integral_pushforwardN (f : R -> \bar R) : + measurable_fun [set: R] f -> (forall r, 0 <= f r) -> \int[mu]_(r in `[0%R, +oo[) f r = \int[mu]_(r in `]-oo, 0%R]) f (- r)%R. Proof. -rewrite (eq_measure_integral (pushforward(T2 := measurableTypeR R) mu -%R)) - => [| A mA /=]; rewrite ?lebesgue_measureN//. -rewrite ge0_integral_pushforward //; last exact: measurable_funS mf. -by congr integral; apply: eq_set => r/=; rewrite !in_itv/= oppr_ge0 andbT. +move=> mf f0; rewrite (_ : `]-oo, 0%R]%classic = + (-%R : _ -> measurableTypeR R) @^-1` `[0%R, +oo[); last first. + by rewrite opp_preimage_itvbndy oppr0. +rewrite -ge0_integral_pushforward//=; last exact: measurable_funS mf. +by apply: eq_measure_integral => //= A mA AS; exact/esym/lebesgue_measureN. Qed. End change_of_variable. diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 4b9e20fe1f..e51f5f88f3 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -33,7 +33,6 @@ From mathcomp Require Import function_spaces. (* {nnsfun T >-> R} == type of non-negative simple functions *) (* indic_sfun mD := mindic _ mD *) (* cst_sfun r == constant simple function *) -(* max_sfun f g := f \max f *) (* cst_nnsfun r == constant simple function *) (* nnsfun0 := cst_nnsfun 0 *) (* add_nnsfun f g := f \+ g *) @@ -210,10 +209,6 @@ Definition indic_sfun (D : set aT) (mD : measurable D) : {sfun aT >-> rT} := HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_sfun k). Definition scale_sfun k f : {sfun aT >-> rT} := k \o* f. -(* NB: already in `measurable_realfun.v` *) -HB.instance Definition _ f g := max_mfun_subproof f g. -Definition max_sfun f g : {sfun aT >-> _} := f \max g. - End ring. Arguments indic_sfun {d aT rT} _. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 1bdafa94af..50b5ccad1a 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -343,6 +343,12 @@ HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R). HB.instance Definition _ (R : realType) := SigmaFiniteMeasure.on (@lebesgue_measure R). +Lemma lebesgue_measure_unique {R : realType} + (mu : {measure set (measurableTypeR R) -> \bar R}) : + (forall X, ocitv X -> lebesgue_measure X = mu X) -> + forall A, measurable A -> lebesgue_measure A = mu A. +Proof. exact: lebesgue_stieltjes_measure_unique. Qed. + Definition completed_lebesgue_measure {R : realType} : set _ -> \bar R := completed_lebesgue_stieltjes_measure idfun. HB.instance Definition _ (R : realType) := diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index 4d3ca1d3a9..d9ae2019c0 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -510,16 +510,17 @@ Definition measurableTypeR (R : realType) := g_sigma_algebraType R.-ocitv.-measurable. Section lebesgue_stieltjes_measure. -Variable R : realType. +Context {R : realType}. +Variable f : cumulative R R. -Lemma lebesgue_stieltjes_measure_unique (f : cumulative R R) +Lemma lebesgue_stieltjes_measure_unique (mu : {measure set (measurableTypeR R) -> \bar R}) : (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) -> - forall X, measurable X -> lebesgue_stieltjes_measure f X = mu X. + forall A, measurable A -> lebesgue_stieltjes_measure f A = mu A. Proof. -move=> muE X mX; apply: measure_extension_unique => //=. +move=> muE A mA; apply: measure_extension_unique => //=. exact: wlength_sigma_finite. -by move=> A mA; rewrite -muE// -measurable_mu_extE. +by move=> X mX; rewrite -muE// -measurable_mu_extE. Qed. End lebesgue_stieltjes_measure. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index ede44a2caa..eedbe7e8a0 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -1176,14 +1176,14 @@ Definition indic_mfun (D : set aT) (mD : measurable D) : {mfun aT >-> rT} := HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst k). Definition scale_mfun k f : {mfun aT >-> rT} := k \o* f. -Lemma max_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \max g). +Let max_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \max g). Proof. by split; apply: measurable_maxr. Qed. HB.instance Definition _ f g := max_mfun_subproof f g. Definition max_mfun f g : {mfun aT >-> _} := f \max g. -Lemma min_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \min g). +Let min_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \min g). Proof. by split; apply: measurable_minr. Qed. HB.instance Definition _ f g := min_mfun_subproof f g. diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index a6cb2ad54e..72f6906604 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -202,37 +202,35 @@ Qed. End pmf_measurable. Section lebesgue_integral_pmf. +Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R) (X : {RV P >-> R}). -Local Open Scope ereal_scope. -Lemma lebesgue_integral_pmf : - \int[lebesgue_measure]_r (pmf X r)%:E = 0. +Local Notation mu := lebesgue_measure. + +Lemma lebesgue_integral_pmf : \int[mu]_r (pmf X r)%:E = 0. Proof. -pose mu := @lebesgue_measure R. -pose pmfP := [set r | (0 < pmf X r)%R]. -pose pmf0 := [set r | (0 = pmf X r)%R]. +pose pmfP := [set r | 0 < pmf X r]%R. +pose pmf0 := [set r | 0 = pmf X r]%R. have Upmf : pmfP `|` pmf0 = setT. rewrite -subTset => r /= _. by case: (ltrgt0P (pmf X r)); [left | rewrite ltNge fine_ge0 | right]. have Ipmf : [disjoint pmfP & pmf0]. rewrite disj_set2E; apply/eqP. - by rewrite -subset0 setIC /pmfP/pmf0 => r /= [] ->; rewrite ltxx. -have pmf0NP : pmf0 = ~`pmfP. + by rewrite -subset0 setIC /pmfP /pmf0 => r /= [] ->; rewrite ltxx. +have pmf0NP : pmf0 = ~` pmfP. rewrite /pmf0 /pmfP seteqP; split=> r /= => [-> | /negP]; rewrite ?ltxx//. - by rewrite -real_leNgt//= => pmfN; apply: le_anti; rewrite pmfN fine_ge0. -have cpmfP : countable pmfP by exact: pmf_gt0_countable. + by rewrite lt_neqAle pmf_ge0 andbT negbK => /eqP. +have cpmfP : countable pmfP := pmf_gt0_countable X. have mpmfP : measurable pmfP by exact: countable_measurable. -have mupmfP : mu pmfP = 0 by exact: countable_lebesgue_measure0. have mpmf : measurable_fun setT (fun r => (pmf X r)%:E). by apply/measurable_EFinP; exact: pmf_measurable. -transitivity - (\int[mu]_(r in pmfP) (pmf X r)%:E + \int[mu]_(r in pmf0) (pmf X r)%:E). - by rewrite -ge0_integral_setU ?Upmf// ?pmf0NP => [| r _]; - [exact: measurableC | exact: fine_ge0]. -rewrite (_ : \int[mu]_(r in pmf0) (pmf X r)%:E = 0) ?addr0; - last by apply: integral0_eq => r <-. -by apply: null_set_integral; [| exact: (measurable_funS(E:=setT)) |]. +rewrite -Upmf ge0_integral_setU ?Upmf//=; last 2 first. + by rewrite pmf0NP; exact: measurableC. + by move=> x _; rewrite lee_fin pmf_ge0. +rewrite [X in _ + X]integral0_eq ?addr0; last by move=> r <-. +apply: null_set_integral => //=; first exact: measurable_funTS. +exact: countable_lebesgue_measure0. Qed. End lebesgue_integral_pmf. @@ -252,13 +250,12 @@ Lemma cdf_le1 r : cdf X r <= 1. Proof. exact: probability_le1. Qed. Lemma cdf_nondecreasing : nondecreasing_fun (cdf X). Proof. by move=> r s rs; rewrite le_measure ?inE//; exact: subitvPr. Qed. -Lemma cdf_measurable : measurable_fun setT (cdf X). +Lemma cdf_measurable : measurable_fun [set: R] (cdf X). Proof. -suff : measurable_fun setT (fine \o (cdf X)) => [/measurable_EFinP |]. - apply: eq_measurable_fun => r _. - by rewrite /comp fineK; last exact: fin_num_measure. -apply: nondecreasing_measurable => // r s rs. -by apply: fine_le; [rewrite fin_num_measure .. | exact: cdf_nondecreasing]. +suff: measurable_fun setT (fine \o cdf X) => [/measurable_EFinP |]. + by apply: eq_measurable_fun => r _/=; rewrite fineK// fin_num_measure. +apply: nondecreasing_measurable => //= r s rs. +by rewrite fine_le ?fin_num_measure// cdf_nondecreasing. Qed. Lemma cvg_cdfy1 : cdf X @ +oo%R --> 1. @@ -451,11 +448,11 @@ Proof. by rewrite -(cdf_ccdf_1 r) addeK ?fin_num_measure. Qed. Lemma ccdf_nonincreasing : nonincreasing_fun (ccdf X). Proof. by move=> r s rs; rewrite le_measure ?inE//; exact: subitvPl. Qed. -Lemma ccdf_measurable : measurable_fun setT (ccdf X). +Lemma ccdf_measurable : measurable_fun [set: R] (ccdf X). Proof. apply: (eq_measurable_fun (fun r => 1 - cdf X r)) => [r _|]. by rewrite ccdf_1_cdf. -by apply: emeasurable_funB; last exact: cdf_measurable. +by apply: emeasurable_funB => //; exact: cdf_measurable. Qed. Lemma cvg_ccdfy0 : ccdf X @ +oo%R --> 0. @@ -637,69 +634,63 @@ by apply: eq_set => r; rewrite in_itv/= s_ge0. Qed. Let ge0_expectation_prob_ge (X : {RV P >-> R}) : (forall x, 0 <= X x)%R -> - 'E_P[X] = \int[mu]_(r in `[0%R, +oo[) P [set x | (r <= X x)%R]. + 'E_P[X] = \int[mu]_(r in `[0%R, +oo[) P (X @^-1` `[r, +oo[). Proof. -have gtpre r : [set x | (r < X x)%R] = X @^-1` `]r, +oo[. - by apply: eq_set => x/=; rewrite in_itv andbT. -have mPeqr : measurable_fun setT (fun r => P [set x | X x = r]). - apply: (eq_measurable_fun (EFin \o (pmf X))) => [r |]. - by rewrite /comp fineK ?fin_num_measure. +have mPeqr : measurable_fun setT (fun r => P (X @^-1` [set r])). + apply: (eq_measurable_fun (EFin \o pmf X)) => [r/= _|]. + by rewrite fineK// fin_num_measure. by apply/measurable_EFinP; exact: pmf_measurable. -have mPgtr : measurable_fun setT (fun r:R => P [set x | (r < X x)%R]). - apply: (eq_measurable_fun (ccdf X)) => [r _|]; rewrite ?gtpre//. +have mPgtr : measurable_fun setT (fun r : R => P (X @^-1` `]r, +oo[)). exact: ccdf_measurable. move=> X_ge0; rewrite ge0_expectation_ccdf//. transitivity - (\int[mu]_(r in `[0%R, +oo[) (P [set x | X x = r] + P [set x | (r < X x)%R])). - rewrite ge0_integralD//=; [| exact: measurable_funTS ..]. - rewrite (_ : \int[mu]_(r in `[0%R, +oo[) P [set x | X x = r] = 0). - by rewrite add0e; apply: eq_integral => r; rewrite gtpre. - rewrite -(lebesgue_integral_pmf X) integral_mkcond; apply: eq_integral => r _. - rewrite patchE; case/asboolP: (r \in `[0%R, +oo[) => [r_ge0 | r_lt0]. + (\int[mu]_(r in `[0%R, +oo[) (P (X @^-1` [set r]) + P (X @^-1` `]r, +oo[))). + rewrite ge0_integralD//=; [|exact: measurable_funTS..]. + rewrite [X in _ = X + _](_ : _ = 0) ?add0e; first exact: eq_integral. + rewrite -(lebesgue_integral_pmf X) integral_mkcond/=. + apply: eq_integral => /= r _. + rewrite patchE; have [r_ge0 | r_lt0] := boolP (r \in `[0%R, +oo[). - by rewrite ifT ?inE// fineK ?fin_num_measure. - - rewrite ifF; [rewrite fineK ?fin_num_measure// | exact: asboolF]. - suff ->: X @^-1` [set r] = set0; first by rewrite measure0. - rewrite -nonemptyPn; apply: contra_not r_lt0. + - rewrite mem_setE (negbTE r_lt0) fineK ?fin_num_measure//. + rewrite (_ : _ @^-1` _ = set0) ?measure0//. + rewrite -nonemptyPn; apply: contraNnot r_lt0. by case=> x <-; rewrite in_itv/= andbT. -apply: eq_integral =>/= r _; rewrite -measureU. -- congr (P _); rewrite seteqP; split=> x/=; first by case=> [->//|]; exact: ltW. - by rewrite le_eqVlt; case/orP => [/eqP|]; [left | right]. -- by rewrite (_ : [set x | X x = r] = X @^-1` [set r]). -- by rewrite gtpre; exact: (measurable_funPTI X). -- by rewrite -subset0 => x []/= ->; rewrite ltxx. +apply: eq_integral =>/= r _; rewrite -measureU//. +- by rewrite -preimage_setU setU1itv. +- exact: measurable_funPTI. +- by rewrite -preimage_setI -subset0 => x/= [->]; rewrite in_itv/= ltxx. Qed. Lemma le0_expectation_cdf (X : {RV P >-> R}) : (forall x, X x <= 0)%R -> 'E_P[X] = - \int[mu]_(r in `]-oo, 0%R[) cdf X r. Proof. pose Y : {RV P >-> R} := (- X)%R. -pose fPleY r := fine (P [set x | (r <= Y x)%R]). -have mgeY r : d.-measurable [set x | (r <= Y x)%R]. - by rewrite -(setTI (mkset _)); exact: measurable_fun_le. +pose fPleY r := fine (P (Y @^-1` `[r, +oo[)). +have mgeY r : d.-measurable (Y @^-1` `[r, +oo[) by exact: measurable_funPTI. have mfPleY : measurable_fun setT fPleY. apply: nonincreasing_measurable => // r s rs. - apply: fine_le; rewrite ?fin_num_measure//. - by apply: le_measure; rewrite ?inE// => x /=; exact: (le_trans rs). + rewrite fine_le ?fin_num_measure ?le_measure ?inE//. + by apply: preimage_subset; apply: subset_itvr; rewrite bnd_simp. move=> X_le0. have Y_ge0 x : (0 <= Y x)%R by rewrite oppr_ge0/=. transitivity (- 'E_P[Y]). - rewrite !expectation_def -integral_ge0N/= => [| x]. + rewrite !expectation_def /Y -integral_ge0N/= => [|x _]. by apply: eq_integral => x _; rewrite opprK. - by rewrite lee_tofin//; exact: Y_ge0. -transitivity (- \int[mu]_(s in `]-oo, 0%R]) P [set x | (- s <= Y x)%R]). + by rewrite lee_fin/= oppr_ge0. +transitivity (- \int[mu]_(s in `]-oo, 0%R]) P (Y @^-1` `[(- s)%R, +oo[)). rewrite ge0_expectation_prob_ge ?ge0_integral_pushforwardN//. - by apply: (eq_measurable_fun (fun r:R => (fine (P [set x | (r <= Y x)%R]))%:E)) + by apply: (eq_measurable_fun (fun r:R => (fine (P (Y @^-1` `[r, +oo[ )))%:E)) => [r _|]; [rewrite fineK ?fin_num_measure | apply/measurable_EFinP]. -transitivity (- \int[mu]_(s in `]-oo, 0%R] `\ 0%R) P [set x | (- s <= Y x)%R]). - congr oppe. +transitivity (- \int[mu]_(s in `]-oo, 0%R] `\ 0%R) P (Y @^-1` `[(- s)%R, +oo[)). + congr -%E. under[LHS] eq_integral => s _ do - rewrite -(@fineK _ (P [set x | (- s <= Y x)%R])) ?fin_num_measure//. + rewrite -(@fineK _ (P (Y @^-1` `[(- s)%R, +oo[))) ?fin_num_measure//. under[RHS] eq_integral => s _ do - rewrite -(@fineK _ (P [set x | (- s <= Y x)%R])) ?fin_num_measure//. + rewrite -(@fineK _ (P (Y @^-1` `[(- s)%R, +oo[))) ?fin_num_measure//. rewrite integral_setD1_EFin//; first exact: measurableD. - by apply: measurable_funTS; exact: (measurableT_comp mfPleY). -rewrite setDitv1r; congr oppe; apply: eq_integral => r _. -by congr (P _); apply: eq_set => x; rewrite lerN2. + exact/measurable_funTS/(measurableT_comp mfPleY). +rewrite setDitv1r; congr -%E; apply: eq_integral => r _. +by rewrite (@comp_preimage _ _ _ _ _ -%R)/= opp_preimage_itvbndy/= opprK. Qed. End tail_expectation_formula. From d589386f85347e215450a43a211706dcc3bd182e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 22 Feb 2026 16:55:01 +0900 Subject: [PATCH 5/9] CI --- theories/probability_theory/random_variable.v | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index 72f6906604..b14f87a7d7 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -626,9 +626,8 @@ apply: eq_integral => s; rewrite /D inE/= in_itv/= andbT => s_ge0. rewrite integral_indic//=. rewrite /ccdf setIT set_itvoy; congr distribution. by apply/funext => r/=; rewrite in_itv/= s_ge0. -pose fgts (r : R) := (s < r)%R. -have : measurable_fun setT fgts by exact: measurable_fun_ltr. -rewrite [X in measurable X](_ : _ = fgts @^-1` [set true]). +have : measurable_fun setT (<%R s) by exact: measurable_fun_ltr. +rewrite [X in measurable X](_ : _ = (<%R s) @^-1` [set true]). by move=> /(_ measurableT [set true]); rewrite setTI; exact. by apply: eq_set => r; rewrite in_itv/= s_ge0. Qed. @@ -648,7 +647,7 @@ transitivity rewrite ge0_integralD//=; [|exact: measurable_funTS..]. rewrite [X in _ = X + _](_ : _ = 0) ?add0e; first exact: eq_integral. rewrite -(lebesgue_integral_pmf X) integral_mkcond/=. - apply: eq_integral => /= r _. + apply: (@eq_integral _ (measurableTypeR R) _ mu setT) => /= r _. rewrite patchE; have [r_ge0 | r_lt0] := boolP (r \in `[0%R, +oo[). - by rewrite ifT ?inE// fineK ?fin_num_measure. - rewrite mem_setE (negbTE r_lt0) fineK ?fin_num_measure//. From f64fb69f26c156ecdce43cfe5c4269626da2cc1b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 22 Feb 2026 21:35:12 +0900 Subject: [PATCH 6/9] CI + minor gen to simp proof --- CHANGELOG_UNRELEASED_new.md | 26 +++ theories/ftc.v | 91 +++++----- .../lebesgue_Rintegral.v | 4 +- .../lebesgue_integral_nonneg.v | 63 ++++--- theories/measurable_realfun.v | 155 ++++++++++-------- theories/probability_theory/random_variable.v | 18 +- 6 files changed, 205 insertions(+), 152 deletions(-) diff --git a/CHANGELOG_UNRELEASED_new.md b/CHANGELOG_UNRELEASED_new.md index 2ff47e896a..cdb5a5470b 100644 --- a/CHANGELOG_UNRELEASED_new.md +++ b/CHANGELOG_UNRELEASED_new.md @@ -23,13 +23,39 @@ + lemmas `lebesgue_integral_pmf`, `cdf_measurable`, `ccdf_measurable`, `le0_expectation_cdf` +- in `lebesgue_integral_nonneg.v`: + + lemma `integral_setU` + +- in `measurable_realfun.v`: + + lemmas `emeasurable_fun_itv_obnd_cbndP`, `emeasurable_fun_itv_bndo_bndcP`, + `emeasurable_fun_itv_cc` + +### Deprecated + +- in `lebesgue_integral_nonneg.v`: + + lemma integral_setU_EFin` + +### Renamed + +- in `lebesgue_integral_nonneg.v`: + + `integral_setD1_EFin` -> `integral_setD1` + +### Generalized + +- in `lebesgue_integral_nonneg.v`: + + lemmas `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd`, + `integral_itv_bndoo` + ### Removed - in `measurable_realfun.v`: + lemma `max_mfun_subproof` (has become a `Let`) + - in `simple_functions.v`: + definition `max_sfun` +- in `lebesgue_integral_nonneg.v`: + + lemma `integral_setU` (was deprecated since version 1.0.1) diff --git a/theories/ftc.v b/theories/ftc.v index b83b6a397f..0f626d1bfe 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -114,20 +114,17 @@ apply: cvg_at_right_left_dnbhs. rewrite (@itv_bndbnd_setU _ _ _ (BLeft x))//=; last 2 first. by case: a ax F => [[|] a|[|]]// /ltW. by rewrite bnd_simp lerDl ltW. - rewrite integral_setU_EFin//=. + rewrite integral_setU//=. - rewrite addeAC -[X in _ - X]integral_itv_bndo_bndc//=; last first. by case: locf => + _ _; exact: measurable_funS. rewrite subee ?add0e//. by apply: integrable_fin_num => //; exact: integrableS intf. - - by case: locf => + _ _; exact: measurable_funS. - - apply/disj_setPRL => z/=. - rewrite /E /= !in_itv/= => /andP[xz zxdn]. + - by case: locf => /measurable_EFinP + _ _; exact: measurable_funS. + - apply/disj_setPRL => z/= zxxdn. move: a ax {F} => [[|] t/=|[_ /=|//]]. - - rewrite lte_fin => tx. - by apply/negP; rewrite negb_and -leNgt xz orbT. - - rewrite lte_fin => tx. - by apply/negP; rewrite negb_and -!leNgt xz orbT. - - by apply/negP; rewrite -leNgt. + - by rewrite lte_fin in_itv/= => tx; rewrite (itvP zxxdn) andbF. + - by rewrite lte_fin in_itv/= => tx; rewrite (itvP zxxdn) andbF. + - by rewrite in_itv/= (itvP zxxdn). rewrite [f in f n @[n --> _] --> _](_ : _ = fun n => (d n)^-1 *: fine (\int[mu]_(t in E x n) (f t)%:E)); last first. apply/funext => n; congr (_ *: _); rewrite -fineB/=. @@ -179,17 +176,15 @@ apply: cvg_at_right_left_dnbhs. rewrite addeC. rewrite (_ : `]-oo, x] = `]-oo, (x + d n)%R] `|` E x n)%classic; last first. by rewrite -itv_bndbnd_setU//= bnd_simp ler_wnDr// ltW. - rewrite integral_setU_EFin//=. - - rewrite addeAC. - rewrite -[X in X - _]integral_itv_bndo_bndc//; last first. + rewrite integral_setU//=. + - rewrite addeAC -[X in X - _]integral_itv_bndo_bndc//; last first. by case: locf => + _ _; exact: measurable_funS. rewrite subee ?add0e//. by apply: integrable_fin_num => //; exact: integrableS intf. - exact: (nice_E _).1. - - by case: locf => + _ _; exact: measurable_funS. - - apply/disj_setPLR => z/=. - rewrite /E /= !in_itv/= leNgt => xdnz. - by apply/negP; rewrite negb_and xdnz. + - by case: locf => /measurable_EFinP + _ _; exact: measurable_funS. + - apply/disj_setPLR => z/= zNyxdn. + by rewrite /E /= !in_itv/= (itvP zNyxdn). move=> b a ax. move/cvgrPdist_le : d0. move/(_ (x - a)%R); rewrite subr_gt0 => /(_ ax)[m _ /=] h. @@ -209,14 +204,14 @@ apply: cvg_at_right_left_dnbhs. rewrite lerBrDl -lerBrDr. by have := h _ mn; rewrite sub0r gtr0_norm. by rewrite opprK bnd_simp -lerBrDl subrr ltW. - rewrite integral_setU_EFin//=. + rewrite integral_setU//=. - rewrite addeAC -[X in X - _]integral_itv_bndo_bndc//; last first. by case: locf => + _ _; exact: measurable_funS. rewrite opprK subee ?add0e//. by apply: integrable_fin_num => //; exact: integrableS intf. - - by case: locf => + _ _; exact: measurable_funS. + - by case: locf => /measurable_EFinP + _ _; exact: measurable_funS. - apply/disj_setPLR => z/=. - rewrite /E /= !in_itv/= => /andP[az zxdn]. + rewrite !in_itv/= => /andP[az zxdn]. by apply/negP; rewrite negb_and -leNgt zxdn. suff: ((d n)^-1 * - fine (\int[mu]_(y in E x n) (f y)%:E))%R @[n --> \oo] --> f x. @@ -446,9 +441,9 @@ have xbab : `]x, b] `<=` `[a, b]. rewrite -addrA subrKC (le_trans (le_normr_Rintegral _ _))//. exact: integrableS intf. rewrite [leLHS](_ : _ = (\int[mu]_(t in `]x, b]) `|fab t|))//; last first. - apply: eq_Rintegral => //= z; rewrite inE/= in_itv/= => /andP[xz zb]. - rewrite /fab patchE ifT// inE/= in_itv/= zb andbT (le_trans _ (ltW xz))//. - by near: x; exact: nbhs_left_ge. + apply: eq_Rintegral => //= z; rewrite inE/= => zxb. + rewrite /fab patchE ifT// inE/=. + by apply: subset_itv (zxb); rewrite bnd_simp// ltW// (itvP zxb). apply/ltW/int_normr_cont => //. rewrite lebesgue_measure_itv/= lte_fin. rewrite ifT// -EFinD lte_fin. @@ -576,8 +571,8 @@ have [k FGk] : exists k : R, {in `]a, b[, (F - G =1 cst k)%R}. have [| |] := @MVT _ (F \- G)%R (F^`() - G^`())%R x y xy. - move=> z zxy; have zab : z \in `]a, b[. move: z zxy; apply: subset_itvW => //. - + by move: xab; rewrite in_itv/= => /andP[/ltW]. - + by move: yab; rewrite in_itv/= => /andP[_ /ltW]. + + by rewrite ltW// (itvP xab). + + by rewrite ltW// (itvP yab). have Fz1 : derivable F z 1. by case: dF => /= + _ _; apply; rewrite inE in zab. have Gz1 : derivable G z 1 by have [|] := G'f z. @@ -587,17 +582,17 @@ have [k FGk] : exists k : R, {in `]a, b[, (F - G =1 cst k)%R}. - apply: derivable_within_continuous => z zxy. apply: derivableB. + case: dF => /= + _ _; apply. - apply: subset_itvSoo zxy => //. - by move: xab; rewrite in_itv/= => /andP[]. - by move: yab; rewrite in_itv/= => /andP[]. - + apply: (G'f _ _).2; apply: subset_itvSoo zxy => //. - by move: xab; rewrite in_itv/= => /andP[]. - by move: yab; rewrite in_itv/= => /andP[]. + apply: subset_itvSoo zxy => //; rewrite bnd_simp. + by rewrite (itvP xab). + by rewrite (itvP yab). + + apply: (G'f _ _).2; apply: subset_itvSoo zxy => //; rewrite bnd_simp. + by rewrite (itvP xab). + by rewrite (itvP yab). - move=> z zxy; rewrite F'G'0. by rewrite /cst/= mul0r => /eqP; rewrite subr_eq0 => /eqP. apply: subset_itvSoo zxy => //=; rewrite bnd_simp. - * by move: xab; rewrite in_itv/= => /andP[/ltW]. - * by move: yab; rewrite in_itv/= => /andP[_ /ltW]. + + by rewrite (itvP xab). + + by rewrite (itvP yab). move=> H; pose c := ((a + b) / 2)%R. exists (F c - G c)%R => u /(H u c); apply. by rewrite in_itv/= midf_lt//= midf_lt. @@ -781,7 +776,7 @@ rewrite (@ge0_continuous_FTC2y (- f)%R (- F)%R _ (- l)%R). - exact: cvgN. - move=> x ax; rewrite derive1E deriveN. by rewrite -derive1E dFE. - by apply: dF; move: ax; rewrite in_itv/= andbT. + by apply: dF; rewrite (itvP ax). Qed. End corollary_FTC1. @@ -879,8 +874,7 @@ Lemma increasing_image_oo F (a b : R) : (a < b)%R -> F @` `]a, b[ `<=` `]F a, F b[. Proof. move=> ab iF ? [x /= xab <-]. -move: xab; rewrite !in_itv/= => /andP[ax xb]. -by apply/andP; split; apply: iF; rewrite // in_itv/= ?lexx !ltW. +by apply/andP; split; apply: iF; rewrite ?(itvP xab)//; exact: subset_itv_oo_cc. Qed. Lemma decreasing_image_oo F (a b : R) : (a < b)%R -> @@ -888,8 +882,7 @@ Lemma decreasing_image_oo F (a b : R) : (a < b)%R -> F @` `]a, b[ `<=` `]F b, F a[. Proof. move=> ab iF ? [x /= xab <-]. -move: xab; rewrite !in_itv/= => /andP[ax xb]. -by apply/andP; split; apply: iF; rewrite // in_itv/= ?lexx !ltW. +by apply/andP; split; apply: iF; rewrite ?(itvP xab)//; exact: subset_itv_oo_cc. Qed. Lemma increasing_cvg_at_right_comp F G a (b : itv_bound R) (l : R) : @@ -1084,7 +1077,7 @@ pose PG x := parameterized_integral mu (F b) x G. have PGFbFa : derivable_oo_LRcontinuous PG (F b) (F a). have [/= dF rF lF] := Fab; split => /=. - move=> x xFbFa /=. - have xFa : (x < F a)%R by move: xFbFa; rewrite in_itv/= => /andP[]. + have xFa : (x < F a)%R. by move: xFbFa; rewrite in_itv/= => /andP[]. apply: (continuous_FTC1 xFa intG _ _).1 => /=. by move: xFbFa; rewrite lte_fin in_itv/= => /andP[]. exact: (within_continuous_continuous _ _ xFbFa). @@ -1405,24 +1398,21 @@ rewrite integration_by_substitution_decreasing. by apply: measurable_funS (mGFNF' n) => //; exact: subset_itv_oo_co. + by apply: measurable_funS (mGFNF' n) => //; exact: subset_itv_oo_co. - by rewrite lerDl. -- move=> x y /=; rewrite !in_itv/= => /andP[ax _] /andP[ay _] yx. - by apply: decrF; rewrite //in_itv/= ?ax ?ay. -- move=> x; rewrite in_itv/= => /andP[ax _]. - by apply: cdF; rewrite in_itv/= ax. +- move=> x y /= xaa yaa yx. + by apply: decrF; rewrite ?in_itv ?andbT/= ?(itvP xaa) ?(itvP yaa). +- by move=> x xaa; apply: cdF; rewrite in_itv/= (itvP xaa). - exact: (cvgP dFa). - apply: (cvgP (F^`() (a + n.+1%:R))); apply/cvg_at_left_filter/cdF. by rewrite in_itv/= andbT ltr_pwDr. - split. - + move=> x; rewrite in_itv/= => /andP[ax _]. - by apply: dF; rewrite in_itv/= ax. + + by move=> x xaa; apply: dF; rewrite in_itv/= (itvP xaa). + exact: cFa. + apply/cvg_at_left_filter/differentiable_continuous/derivable1_diffP/dF. by rewrite in_itv/= andbT ltr_pwDr. - apply/continuous_within_itvP. + by rewrite decrF ?ltr_pwDr ?in_itv ?andbT//= lerDl. + split. - * move=> y; rewrite in_itv/= => /andP[_ yFa]. - by apply: cG; rewrite in_itv/= yFa. + * by move=> y yFaFa; apply: cG; rewrite in_itv/= (itvP yFaFa). * apply/cvg_at_right_filter/cG. by rewrite in_itv/= decrF ?in_itv/= ?andbT ?lerDl// ltr_pwDr. * exact: cGFa. @@ -1511,8 +1501,8 @@ rewrite (@decreasing_ge0_integration_by_substitutiony (- F)%R); first last. - by move=> x y ax ay yx; rewrite ltrN2; exact: incrF. have mGF : measurable_fun `]a, +oo[ (G \o F). apply: (@measurable_comp _ _ _ _ _ _ `]F a, +oo[%classic) => //. - - move=> /= _ [x] /[!in_itv]/= /andP[ax xb] <-. - by rewrite incrF ?incrF// in_itv/= ?lexx/= ?(ltW ab)//= ?(ltW ax) ?(ltW xb). + - move=> /= _ [x] xab <-. + by rewrite in_itv/= incrF ?incrF ?in_itv/= ?lexx//= (itvP xab). - apply: open_continuous_measurable_fun; first exact: interval_open. by move=> x; rewrite inE/= => Fax; exact: cG. - apply: subspace_continuous_measurable_fun => //. @@ -1536,9 +1526,8 @@ rewrite -!integral_itv_obnd_cbnd; last 2 first. by move=> x; rewrite inE/=; exact: cF'. apply: measurable_funM; last exact: measurableT_comp. apply: (measurable_comp (measurable_itv `]-oo, (- F a)%R[)). - - move=> _ /= [x + <-]. - rewrite !in_itv/= andbT=> ax. - by rewrite ltrN2 incrF// ?in_itv/= ?andbT// ltW. + - move=> _ /= [x + <-] => ax. + by rewrite in_itv/= ltrN2 incrF ?in_itv/= ?lexx//= (itvP ax). - apply: open_continuous_measurable_fun; first exact: interval_open. by move=> x; rewrite inE/=; exact: cGN. - apply: measurableT_comp => //. diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v index 5f0fe74e9e..4da1e92903 100644 --- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v +++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v @@ -206,7 +206,7 @@ Lemma Rintegral_itv_bndo_bndc (a : itv_bound R) (r : R) f : \int[mu]_(x in [set` Interval a (BRight r)]) (f x). Proof. move=> mf; rewrite /Rintegral integral_itv_bndo_bndc//. -by apply/measurable_EFinP; exact: (measurable_int mu). +exact: (measurable_int mu). Qed. Lemma Rintegral_itv_obnd_cbnd (r : R) (b : itv_bound R) f : @@ -215,7 +215,7 @@ Lemma Rintegral_itv_obnd_cbnd (r : R) (b : itv_bound R) f : \int[mu]_(x in [set` Interval (BLeft r) b]) (f x). Proof. move=> mf; rewrite /Rintegral integral_itv_obnd_cbnd//. -by apply/measurable_EFinP; exact: (measurable_int mu). +exact: (measurable_int mu). Qed. Lemma Rintegral_set1 f (r : R) : \int[mu]_(x in [set r]) f x = 0. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index 2e2ee36ed9..feb15c790e 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -934,25 +934,23 @@ by apply: ge0_subset_integral => //; exact: measurableT_comp. Qed. End subset_integral. -#[deprecated(since="mathcomp-analysis 1.0.1", note="use `ge0_integral_setU` instead")] -Notation integral_setU := ge0_integral_setU (only parsing). Section integral_setU_EFin. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}). -Lemma integral_setU_EFin (A B : set T) (f : T -> R) : +Lemma integral_setU (A B : set T) (f : T -> \bar R) : measurable A -> measurable B -> measurable_fun (A `|` B) f -> [disjoint A & B] -> - \int[mu]_(x in (A `|` B)) (f x)%:E = \int[mu]_(x in A) (f x)%:E + - \int[mu]_(x in B) (f x)%:E. + \int[mu]_(x in (A `|` B)) f x = \int[mu]_(x in A) f x + + \int[mu]_(x in B) f x. Proof. move=> mA mB ABf AB. rewrite integralE/=. -rewrite ge0_integral_setU//; last exact/measurable_funepos/measurable_EFinP. -rewrite ge0_integral_setU//; last exact/measurable_funeneg/measurable_EFinP. +rewrite ge0_integral_setU//; last exact/measurable_funepos. +rewrite ge0_integral_setU//; last exact/measurable_funeneg. rewrite [X in _ = X + _]integralE/=. rewrite [X in _ = _ + X]integralE/=. set ap : \bar R := \int[mu]_(x in A) _; set an : \bar R := \int[mu]_(x in A) _. @@ -961,6 +959,16 @@ rewrite oppeD 1?addeACA//. by rewrite ge0_adde_def// inE integral_ge0. Qed. +Lemma __deprecated__integral_setU_EFin (A B : set T) (f : T -> R) : + measurable A -> measurable B -> + measurable_fun (A `|` B) f -> + [disjoint A & B] -> + \int[mu]_(x in (A `|` B)) (f x)%:E = \int[mu]_(x in A) (f x)%:E + + \int[mu]_(x in B) (f x)%:E. +Proof. +by move=> mA mB ABf AB; apply: integral_setU => //; exact/measurable_EFinP. +Qed. + Lemma integral_bigsetU_EFin (I : eqType) (F : I -> set T) (f : T -> R) (s : seq I) : (forall i, d.-measurable (F i)) -> @@ -971,7 +979,7 @@ Lemma integral_bigsetU_EFin (I : eqType) (F : I -> set T) (f : T -> R) Proof. move=> mF; elim: s => [|h t ih] us tF D mf. by rewrite /D 2!big_nil integral_set0. -rewrite /D big_cons integral_setU_EFin//. +rewrite /D big_cons __deprecated__integral_setU_EFin//. - rewrite big_cons ih//. + by move: us => /= /andP[]. + by apply: sub_trivIset tF => /= i /= it; rewrite inE it orbT. @@ -986,6 +994,8 @@ rewrite /D big_cons integral_setU_EFin//. Qed. End integral_setU_EFin. +#[deprecated(since="mathcomp-analysis 1.16.0", note="use `integral_setU instead`")] +Notation integral_setU_EFin := __deprecated__integral_setU_EFin (only parsing). Section ge0_integral_bigcup. Local Open Scope ereal_scope. @@ -1520,41 +1530,41 @@ rewrite ge0_integral_setU//=. - by apply/disj_setPRL => x /[swap] ->; rewrite /ball/= subKr gtr0_norm// ltxx. Qed. -Lemma integral_setD1_EFin (f : R -> R) r (D : set R) : +Lemma integral_setD1 (f : R -> \bar R) r (D : set R) : measurable (D `\ r) -> measurable_fun (D `\ r) f -> - \int[mu]_(x in D `\ r) (f x)%:E = \int[mu]_(x in D) (f x)%:E. + \int[mu]_(x in D `\ r) f x = \int[mu]_(x in D) f x. Proof. move=> mD mfl; have [Dr|NDr] := pselect (D r); last by rewrite not_setD1. -rewrite -[in RHS](@setD1K _ r D)// integral_setU_EFin//=. +rewrite -[in RHS](@setD1K _ r D)// integral_setU//=. - by rewrite integral_set1// add0e. - by apply/measurable_funU => //; split => //; exact: measurable_fun_set1. - by rewrite disj_set2E setDIK. Qed. -Lemma integral_itv_bndo_bndc (a : itv_bound R) (r : R) (f : R -> R) : +Lemma integral_itv_bndo_bndc (a : itv_bound R) (r : R) (f : R -> \bar R) : measurable_fun [set` Interval a (BLeft r)] f -> - \int[mu]_(x in [set` Interval a (BLeft r)]) (f x)%:E = - \int[mu]_(x in [set` Interval a (BRight r)]) (f x)%:E. + \int[mu]_(x in [set` Interval a (BLeft r)]) f x = + \int[mu]_(x in [set` Interval a (BRight r)]) f x. Proof. move=> mf; have [ar|ar] := leP a (BLeft r). -- by rewrite -[RHS](@integral_setD1_EFin _ r) ?setDitv1r. +- by rewrite -[RHS](@integral_setD1 _ r) ?setDitv1r. - by rewrite !set_itv_ge// -leNgt// ltW. Qed. -Lemma integral_itv_obnd_cbnd (r : R) (b : itv_bound R) (f : R -> R) : +Lemma integral_itv_obnd_cbnd (r : R) (b : itv_bound R) (f : R -> \bar R) : measurable_fun [set` Interval (BRight r) b] f -> - \int[mu]_(x in [set` Interval (BRight r) b]) (f x)%:E = - \int[mu]_(x in [set` Interval (BLeft r) b]) (f x)%:E. + \int[mu]_(x in [set` Interval (BRight r) b]) f x = + \int[mu]_(x in [set` Interval (BLeft r) b]) f x. Proof. move=> mf; have [rb|rb] := leP (BRight r) b. -- by rewrite -[RHS](@integral_setD1_EFin _ r) ?setDitv1l. +- by rewrite -[RHS](@integral_setD1 _ r) ?setDitv1l. - by rewrite !set_itv_ge// -leNgt -?ltBRight_leBLeft// ltW. Qed. -Lemma integral_itv_bndoo (x y : R) (f : R -> R) (b0 b1 : bool) : +Lemma integral_itv_bndoo (x y : R) (f : R -> \bar R) (b0 b1 : bool) : measurable_fun `]x, y[ f -> - \int[mu]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (f z)%:E = - \int[mu]_(z in `]x, y[) (f z)%:E. + \int[mu]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) f z = + \int[mu]_(z in `]x, y[) f z. Proof. have [xy|yx _|-> _] := ltgtP x y; last 2 first. - rewrite !set_itv_ge ?integral_set0//=. @@ -1562,9 +1572,9 @@ have [xy|yx _|-> _] := ltgtP x y; last 2 first. + by move: b0 b1 => [|] [|]; rewrite bnd_simp ?lt_geF// le_gtF// ltW. - by move: b0 b1 => [|] [|]; rewrite !set_itvE ?integral_set0 ?integral_set1. move=> mf. -transitivity (\int[mu]_(z in [set` Interval (BSide b0 x) (BLeft y)]) (f z)%:E). +transitivity (\int[mu]_(z in [set` Interval (BSide b0 x) (BLeft y)]) f z). case: b1 => //; rewrite -integral_itv_bndo_bndc//. - by case: b0 => //; exact/measurable_fun_itv_obnd_cbndP. + by case: b0 => //; exact/emeasurable_fun_itv_obnd_cbndP. by case: b0 => //; rewrite -integral_itv_obnd_cbnd. Qed. @@ -1575,12 +1585,15 @@ Lemma eq_integral_itv_bounded (x y : R) (g f : R -> R) (b0 b1 : bool) : \int[mu]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (g z)%:E. Proof. move=> mf mg fg. -rewrite integral_itv_bndoo// (@integral_itv_bndoo _ _ g)//. +rewrite integral_itv_bndoo//; last exact/measurable_EFinP. +rewrite (@integral_itv_bndoo _ _ (EFin \o g))//; last exact/measurable_EFinP. by apply: eq_integral => z; rewrite inE/= => zxy; congr EFin; exact: fg. Qed. End lebesgue_measure_integral. Arguments integral_Sset1 {R f A} r. +#[deprecated(since="mathcomp-analysis 1.16.0", note="renamed_to `integral_setD1`")] +Notation integral_setD1_EFin := integral_setD1 (only parsing). Section ge0_nondecreasing_set_cvg_integral. Context {d : measure_display} {T : measurableType d} {R : realType}. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index eedbe7e8a0..2ce14c69ee 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -190,70 +190,6 @@ End puncture_ereal_itv. Section salgebra_R_ssets. Variable R : realType. -Lemma measurable_fun_itv_bndo_bndcP (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. -split; [have [ab ?|ab _] := leP a (BLeft b) |have [ab _|ab] := leP (BLeft b) a]. -- rewrite -setUitv1//; apply/measurable_funU => //; split => //. - exact: measurable_fun_set1. -- by rewrite set_itv_ge -?leNgt//; exact: measurable_fun_set0. -- by rewrite set_itv_ge -?leNgt//; exact: measurable_fun_set0. -- by rewrite -setUitv1 ?ltW// => /measurable_funU[]. -Qed. - -Lemma measurable_fun_itv_obnd_cbndP (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. -split; [have [ab mf|ab _] := leP (BRight a) b| - have [ab _|ab] := leP b (BRight a)]. -- rewrite -setU1itv//; apply/measurable_funU => //; split => //. - exact: measurable_fun_set1. -- rewrite set_itv_ge; first exact: measurable_fun_set0. - by rewrite -leNgt; case: b ab => -[]. -- by rewrite set_itv_ge// -?leNgt//; exact: measurable_fun_set0. -- by rewrite -setU1itv ?ltW// => /measurable_funU[]. -Qed. - -#[deprecated(since="mathcomp-analysis 1.9.0", note="use `measurable_fun_itv_obnd_cbnd` instead")] -Lemma measurable_fun_itv_co (x y : R) b0 b1 (f : R -> R) : - measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> - measurable_fun `[x, y[ f. -Proof. -move: b0 b1 => [|] [|]//. -- by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp. -- by move/measurable_fun_itv_obnd_cbndP. -- move=> mf. - have : measurable_fun `[x, y] f by exact/measurable_fun_itv_obnd_cbndP. - by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp. -Qed. - -#[deprecated(since="mathcomp-analysis 1.9.0", note="use `measurable_fun_itv_bndo_bndc` instead")] -Lemma measurable_fun_itv_oc (x y : R) b0 b1 (f : R -> R) : - measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> - measurable_fun `]x, y] f. -Proof. -move: b0 b1 => [|] [|]//. -- move=> mf. - have : measurable_fun `[x, y] f by exact/measurable_fun_itv_bndo_bndcP. - by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp. -- by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp. -- by move/measurable_fun_itv_bndo_bndcP. -Qed. - -Lemma measurable_fun_itv_cc (x y : R) b0 b1 (f : R -> R) : - measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> - measurable_fun `[x, y] f. -Proof. -move: b0 b1 => [|] [|]//. -- by move/measurable_fun_itv_bndo_bndcP. -- move=> mf. - have : measurable_fun `[x, y[ f by exact/measurable_fun_itv_obnd_cbndP. - by move/measurable_fun_itv_bndo_bndcP. -- by move/measurable_fun_itv_obnd_cbndP. -Qed. - HB.instance Definition _ := (ereal_isMeasurable (R.-ocitv.-measurable)). (* NB: Until we dropped support for Coq 8.12, we were using HB.instance (\bar (Real.sort R)) @@ -1462,6 +1398,96 @@ congr (_ `&` _);rewrite eqEsubset; split=> [|? []/= _ /[swap] -[->//]]. by move=> ? ?; exact: preimage_image. Qed. +Section measurable_fun_itvW. +Context {R : realType}. + +Lemma emeasurable_fun_itv_obnd_cbndP (a : R) (b : itv_bound R) (f : R -> \bar R) : + measurable_fun [set` Interval (BRight a) b] f <-> + measurable_fun [set` Interval (BLeft a) b] f. +Proof. +split; [have [ab mf|ab _] := leP (BRight a) b| + have [ab _|ab] := leP b (BRight a)]. +- rewrite -setU1itv//; apply/measurable_funU => //; split => //. + exact: measurable_fun_set1. +- rewrite set_itv_ge; first exact: measurable_fun_set0. + by rewrite -leNgt; case: b ab => -[]. +- by rewrite set_itv_ge// -?leNgt//; exact: measurable_fun_set0. +- by rewrite -setU1itv ?ltW// => /measurable_funU[]. +Qed. + +Lemma measurable_fun_itv_obnd_cbndP (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. +by split => /measurable_EFinP/emeasurable_fun_itv_obnd_cbndP/measurable_EFinP. +Qed. + +Lemma emeasurable_fun_itv_bndo_bndcP (a : itv_bound R) (b : R) (f : R -> \bar R) : + measurable_fun [set` Interval a (BLeft b)] f <-> + measurable_fun [set` Interval a (BRight b)] f. +Proof. +split; [have [ab ?|ab _] := leP a (BLeft b) |have [ab _|ab] := leP (BLeft b) a]. +- rewrite -setUitv1//; apply/measurable_funU => //; split => //. + exact: measurable_fun_set1. +- by rewrite set_itv_ge -?leNgt//; exact: measurable_fun_set0. +- by rewrite set_itv_ge -?leNgt//; exact: measurable_fun_set0. +- by rewrite -setUitv1 ?ltW// => /measurable_funU[]. +Qed. + +Lemma measurable_fun_itv_bndo_bndcP (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. +by split => /measurable_EFinP/emeasurable_fun_itv_bndo_bndcP/measurable_EFinP. +Qed. + +#[deprecated(since="mathcomp-analysis 1.9.0", note="use `measurable_fun_itv_obnd_cbnd` instead")] +Lemma measurable_fun_itv_co (x y : R) b0 b1 (f : R -> R) : + measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> + measurable_fun `[x, y[ f. +Proof. +move: b0 b1 => [|] [|]//. +- by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp. +- by move/measurable_fun_itv_obnd_cbndP. +- move=> mf. + have : measurable_fun `[x, y] f by exact/measurable_fun_itv_obnd_cbndP. + by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp. +Qed. + +#[deprecated(since="mathcomp-analysis 1.9.0", note="use `measurable_fun_itv_bndo_bndc` instead")] +Lemma measurable_fun_itv_oc (x y : R) b0 b1 (f : R -> R) : + measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> + measurable_fun `]x, y] f. +Proof. +move: b0 b1 => [|] [|]//. +- move=> mf. + have : measurable_fun `[x, y] f by exact/measurable_fun_itv_bndo_bndcP. + by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp. +- by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp. +- by move/measurable_fun_itv_bndo_bndcP. +Qed. + +Lemma emeasurable_fun_itv_cc (x y : R) b0 b1 (f : R -> \bar R) : + measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> + measurable_fun `[x, y] f. +Proof. +move: b0 b1 => [|] [|]//. +- by move/emeasurable_fun_itv_bndo_bndcP. +- move=> mf. + have : measurable_fun `[x, y[ f by exact/emeasurable_fun_itv_obnd_cbndP. + by move/emeasurable_fun_itv_bndo_bndcP. +- by move/emeasurable_fun_itv_obnd_cbndP. +Qed. + +Lemma measurable_fun_itv_cc (x y : R) b0 b1 (f : R -> R) : + measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f -> + measurable_fun `[x, y] f. +Proof. +by move=> /measurable_EFinP/emeasurable_fun_itv_cc/measurable_EFinP. +Qed. + +End measurable_fun_itvW. + Lemma measurable_fun_dirac d {T : measurableType d} {R : realType} D (U : set T) : measurable U -> measurable_fun D (fun x => \d_x U : \bar R). @@ -1562,6 +1588,7 @@ apply: (eq_measurable_fun (fun x => limn_esup (f_ ^~ x))) => //. by move=> x; rewrite inE => Dx; rewrite fE. exact: measurable_fun_limn_esup. Qed. + End emeasurable_fun. Arguments emeasurable_fun_cvg {d T R D} f_. diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index b14f87a7d7..05759772a5 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -644,10 +644,10 @@ have mPgtr : measurable_fun setT (fun r : R => P (X @^-1` `]r, +oo[)). move=> X_ge0; rewrite ge0_expectation_ccdf//. transitivity (\int[mu]_(r in `[0%R, +oo[) (P (X @^-1` [set r]) + P (X @^-1` `]r, +oo[))). - rewrite ge0_integralD//=; [|exact: measurable_funTS..]. + rewrite ge0_integralD//; [|exact: measurable_funTS..]. rewrite [X in _ = X + _](_ : _ = 0) ?add0e; first exact: eq_integral. - rewrite -(lebesgue_integral_pmf X) integral_mkcond/=. - apply: (@eq_integral _ (measurableTypeR R) _ mu setT) => /= r _. + rewrite -(lebesgue_integral_pmf X) integral_mkcond. + apply: eq_integral => /= r _. rewrite patchE; have [r_ge0 | r_lt0] := boolP (r \in `[0%R, +oo[). - by rewrite ifT ?inE// fineK ?fin_num_measure. - rewrite mem_setE (negbTE r_lt0) fineK ?fin_num_measure//. @@ -681,13 +681,11 @@ transitivity (- \int[mu]_(s in `]-oo, 0%R]) P (Y @^-1` `[(- s)%R, +oo[)). by apply: (eq_measurable_fun (fun r:R => (fine (P (Y @^-1` `[r, +oo[ )))%:E)) => [r _|]; [rewrite fineK ?fin_num_measure | apply/measurable_EFinP]. transitivity (- \int[mu]_(s in `]-oo, 0%R] `\ 0%R) P (Y @^-1` `[(- s)%R, +oo[)). - congr -%E. - under[LHS] eq_integral => s _ do - rewrite -(@fineK _ (P (Y @^-1` `[(- s)%R, +oo[))) ?fin_num_measure//. - under[RHS] eq_integral => s _ do - rewrite -(@fineK _ (P (Y @^-1` `[(- s)%R, +oo[))) ?fin_num_measure//. - rewrite integral_setD1_EFin//; first exact: measurableD. - exact/measurable_funTS/(measurableT_comp mfPleY). + congr -%E; rewrite setDitv1r integral_itv_bndo_bndc//=. + apply/measurable_funTS => /=. + under eq_fun => s + do rewrite -(@fineK _ (P (Y @^-1` `[(- s)%R, +oo[))) ?fin_num_measure//. + exact/measurableT_comp/(measurableT_comp mfPleY). rewrite setDitv1r; congr -%E; apply: eq_integral => r _. by rewrite (@comp_preimage _ _ _ _ _ -%R)/= opp_preimage_itvbndy/= opprK. Qed. From bea0a38f40557d4914a81a7d9a750a6f6b6c667c Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Sun, 22 Feb 2026 21:39:27 +0900 Subject: [PATCH 7/9] Apply suggestion from @t6s Co-authored-by: Takafumi Saikawa --- theories/probability_theory/random_variable.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index 05759772a5..4c8faa9a56 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -137,8 +137,7 @@ Proof. by move=> mf intf; rewrite integral_pushforward. Qed. End transfer_probability. Section pmf_definition. -Context {d} {T : measurableType d} {R : realType}. -Variables (P : probability T R). +Context {d} {T : measurableType d} {R : realType} (P : probability T R). Definition pmf (X : {RV P >-> R}) (r : R) : R := fine (P (X @^-1` [set r])). From 744827e7a4c3f03bb26cec133242b98349983d1b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 23 Feb 2026 12:12:57 +0900 Subject: [PATCH 8/9] CI --- theories/ftc.v | 66 ++++++++++++++++++++++++++++---------------------- 1 file changed, 37 insertions(+), 29 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 0f626d1bfe..ad662b422e 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -109,14 +109,14 @@ apply: cvg_at_right_left_dnbhs. have ixdf n : \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E - \int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E = \int[mu]_(y in E x n) (f y)%:E. - rewrite -[in X in X - _]integral_itv_bndo_bndc//=; last first. - by case: locf => + _ _; exact: measurable_funS. + rewrite -[in X in X - _]integral_itv_bndo_bndc; last first. + by case: locf => /measurable_EFinP + _ _; exact: measurable_funS. rewrite (@itv_bndbnd_setU _ _ _ (BLeft x))//=; last 2 first. by case: a ax F => [[|] a|[|]]// /ltW. by rewrite bnd_simp lerDl ltW. rewrite integral_setU//=. - - rewrite addeAC -[X in _ - X]integral_itv_bndo_bndc//=; last first. - by case: locf => + _ _; exact: measurable_funS. + - rewrite addeAC -[X in _ - X]integral_itv_bndo_bndc; last first. + by case: locf => /measurable_EFinP + _ _; exact: measurable_funS. rewrite subee ?add0e//. by apply: integrable_fin_num => //; exact: integrableS intf. - by case: locf => /measurable_EFinP + _ _; exact: measurable_funS. @@ -167,8 +167,8 @@ apply: cvg_at_right_left_dnbhs. case: a ax {F}; last first. move=> [_|//]. apply: nearW => n. - rewrite -[in LHS]integral_itv_bndo_bndc//=; last first. - by case: locf => + _ _; exact: measurable_funS. + rewrite -[in LHS]integral_itv_bndo_bndc; last first. + by case: locf => /measurable_EFinP + _ _; exact: measurable_funS. rewrite -/mu -[LHS]oppeK; congr oppe. rewrite oppeB; last first. rewrite fin_num_adde_defl// fin_numN//. @@ -177,8 +177,8 @@ apply: cvg_at_right_left_dnbhs. rewrite (_ : `]-oo, x] = `]-oo, (x + d n)%R] `|` E x n)%classic; last first. by rewrite -itv_bndbnd_setU//= bnd_simp ler_wnDr// ltW. rewrite integral_setU//=. - - rewrite addeAC -[X in X - _]integral_itv_bndo_bndc//; last first. - by case: locf => + _ _; exact: measurable_funS. + - rewrite addeAC -[X in X - _]integral_itv_bndo_bndc; last first. + by case: locf => /measurable_EFinP + _ _; exact: measurable_funS. rewrite subee ?add0e//. by apply: integrable_fin_num => //; exact: integrableS intf. - exact: (nice_E _).1. @@ -190,8 +190,8 @@ apply: cvg_at_right_left_dnbhs. move/(_ (x - a)%R); rewrite subr_gt0 => /(_ ax)[m _ /=] h. near=> n. have mn : (m <= n)%N by near: n; exists m. - rewrite -[in X in X - _]integral_itv_bndo_bndc//=; last first. - by case: locf => + _ _; exact: measurable_funS. + rewrite -[in X in X - _]integral_itv_bndo_bndc; last first. + by case: locf => /measurable_EFinP + _ _; exact: measurable_funS. rewrite -/mu -[LHS]oppeK; congr oppe. rewrite oppeB; last first. rewrite fin_num_adde_defl// fin_numN//. @@ -205,8 +205,8 @@ apply: cvg_at_right_left_dnbhs. by have := h _ mn; rewrite sub0r gtr0_norm. by rewrite opprK bnd_simp -lerBrDl subrr ltW. rewrite integral_setU//=. - - rewrite addeAC -[X in X - _]integral_itv_bndo_bndc//; last first. - by case: locf => + _ _; exact: measurable_funS. + - rewrite addeAC -[X in X - _]integral_itv_bndo_bndc; last first. + by case: locf => /measurable_EFinP + _ _; exact: measurable_funS. rewrite opprK subee ?add0e//. by apply: integrable_fin_num => //; exact: integrableS intf. - by case: locf => /measurable_EFinP + _ _; exact: measurable_funS. @@ -654,7 +654,8 @@ move=> f_ge0 cf Fxl dF Fa dFE. have mf : measurable_fun `]a, +oo[ f. apply: open_continuous_measurable_fun => //. by move: cf => /continuous_within_itvcyP[/in_continuous_mksetP cf _]. -rewrite -integral_itv_obnd_cbnd// itv_bndy_bigcup_BRight seqDU_bigcup_eq. +rewrite -integral_itv_obnd_cbnd//; last exact/measurable_EFinP. +rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq. rewrite ge0_integral_bigcup//=; last 3 first. - by move=> k; apply: measurableD => //; exact: bigsetU_measurable. - by rewrite -seqDU_bigcup_eq -itv_bndy_bigcup_BRight; exact: measurableT_comp. @@ -682,7 +683,7 @@ transitivity (\sum_(0 <= i n _. rewrite seqDUE/= integral_itv_obnd_cbnd; last first. - apply/measurable_fun_itv_bndo_bndcP. + apply/measurable_EFinP/measurable_fun_itv_bndo_bndcP. apply: open_continuous_measurable_fun => //. move: cf => /continuous_within_itvcyP[cf _] x. rewrite inE/= in_itv/= => /andP[anx _]. @@ -1254,7 +1255,8 @@ have mGF : measurable_fun `]a, b[ (G \o F). have mF' : measurable_fun `]a, b[ F^`(). apply: subspace_continuous_measurable_fun => //. by apply: continuous_in_subspaceT => x /[!inE] xab; exact: cF'. -rewrite integral_itv_bndoo//; last first. +rewrite integral_itv_bndoo; last first. + apply/measurable_EFinP. rewrite compA -(compA G -%R) (_ : -%R \o -%R = id); last first. by apply/funext => y; rewrite /= opprK. apply: measurable_funM => //; apply: measurableT_comp => //. @@ -1262,7 +1264,7 @@ rewrite integral_itv_bndoo//; last first. move=> x /[!inE] xab; rewrite [in RHS]derive1E deriveN -?derive1E//. by case: Fab => + _ _; apply. exact: measurableT_comp. -rewrite [in RHS]integral_itv_bndoo//; last exact: measurable_funM. +rewrite [in RHS]integral_itv_bndoo; last exact/measurable_EFinP/measurable_funM. apply: eq_integral => x /[!inE] xab; rewrite !fctE !opprK derive1E deriveN. - by rewrite opprK -derive1E. - by case: Fab => + _ _; exact. @@ -1299,7 +1301,7 @@ have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)[ ((G \o F) * - F^`())%R. by apply; rewrite inE/= in_itv/= andbT. by apply: cG; rewrite in_itv/=; apply: decrF; rewrite ?in_itv/= ?lexx ?ltW. rewrite -integral_itv_bndo_bndc; last first. - apply: open_continuous_measurable_fun => // x. + apply/measurable_EFinP; apply: open_continuous_measurable_fun => // x. by rewrite inE => /cG. transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a[) (G x)%:E)). rewrite (decreasing_itvNyo_bigcup decrF Fny). @@ -1331,7 +1333,7 @@ transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a[) (G x)%:E)). rewrite -(bigcup_mkord _ (fun k => `]F (a + k.+1%:R), F a[%classic)). by move: x; apply: bigcup_sub => k/= nk; exact: subset_itvr. rewrite -integral_itv_obnd_cbnd; last first. - case: n => [|n]. + apply/measurable_EFinP; case: n => [|n]. by rewrite addr0 set_itvoo0; exact: measurable_fun_set0. by apply: measurable_funS (mG n) => //; exact: subset_itvW. congr (integral _). @@ -1341,6 +1343,7 @@ transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a[) (G x)%:E)). transitivity (limn (fun n => \int[mu]_(x in `]a, (a + n%:R)%R[) (((G \o F) * - F^`()) x)%:E)); last first. rewrite -integral_itv_obnd_cbnd; last first. + apply/measurable_EFinP. rewrite (@itv_bndy_bigcup_BLeft_shift _ _ _ 1). under eq_bigcupr do rewrite addn1. apply/measurable_fun_bigcup => // n. @@ -1389,14 +1392,18 @@ transitivity (limn (fun n => apply: congr_lim; apply/funext => -[|n]. by rewrite addr0 set_itvco0 set_itvoo0 !integral_set0. rewrite integral_itv_bndo_bndc; last first. + apply/measurable_EFinP. apply/measurable_fun_itv_obnd_cbndP; apply: measurable_funS (mG n) => //. by apply: subset_itvl; rewrite bnd_simp. rewrite integration_by_substitution_decreasing. -- rewrite integral_itv_bndo_bndc// ?integral_itv_obnd_cbnd//. - + rewrite -setUitv1; last by rewrite bnd_simp ltrDl. - rewrite measurable_funU//; split; last exact: measurable_fun_set1. +- rewrite integral_itv_bndo_bndc; last first. + apply/measurable_EFinP. by apply: measurable_funS (mGFNF' n) => //; exact: subset_itv_oo_co. - + by apply: measurable_funS (mGFNF' n) => //; exact: subset_itv_oo_co. + rewrite integral_itv_obnd_cbnd//. + apply/measurable_EFinP. + rewrite -setUitv1; last by rewrite bnd_simp ltrDl. + rewrite measurable_funU//; split; last exact: measurable_fun_set1. + by apply: measurable_funS (mGFNF' n) => //; exact: subset_itv_oo_co. - by rewrite lerDl. - move=> x y /= xaa yaa yx. by apply: decrF; rewrite ?in_itv ?andbT/= ?(itvP xaa) ?(itvP yaa). @@ -1521,10 +1528,10 @@ have mF' : measurable_fun `]a, +oo[ (- F)%R^`(). rewrite near_nbhs. exact: near_in_itvoy. rewrite -!integral_itv_obnd_cbnd; last 2 first. - apply: measurable_funM => //. + apply/measurable_EFinP; apply: measurable_funM => //. apply: open_continuous_measurable_fun; first exact: interval_open. by move=> x; rewrite inE/=; exact: cF'. - apply: measurable_funM; last exact: measurableT_comp. + apply/measurable_EFinP; apply: measurable_funM; last exact: measurableT_comp. apply: (measurable_comp (measurable_itv `]-oo, (- F a)%R[)). - move=> _ /= [x + <-] => ax. by rewrite in_itv/= ltrN2 incrF ?in_itv/= ?lexx//= (itvP ax). @@ -1674,7 +1681,7 @@ have mF : measurable_fun `]-oo, b[ F. move/derivable_within_continuous : dF. by rewrite continuous_open_subspace; [exact|exact: interval_open]. rewrite -[RHS]integral_itv_obnd_cbnd; last first. - apply: (@measurable_comp _ _ _ _ _ _ `]-oo, b]) => //=. + apply/measurable_EFinP/(@measurable_comp _ _ _ _ _ _ `]-oo, b]) => //=. rewrite opp_itv_bndy opprK/=. by apply: subset_itvl; rewrite bnd_simp. apply/measurable_fun_itv_bndo_bndcP; apply: measurable_funM => //. @@ -1684,7 +1691,7 @@ rewrite -[RHS]integral_itv_obnd_cbnd; last first. - apply: open_continuous_measurable_fun; first by []. by move=> x/=; rewrite inE => /cdF. rewrite -[LHS]integral_itv_obnd_cbnd; last first. - apply: measurable_funM. + apply/measurable_EFinP/measurable_funM. apply: (@measurable_comp _ _ _ _ _ _ `](- F b)%R, +oo[) => //=. - move=> x/= [r]; rewrite in_itv/= andbT => br <-{x}. by rewrite in_itv/= andbT ltrN2 ndF ?in_itv//= 1?ltrNl// lerNl ltW. @@ -1754,7 +1761,8 @@ rewrite -{2}setC0 -(set_itvoc0 0%R) setCitv/= ge0_integral_setU//=; first last. + by move=> ? ? _ _; exact: ndF. + by rewrite interiorT. - by apply/measurable_EFinP; rewrite -setCitvr setvU; exact: mGFF'. -rewrite integral_itv_obnd_cbnd; last by apply: measurable_funTS; apply: mGFF'. +rewrite integral_itv_obnd_cbnd; last first. + by apply/measurable_EFinP/measurable_funTS; exact: mGFF'. rewrite -(increasing_ge0_integration_by_substitutiony _ _ _ cvgFy); first last. - by move=> x; rewrite in_itv/= andbT => F0x; exact: G0. - exact: continuous_subspaceT. @@ -1775,7 +1783,7 @@ rewrite -(increasing_ge0_integration_by_substitutionNy _ _ cvgFNy); first last. - by move=> x _; exact: cdF. - by move=> x y _ _; exact: ndF. rewrite -integral_itv_obnd_cbnd; last first. - by apply: measurable_funTS; exact: continuous_measurable_fun. + by apply/measurable_EFinP/measurable_funTS; exact: continuous_measurable_fun. rewrite -ge0_integral_setU//=; first last. - rewrite disj_set2E; apply/eqP; rewrite -subset0 => x/=. by rewrite !in_itv/= andbT ltNge => -[? /negP]. @@ -1847,7 +1855,7 @@ rewrite -(setUv [set x : R | 0 <= x]%R) ge0_integral_setU//= ; last 4 first. exact/disj_setPCl. rewrite mule_natl mule2n; congr +%E. rewrite -set_itvcy// setCitvr. -rewrite integral_itv_bndo_bndc; last exact: measurable_funTS. +rewrite integral_itv_bndo_bndc; last exact/measurable_EFinP/measurable_funTS. rewrite -{1}oppr0 ge0_integration_by_substitutionNy//. - apply: eq_integral => /= x; rewrite inE/= in_itv/= andbT => x0. by rewrite (evenf x). From 8f9cd8c94a3a7a0d78032d7a5799855a426f2a6c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 23 Feb 2026 21:47:30 +0900 Subject: [PATCH 9/9] changelog --- CHANGELOG_UNRELEASED.md | 45 ++++++++++++++ CHANGELOG_UNRELEASED_new.md | 61 ------------------- .../lebesgue_integral_nonneg.v | 16 ++--- theories/probability_theory/random_variable.v | 4 +- 4 files changed, 55 insertions(+), 71 deletions(-) delete mode 100644 CHANGELOG_UNRELEASED_new.md diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 318217cd50..05d8a5fe35 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -21,6 +21,32 @@ + lemma `pmf_ge0` + lemmas `pmf_gt0_countable`, `pmf_measurable` +- in `unstable.v`: + + lemmas `oppr_itvNy`, `oppr_itvy` + +- in `set_interval.v`: + + lemmas `opp_preimage_itvbndy`, `opp_preimage_itvbndbnd` + +- in `lebesgue_measure.v`: + + lemma `lebesgue_measure_unique` + +- in `lebesgue_integral_nonneg.v`: + + lemmas `lebesgue_measureN`, `ge0_integration_by_substitution0` + +- in `measurable_realfun.v`: + + definition `min_mfun` + +- in `random_variable.v` + + lemmas `lebesgue_integral_pmf`, `cdf_measurable`, `ccdf_measurable`, + `le0_expectation_cdf` + +- in `lebesgue_integral_nonneg.v`: + + lemma `integral_setU` + +- in `measurable_realfun.v`: + + lemmas `emeasurable_fun_itv_obnd_cbndP`, `emeasurable_fun_itv_bndo_bndcP`, + `emeasurable_fun_itv_cc` + ### Changed - in set_interval.v + `itv_is_closed_unbounded` (fix the definition) @@ -163,10 +189,20 @@ + `weak_sep_openE` -> `initial_sep_openE` + `join_product_weak` -> `join_product_initial` +- in `lebesgue_integral_nonneg.v`: + + `integral_setD1_EFin` -> `integral_setD1` + ### Generalized +- in `lebesgue_integral_nonneg.v`: + + lemmas `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd`, + `integral_itv_bndoo` + ### Deprecated +- in `lebesgue_integral_nonneg.v`: + + lemma `integral_setU_EFin` + ### Removed - in `weak_topology.v`: @@ -175,6 +211,15 @@ `weak_pseudo_metric_entourageE` (now `Let`'s in `initial_topology.v`) +- in `measurable_realfun.v`: + + lemma `max_mfun_subproof` (has become a `Let`) + +- in `simple_functions.v`: + + definition `max_sfun` + +- in `lebesgue_integral_nonneg.v`: + + lemma `integral_setU` (was deprecated since version 1.0.1) + ### Infrastructure ### Misc diff --git a/CHANGELOG_UNRELEASED_new.md b/CHANGELOG_UNRELEASED_new.md deleted file mode 100644 index cdb5a5470b..0000000000 --- a/CHANGELOG_UNRELEASED_new.md +++ /dev/null @@ -1,61 +0,0 @@ -# Changelog (unreleased) - -## [Unreleased] - -### Added - -- in `unstable.v`: - + lemmas `oppr_itvNy`, `oppr_itvy` - -- in `set_interval.v`: - + lemmas `opp_preimage_itvbndy`, `opp_preimage_itvbndbnd` - -- in `lebesgue_measure.v`: - + lemma `lebesgue_measure_unique` - -- in `lebesgue_integral_nonneg.v`: - + lemmas `lebesgue_measureN`, `ge0_integral_pushforwardN` - -- in `measurable_realfun.v`: - + definition `min_mfun` - -- in `random_variable.v` - + lemmas `lebesgue_integral_pmf`, `cdf_measurable`, `ccdf_measurable`, - `le0_expectation_cdf` - -- in `lebesgue_integral_nonneg.v`: - + lemma `integral_setU` - -- in `measurable_realfun.v`: - + lemmas `emeasurable_fun_itv_obnd_cbndP`, `emeasurable_fun_itv_bndo_bndcP`, - `emeasurable_fun_itv_cc` - -### Deprecated - -- in `lebesgue_integral_nonneg.v`: - + lemma integral_setU_EFin` - -### Renamed - -- in `lebesgue_integral_nonneg.v`: - + `integral_setD1_EFin` -> `integral_setD1` - -### Generalized - -- in `lebesgue_integral_nonneg.v`: - + lemmas `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd`, - `integral_itv_bndoo` - -### Removed - -- in `measurable_realfun.v`: - + lemma `max_mfun_subproof` (has become a `Let`) - -- in `simple_functions.v`: - + definition `max_sfun` - -- in `lebesgue_integral_nonneg.v`: - + lemma `integral_setU` (was deprecated since version 1.0.1) - - - diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index feb15c790e..1df878888c 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -582,7 +582,7 @@ rewrite /pushforward opp_preimage_itvbndbnd/= !lebesgue_measure_itv/=. by rewrite !lte_fin ltrN2 opprK addrC. Qed. -Lemma ge0_integral_pushforwardN (f : R -> \bar R) : +Lemma ge0_integration_by_substitution0 (f : R -> \bar R) : measurable_fun [set: R] f -> (forall r, 0 <= f r) -> \int[mu]_(r in `[0%R, +oo[) f r = \int[mu]_(r in `]-oo, 0%R]) f (- r)%R. Proof. @@ -1388,11 +1388,11 @@ Proof. move=> mD mf mg f0 g0 [N [mN N0 subN]]. rewrite integralEpatch// [RHS]integralEpatch//. rewrite (ge0_negligible_integral mN)//; last 2 first. - - by apply/measurable_restrict => //; rewrite setIidr. - - by move=> x Dx; rewrite /= patchE (mem_set Dx) f0. +- by apply/measurable_restrict => //; rewrite setIidr. +- by move=> x Dx; rewrite /= patchE (mem_set Dx) f0. rewrite [RHS](ge0_negligible_integral mN)//; last 2 first. - - by apply/measurable_restrict => //; rewrite setIidr. - - by move=> x Dx; rewrite /= patchE (mem_set Dx) g0. +- by apply/measurable_restrict => //; rewrite setIidr. +- by move=> x Dx; rewrite /= patchE (mem_set Dx) g0. apply: eq_integral => x;rewrite in_setD => /andP[_ xN]. apply: contrapT; rewrite !patchE; case: ifPn => xD //. move: xN; rewrite notin_setE; apply: contra_not => fxgx; apply: subN => /=. @@ -1405,10 +1405,10 @@ Lemma ae_eq_integral (D : set T) (g f : T -> \bar R) : Proof. move=> mD mf mg /ae_eq_funeposneg[Dfgp Dfgn]. rewrite integralE// [in RHS]integralE//; congr (_ - _). - by apply: ge0_ae_eq_integral => //; [exact: measurable_funepos| +- by apply: ge0_ae_eq_integral => //; [exact: measurable_funepos| exact: measurable_funepos]. -by apply: ge0_ae_eq_integral => //; [exact: measurable_funeneg| - exact: measurable_funeneg]. +- by apply: ge0_ae_eq_integral => //; [exact: measurable_funeneg| + exact: measurable_funeneg]. Qed. End ae_eq_integral. diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index 4c8faa9a56..c8131df2a6 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -631,7 +631,7 @@ rewrite [X in measurable X](_ : _ = (<%R s) @^-1` [set true]). by apply: eq_set => r; rewrite in_itv/= s_ge0. Qed. -Let ge0_expectation_prob_ge (X : {RV P >-> R}) : (forall x, 0 <= X x)%R -> +Let ge0_expectation_preimage (X : {RV P >-> R}) : (forall x, 0 <= X x)%R -> 'E_P[X] = \int[mu]_(r in `[0%R, +oo[) P (X @^-1` `[r, +oo[). Proof. have mPeqr : measurable_fun setT (fun r => P (X @^-1` [set r])). @@ -676,7 +676,7 @@ transitivity (- 'E_P[Y]). by apply: eq_integral => x _; rewrite opprK. by rewrite lee_fin/= oppr_ge0. transitivity (- \int[mu]_(s in `]-oo, 0%R]) P (Y @^-1` `[(- s)%R, +oo[)). - rewrite ge0_expectation_prob_ge ?ge0_integral_pushforwardN//. + rewrite ge0_expectation_preimage ?ge0_integration_by_substitution0//. by apply: (eq_measurable_fun (fun r:R => (fine (P (Y @^-1` `[r, +oo[ )))%:E)) => [r _|]; [rewrite fineK ?fin_num_measure | apply/measurable_EFinP]. transitivity (- \int[mu]_(s in `]-oo, 0%R] `\ 0%R) P (Y @^-1` `[(- s)%R, +oo[)).