From 09ac8fd58a7a22eecf314e48711600f3b3035403 Mon Sep 17 00:00:00 2001 From: Lionel Blatter Date: Wed, 29 Jul 2026 22:26:12 +0200 Subject: [PATCH] Connection between esum and lesbegue_integral --- _CoqProject | 2 + classical/classical_sets.v | 3 + theories/esum_counting.v | 148 +++++++++++++++++++++++++++++++++++++ 3 files changed, 153 insertions(+) create mode 100644 theories/esum_counting.v diff --git a/_CoqProject b/_CoqProject index 21917e35d5..041f7d878a 100644 --- a/_CoqProject +++ b/_CoqProject @@ -154,5 +154,7 @@ theories/all_analysis.v theories/showcase/summability.v theories/showcase/pnt.v +theories/esum_counting.v + analysis_stdlib/Rstruct_topology.v analysis_stdlib/showcase/uniform_bigO.v diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 763263f7d8..418396d5b8 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2191,6 +2191,9 @@ End bigop_lemmas. Arguments bigcup_setD1 {T I} x. Arguments bigcap_setD1 {T I} x. +Lemma bigcup_id {T: Type} (P: set T) : \bigcup_(i in P) [set i] = P. +Proof. by rewrite bigcup_imset1 // image_id. Qed. + Lemma setD_bigcup {T} (I : eqType) (F : I -> set T) (P : set I) (j : I) : P j -> F j `\` \bigcup_(i in [set k | P k /\ k != j]) (F j `\` F i) = \bigcap_(i in P) F i. diff --git a/theories/esum_counting.v b/theories/esum_counting.v new file mode 100644 index 0000000000..f3df1cc03e --- /dev/null +++ b/theories/esum_counting.v @@ -0,0 +1,148 @@ +From HB Require Import structures. +From mathcomp Require Import boot order algebra. +From mathcomp.classical Require Import boolp classical_sets mathcomp_extra functions. +From mathcomp Require Import xfinmap constructive_ereal reals discrete. +From mathcomp Require Import realseq realsum. +From mathcomp Require Import esum sequences normedtype ereal cardinality fsbigop. +From mathcomp Require Import measure lebesgue_integral. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Unset SsrOldRewriteGoalsOrder. (* remove this line when requiring MathComp >= 2.6 *) + +Import Order.TTheory GRing.Theory Num.Theory. + +Local Open Scope ring_scope. + +(* -------------------------------------------------------------------- *) +Local Notation simpm := Monoid.simpm. + +Local Open Scope classical_set_scope. + +(* -------------------------------------------------------------------- *) + +Definition discrete_measurable_space (T : choiceType) : Type := T. + +HB.instance Definition _ (T : choiceType) := + Choice.on (discrete_measurable_space T). + +HB.instance Definition _ (T : choiceType) := @isMeasurable.Build + default_measure_display + (discrete_measurable_space T) discrete_measurable discrete_measurable0 + discrete_measurableC discrete_measurableU. + + +Section Counting. + Context (R : realType) (T : choiceType). + +Lemma esum_bigcup_set (T1 T2 : choiceType) (K : set T1) (J : T1 -> set T2) + (a : T2 -> \bar R) : + trivIset setT J -> (forall x, (0 <= a x)%E) -> + (\esum_(i in \bigcup_(k in K) J k) a i = + \esum_(k in K) \esum_(j in J k) a j)%E. +Proof. +move=> tJ a0; rewrite esum_esum//; apply: reindex_esum => //; split. +- by move=> [/= i j] [Ki Jij]; exists i. +- move=> [/= i1 j1] [/= i2 j2] /set_mem/= [Ki1 Jij1] /set_mem/= [Ki2 Jij2] /= j12. + have iE : i1 = i2. + by apply: (tJ i1 i2) => //; exists j1; split=> //; rewrite j12. + by rewrite iE j12. +- by move=> j [i Ki Jij]/=; exists (i, j). +Qed. + +Lemma counting_esum_cst (c : R) (A : set T) : (0 <= c)%R -> + (c%:E * @counting (discrete_measurable_space T) R A + = \esum_(x in A) c%:E)%E. +Proof. +move=> c0. +have [-> | c_neq] := eqVneq c 0%R. + by rewrite mul0e; apply/esym/esum1. +have c_pos : (0 < c)%R by rewrite lt_def c_neq. +have [finA|infA] := pselect (finite_set A). ++ rewrite /counting (asboolT finA). + rewrite esum_fset// fsbig_finite//=. + rewrite sumEFin big_const_seq count_predT iter_addr addr0. + rewrite -EFinM; congr (_%:E). + rewrite mulr_natr; congr (c *+ _). + apply: (elimT (@fcard_eq (discrete_measurable_space T) T A A finA finA)). + exact: card_eqxx. ++ rewrite /counting asboolF//=. + rewrite mulry gtr0_sg// mul1e. + apply/esym/eqyP => r r0. + have [B BA Brc] := infinite_set_fset (Num.Def.truncn (c^-1 * r)).+1 infA. + apply: esum_ge => // ; exists [set` B]. + by split=> //; apply/subsetP => x; rewrite inE => /BA. + rewrite fsbig_finite//= set_fsetK sumEFin big_const_seq count_predT. + rewrite iter_addr addr0 -mulr_natr lee_fin -ler_pdivrMl//. + apply: (@le_trans _ _ (((Num.Def.truncn (c^-1 * r)).+1)%:R)). + exact: ltW (truncnS_gt _). + rewrite ler_nat. + exact: Brc. +Qed. + +Import HBNNSimple. + +Lemma sintegral_counting_esum + (h : {nnsfun (discrete_measurable_space T) >-> R}) : + (sintegral (@counting (discrete_measurable_space T) R) h + = \esum_(x in [set: T]) (h x)%:E)%E. +Proof. +rewrite sintegralE //=. +transitivity (\sum_(c \in range h) + \esum_(x in (h @^-1` [set c] : set T)) (h x)%:E)%E. ++ apply: eq_fsbigr => c /set_mem/= -[x _ <-{c}]. + rewrite counting_esum_cst//. + by apply: (eq_esum _ (fun=> (h x)%:E)) => x0 ->. ++ rewrite -esum_fset//. + + by move=> ? _; apply: esum_ge0 => ? _; rewrite lee_fin. + rewrite -esum_bigcup_set. + + exact: trivIset_preimage1. + + by move=> ?; rewrite lee_fin. + + suff -> : \bigcup_(c in range h) h @^-1` [set c] = [set: T] by []. + apply/seteqP; split => [//|y _]. + by exists (h y); [exists y|]. +Qed. + +Lemma integral_set1 f i : +(\int[@counting (discrete_measurable_space T) R]_(x in [set i]) f x = f i)%E. +Proof. +transitivity (\int[@counting (discrete_measurable_space T) R]_(x in [set i]) + cst (f i) x)%E. ++ by apply: eq_integral => x /set_mem/= ->. +rewrite integral_cst// -[X in _ = X](mule1 (f i)). +congr (f i * _)%E => /=. +rewrite /counting (asboolT (finite_set1 i)). +by rewrite fset_set1 cardfs1. +Qed. + +Lemma integral_sum f : forall A : set T, finite_set A -> +(forall x, (0 <= f x)%E) -> +(\int[@counting (discrete_measurable_space T) R]_(x in A) f x = \sum_(x \in A) f x)%E. +Proof. +move=> A finA ?. +rewrite fsbig_finite//=. +rewrite (eq_bigr (fun i => (\int[counting]_(x in [set i]) f x)%E)). ++ by move => ??;rewrite integral_set1. +rewrite -ge0_integral_bigsetU //=. +- exact: fset_uniq. +- by move=> i j _ _ [x [-> ->]]. +- by rewrite (@bigsetU_fset_set _ _ _ _ finA) bigcup_id. +Qed. + +Lemma integral_counting_esum (f : T -> \bar R) : + (forall x, (0 <= f x)%E) -> + (\int[@counting (discrete_measurable_space T) R]_x f x + = \esum_(x in [set: T]) f x)%E. +Proof. +move=> f0 ; apply/eqP; rewrite eq_le; apply/andP; split. +- rewrite ge0_integralTE //=. + apply: ge_ereal_sup => /= _ [h /= hf] <-. + rewrite sintegral_counting_esum. + apply: le_esum => x _; exact: hf. +- rewrite ge0_esum //; apply: ge_ereal_sup => /= _ [A [finA _] <-]. + rewrite -integral_sum//. + by apply: ge0_subset_integral => //. +Qed. + +End Counting.