From 5029183bf39f7de135938fbd59e4b9d9e0a5a3be Mon Sep 17 00:00:00 2001 From: Yosuke-Ito-345 Date: Sat, 28 Feb 2026 13:55:02 +0900 Subject: [PATCH 1/2] add expectation_cdf_ccdf --- CHANGELOG_UNRELEASED.md | 2 +- theories/probability_theory/random_variable.v | 31 +++++++++++++++++++ 2 files changed, 32 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 42aa1376b..d51a2e7f9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -47,7 +47,7 @@ - in `random_variable.v` + lemmas `lebesgue_integral_pmf`, `cdf_measurable`, `ccdf_measurable`, - `le0_expectation_cdf` + `le0_expectation_cdf`, `expectation_cdf_ccdf` - in `lebesgue_integral_nonneg.v`: + lemma `integral_setU` diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index e46c95a88..0c4725097 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -688,6 +688,37 @@ rewrite setDitv1r; congr -%E; apply: eq_integral => r _. by rewrite (@comp_preimage _ _ _ _ _ -%R)/= opp_preimage_itvbndy/= opprK. Qed. +Lemma expectation_cdf_ccdf (X : {RV P >-> R}) : Lfun P 1 X -> + 'E_P[X] = \int[mu]_(r in `[0%R, +oo[) ccdf X r + - \int[mu]_(r in `]-oo, 0%R[) cdf X r. +Proof. +move=> L1X. +pose Xp := (cst 0%R) \max X. +pose Xm := (cst 0%R) \min X. +have Xp_leX x : setT x -> `|(Xp x)%:E| <= `|(X x)%:E|. + by rewrite lee_tofin// ger0_norm ?le_max ?lexx// ge_max normr_ge0 ler_norm. +have Xm_leX x : setT x -> `|(Xm x)%:E| <= `|(X x)%:E|. + rewrite /Xm lee_tofin//=. + by have [//=| Xle0 |] := (@real_le0P _ (X x)); + [rewrite ler0_norm | rewrite normr0; exact: ltW]. +have XpP1 : Xp \in Lfun P 1. + by rewrite Lfun1_integrable; apply: (le_integrable _ _ Xp_leX); + [| apply/measurable_EFinP | rewrite -Lfun1_integrable]. +have XmP1: Xm \in Lfun P 1. + by rewrite Lfun1_integrable; apply: (le_integrable _ _ Xm_leX); + [| apply/measurable_EFinP | rewrite -Lfun1_integrable]. +rewrite (_ : MeasurableFun.sort X = (Xp \+ Xm)%R) ?expectationD//; + last by apply: funext => x; rewrite /= addr_max_min add0r. +rewrite (_ : 'E_P[Xp] = \int[mu]_(r in `[0%R, +oo[) ccdf X r); last first. + rewrite ge0_expectation_ccdf/= => [|x]; last by case: ler0P; last exact: ltW. + apply: eq_integral => r; rewrite inE/= in_itv/= andbT => r_ge0; congr (P _). + by apply: eq_set => x/=; rewrite !in_itv/= !andbT lt_max ltNge r_ge0. +rewrite (_ : 'E_P[Xm] = - \int[mu]_(r in `]-oo, 0%R[) cdf X r)//. +rewrite le0_expectation_cdf/= => [|x]; last by rewrite ge_min ?lexx. +congr -%E; apply: eq_integral => r; rewrite inE/= in_itv/= => r_le0. +by congr (P _); apply: eq_set => x/=; rewrite !in_itv/= ge_min leNgt r_le0. +Qed. + End tail_expectation_formula. HB.lock Definition covariance {d} {T : measurableType d} {R : realType} From 86c3edd9d8aeb9630785103f2f503f2dea947bb5 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 12 Mar 2026 17:46:10 +0900 Subject: [PATCH 2/2] trying to use funrpos/funrneg --- CHANGELOG_UNRELEASED.md | 17 ++ classical/functions.v | 4 + .../lebesgue_integrable.v | 8 + theories/measurable_realfun.v | 19 +++ theories/numfun.v | 149 +++++++++++++++++- theories/probability_theory/random_variable.v | 50 +++--- 6 files changed, 219 insertions(+), 28 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d51a2e7f9..c5390c859 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -84,6 +84,23 @@ - in `separation_axioms.v`: + lemmas `limit_point_closed` +- in `functions.v`: + + lemma `addBrfctE` + +- in `numfun.v`: + + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-` + + lemmas `funrpos_ge0`, `funrneg_ge0`, `funrposN`, `funrnegN`, `ge0_funrposE`, + `ge0_funrnegE`, `le0_funrposE`, `le0_funrnegE`, `ge0_funrposM`, `ge0_funrnegM`, + `le0_funrposM`, `le0_funrnegM`, `funrposDneg`, `funrposBneg`, + `funrD_posD`, `funrpos_le`, `funrneg_le` + + lemmas `funerpos`, `funerneg` + +- in `lebesgue_integrable.v`: + + lemmas `integrable_funrpos`, `integrable_funrneg` + +- in `measurable_realfun.v`: + + lemmas `measurable_funrpos`, `measurable_funrneg` + ### Changed - in `constructive_ereal.v`: fixed the infamous `%E` scope bug. diff --git a/classical/functions.v b/classical/functions.v index 9d6137b50..be9132cd5 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -2719,6 +2719,10 @@ Proof. by elim: n => [//|n h]; rewrite funeqE=> ?; rewrite !mulrSr h. Qed. Lemma opprfctE (T : Type) (K : zmodType) (f : T -> K) : - f = (fun x => - f x). Proof. by []. Qed. +Lemma addBrfctE (U : Type) (K : zmodType) : + @interchange (U -> K) (fun a b => a - b) (fun a b => a + b). +Proof. by move=> a b c d; apply/funext => x; rewrite addrACA -opprD. Qed. + Lemma mulrfctE (T : Type) (K : pzRingType) (f g : T -> K) : f * g = (fun x => f x * g x). Proof. by []. Qed. diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index 06f888196..d71971d6c 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -372,6 +372,14 @@ have [M [_ mrt]] := bdA; apply: le_lt_trans. by rewrite lte_mul_pinfty. Qed. +Lemma integrable_funrpos A f : measurable A -> + mu.-integrable A (EFin \o f) -> mu.-integrable A (EFin \o f^\+). +Proof. by move/integrable_funepos => /[apply]; rewrite funerpos. Qed. + +Lemma integrable_funrneg A f : measurable A -> + mu.-integrable A (EFin \o f) -> mu.-integrable A (EFin \o f^\-). +Proof. by move/integrable_funeneg => /[apply]; rewrite funerneg. Qed. + End Rintegrable. Lemma integrable_indic_itv {R : realType} (a b : R) (b0 b1 : bool) : diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 92e62fc23..6c0f22259 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -907,6 +907,12 @@ by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //; [exact: measurable_fun_ltr|exact: measurable_funS mg|exact: measurable_funS mf]. Qed. +Lemma measurable_funrpos D f : measurable_fun D f -> measurable_fun D f^\+. +Proof. by move=> mf; exact: measurable_maxr. Qed. + +Lemma measurable_funrneg D f : measurable_fun D f -> measurable_fun D f^\-. +Proof. by move=> mf; apply: measurable_maxr => //; exact: measurableT_comp. Qed. + Lemma measurable_minr D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \min g). Proof. @@ -999,6 +1005,19 @@ Qed. End measurable_fun_realType. +Section funrposneg_measurable. +Context {d} {aT : measurableType d} {rT : realType}. + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ f^\+ + (measurable_funrpos (@measurable_funPT _ _ _ _ f)). + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ f^\- + (measurable_funrneg (@measurable_funPT _ _ _ _ f)). + +End funrposneg_measurable. + Section mono_measurable. Context {R : realType}. diff --git a/theories/numfun.v b/theories/numfun.v index d56e400fb..77d096987 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -27,12 +27,15 @@ From mathcomp Require Import topology normedtype sequences. (* bounded_variation a b f == all variations of f are bounded *) (* {nnfun T >-> R} == type of non-negative functions *) (* f ^\+ == the function formed by the non-negative outputs *) -(* of f (from a type to the type of extended real *) -(* numbers) and 0 otherwise *) -(* rendered as f ⁺ with company-coq (U+207A) *) +(* of f and 0 otherwise *) +(* The codomain of f is the real numbers in scope *) +(* ring_scope and the extended real numbers in *) +(* scope ereal_scope. *) +(* Rendered as f ⁺ with company-coq (U+207A). *) (* f ^\- == the function formed by the non-positive outputs *) (* of f and 0 o.w. *) -(* rendered as f ⁻ with company-coq (U+207B) *) +(* Similar to ^\+. *) +(* Rendered as f ⁻ with company-coq (U+207B). *) (* \1_ A == indicator function 1_A *) (* ``` *) (* *) @@ -682,6 +685,133 @@ Proof. by apply/funext=> x; rewrite /patch/=; case: ifP; rewrite ?mule0. Qed. End erestrict_lemmas. +Section funrposneg. +Local Open Scope ring_scope. + +Definition funrpos T (R : realDomainType) (f : T -> R) := + fun x => Num.max (f x) 0. +Definition funrneg T (R : realDomainType) (f : T -> R) := + fun x => Num.max (- f x) 0. + +End funrposneg. + +Notation "f ^\+" := (funrpos f) : ring_scope. +Notation "f ^\-" := (funrneg f) : ring_scope. + +Section funrposneg_lemmas. +Local Open Scope ring_scope. +Variables (T : Type) (R : realDomainType) (D : set T). +Implicit Types (f g : T -> R) (r : R). + +Lemma funrpos_ge0 f x : 0 <= f^\+ x. +Proof. by rewrite /funrpos /= le_max lexx orbT. Qed. + +Lemma funrneg_ge0 f x : 0 <= f^\- x. +Proof. by rewrite /funrneg le_max lexx orbT. Qed. + +Lemma funrposN f : (\- f)^\+ = f^\-. Proof. exact/funext. Qed. + +Lemma funrnegN f : (\- f)^\- = f^\+. +Proof. by apply/funext => x; rewrite /funrneg opprK. Qed. + +(* TODO: the following lemmas require a pointed type and realDomainType does +not seem to be at this point + +Lemma funrpos_restrict f : (f \_ D)^\+ = (f^\+) \_ D. +Proof. +by apply/funext => x; rewrite /patch/_^\+; case: ifP; rewrite //= maxxx. +Qed. + +Lemma funrneg_restrict f : (f \_ D)^\- = (f^\-) \_ D. +Proof. +by apply/funext => x; rewrite /patch/_^\-; case: ifP; rewrite //= oppr0 maxxx. +Qed.*) + +Lemma ge0_funrposE f : (forall x, D x -> 0 <= f x) -> {in D, f^\+ =1 f}. +Proof. by move=> f0 x; rewrite inE => Dx; apply/max_idPl/f0. Qed. + +Lemma ge0_funrnegE f : (forall x, D x -> 0 <= f x) -> {in D, f^\- =1 cst 0}. +Proof. +by move=> f0 x; rewrite inE => Dx; apply/max_idPr; rewrite lerNl oppr0 f0. +Qed. + +Lemma le0_funrposE f : (forall x, D x -> f x <= 0) -> {in D, f^\+ =1 cst 0}. +Proof. by move=> f0 x; rewrite inE => Dx; exact/max_idPr/f0. Qed. + +Lemma le0_funrnegE f : (forall x, D x -> f x <= 0) -> {in D, f^\- =1 \- f}. +Proof. +by move=> f0 x; rewrite inE => Dx; apply/max_idPl; rewrite lerNr oppr0 f0. +Qed. + +Lemma ge0_funrposM r f : (0 <= r)%R -> + (fun x => r * f x)^\+ = (fun x => r * (f^\+ x)). +Proof. by move=> ?; rewrite funeqE => x; rewrite /funrpos maxr_pMr// mulr0. Qed. + +Lemma ge0_funrnegM r f : (0 <= r)%R -> + (fun x => r * f x)^\- = (fun x => r * (f^\- x)). +Proof. +by move=> r0; rewrite funeqE => x; rewrite /funrneg -mulrN maxr_pMr// mulr0. +Qed. + +Lemma le0_funrposM r f : (r <= 0)%R -> + (fun x => r * f x)^\+ = (fun x => - r * (f^\- x)). +Proof. +move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr. +by rewrite funrposN ge0_funrnegM ?oppr_ge0. +Qed. + +Lemma le0_funrnegM r f : (r <= 0)%R -> + (fun x => r * f x)^\- = (fun x => - r * (f^\+ x)). +Proof. +move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr. +by rewrite funrnegN ge0_funrposM ?oppr_ge0. +Qed. + +Lemma funrposDneg f : f^\+ + f^\- = Num.norm \o f. +Proof. +rewrite funeqE => x /=; rewrite !fctE/=; have [fx0|/ltW fx0] := leP (f x) 0. +- rewrite ler0_norm// /funrpos /funrneg. + move/max_idPr : (fx0) => ->; rewrite add0r. + by move: fx0; rewrite -{1}oppr0 lerNr => /max_idPl ->. +- rewrite ger0_norm// /funrpos /funrneg; move/max_idPl : (fx0) => ->. + by move: fx0; rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0. +Qed. + +Lemma funrposBneg f : f^\+ - f^\- = f. +Proof. +apply/funext => x. +rewrite /funrpos /funrneg/= !fctE; have [|/ltW] := leP (f x) 0. + by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite opprK add0r. +by rewrite -{1}oppr0 -lerNl => /max_idPr ->; rewrite subr0. +Qed. + +Lemma funrDB f g : (f^\+ + g^\+) - (f^\- + g^\-) = f + g. +Proof. by rewrite addBrfctE !funrposBneg. Qed. + +Lemma funrpos_le f g : + {in D, forall x, f x <= g x} -> {in D, forall x, f^\+ x <= g^\+ x}. +Proof. +move=> fg x Dx; rewrite /funrpos /Num.max; case: ifPn => fx; case: ifPn => gx//. +- by rewrite leNgt. +- by move: fx; rewrite -leNgt => /(lt_le_trans gx); rewrite ltNge fg. +- exact: fg. +Qed. + +Lemma funrneg_le f g : + {in D, forall x, f x <= g x} -> {in D, forall x, g^\- x <= f^\- x}. +Proof. +move=> fg x Dx; rewrite /funrneg /Num.max; case: ifPn => gx; case: ifPn => fx//. +- by rewrite leNgt. +- by move: gx; rewrite -leNgt => /(lt_le_trans fx); rewrite ltrN2 ltNge fg. +- by rewrite lerN2; exact: fg. +Qed. + +End funrposneg_lemmas. +#[global] +Hint Extern 0 (is_true (0%R <= _ ^\+ _)%R) => solve [apply: funrpos_ge0] : core. +#[global] +Hint Extern 0 (is_true (0%R <= _ ^\- _)%R) => solve [apply: funrneg_ge0] : core. + HB.lock Definition funepos T (R : realDomainType) (f : T -> \bar R) := fun x => maxe (f x) 0. @@ -847,6 +977,17 @@ Hint Extern 0 (is_true (0%R <= _ ^\+ _)%E) => solve [apply: funepos_ge0] : core. #[global] Hint Extern 0 (is_true (0%R <= _ ^\- _)%E) => solve [apply: funeneg_ge0] : core. +Section funrpos_funepos_lemmas. +Context {T : Type} {R : realDomainType}. + +Lemma funerpos (f : T -> R) : (EFin \o f)^\+%E = (EFin \o f^\+). +Proof. by apply/funext => x; rewrite funeposE /funrpos/= EFin_max. Qed. + +Lemma funerneg (f : T -> R) : (EFin \o f)^\-%E = (EFin \o f^\-). +Proof. by apply/funext => x; rewrite funenegE /funrneg/= EFin_max. Qed. + +End funrpos_funepos_lemmas. + Definition indic {T} {R : pzRingType} (A : set T) (x : T) : R := (x \in A)%:R. Reserved Notation "'\1_' A" (at level 8, A at level 2, format "'\1_' A") . Notation "'\1_' A" := (indic A) : ring_scope. diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index 0c4725097..72c59d1c4 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -688,35 +688,37 @@ rewrite setDitv1r; congr -%E; apply: eq_integral => r _. by rewrite (@comp_preimage _ _ _ _ _ -%R)/= opp_preimage_itvbndy/= opprK. Qed. +Let preimage_funrpos (f : T -> R) r : (0 <= r)%R -> + (f^\+)%R @^-1` `]r, +oo[ = f @^-1` `]r, +oo[. +Proof. +move=> r0; apply: eq_set => a/=. +by rewrite !in_itv/= !andbT lt_max (ltNge r 0%R) r0 orbF. +Qed. + +Let preimage_funrneg (f : T -> R) r : (r < 0)%R -> + (- f^\-)%R @^-1` `]-oo, r] = (f)%R @^-1` `]-oo, r]. +Proof. +move=> r0; apply: eq_set => a/=. +by rewrite !in_itv/= lerNl le_max lerN2 (leNgt _ 0%R) oppr_gt0 r0 orbF. +Qed. + Lemma expectation_cdf_ccdf (X : {RV P >-> R}) : Lfun P 1 X -> 'E_P[X] = \int[mu]_(r in `[0%R, +oo[) ccdf X r - \int[mu]_(r in `]-oo, 0%R[) cdf X r. Proof. move=> L1X. -pose Xp := (cst 0%R) \max X. -pose Xm := (cst 0%R) \min X. -have Xp_leX x : setT x -> `|(Xp x)%:E| <= `|(X x)%:E|. - by rewrite lee_tofin// ger0_norm ?le_max ?lexx// ge_max normr_ge0 ler_norm. -have Xm_leX x : setT x -> `|(Xm x)%:E| <= `|(X x)%:E|. - rewrite /Xm lee_tofin//=. - by have [//=| Xle0 |] := (@real_le0P _ (X x)); - [rewrite ler0_norm | rewrite normr0; exact: ltW]. -have XpP1 : Xp \in Lfun P 1. - by rewrite Lfun1_integrable; apply: (le_integrable _ _ Xp_leX); - [| apply/measurable_EFinP | rewrite -Lfun1_integrable]. -have XmP1: Xm \in Lfun P 1. - by rewrite Lfun1_integrable; apply: (le_integrable _ _ Xm_leX); - [| apply/measurable_EFinP | rewrite -Lfun1_integrable]. -rewrite (_ : MeasurableFun.sort X = (Xp \+ Xm)%R) ?expectationD//; - last by apply: funext => x; rewrite /= addr_max_min add0r. -rewrite (_ : 'E_P[Xp] = \int[mu]_(r in `[0%R, +oo[) ccdf X r); last first. - rewrite ge0_expectation_ccdf/= => [|x]; last by case: ler0P; last exact: ltW. - apply: eq_integral => r; rewrite inE/= in_itv/= andbT => r_ge0; congr (P _). - by apply: eq_set => x/=; rewrite !in_itv/= !andbT lt_max ltNge r_ge0. -rewrite (_ : 'E_P[Xm] = - \int[mu]_(r in `]-oo, 0%R[) cdf X r)//. -rewrite le0_expectation_cdf/= => [|x]; last by rewrite ge_min ?lexx. -congr -%E; apply: eq_integral => r; rewrite inE/= in_itv/= => r_le0. -by congr (P _); apply: eq_set => x/=; rewrite !in_itv/= ge_min leNgt r_le0. +rewrite -[in LHS](funrposBneg X) expectationD; last 2 first. +- exact/Lfun1_integrable/integrable_funrpos/Lfun1_integrable. +- rewrite rpredN/=. + exact/Lfun1_integrable/integrable_funrneg/Lfun1_integrable. +rewrite (_ : 'E_P[X^\+] = \int[mu]_(r in `[0%R, +oo[) ccdf X r); last first. + rewrite ge0_expectation_ccdf/= => [|?]; last by rewrite funrpos_ge0. + apply: eq_integral => r; rewrite inE/= in_itv/= andbT => r0; congr (P _). + by rewrite preimage_funrpos. +rewrite (_ : 'E_P[- X^\-] = - \int[mu]_(r in `]-oo, 0%R[) cdf X r)//. +rewrite le0_expectation_cdf/= => [|x]; last by rewrite oppr_le0 funrneg_ge0. +congr -%E; apply: eq_integral => r; rewrite inE/= in_itv/= => r0; congr (P _). +by rewrite preimage_funrneg. Qed. End tail_expectation_formula.