From 007dc883496c2ebc24d4b443c3bf12f35ec84aec Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 28 Jun 2025 12:21:53 +0900 Subject: [PATCH 1/2] ports from the sampling branch - rm dead code in hoelder.v - reestablish the notation for mmt_gen_fun - small technical lemmas from the sampling branch --- reals/constructive_ereal.v | 11 ++++-- theories/hoelder.v | 73 ++++++++++++++++++-------------------- theories/probability.v | 56 ++++++++++++++--------------- 3 files changed, 72 insertions(+), 68 deletions(-) diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index 62d1e593df..1837ea99f6 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) (* -------------------------------------------------------------------- *) (* Copyright (c) - 2015--2016 - IMDEA Software Institute *) (* Copyright (c) - 2015--2018 - Inria *) @@ -2599,6 +2599,13 @@ move=> [x| |] [y| |] //=; first by rewrite normrM. - by rewrite -abseN -muleNN abseN -EFinN xoo normrN. Qed. +Lemma abse_prod {I : Type} (r : seq I) (P : pred I) (F : I -> \bar R) : + `|\prod_(i <- r | P i) F i| = \prod_(i <- r | P i) `|F i|. +Proof. +elim/big_ind2 : _ => //; first by rewrite abse1. +by move=> x1 x2 ? ? <- <-; rewrite abseM. +Qed. + Lemma fine_max : {in fin_num &, {mono @fine R : x y / maxe x y >-> (Num.max x y)%:E}}. Proof. @@ -2606,7 +2613,7 @@ by move=> [x| |] [y| |]//= _ _; apply/esym; have [ab|ba] := leP x y; [apply/max_idPr; rewrite lee_fin|apply/max_idPl; rewrite lee_fin ltW]. Qed. -Lemma EFin_bigmax {I : Type} (s : seq I) (P : I -> bool) (F : I -> R) r : +Lemma EFin_bigmax {I : Type} (s : seq I) (P : I -> bool) (F : I -> R) r : \big[maxe/r%:E]_(i <- s | P i) (F i)%:E = (\big[Num.max/r]_(i <- s | P i) F i)%:E. Proof. by rewrite (big_morph _ EFin_max erefl). Qed. diff --git a/theories/hoelder.v b/theories/hoelder.v index 3dd2963164..15db239b34 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import mathcomp_extra unstable boolp interval_inference. @@ -95,7 +95,7 @@ Qed. Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|. Proof. -rewrite unlock invr1// poweRe1//; under eq_integral do [rewrite poweRe1//=] => //. +rewrite unlock invr1 ?poweRe1//; under eq_integral do [rewrite poweRe1//] => //. exact: integral_ge0. Qed. @@ -109,10 +109,9 @@ move=> r0; rewrite unlock -poweRrM mulVf// poweRe1//. by apply: integral_ge0 => x _; exact: poweR_ge0. Qed. -Lemma oppe_Lnorm f p : 'N_p[\- f]%E = 'N_p[f]. +Lemma oppe_Lnorm f p : 'N_p[\- f] = 'N_p[f]. Proof. -have NfE : abse \o (\- f) = abse \o f. - by apply/funext => x /=; rewrite abseN. +have NfE : abse \o (\- f) = abse \o f by apply/funext => x /=; rewrite abseN. rewrite unlock /Lnorm NfE; case: p => /= [r|//|//]. by under eq_integral => x _ do rewrite abseN. Qed. @@ -130,29 +129,22 @@ rewrite unlock; move: p => [r/=|/=|//]; first exact: poweR_ge0. - by case: ifPn => // muT0; apply/ess_infP/nearW => x /=. Qed. -Lemma Lnorm_eq0_eq0 f p : - measurable_fun setT f -> (0 < p)%E -> 'N_p[f] = 0 -> f = \0 %[ae mu]. +Lemma Lnorm_eq0_eq0 f p : measurable_fun [set: T] f -> 0 < p -> + 'N_p[f] = 0 -> f = \0 %[ae mu]. Proof. -rewrite unlock /Lnorm => mf. -case: p => [r||//]. +rewrite unlock /Lnorm => mf; case: p => [r||//]. - rewrite lte_fin => r0 /poweR_eq0_eq0 => /(_ (integral_ge0 _ _)) h. - have : \int[mu]_x `|f x| `^ r = 0. - by apply: h => x _; rewrite poweR_ge0. - move=> H. - have {H} : \int[mu]_x `| `|f x| `^ r | = 0%R. + have : \int[mu]_x `| `|f x| `^ r | = 0%R. under eq_integral. - move=> x _. - rewrite gee0_abs; last by rewrite poweR_ge0. - over. - exact: H. - have mp : measurable_fun [set: T] (fun x : T => `|f x| `^ r). + move=> x _; rewrite gee0_abs; last by rewrite poweR_ge0. over. + by apply: h => x _; rewrite poweR_ge0. + have mp : measurable_fun [set: T] (fun x => `|f x| `^ r). apply: (@measurableT_comp _ _ _ _ _ _ (fun x => x `^ r)) => //=. - by apply (measurableT_comp (measurable_poweR _)) => //. + exact: (measurableT_comp (measurable_poweR _)). exact: measurableT_comp. move/(ae_eq_integral_abs mu measurableT mp). apply: filterS => x/= /[apply]. - move=> /poweR_eq0_eq0 /eqP => /(_ (abse_ge0 _)). - by rewrite abse_eq0 => /eqP. + by move=> /poweR_eq0_eq0 /eqP => /(_ (abse_ge0 _)); rewrite abse_eq0 => /eqP. - case: ifPn => [mu0 _|]. move=> /abs_sup_eq0_ae_eq/=. by apply: filterS => x/= /(_ I) /eqP + _ => /eqP. @@ -164,12 +156,16 @@ Qed. Lemma powR_Lnorm f r : r != 0%R -> 'N_r%:E[f] `^ r = \int[mu]_x `| f x | `^ r. Proof. by move=> r0; rewrite poweR_Lnorm. Qed. -End Lnorm_properties. - -#[global] -Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core. +Lemma Lnorm_abse f p : 'N_p[abse \o f] = 'N_p[f]. +Proof. +rewrite unlock/=; have -> : abse \o (abse \o f) = abse \o f. + by apply: funext => x/=; rewrite abse_id. +by case: p => [r|//|//]; under eq_integral => x _ do rewrite abse_id. +Qed. +End Lnorm_properties. Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f) : ereal_scope. +#[global] Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core. Section lnorm. Context d {T : measurableType d} {R : realType}. @@ -185,15 +181,6 @@ Qed. End lnorm. -Section ereal. -Context {R : realFieldType}. -Implicit Type x y : \bar R. -Local Open Scope ereal_scope. - - - -End ereal. - Section hoelder_conjugate. Context d (T : measurableType d) (R : realType). Variables (mu : {measure set T -> \bar R}). @@ -432,14 +419,14 @@ Lemma hoelder (f g : T -> R) p q : 'N_1[(f \* g)%R] <= 'N_p%:E[f] * 'N_q%:E[g]. Proof. move=> mf mg p0 q0 pq. -have [f0|f0] := eqVneq 'N_p%:E[f] 0%E; first exact: hoelder0. -have [g0|g0] := eqVneq 'N_q%:E[g] 0%E. +have [f0|f0] := eqVneq 'N_p%:E[f] 0; first exact: hoelder0. +have [g0|g0] := eqVneq 'N_q%:E[g] 0. rewrite muleC; apply: le_trans; last by apply: hoelder0 => //; rewrite addrC. by under eq_Lnorm do rewrite /= mulrC. have {f0}fpos : 0 < 'N_p%:E[f] by rewrite lt0e f0 Lnorm_ge0. have {g0}gpos : 0 < 'N_q%:E[g] by rewrite lt0e g0 Lnorm_ge0. -have [foo|foo] := eqVneq 'N_p%:E[f] +oo%E; first by rewrite foo gt0_mulye ?leey. -have [goo|goo] := eqVneq 'N_q%:E[g] +oo%E; first by rewrite goo gt0_muley ?leey. +have [foo|foo] := eqVneq 'N_p%:E[f] +oo; first by rewrite foo gt0_mulye ?leey. +have [goo|goo] := eqVneq 'N_q%:E[g] +oo; first by rewrite goo gt0_muley ?leey. pose F := normalized p f; pose G := normalized q g. rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p%:E[f] * 'N_q%:E[g]); last first. rewrite !Lnorm1; under [in RHS]eq_integral. @@ -1072,6 +1059,16 @@ Definition LType1 := LType mu (@lexx _ _ 1%E). Definition LType2 := LType mu (lee1n 2). +Lemma Lfun_norm (f : T -> R) : f \in Lfun mu 1 -> normr \o f \in Lfun mu 1. +Proof. +move=> /andP[]. +rewrite !inE/= => mf finf; apply/andP; split. + by rewrite inE/=; exact: measurableT_comp. +rewrite inE/=/finite_norm. +under [X in ('N[_]__[X])%E]eq_fun => x do rewrite -abse_EFin. +by rewrite Lnorm_abse. +Qed. + Lemma Lfun_integrable (f : T -> R) r : 1 <= r -> f \in Lfun mu r%:E -> mu.-integrable setT (fun x => (`|f x| `^ r)%:E). diff --git a/theories/probability.v b/theories/probability.v index b5bcf58e6f..ef8f2ed7b0 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -1,7 +1,7 @@ -(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect. -From mathcomp Require Import ssralg poly ssrnum ssrint interval archimedean finmap. +From mathcomp Require Import all_ssreflect ssralg. +From mathcomp Require Import poly ssrnum ssrint interval archimedean finmap. From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. From mathcomp Require Import functions cardinality fsbigop. From mathcomp Require Import exp numfun lebesgue_measure lebesgue_integral. @@ -21,27 +21,26 @@ From mathcomp Require Import ftc gauss_integral hoelder. (* `lebesgue_integral.v`. *) (* *) (* ``` *) -(* {RV P >-> T'} == random variable: a measurable function to the *) -(* measurableType T' from the measured space *) -(* characterized by the probability P *) -(* distribution P X == measure image of the probability measure P by the *) -(* random variable X : {RV P -> T'} *) -(* P as type probability T R with T of type *) -(* measurableType. *) -(* Declared as an instance of probability measure. *) -(* 'E_P[X] == expectation of the real measurable function X *) -(* covariance X Y == covariance between real random variable X and Y *) -(* 'V_P[X] == variance of the real random variable X *) -(* 'M_ X == moment generating function of the random variable *) -(* X *) -(* {dmfun T >-> R} == type of discrete real-valued measurable functions *) -(* {dRV P >-> R} == real-valued discrete random variable *) -(* dRV_dom X == domain of the discrete random variable X *) -(* dRV_enum X == bijection between the domain and the range of X *) -(* pmf X r := fine (P (X @^-1` [set r])) *) -(* cdf X r == cumulative distribution function of X *) -(* := distribution P X `]-oo, r] *) -(* enum_prob X k == probability of the kth value in the range of X *) +(* {RV P >-> T'} == random variable: a measurable function to the *) +(* measurableType T' from the measured space *) +(* characterized by the probability P *) +(* distribution P X == measure image of the probability measure P by the *) +(* random variable X : {RV P -> T'} *) +(* P as type probability T R with T of type *) +(* measurableType. *) +(* Declared as an instance of probability measure. *) +(* 'E_P[X] == expectation of the real measurable function X *) +(* covariance X Y == covariance between real random variable X and Y *) +(* 'V_P[X] == variance of the real random variable X *) +(* 'M_ X == moment generating function of the random variable X *) +(* {dmfun T >-> R} == type of discrete real-valued measurable functions *) +(* {dRV P >-> R} == real-valued discrete random variable *) +(* dRV_dom X == domain of the discrete random variable X *) +(* dRV_enum X == bijection between the domain and the range of X *) +(* pmf X r := fine (P (X @^-1` [set r])) *) +(* cdf X r == cumulative distribution function of X *) +(* := distribution P X `]-oo, r] *) +(* enum_prob X k == probability of the kth value in the range of X *) (* ``` *) (* *) (* ``` *) @@ -618,6 +617,10 @@ Qed. End variance. Notation "'V_ P [ X ]" := (variance P X). +Definition mmt_gen_fun d (T : measurableType d) (R : realType) + (P : probability T R) (X : T -> R) (t : R) := ('E_P[expR \o t \o* X])%E. +Notation "'M_ X t" := (mmt_gen_fun X t). + Section markov_chebyshev_cantelli. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). @@ -639,11 +642,8 @@ apply: (le_trans (@le_integral_comp_abse _ _ _ P _ measurableT (EFin \o X) - by rewrite unlock. Qed. -Definition mmt_gen_fun (X : T -> R) (t : R) := 'E_P[expR \o t \o* X]. -Local Notation "'M_ X t" := (mmt_gen_fun X t). - Lemma chernoff (X : {RV P >-> R}) (r a : R) : (0 < r)%R -> - P [set x | X x >= a]%R <= 'M_X r * (expR (- (r * a)))%:E. + P [set x | X x >= a]%R <= 'M_P X r * (expR (- (r * a)))%:E. Proof. move=> t0; rewrite /mmt_gen_fun. have -> : expR \o r \o* X = (normr \o normr) \o (expR \o r \o* X). From e0262186231679b21e79e30866845ea2b1927ae3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 28 Jun 2025 16:17:11 +0900 Subject: [PATCH 2/2] addressing comments --- CHANGELOG_UNRELEASED.md | 6 ++++++ reals/constructive_ereal.v | 2 +- theories/hoelder.v | 3 +-- 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1e433f23cb..2a00f0e789 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -91,6 +91,12 @@ - in `lebesgue_integrable.v`: + lemma `integral_sum` +- in `constructive_ereal.v`: + + lemmas `abse_prod` + +- in `hoelder.v`: + + lemmas `Lnorm_abse`, `Lfun_norm` + ### Changed - in `convex.v`: diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index 1837ea99f6..1be00e5512 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -2603,7 +2603,7 @@ Lemma abse_prod {I : Type} (r : seq I) (P : pred I) (F : I -> \bar R) : `|\prod_(i <- r | P i) F i| = \prod_(i <- r | P i) `|F i|. Proof. elim/big_ind2 : _ => //; first by rewrite abse1. -by move=> x1 x2 ? ? <- <-; rewrite abseM. +by move=> ? ? ? ? <- <-; rewrite abseM. Qed. Lemma fine_max : diff --git a/theories/hoelder.v b/theories/hoelder.v index 15db239b34..d2d628f93a 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -1061,8 +1061,7 @@ Definition LType2 := LType mu (lee1n 2). Lemma Lfun_norm (f : T -> R) : f \in Lfun mu 1 -> normr \o f \in Lfun mu 1. Proof. -move=> /andP[]. -rewrite !inE/= => mf finf; apply/andP; split. +case/andP; rewrite !inE/= => mf finf; apply/andP; split. by rewrite inE/=; exact: measurableT_comp. rewrite inE/=/finite_norm. under [X in ('N[_]__[X])%E]eq_fun => x do rewrite -abse_EFin.