From ebf1083dfdcd4ccfd728bda7c2784aa01a16124c Mon Sep 17 00:00:00 2001 From: Lionel Blatter Date: Tue, 31 Mar 2026 00:28:05 +0200 Subject: [PATCH] Add missing lemmas for distr --- _CoqProject | 1 + experimental_reals/distr.v | 229 +++++++++++++ experimental_reals/edistr.v | 103 ++++++ experimental_reals/realsum.v | 81 ++++- rocq-mathcomp-experimental-reals.opam | 1 + theories/esum.v | 442 ++++++++++++++++++++++++++ 6 files changed, 855 insertions(+), 2 deletions(-) create mode 100644 experimental_reals/edistr.v diff --git a/_CoqProject b/_CoqProject index 431cbb08bc..ce426735af 100644 --- a/_CoqProject +++ b/_CoqProject @@ -39,6 +39,7 @@ experimental_reals/discrete.v experimental_reals/realseq.v experimental_reals/realsum.v experimental_reals/distr.v +experimental_reals/edistr.v reals_stdlib/Rstruct.v reals_stdlib/nsatz_realtype.v diff --git a/experimental_reals/distr.v b/experimental_reals/distr.v index 26f82b3ef8..2bbac0aae7 100644 --- a/experimental_reals/distr.v +++ b/experimental_reals/distr.v @@ -8,6 +8,7 @@ From mathcomp Require Import all_ssreflect_compat all_algebra. From mathcomp.classical Require Import boolp classical_sets mathcomp_extra. From mathcomp Require Import xfinmap constructive_ereal reals discrete. From mathcomp Require Import realseq realsum. +From mathcomp Require Import fsbigop. Set Implicit Arguments. Unset Strict Implicit. @@ -1266,3 +1267,231 @@ End Jensen. Notation convex f := (convexon \-inf \+inf f). (* -------------------------------------------------------------------- *) + +Section mono. + Context + {R : realType} + {T : choiceType} + {f : nat -> distr R T} + (hmono : (forall n m : nat, (n <= m)%N -> forall x : T, f n x <= f m x)). + + Lemma cvg_f: forall x, exists l, ncvg (fun n => f n x) l%:E. + Proof. + move=> x; apply: ncvg_mono_bnd; first by move=> *; apply: hmono. + apply/asboolP/nboundedP => /=; exists 2%:R => //. + move=> n; rewrite ger0_norm ?ge0_mu //; apply: (@le_lt_trans _ _ 1%:R). + - by apply: le1_mu1. + by apply: ltr_nat. + Qed. + + Lemma cvg_l : exists l, forall x, ncvg (fun n => f n x) (l x)%:E. + Proof. + have wtn: forall x, exists l, `[< ncvg (fun n => f n x) l%:E >]. + - by move=> x; apply/exists_asboolP/asboolP/cvg_f. + exists (fun x => xchoose (wtn x)) => x. + by apply/asboolP/(xchooseP (wtn x)). + Qed. +End mono. + +Section mono_sum. + Context + {R : realType} + {T : choiceType} + {f : nat -> distr R T} + (hmono : (forall n m : nat, (n <= m)%N -> forall x : T, f n x <= f m x)). + + Lemma mono_psum_Efn (E: T -> R): + (forall m, 0 <= E m)%R -> + (forall n, summable (fun x => E x * f n x)) -> + forall m n, (m <= n)%N -> + psum (fun x => E x * f m x) <= psum (fun x => E x * f n x). + Proof. + move=> hE smb_Efn m n le_mn. + apply /le_psum /smb_Efn. + move => x; rewrite mulr_ge0 //=. + by apply: ler_pM => //; apply: hmono. + Qed. + + Lemma ncvg_lp (E: T -> R) r: + (forall m, 0 <= E m)%R -> + (forall n, summable (fun x => E x * f n x)) -> + (forall n : nat, psum (fun x => E x * f n x) <= r) -> + exists lp, ncvg (fun n => psum (fun x => E x * f n x)) lp%:E. + Proof. + move => He smb_Efn h. + have hr : (0 <= r)%R. + - apply: (le_trans (y:= psum (fun x => E x * f 0 x))). + - by apply: ge0_psum. + by apply: h. + apply: ncvg_mono_bnd ; first by apply: mono_psum_Efn. + apply/asboolP/nboundedP => /=. + exists (r + 1). + - by apply ltr_wpDl. + move => n; rewrite ger0_norm 1?ge0_psum //; apply/(le_lt_trans (y := r)). + - apply h. + by apply ltr_pwDr. + Qed. + + Lemma sum_dlim_r [E : T -> R] [r : R]: + summable E -> + (forall m, 0 <= E m)%R -> + (forall (n : nat), psum (fun x : T => E x * f n x) <= r)%R -> + (psum (fun x : T => E x * (\dlim_(n) f n) x) <= r)%R. + Proof. + move => smb_E hE h. + have [l cvgfx]:= @cvg_l R T f hmono. + have ge0_l: forall x, 0 <= l x. + - by move=> x; apply: (ncvg_geC _ (cvgfx x)) => n; apply: ge0_mu. + have cvgEfx: forall x, ncvg (fun n => E x * f n x) (E x * l x)%:E. + - by move=> x; apply/ncvgZ. + rewrite (@eq_psum _ _ _ (fun x => fine (nlim (fun n => E x * f n x)))). + - move => x /=; rewrite dlimE (nlimE (cvgfx x)) /=. + by have /(ncvgZ (c := E x)) /nlimE -> /= := cvgfx x. + rewrite (@eq_psum _ _ _ (fun x => E x * l x)). + - by move=> x /=; have /(ncvgZ (c := E x)) /nlimE -> := cvgfx x. + apply: psum_le => J uqJ. + have ncvgJ: ncvg (fun n => \sum_(j <- J) E j * f n j) (\sum_(j <- J) E j * (l j))%:E. + - by apply: (ncvg_mono_sum cvgEfx). + have smb_Efn: forall n, summable (fun x => E x * f n x). + - move=> n; apply summableM. + exact: smb_E. + apply summable_mu. + have [lp ncvg_lp] := @ncvg_lp _ r hE smb_Efn h. + have le1_lp: lp <= r. + - apply: (@ncvg_leC _ r _ _ _ ncvg_lp). + exact : h. + apply: (le_trans (y :=fine (nlim (fun n : nat => \sum_(j <- J) E j * f n j)))). + - rewrite (nlimE ncvgJ) /=; apply: ler_sum => x _. + rewrite ger0_norm; auto. + by apply mulr_ge0. + rewrite (nlimE ncvgJ) /=. + apply (le_trans (y:= lp)). + - apply: (ncvg_le _ ncvg_lp ncvgJ) => n. + apply/(le_trans _): (ger_big_psum uqJ (smb_Efn n)). + by apply/ler_sum => x _; apply/ler_norm. + exact: le1_lp. + Qed. + + Lemma sum_dlim (E : pred T) : + psum (fun x : T => (E x)%:R * (\dlim_(n) f n) x) = + fine (nlim (fun n => psum (fun x : T => (E x)%:R * f n x))). + Proof. + have [l cvgfx]:= @cvg_l R T f hmono. + have cvgEfx: forall x, ncvg (fun n => (E x)%:R * f n x) ((E x)%:R * l x)%:E. + - by move=> x; apply/ncvgZ. + have ge0_l: forall x, 0 <= l x. + - by move=> x; apply: (ncvg_geC _ (cvgfx x)) => n; apply: ge0_mu. + transitivity (psum (fun x => fine (nlim (fun n => (E x)%:R * f n x)))). + - apply: eq_psum => x /=; rewrite dlimE (nlimE (cvgfx x)) /=. + by have /(ncvgZ (c := (E x)%:R)) /nlimE -> /= := cvgfx x. + transitivity (psum (fun x => (E x)%:R * l x)); first apply: eq_psum. + - by move=> x /=; have /(ncvgZ (c := (E x)%:R)) /nlimE -> := cvgfx x. + have smb_Efn: forall n, summable (fun x => (E x)%:R * f n x). + - by move=> n; apply: (summable_pr E (f n)). + have le1_psum_Efn: forall n, psum (fun x => (E x)%:R * f n x) <= 1. + - by move=> n; apply/le1_pr. + have hE: forall x : T, 0 <= (E x)%:R. by auto. + have [lp ncvg_lp] := @ncvg_lp _ _ (hE R) smb_Efn le1_psum_Efn. + have le1_lp: lp <= 1. + - by move/ncvg_leC: ncvg_lp; apply; apply/le1_psum_Efn. + have smb_Ef: summable (fun x => (E x)%:R * l x). + - exists 1 => J; rewrite -(finmap.big_seq_fsetE _ _ predT (fun x => `|(E x)%:R * l x|)) /=. + apply: (le_trans (y := \sum_(x <- finmap.enum_fset J) (l x))). + - apply: ler_sum => /= j _; rewrite ger0_norm 1?mulr_ge0 //. + by apply: ler_piMl => //; case: (E _). + have: ncvg (fun n => \sum_(x <- finmap.enum_fset J) (f n x)) (\sum_(x <- finmap.enum_fset J) l x)%:E. + - by apply: ncvg_mono_sum. + move/ncvg_leC => /(_ 1); apply => n /=. + have /gerfin_psum := summable_mu (f n) => /(_ J). + move/le_trans => /= /(_ _ (le1_mu (f n))); apply/le_trans. + by rewrite finmap.big_seq_fsetE; apply: ler_sum => j _ /=; apply/ler_norm. + apply/eqP; rewrite eq_le; apply/andP; split. + - apply: psum_le => J uqJ. + have ncvgJ: + ncvg (fun n => \sum_(j <- J) (E j)%:R * f n j) (\sum_(j <- J) (E j)%:R * (l j))%:E. + - by apply: (ncvg_mono_sum cvgEfx). + apply: (le_trans (y := fine (nlim (fun n => \sum_(j <- J) (E j)%:R * f n j)))); last first. + - rewrite (nlimE ncvgJ) (nlimE ncvg_lp) /=. + apply: (ncvg_le _ ncvg_lp ncvgJ) => n. + apply/(le_trans _): (ger_big_psum uqJ (smb_Efn n)). + by apply/ler_sum => x _; apply/ler_norm. + rewrite (nlimE ncvgJ) /=; apply: ler_sum => x _. + by rewrite ger0_norm // mulr_ge0. + - rewrite (nlimE ncvg_lp) /=; apply: (ncvg_leC _ ncvg_lp) => n. + apply: le_psum => // x; rewrite mulr_ge0 //=. + apply: ler_pM => //; apply: (ncvg_homo_le _ (cvgfx x)). + by move=> *; apply: hmono. + Qed. + +End mono_sum. + +From mathcomp Require Import ereal esum. + +Section mono_esum. + Context + {R : realType} + {T : choiceType} + {f : nat -> distr R T} + (hmono : (forall n m : nat, (n <= m)%N -> forall x : T, f n x <= f m x)). + + Lemma mono_esum_Efn (E: T -> \bar R): + (forall m, 0 <= E m)%E -> + forall m n, (m <= n)%N -> + (esum [set:T] (fun x => E x * (f m x)%:E) <= + esum [set:T] (fun x => E x * (f n x)%:E))%E. + Proof. + move=> hE m n le_mn. + apply /esum.le_esum. + move => ??; rewrite lee_pmul => //=. + - rewrite lee_tofin //. + - rewrite lee_tofin //; exact: hmono. + Qed. + + Lemma ncvg_dlim a : ncvg (fun n : nat => f n a) ((\dlim_(n) f n) a)%:E. + Proof. + case : (dlimP (fun n => f n) a) => [l _ _ h | habs] //. + exfalso; apply habs. + apply dcvg_homo => n m hnm b. + by rewrite hmono. + Qed. + + Lemma ereal_sup_sup a : + ereal_sup (range (fun n => (f n a)%:E)) = (sup ([set r | exists n, r = (f n a) ]))%:E. + Proof. + rewrite -ereal_sup_EFin. + - exists 1%R => r //= [n ->]; exact: le1_mu1. + - exists (f 0%N a); exists 0%N => //. + - congr ereal_sup. + apply /seteqP; split. + - by move => p [n _ hn]; exists (f n a) => //; exists n. + - by move => x [_ [n ->] <- ] //=; exists n. + Qed. + + Lemma distr_lub_sup a : + ((dlim f) a)%:E = ereal_sup (range (fun n => (f n a)%:E)). + Proof. + unfold image. + rewrite ereal_sup_sup. + apply /ereal_eqP /eqP /esym; apply :nlim_sup. + - by move => n m h; rewrite hmono. + - exact: ncvg_dlim. + Qed. + + Lemma esum_dlim_r [E : T -> \bar R] [r : \bar R]: + (forall m, 0 <= E m)%E -> + (forall (n : nat), esum [set:T] (fun x : T => E x * (f n x)%:E) <= r)%E -> + (esum [set:T] (fun x : T => E x * ((\dlim_(n) f n) x)%:E) <= r)%E. + Proof. + move => hE h. + rewrite (@esum.eq_esum _ _ _ _ (fun x => ereal_sup (range (fun n => E x * (f n x)%:E)%E))). + - move => ??; rewrite distr_lub_sup. + rewrite (@esupZl_range R T (fun a b => (f b a)%:E)) //. + move => ??; rewrite lee_tofin //. + rewrite esum_esup_comm //. + - by move => ??; rewrite mule_ge0 // lee_tofin. + - by move => ????; rewrite lee_pmul // ?lee_tofin // hmono. + rewrite ge_ereal_sup//= => x [n s] <-. + apply h. + Qed. + +End mono_esum. diff --git a/experimental_reals/edistr.v b/experimental_reals/edistr.v new file mode 100644 index 0000000000..e909f369b0 --- /dev/null +++ b/experimental_reals/edistr.v @@ -0,0 +1,103 @@ +From mathcomp Require Import all_boot all_order all_algebra. +From mathcomp.classical Require Import boolp fsbigop. +From mathcomp Require Import xfinmap constructive_ereal reals discrete realseq. +From mathcomp.classical Require Import classical_sets functions. +From mathcomp.experimental_reals Require Import realsum distr. +From mathcomp.analysis Require Import esum ereal. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Unset SsrOldRewriteGoalsOrder. + +Import Order.TTheory GRing.Theory Num.Theory. + +Local Open Scope fset_scope. +Local Open Scope ring_scope. + +(* -------------------------------------------------------------------- *) +Reserved Notation "\Ee_[ mu ] f" (at level 2, format "\Ee_[ mu ] f"). + +Section Esp. + Context {R : realType} {T : choiceType}. + + Implicit Types (mu : {distr T / R}) (f : T -> \bar R). + + Definition espe mu f := sum (fun x => mule (f x) ((mu x)%:E)). + + Notation "\Ee_[ mu ] f" := (espe mu f). +End Esp. + +Section PrCoreTheory. + Context {R : realType} {T : choiceType}. + + Implicit Types (mu : {distr T / R}) (A B E : pred T). + + Lemma exp_dunit (f : T -> \bar R) (x : T) : + espe (dunit x) f = f x. + Proof. + rewrite /espe. + rewrite (@eq_sum _ _ _ (fun y : T => if x == y then f y else 0%R)%E). + + move => x0. rewrite dunit1E. + by case (x == x0) => //=; rewrite ?mule1 ?mule0. + by rewrite sum_unit. + Qed. + + Lemma exp_cst mu r : (espe mu (fun _ => r) = (\P_[mu] predT)%:E * r)%E. + Proof. + rewrite pr_predT psum_sum /espe //. + rewrite sumZ. + - move => ?. rewrite lee_fin //. + by rewrite sum_sum // muleC. + Qed. + + Lemma exp0 mu : espe mu (fun _ => 0) = 0. + Proof. by rewrite exp_cst mule0. Qed. + + Lemma exp_dlet {U: choiceType} mu (nu : T -> {distr U / R}) F : + (forall x, 0%:E <= F x)%E -> + espe (dlet nu mu) F = espe mu (fun x => espe (nu x) F). + Proof. + move => HF. + have pos : (forall (i : T) (j : U), (0%R <= F j * ((mu i)%:E * (nu i j)%:E))%E). + - move => i j; rewrite mule_ge0 //. + by rewrite mule_ge0 // lee_tofin. + rewrite /espe. + rewrite (eq_sum + (S1:=fun x : U => (F x * ((\dlet_(i <- mu) nu i) x)%:E)%E) + (S2:=fun x : U => (F x * esum [set:T] (fun y : T => (mu y * nu y x)%:E)))%E). + - move => x; rewrite dletE. + congr ( _ * _)%E. + rewrite -esum_psum //. + - by move => i; rewrite mulr_ge0. + - apply/(le_summable (F2 := mu)) => //. + by move=> x0; rewrite mulr_ge0 //= ler_piMr ?le1_mu1. + symmetry. + rewrite (eq_sum + (S1:=(fun x : T => (sum (fun x0 : U => F x0 * (nu x x0)%:E) * (mu x)%:E)%E)) + (S2:=(fun x : T => (esum [set:U] (fun x0 : U => F x0 * ((mu x)%:E * (nu x x0)%:E))%E)))). + - move => x; rewrite muleC. + rewrite -sumZ. + - move => x1; rewrite mule_ge0 //=. + - exact: (ge0_mu (nu x) x1). + rewrite (eq_sum + (S1:=(fun x0 : U => (mu x)%:E * (F x0 * (nu x x0)%:E))%E) + (S2:=(fun x0 : U => F x0 * ((mu x)%:E * (nu x x0)%:E))%E)) //. + - by move => ?; rewrite muleCA. + rewrite esum_sum' //. + rewrite esum_sum'. + - by move => ?; rewrite esum_ge0 //. + rewrite esum_esum' //. + rewrite esum_sum'. + - move => ?; rewrite mule_ge0 // esum_ge0 //. + by move => ??; rewrite lee_tofin // mulr_ge0. + rewrite {1}(eq_esum + (b:= fun x => (F x * (\esum_(y in [set: T]) (mu y * nu y x)%:E))%E)) //. + - move => ??. rewrite esumZ //. + by move => ?; rewrite mule_ge0 // lee_tofin. + Qed. + + (* Lemma expZ mu F c : \E_[mu] (c \*o F) = c * \E_[mu] F. *) + (* Proof. by rewrite -sumZ; apply/eq_sum=> x /=; rewrite mulrA. Qed. *) + +End PrCoreTheory. diff --git a/experimental_reals/realsum.v b/experimental_reals/realsum.v index 267b1b7688..fbda74147c 100644 --- a/experimental_reals/realsum.v +++ b/experimental_reals/realsum.v @@ -3,12 +3,13 @@ (* Copyright (c) - 2015--2018 - Inria *) (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From mathcomp Require Import all_ssreflect_compat all_algebra. +From mathcomp Require Import all_boot all_order all_algebra. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp.classical Require Import boolp. +From mathcomp.classical Require Import boolp fsbigop. From mathcomp Require Import xfinmap constructive_ereal reals discrete realseq. From mathcomp.classical Require Import classical_sets functions. +From mathcomp.analysis Require Import esum ereal. Set Implicit Arguments. Unset Strict Implicit. @@ -194,6 +195,18 @@ case/(_ (NPInf M)): cu => K /= /(_ K (leqnn _)). rewrite inE/= => /ltW /le_trans /(_ (ler_norm _)). by move/le_lt_trans/(_ (bdu _)); rewrite ltxx. Qed. + +Lemma ncvg_mono_sum {T : eqType} [f : nat -> T -> R] [l : T -> R] [J : seq T] : + (forall x, ncvg (fun n => f n x) (l x)%:E) -> + ncvg (fun n => \sum_(x <- J) f n x) (\sum_(x <- J) l x)%:E. +Proof. +move=> hcvg; elim: J => //= [|j J ih]. +- rewrite big_nil; apply/(@ncvg_eq _ (fun _ => 0))/ncvgC. + by move=> n /=; rewrite big_nil. +- rewrite big_cons; have := ncvgD (hcvg j) ih; apply/ncvg_eq. + by move=> n /=; rewrite big_cons. +Qed. + End PosCnv. (* -------------------------------------------------------------------- *) @@ -343,6 +356,47 @@ by case=> /= [|J lt_lJ _]; [apply/summable_sup | exists J]. Qed. End SumTh. +(* -------------------------------------------------------------------- *) +Section Esum. + + Context {R : realType} {T : choiceType}. + + Lemma esum_psum (S: T -> R) : + (forall i : T, 0%R <= S i) -> + summable S -> + esum [set:T] (fun x => (S x)%:E) = (psum S)%:E. + Proof. + move => Sg0 h; apply/eqP; rewrite eq_le; apply/andP; split. + - rewrite ge_ereal_sup//= => x [] X [] finX XT. + rewrite fsumEFin // => <-. + rewrite lee_fin. + rewrite fsbig_finite //=. + revert finX. + rewrite cardinality.finite_fsetP. + move => [] J ->. + rewrite cardinality.set_fsetK. + apply: (le_trans _ (gerfin_psum J h)). + rewrite -(@big_fset_seq R _ _ T J S) //=. + apply: (le_trans _ (ler_norm_sum _ _ _)). + exact : ler_norm. + - rewrite (eq_esum (b:= fun x => `| S x |%:E)%E). + - by move => ??; rewrite ger0_norm. + have [H1 H3] := (summable_sup h). + rewrite psum_absE //. + rewrite -(ereal_sup_EFin H3 H1). + rewrite ge_ereal_sup//= => x [] X [] Fs XT <-. + rewrite esum_ge //. + exists ([set` Fs]%classic) => //. + rewrite fsumEFin //. + rewrite lee_fin. + rewrite XT. + rewrite (@big_fset_seq R _ _ T _ (fun x => `|S x|)) //=. + rewrite -{1}(cardinality.set_fsetK Fs). + by rewrite -fsbig_finite. + Qed. + +End Esum. + (* -------------------------------------------------------------------- *) Lemma max_sup {R : realType} x (E : set R) : (E `&` ubound E)%classic x -> sup E = x. @@ -694,6 +748,29 @@ Qed. End SummableAlg. +(* -------------------------------------------------------------------- *) +Section Sum_Sum. + Context {T: choiceType} {R : realType}. + + Lemma sum_sum (S: T -> R) : + summable S -> + esum.sum (fun x => (S x)%:E) = (sum S)%:E. + Proof. + move => hs. rewrite /esum.sum /sum. + rewrite (eq_esum (a:= esum.fpos (fun x => (S x)%:E)) (b:= fun x => (fpos S x)%:E)). + - by move => ??; rewrite /esum.fpos /fpos -fine_max. + rewrite (eq_esum (a:= esum.fneg (fun x => (S x)%:E)) (b:= fun x => (realsum.fneg S x)%:E)). + - by move => ??; rewrite /esum.fneg /fneg -fine_min. + rewrite esum_psum //. + - move => ?. rewrite /realsum.fpos. exact : normr_ge0. + - exact : summable_fpos. + rewrite esum_psum //. + - move => ?. rewrite /realsum.fneg. exact : normr_ge0. + - exact : summable_fneg. + Qed. + +End Sum_Sum. + (* -------------------------------------------------------------------- *) Section StdSum. Context {R : realType} (T : choiceType) (I : Type). diff --git a/rocq-mathcomp-experimental-reals.opam b/rocq-mathcomp-experimental-reals.opam index 83179674dd..234d011a17 100644 --- a/rocq-mathcomp-experimental-reals.opam +++ b/rocq-mathcomp-experimental-reals.opam @@ -19,6 +19,7 @@ build: [make "-C" "experimental_reals" "-j%{jobs}%"] install: [make "-C" "experimental_reals" "install"] depends: [ "rocq-mathcomp-reals" { = version} + "rocq-mathcomp-analysis" { = "dev"} "rocq-mathcomp-bigenough" { (>= "1.0.0") } ] diff --git a/theories/esum.v b/theories/esum.v index 486d54a46f..ea2b226aad 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -100,6 +100,21 @@ Proof. by move=> ?; rewrite esum_fset// ?fset_set1// ?fsbig_set1// => t' /[!inE] ->. Qed. +Lemma esum_pos_e a: + ((forall i : T, 0%R <= a i) -> + (0%R = \esum_(x in [set: T]) a x) -> + forall x: T, 0%R = a x)%E. +Proof. + move => hi hs x. + apply/eqP;rewrite eq_le; apply/andP; split. + + by apply hi. + + rewrite hs. + apply ereal_sup_ubound => //=. + rewrite -esum_set1 //. + exists [set x]%classic => //. + by rewrite esum_fset. +Qed. + End esum_realType. Lemma esum1 [R : realFieldType] [I : choiceType] (D : set I) (a : I -> \bar R) : @@ -129,6 +144,46 @@ Lemma eq_esum [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) : \esum_(i in I) a i = \esum_(i in I) b i. Proof. by move=> e; apply/eqP; rewrite eq_le !le_esum// => i Ii; rewrite e. Qed. +Lemma esumZ [R : realType] [T : choiceType] S (c : \bar R) : + (0 <= c -> (forall i : T, 0 <= S i) -> + esum [set:T] (fun x => c * (S x)) = c * (esum [set:T] S))%E. +Proof. + rewrite le_eqVlt => /orP[/eqP<-|cgt0]. + - by rewrite mul0e esum1 // => ??; rewrite mul0e. + move => Sg0; apply/eqP; rewrite eq_le; apply/andP; split. + - rewrite ge_ereal_sup//= => x [X [finX XI]] <-. + setoid_rewrite <- (@ge0_mule_fsumr _ _ c S X Sg0). + rewrite lee_pmul //. + + by rewrite ltW. + + by rewrite fsume_ge0 //. + + by rewrite ereal_sup_ubound //=; exists X. + - revert cgt0. + case c => //. + + move => s hs. + rewrite -lee_pdivlMl //. + rewrite ge_ereal_sup//= => _ [X [finX XI]] <-. + rewrite lee_pdivlMl //. + rewrite ge0_mule_fsumr //. + by rewrite ereal_sup_ubound //=; exists X. + + move => h. + have he: (0 <= \esum_(x in [set: T]) S x)%E. + - by apply esum_ge0; move => ??; apply Sg0. + rewrite le_eqVlt in he;revert he. + move => /orP [/eqP Sgt0|Sgt0]. + + rewrite -Sgt0 mule0. + rewrite (eq_esum (b := (fun _ => 0)%E)). + - by intros ??; rewrite -(esum_pos_e (a:= S)) // mule0. + by rewrite esum1. + + rewrite gt0_mulye //. + have [y [H ? ? ?]] := (ereal_sup_gt Sgt0). + rewrite leye_eq; apply/eqP /eq_infty => y'; rewrite esum_ge//. + exists H; move => //. + rewrite -ge0_mule_fsumr //. + subst. + rewrite gt0_mulye //. + by rewrite leey. +Qed. + Lemma esumD [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) : (forall i, I i -> 0 <= a i) -> (forall i, I i -> 0 <= b i) -> \esum_(i in I) (a i + b i) = \esum_(i in I) a i + \esum_(i in I) b i. @@ -356,6 +411,23 @@ by rewrite -fsbig_finite//; apply: eq_fsbigr=> x /[!inE]/XQ ?; rewrite invK ?inE Qed. Arguments reindex_esum {R T T'} P Q e a. +Lemma esum_esum' [R : realType] [T U : choiceType] (f: T -> U -> \bar R): + (forall i j, (0%R <= f i j)%E) -> + esum [set:T] (fun x => esum [set:U] (fun y => f x y)) = + esum [set:U] (fun y => esum [set:T] (fun x => f x y)). +Proof. + move => h. + rewrite !esum_esum //=. + rewrite /setXR. + rewrite (reindex_esum + (fun z=> [set: U]%classic z.1 /\ [set: T]%classic z.2) + (fun z => [set: T]%classic z.1 /\ [set: U]%classic z.2) + (fun x => (x.2, x.1))) //=. + - split => //=. + by move=> [i1 i2] [j1 j2] /= _ _ [] -> ->. + by move=> [i1 i2] [Pi1 Qi2] /=; exists (i2, i1). +Qed. + Section nneseries_interchange. Local Open Scope ereal_scope. @@ -665,3 +737,373 @@ by rewrite ge0_esum_posneg// ge0_esum_posneg// => /eqP ->. Qed. End esumB. + + +(* This should go to ereal*) +Section Ereal. + Context {R : realType}. + + Definition esg (x: \bar R) : \bar R := + (if x == 0 then 0 else if x < 0 then -1 else 1)%E. + + Lemma numEsg (x : \bar R): (x = esg x * `|x|)%E. + Proof. + rewrite /esg. + case (comparable_ltgtP (comparableT x 0)%E) => h. + + by rewrite (lt_eqF h) h lte0_abs // muleNN mul1e. + + by rewrite (gt_eqF h) (lt_gtF h) gte0_abs // mul1e. + + by rewrite h eq_refl mul0e. + Qed. + + Lemma gte0_esg (x : \bar R): (x < 0 -> esg x = -1)%E. + Proof. + by move => h; rewrite /esg (lt_eqF h) h. + Qed. + + Lemma lte0_esg (x : \bar R): (0 < x -> esg x = 1)%E. + Proof. + by move => h; rewrite /esg (gt_eqF h) (lt_gtF h). + Qed. + + Lemma esg0 : (esg 0 = 0)%E. + Proof. + by rewrite /esg eq_refl. + Qed. + +End Ereal. + + +Section Sum. + Context {R : realType} {T : choiceType}. + + Implicit Types f (* g *) : T -> \bar R. + +(* Use the following function (numfun.funepos.body f \+ numfun.funeneg.body f)%E *) + + Definition fpos f := fun x => `|maxe 0%E (f x)|%E. + Definition fneg f := fun x => `|mine 0%E (f x)|%E. + + Lemma min_l (x y : \bar R) : (x <= y -> mine x y = x)%E. Proof. by case: comparableP. Qed. + + Lemma min_r (x y : \bar R) : (y <= x -> mine x y = y)%E. Proof. by case: comparableP. Qed. + + Lemma max_l (x y : \bar R) : (y <= x -> maxe x y = x)%E. Proof. by case: comparableP. Qed. + + Lemma max_r (x y : \bar R) : (x <= y -> maxe x y = y)%E. Proof. by case: comparableP. Qed. + + Lemma fneg_ge0 f x : (forall x, 0%R <= f x)%E -> fneg f x = 0. + Proof. by move => ?; rewrite /fneg min_l ?abse0. Qed. + + Lemma fpos_ge0 f x : (forall x, 0%R <= f x )%E -> fpos f x = f x. + Proof. by move=> ?; rewrite /fpos max_r ?gee0_abs. Qed. + + Lemma fpos0 x : fpos (fun _ : T => 0) x = 0. + Proof. by rewrite /fpos /maxe ltxx abse0. Qed. + + Lemma fneg0 x : fneg (fun _ : T => 0) x = 0. + Proof. by rewrite /fneg /mine ltxx abse0. Qed. + + Lemma fnegN f : (fneg (\- f ) =1 fpos f)%E. + Proof. by move => x; rewrite /fpos /fneg -{1}oppe0 -oppe_max abseN. Qed. + + Lemma fposN f : (fpos (\- f ) =1 fneg f)%E. + Proof. by move=> x; rewrite /fpos /fneg -{1}oppe0 -oppe_min abseN. Qed. + + Lemma le_fpos f1 f2 : ((forall x, f1 x <= f2 x) -> (forall x, fpos f1 x <= fpos f2 x))%E. + Proof. + move=> le_f x; rewrite /fpos !gee0_abs ?le_max ?lexx //. + by rewrite ge_max lexx /=; case: ltP => //=; rewrite le_f. + Qed. + + Definition sum f : \bar R := esum [set:T] (fpos f) - esum [set:T] (fneg f). +End Sum. + +Section SumTheory. + Context {R : realType} {T : choiceType}. + Implicit Types (S : T -> \bar R). + + Lemma sum0 : @sum R _ (fun _ : T => 0%E) = 0%E. + Proof. + rewrite /sum esum1. + + by move => ??; rewrite max_l; [| rewrite abse0]. + by rewrite sube0. + Qed. + + Lemma eq_sum S1 S2: S1 =1 S2 -> sum S1 = sum S2. + Proof. + move=> eq_fg; rewrite /sum. + rewrite (eq_esum (a:= fpos S2) (b:= fpos S1)). + - by move => ??; rewrite /fpos eq_fg. + rewrite (eq_esum (a:= fneg S2) (b:= fneg S1)). + - by move => ??; rewrite /fneg eq_fg. + by idtac. + Qed. + + Lemma esum_unit S x : + esum [set:T] (fun y => if x == y then S y else 0) = \esum_(i in [set x]) S i. + Proof. + rewrite (esum_mkcond [set x] S). + apply eq_esum => i ? //=. + by case_eq (x == i);rewrite eq_sym -in_fset1 -cardinality.fset_set1 + cardinality.in_fset_set => //= ->. + Qed. + + Lemma sum_unit S x : sum (fun y => if x == y then S y else 0) = S x. + Proof. + rewrite /sum. + rewrite (@eq_esum _ _ _ (fpos _) (fun y : T => if x == y then fpos S y else 0%R)). + + move => i ? ; rewrite /fpos /maxe => //=. + case (x == i) => //=. + by case (_ < _)%E; rewrite abse0. + rewrite (@eq_esum _ _ _ (fneg _) (fun y : T => if x == y then fneg S y else 0%R)). + + move => i ? ; rewrite /fneg /mine => //=. + case (x == i) => //=. + by case (_ < _)%E; rewrite abse0. + rewrite !esum_unit. + case (comparable_ltP (comparableT (S x) 0)%E) => h;last first. + + rewrite esum_set1. + + by rewrite /fpos max_r ?gee0_abs. + rewrite esum1. + + by move => i //= ->; rewrite /fneg min_l ?gee0_abs. + by rewrite /fpos max_r ?gee0_abs ?sube0. + rewrite esum1. + + by move => i //= ->; rewrite /fpos max_l ?abse0 => //=; apply ltW. + rewrite esum_set1. + + by rewrite /fneg min_r ?lte0_abs ?oppe_ge0 => //=; apply ltW. + rewrite /fneg min_r. + + by apply ltW. + rewrite lte0_abs ?sub0e => //=. + by apply (eqe_oppLRP (- (S x))). + Qed. + + Section SumTheoryP. + + Lemma esum_sum' S : (forall x, 0%:E <= S x)%E -> sum S = esum [set:T] S. + Proof. + move=> ge0_S; rewrite /sum. rewrite (@esum1 R T [set:T] (fneg S)). + + by move => x ?; rewrite fneg_ge0. + by rewrite sube0; apply eq_esum => x ?; rewrite fpos_ge0. + Qed. + + Lemma sum_pos S : (forall x, 0%:E <= S x)%E -> (0%R <= sum S)%E. + Proof. + by move=> ge0_S; rewrite esum_sum' // esum_ge0. + Qed. + + Lemma le_sum S1 S2: + ((forall x, 0%:E <= S1 x) -> + (forall x, 0%:E <= S2 x) -> + (forall x, S1 x <= S2 x) -> + sum S1 <= sum S2)%E. + Proof. + move=> pS1 pS2 leS. rewrite /sum leeB //. + + apply le_esum. + by move => ??; rewrite !fpos_ge0. + apply le_esum. + by move => ??; rewrite !fneg_ge0. + Qed. + + Lemma sumN S : + (forall x, 0%:E <= S x)%E -> + (sum (\- S ) = - sum S)%E. + Proof. + move => h; rewrite /sum. + rewrite (eq_esum (a:=fpos _) (b:=fun _ : T => 0%E)). + + by move => ?? ; rewrite fposN fneg_ge0. + rewrite (eq_esum (a:= fneg S) (b:= fun _ : T => 0%E)). + + by move => ?? ; rewrite fneg_ge0. + rewrite (eq_esum (a:=fneg (\- S)%E) (b:=fpos S)). + + by move => ?? ; rewrite fnegN. + rewrite esum1 => //=. + by rewrite sube0 sub0e. + Qed. + + Lemma sumZ S c : + (forall x, 0%:E <= S x)%E -> + (sum (fun x => mule c (S x)) = mule c (sum S))%E. + Proof. + move => h. + rewrite (eq_sum (S2 := fun x => esg c * (`|c| * S x))%E). + by move=> x ; rewrite muleA -numEsg. + transitivity (esg c * sum (fun x => `|c| * (S x)))%E. + - case (comparable_ltgtP (comparableT c 0)%E) => hc. + + rewrite {1}lte0_abs // gte0_esg //. + rewrite (eq_sum (S2 := fun x : T => (- (- c * S x))%E)). + - by move => ?; rewrite mulN1e. + rewrite mulN1e -sumN;[|rewrite lte0_abs //]. + by move => ?; rewrite mule_ge0. + + rewrite gte0_abs // lte0_esg // mul1e. + rewrite (eq_sum (S2 := fun x : T => ( c * S x)%E)). + - by move => ?; rewrite mul1e. + by idtac. + + rewrite hc esg0 mul0e. + rewrite (eq_sum (S2 := fun _ : T => 0%E)). + - by move => ?; rewrite mul0e. + by rewrite sum0. + - rewrite {1}/sum. + rewrite (eq_esum (a:= fpos _) (b:= (fun x : T => `|c| * S x)%E)). + + by move => ??; rewrite fpos_ge0 // => x; rewrite mule_ge0. + rewrite (eq_esum (a:=fneg _) (b:=fun _ : T => 0%E)). + + by move => ?? ; rewrite fneg_ge0 // => x; rewrite mule_ge0. + rewrite (esum1 (a:= fun _ => 0%E)) // sube0. + by rewrite esumZ // muleA -numEsg esum_sum'. + Qed. + + End SumTheoryP. + + Section SumTheoryS. + + Lemma le_sum_s S1 S2 : + (summable [set:T] S1 -> summable [set : T] S2 -> + (forall x, S1 x <= S2 x) -> + sum S1 <= sum S2)%E. + Proof. + move=> smS1 smS2 leS; rewrite /sum leeB //. + + by apply le_esum => ??; apply le_fpos. + apply le_esum => ??. + rewrite -!fposN. apply le_fpos => ?. + by rewrite leeN2. + Qed. + + End SumTheoryS. + +End SumTheory. + +Lemma ereal_sup_comm {R:realType} {X Y : Type} (f : X -> Y -> \bar R) (A : set X) (B : set Y) : + ereal_sup [set ereal_sup [set f x y | y in B] | x in A] = + ereal_sup [set ereal_sup [set f x y | x in A] | y in B]. +Proof. + suff key : forall (X' Y' : Type) (g : X' -> Y' -> \bar R) (C : set X') (D : set Y'), + ereal_sup [set ereal_sup [set g x y | y in D] | x in C] <= + ereal_sup [set ereal_sup [set g x y | x in C] | y in D]. + apply: le_anti. apply/andP; split; [exact: key | exact: (key _ _ (fun y x => f x y) B A)]. + move=> X' Y' g C D. + apply/ereal_supP => _ [x hx <-]. + apply/ereal_supP => _ [y hy <-]. + apply: le_ereal_sup_tmp; exists (ereal_sup [set g x0 y | x0 in C]). + - exists y => //. + - apply: le_ereal_sup_tmp; exists (g x y); [exists x => // | exact: le_refl]. +Qed. + + +Section mono_esum. + Context + {R : realType} + {T : choiceType} + {f : T -> nat -> \bar R} + {fpos : forall t n, 0 <= f t n} + (hmono : (forall n m : nat, (n <= m)%N -> forall x : T, f x n <= f x m)). + +Lemma esupZl (c : \bar R) (X : set \bar R): + 0 <= c -> + X != set0 -> + (forall x, X x -> 0 <= x) -> + ereal_sup [ set c * x | x in X ] = c * ereal_sup X. +Proof. +move=> cpos Xne Xpos. + have /set0P [x Xx] := Xne. + case: c cpos => [r|_|//]. + - move=> hr. + case: (eqVneq r 0%R) => [-> | rne0]. + + rewrite mul0e. + under eq_imagel => a _ do rewrite mul0e. + rewrite ereal_sup_cst //. + exact: ereal_supZl Xne hr. + - case: (boolp.pselect (forall a, X a -> a = 0)) => [hall | hnall]. + + have -> : [set +oo * x | x in X] = [set 0]. { + apply/seteqP; split. + + by move=> _ [z Xz <-]; rewrite (hall _ Xz) mule0 //. + + by move=> y /= ->; exists x => //; rewrite (hall _ Xx) mule0. + } + have -> : X = [set 0]. { + apply/seteqP; split. + + by move=> y Xy; rewrite (hall _ Xy)=> //. + + by move=> y /= ->; rewrite -(hall _ Xx) //. + } + by rewrite ereal_sup1 mule0. + + move: hnall; rewrite -boolp.existsNE. + move => [y /boolp.not_implyP [Xy hy] ]. + have ygt0: 0 < y by rewrite lt_def Xpos // andbT; apply/eqP. + rewrite gt0_mulye //. + - apply: (lt_le_trans ygt0); exact: ereal_sup_ubound. + apply: ereal_supy. exists y => //. exact: gt0_mulye. +Qed. + + Lemma esupZl_range (c : \bar R) (x : T) (cpos : 0 <= c) : + (c * ereal_sup (range (f x)) = + ereal_sup (range (fun n => c * f x n)))%E. + Proof. + have seteq : + [set c * y | y in range (f x)] = range (fun n => c * f x n). + apply/seteqP; split. + - by move=> _ [_ [n _ <-] <-]; exists n. + - by move=> _ [n _ <-]; exists (f x n) => //; exists n. + rewrite -seteq esupZl //. + - by apply/set0P; exists (f x 0%N), 0%N. + - by move=> _ [n _ <-]; exact: fpos. + Qed. + + Lemma esup_add (u v : nat -> \bar R) : + (forall n, 0 <= u n) -> (forall n, 0 <= v n) -> + nondecreasing_seq u -> nondecreasing_seq v -> + ereal_sup (range u) + ereal_sup (range v) = + ereal_sup (range (fun n => u n + v n)). + Proof. + move=> u0 v0 ndu ndv. + have su_ge0 : 0 <= ereal_sup (range u). + by rewrite (le_trans (u0 0%N))// ereal_sup_ubound//; exists 0%N. + have sv_ge0 : 0 <= ereal_sup (range v). + by rewrite (le_trans (v0 0%N))// ereal_sup_ubound//; exists 0%N. + have ndsum : nondecreasing_seq (fun n => u n + v n). + by move=> n m nm; apply: leeD; [exact: ndu | exact: ndv]. + have cuv_add : + (fun n => u n + v n) @ \oo --> + ereal_sup (range u) + ereal_sup (range v). + apply: cvgeD. + - by apply: ge0_adde_def; rewrite inE. + - exact: ereal_nondecreasing_cvgn. + - exact: ereal_nondecreasing_cvgn. + have cuv_sup : + (fun n => u n + v n) @ \oo --> + ereal_sup (range (fun n => u n + v n)). + exact: ereal_nondecreasing_cvgn. + exact: cvg_unique cuv_add cuv_sup. + Qed. + + Lemma ereal_sup_sum (A : {fset T}) : + \sum_(x <- A) ereal_sup (range (f x)) = + ereal_sup (range (fun n => \sum_(x <- A) f x n)). + Proof. + have key (l : seq T) : + \sum_(x <- l) ereal_sup (range (f x)) = + ereal_sup (range (fun n => \sum_(x <- l) f x n)). + elim: l => [|x xs IH]. + - rewrite big_nil. + under eq_fun => n do rewrite big_nil. + by rewrite ereal_sup_cst//; apply/set0P; exists 0%N. + - rewrite big_cons IH. + under [in RHS]eq_fun => n do rewrite big_cons. + apply: esup_add. + + by move=> n; exact: fpos. + + by move=> n; apply: sume_ge0 => y _; exact: fpos. + + by move=> n m nm; exact: hmono. + + by move=> n m nm; apply: lee_sum => y _; exact: hmono. + exact: key. + Qed. + + Lemma esum_esup_comm : + (\esum_(i in [set: T]) ereal_sup (range (f i)))%E = + (ereal_sup (range (fun n => esum [set:T] (fun x : T => f x n))))%E. + Proof. + rewrite /esum. + under eq_imagel => A [fin ?] do + rewrite fsbig_finite // ereal_sup_sum //. + rewrite ereal_sup_comm. + congr ereal_sup. + apply: eq_imagel => n S. + congr ereal_sup. + apply: eq_imagel => n' [A _]. + rewrite fsbig_finite //. +Qed. + +End mono_esum.