From 9f64824046f42d53928ef9b6f0d9d95be00fb04b Mon Sep 17 00:00:00 2001 From: Hei Li Date: Thu, 25 Jan 2024 16:48:06 +0100 Subject: [PATCH 1/4] First draft --- theories/prob/countable_sum.v | 49 ++++++++++++++++++++++++++++------- 1 file changed, 40 insertions(+), 9 deletions(-) diff --git a/theories/prob/countable_sum.v b/theories/prob/countable_sum.v index 8eeb395f..352d3cb3 100644 --- a/theories/prob/countable_sum.v +++ b/theories/prob/countable_sum.v @@ -1001,15 +1001,6 @@ Section fubini. Context `{Countable A, Countable B}. - (* A lemma about rearranging SeriesC along an injective function *) - - Lemma SeriesC_le_inj (f : B -> R) (h : A -> option B) : - (∀ n, 0 <= f n) → - (forall n1 n2 m, h n1 = Some m -> h n2 = Some m -> n1 = n2) -> - ex_seriesC f → - SeriesC (λ a, from_option f 0 (h a)) <= SeriesC f. - Admitted. - (* The following three lemmas have been proven for Series, so the only missing part is lifting them @@ -1133,6 +1124,7 @@ Section fubini. apply Series_0; auto. Qed. + End fubini. Section mct. @@ -1674,3 +1666,42 @@ Section double. Qed. End double. + +Section inj. + Context `{Countable A, Countable B}. + + (* A lemma about rearranging SeriesC along an injective function *) + + Lemma SeriesC_le_inj (f : B -> R) (h : A -> option B) : + (∀ n, 0 <= f n) → + (forall n1 n2 m, h n1 = Some m -> h n2 = Some m -> n1 = n2) -> + ex_seriesC f → + SeriesC (λ a, from_option f 0 (h a)) <= SeriesC f. + Proof. + intros Hf Hinj Hex. + pose (λ '(a,b), if bool_decide (Some b = h a) then f b else 0) as P. + rewrite (SeriesC_ext _ (λ a, SeriesC (λ b, P (a, b)))); last first. + { intros. rewrite /P. + destruct (h n) eqn:H1 => /=. + - rewrite <- SeriesC_singleton_dependent. + apply SeriesC_ext. intros. + repeat case_bool_decide; try lra. + all: (exfalso; subst). + + by apply H3. + + apply H2. by inversion H3. + - rewrite SeriesC_0; try lra. by intros. + } + rewrite -fubini_pos_seriesC_prod_lr. + - rewrite fubini_pos_seriesC_prod_rl. + + apply SeriesC_le; last done. + intros; split. + * rewrite /P. apply SeriesC_ge_0'. intros; case_bool_decide; try lra. apply Hf. + * (* case split *) admit. + + intros. rewrite /P. case_bool_decide; try lra. apply Hf. + + rewrite /P. admit. + - intros. rewrite /P. case_bool_decide; try lra. apply Hf. + - admit. + Admitted. + + +End inj. From 1b00086b2a54ba4fdcaa0d1e36c3d511c748064b Mon Sep 17 00:00:00 2001 From: Hei Li Date: Thu, 25 Jan 2024 21:09:40 +0100 Subject: [PATCH 2/4] completed SeriesC_le_inj cause otherwise I wont be able to sleep cause the only thing that keeps me awake is the inevitable arrival of death that follows from the brutal and steady march and time, or an admitted lemma that alejandro told me not to waste time on even if it looks doable --- theories/prob/countable_sum.v | 89 ++++++++++++++++++++++++++--------- 1 file changed, 67 insertions(+), 22 deletions(-) diff --git a/theories/prob/countable_sum.v b/theories/prob/countable_sum.v index 352d3cb3..5cf5aec7 100644 --- a/theories/prob/countable_sum.v +++ b/theories/prob/countable_sum.v @@ -1679,28 +1679,73 @@ Section inj. SeriesC (λ a, from_option f 0 (h a)) <= SeriesC f. Proof. intros Hf Hinj Hex. - pose (λ '(a,b), if bool_decide (Some b = h a) then f b else 0) as P. - rewrite (SeriesC_ext _ (λ a, SeriesC (λ b, P (a, b)))); last first. - { intros. rewrite /P. - destruct (h n) eqn:H1 => /=. - - rewrite <- SeriesC_singleton_dependent. - apply SeriesC_ext. intros. - repeat case_bool_decide; try lra. - all: (exfalso; subst). - + by apply H3. - + apply H2. by inversion H3. - - rewrite SeriesC_0; try lra. by intros. - } - rewrite -fubini_pos_seriesC_prod_lr. - - rewrite fubini_pos_seriesC_prod_rl. - + apply SeriesC_le; last done. - intros; split. - * rewrite /P. apply SeriesC_ge_0'. intros; case_bool_decide; try lra. apply Hf. - * (* case split *) admit. - + intros. rewrite /P. case_bool_decide; try lra. apply Hf. - + rewrite /P. admit. - - intros. rewrite /P. case_bool_decide; try lra. apply Hf. - - admit. + rewrite {1}/SeriesC/Series. + apply Series_Ext.Lim_seq_le_loc_const. + - by apply SeriesC_ge_0'. + - rewrite /eventually. exists 0%nat. + intros n Hn. + assert (∃ l : list _, (∀ m, m∈l->(∃ k a, (k<=n)%nat /\ + (@encode_inv_nat A _ _ k%nat) = Some a /\ + h a = Some m)) /\ + sum_n (countable_sum (λ a : A, from_option f 0 (h a))) n <= + SeriesC (λ a, if bool_decide(a ∈ l) then f a else 0) + ) as H'; last first. + { destruct H' as [?[??]]. + etrans; first exact. + apply SeriesC_le'; try done. + - intros. case_bool_decide; try lra. apply Hf. + - apply ex_seriesC_list. + } + induction n. + + destruct (@encode_inv_nat A _ _ 0%nat) eqn:Ha. + * destruct (h a) eqn : Hb. + -- exists [b]. split. + ++ intros. exists 0%nat, a. + repeat split; try lia; try done. + rewrite Hb. f_equal. set_solver. + ++ rewrite sum_O. rewrite /countable_sum. + rewrite Ha. simpl. rewrite Hb. simpl. + erewrite SeriesC_ext. + ** erewrite SeriesC_singleton_dependent. done. + ** intro. simpl. + repeat case_bool_decide; set_solver. + -- exists []. split. + ++ intros; set_solver. + ++ rewrite sum_O. rewrite /countable_sum. + rewrite Ha. simpl. rewrite Hb. simpl. + rewrite SeriesC_0; intros; lra. + * exists []. split. + ++ intros; set_solver. + ++ rewrite sum_O. rewrite /countable_sum. + rewrite Ha. simpl. + rewrite SeriesC_0; intros; lra. + + assert (0<=n)%nat as Hge0. + * lia. + * specialize (IHn Hge0) as [l[H1 H2]]. + destruct (@encode_inv_nat A _ _ (S n)%nat) eqn:Ha. + -- destruct (h a) eqn : Hb. + ++ exists (b::l). split. + ** intros. set_unfold. + destruct H3; subst. + --- exists (S n), a. split; try lia. split; done. + --- specialize (H1 m H3). + destruct H1 as [?[?[?[??]]]]. + exists x, x0. split; try lia. by split. + ** rewrite sum_Sn. rewrite {2}/countable_sum. + rewrite Ha. simpl. rewrite Hb. simpl. + rewrite (SeriesC_ext _ (λ x, (if bool_decide (x=b) then f b else 0) + + if bool_decide (x∈l) then f x else 0 + )); last first. + { intros. + case_bool_decide. + - set_unfold. destruct H3. + + admit. + + admit. + - admit. + } + admit. + ++ admit. + -- admit. Admitted. From 30f59993bfb60cd348212846874d2ba67460ac5a Mon Sep 17 00:00:00 2001 From: Hei Li Date: Thu, 25 Jan 2024 21:19:09 +0100 Subject: [PATCH 3/4] Add full proof --- theories/prob/countable_sum.v | 50 ++++++++++++++++++++++++++++++----- 1 file changed, 43 insertions(+), 7 deletions(-) diff --git a/theories/prob/countable_sum.v b/theories/prob/countable_sum.v index 5cf5aec7..d7495018 100644 --- a/theories/prob/countable_sum.v +++ b/theories/prob/countable_sum.v @@ -1739,14 +1739,50 @@ Section inj. { intros. case_bool_decide. - set_unfold. destruct H3. - + admit. - + admit. - - admit. + + case_bool_decide; last done. + case_bool_decide. + * subst. specialize (H1 b H5). + destruct H1 as [?[?[?[??]]]]. + rewrite -H6 in Hb. + assert (a = x0). + { eapply Hinj; try done. rewrite Hb. done. } + subst. exfalso. + rewrite -H3 in Ha. assert (x≠ (S n)) by lia. + apply H7. by eapply encode_inv_nat_some_inj. + * subst. lra. + + case_bool_decide. + { subst. specialize (H1 b H3) as [?[?[?[??]]]]. + assert (x ≠ S n) by lia. + exfalso. apply H6. eapply encode_inv_nat_some_inj; try done. + rewrite Ha H4. f_equal. + by eapply Hinj. + } + case_bool_decide; try done. lra. + - repeat case_bool_decide. + + set_solver. + + set_solver. + + set_solver. + + lra. } - admit. - ++ admit. - -- admit. - Admitted. + rewrite SeriesC_plus; last first. + { by apply ex_seriesC_filter_pos. } + { by apply ex_seriesC_singleton. } + rewrite Rplus_comm. rewrite SeriesC_singleton. + trans ((sum_n (countable_sum (λ a0 : A, from_option f 0 (h a0))) n) + f b); try lra. + done. + ++ exists l. split. + ** intros. specialize (H1 _ H3) as [?[?[?[??]]]]. + exists x, x0. repeat split; try done. lia. + ** rewrite sum_Sn. rewrite {2}/countable_sum. rewrite Ha. simpl. + rewrite Hb. simpl. etrans; last exact. + rewrite /plus. rewrite AbelianGroup.ax3. done. + -- exists l. split. + ++ intros. specialize (H1 _ H3) as [?[?[?[??]]]]. + exists x, x0. repeat split; try done. lia. + ++ rewrite sum_Sn. rewrite {2}/countable_sum. rewrite Ha. simpl. + etrans; last exact. + rewrite /plus. rewrite AbelianGroup.ax3. done. + Qed. End inj. From 4867bed679a1228a98857a2bd32ca9d7d12196c7 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Thu, 25 Jan 2024 21:29:01 +0100 Subject: [PATCH 4/4] Use simpler lemma that the checker has. it doesnt have abelian group ax 3 --- theories/prob/countable_sum.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/prob/countable_sum.v b/theories/prob/countable_sum.v index d7495018..62332af8 100644 --- a/theories/prob/countable_sum.v +++ b/theories/prob/countable_sum.v @@ -1775,13 +1775,13 @@ Section inj. exists x, x0. repeat split; try done. lia. ** rewrite sum_Sn. rewrite {2}/countable_sum. rewrite Ha. simpl. rewrite Hb. simpl. etrans; last exact. - rewrite /plus. rewrite AbelianGroup.ax3. done. + by rewrite plus_zero_r. -- exists l. split. ++ intros. specialize (H1 _ H3) as [?[?[?[??]]]]. exists x, x0. repeat split; try done. lia. ++ rewrite sum_Sn. rewrite {2}/countable_sum. rewrite Ha. simpl. etrans; last exact. - rewrite /plus. rewrite AbelianGroup.ax3. done. + by rewrite plus_zero_r. Qed.