diff --git a/coq/QLearn/jaakkola_vector.v b/coq/QLearn/jaakkola_vector.v index ba08557d..d3cb6d0c 100644 --- a/coq/QLearn/jaakkola_vector.v +++ b/coq/QLearn/jaakkola_vector.v @@ -3685,11 +3685,13 @@ Section jaakola_vector2. (γ * (Rvector_max_abs (X k ω)))) -> (exists (C : R), - 0 < C /\ - forall k i pf ω, - Rbar_le ((FiniteConditionalVariance prts (filt_sub k) (vecrvnth i pf (XF k))) ω) - (C * (1 + Rvector_max_abs (X k ω))^2)) -> - (exists (C : R), forall k ω, Rvector_max_abs (X k ω) <= C) -> + (0 < C) /\ + (forall k i pf ω, + Rbar_le ((FiniteConditionalVariance prts (filt_sub k) (vecrvnth i pf (XF k))) ω) + (C * (1 + Rvector_max_abs (X k ω))^2))) -> + (exists (C : Ts -> R), + (RandomVariable (F 0%nat) borel_sa C) /\ + (forall k ω, Rvector_max_abs (X k ω) <= C ω)) -> (forall k, rv_eq (X (S k)) (vecrvplus (vecrvminus (X k) (vecrvmult (α k) (X k))) (vecrvmult (β k) (XF k)))) -> almost prts (fun ω => @@ -3761,25 +3763,38 @@ Section jaakola_vector2. end. lra. } - assert (exists C, forall k i pf ω, (FiniteConditionalVariance prts (filt_sub k) (vecrvnth i pf (XF k)) ω) <= C). + assert (exists (C : Ts -> R), + (RandomVariable (F 0%nat) borel_sa C) /\ + (forall k i pf ω, (FiniteConditionalVariance prts (filt_sub k) (vecrvnth i pf (XF k)) ω) <= C ω)). { + destruct H8 as [? [??]]. - destruct H9. - exists (x * (1 + x0)^2). + destruct H9 as [? [??]]. + exists (rvscale x (rvsqr (rvplus (const 1) x0))). + split. + { + apply rvscale_rv. + apply rvsqr_rv. + apply rvplus_rv; trivial. + apply rvconst. + } intros. + specialize (H12 k i pf ω). eapply Rle_trans. + simpl in H12. apply H12. - simpl. + unfold rvmult, rvsqr, rvplus, const. apply Rmult_le_compat_l; try lra. - repeat rewrite Rmult_1_r. - assert (0 <= x0). + unfold Rsqr. + rewrite Rmult_1_r. + assert (0 <= x0 ω). { eapply Rle_trans; cycle 1. - apply (H9 0%nat ω). + apply (H13 0%nat ω). apply Rvector_max_abs_nonneg. } generalize (Rvector_max_abs_nonneg (X k ω)); intros. - specialize (H9 k ω). + specialize (H13 k ω). apply Rmult_le_compat; try lra. } assert (forall k i pf, @@ -3893,26 +3908,18 @@ Section jaakola_vector2. f_equal. now rewrite eqvec. } - assert (exists B, - forall k i pf ω, - (FiniteConditionalExpectation prts (filt_sub k) (rvsqr (vecrvnth i pf (r k)))) ω <= (Rsqr B)). + assert (exists (B : Ts -> R), + (RandomVariable (F 0%nat) borel_sa B) /\ + (forall k i pf ω, + (FiniteConditionalExpectation prts (filt_sub k) (rvsqr (vecrvnth i pf (r k)))) ω <= (B ω))). { unfold FiniteConditionalVariance in H12. - destruct H12 as [C ?]. - assert (0 <= Rmax 0 C). - { - apply Rmax_l. - } - exists (Rsqrt (mknonnegreal _ H18)). + destruct H12 as [C [rvC H12]]. + exists C. + split; trivial. intros. specialize (H12 k i pf ω). unfold r. - unfold Rsqr. - rewrite Rsqrt_Rsqrt. - simpl. - assert (C <= Rmax 0 C) by apply Rmax_r. - eapply Rle_trans; cycle 1. - apply H19. eapply Rle_trans; cycle 1. apply H12. right. @@ -3922,19 +3929,32 @@ Section jaakola_vector2. f_equal. now rewrite eqvec. } - destruct H18 as [B ?]. + destruct H18 as [B [??]]. assert (lim_w_0: forall (i : nat) (pf : (i < S N)%nat), almost prts (fun ω : Ts => is_lim_seq (fun n0 : nat => vector_nth i pf (w n0 ω)) 0)). { intros n1 pf. - generalize (fun i pf => lemma1_bounded_alpha_beta + generalize (fun i pf => lemma1_alpha_beta (fun k ω => vector_nth i pf (α k ω)) (fun k ω => vector_nth i pf (β k ω)) (fun k ω => vector_nth i pf (r k ω)) - (fun k ω => vector_nth i pf (w k ω)) Ca Cb); intros. - specialize (H19 n1 pf B _ isfilt filt_sub _ _). - apply H19; clear H19. + (fun k ω => B ω) + (fun k ω => vector_nth i pf (w k ω))); intros. + specialize (H20 n1 pf Ca Cb F isfilt filt_sub _ _). + apply H20; clear H20. + - unfold IsAdapted; intros. + unfold IsFiltration in isfilt. + assert (sa_sub (F 0%nat) (F n)). + { + induction n. + - apply sa_equiv_sub. + reflexivity. + - rewrite IHn. + apply isfilt. + } + apply (RandomVariable_sa_sub H20). + apply H18. - unfold IsAdapted; intros. apply vecrvnth_rv. unfold r. @@ -3950,13 +3970,17 @@ Section jaakola_vector2. intros. apply vecrvnth_rv. apply adapt_beta. + - intros. + apply Condexp_cond_exp. + apply H15. - intros. apply H16. - intros. - specialize (H18 n n1 pf). + specialize (H19 n n1 pf). apply all_almost; intros. + specialize (H19 x). generalize (FiniteCondexp_eq prts (filt_sub n)); intros. - specialize (H19 (rvsqr (fun ω : Ts => vector_nth n1 pf (r n ω))) + specialize (H20 (rvsqr (fun ω : Ts => vector_nth n1 pf (r n ω))) (@rvsqr_rv Ts dom (@vecrvnth Ts R (S N) n1 pf (r n)) (H13 n n1 pf))). assert (IsFiniteExpectation prts (rvsqr (fun ω : Ts => vector_nth n1 pf (r n ω)))). { @@ -3969,12 +3993,13 @@ Section jaakola_vector2. rewrite <- eqvec. reflexivity. } - specialize (H19 H20). + specialize (H20 H21). unfold vecrvnth in H19. - rewrite H19. + unfold vecrvnth in H20. + rewrite H20. simpl. unfold const. - eapply Rle_trans; [| apply (H18 x)]. + eapply Rle_trans; [| apply H19]. right. apply FiniteConditionalExpectation_ext. reflexivity. @@ -4013,10 +4038,14 @@ Section jaakola_vector2. rewrite Rvector_nth_scale. repeat rewrite Rvector_nth_mult. lra. + - exists B. + apply all_almost. + intros. + apply Rle_abs. } apply almost_bounded_forall; intros. - apply lt_dec. - - revert H19. + - revert H20. apply is_lim_seq_ext. intros. apply vector_nth_ext. @@ -4053,7 +4082,7 @@ Section jaakola_vector2. lra. - field_simplify; lra. } - destruct H22 as [C [? ?]]. + destruct H23 as [C [? ?]]. assert (forall (eps : posreal), forall k ω, Rvector_max_abs(δ k ω) > C * eps -> @@ -4144,7 +4173,7 @@ Section jaakola_vector2. generalize (Rabs_pos (vector_nth i0 pf1 (w n0 ω))); intros. rewrite (Rabs_right (Rabs (vector_nth i0 pf1 (δ n0 ω)) + Rabs (vector_nth i0 pf1 (w n0 ω)))); lra. } - apply H25. + apply H26. eapply Rle_trans; cycle 1. apply H7. right. @@ -4234,10 +4263,10 @@ Section jaakola_vector2. >= 1-eps )). { intros. - generalize (almost_and _ (almost_and _ H0 H1) H25); intros. - destruct H28 as [? [??]]. - specialize (H21 eps eps). - revert H21. + generalize (almost_and _ (almost_and _ H0 H1) H26); intros. + destruct H29 as [? [??]]. + specialize (H22 eps eps). + revert H22. apply eventually_impl. apply all_eventually. intros ??. @@ -4251,25 +4280,25 @@ Section jaakola_vector2. now rewrite ps_inter_l1. } eapply Rge_trans; cycle 1. - apply H30. + apply H31. apply Rle_ge. apply ps_sub. intros ??. - simpl in H31. - unfold pre_event_inter in H31. - destruct H31. - specialize (H29 x1 H31). + simpl in H32. + unfold pre_event_inter in H32. + destruct H32. + specialize (H30 x1 H32). unfold inter_of_collection, bounded_inter_of_collection, pre_bounded_inter_of_collection, event_Rle, event_Rge, proj1_sig. intros. apply Rle_ge. unfold rvabs. eapply Rle_trans. - apply H29. + apply H30. unfold vecrvnth, vecrvminus, vecrvplus, vecrvopp, rvscale. unfold rvplus, rvmult, vecrvconst, vecrvscale, vecrvmult. rewrite Rvector_nth_plus, Rvector_nth_scale, Rvector_nth_mult. unfold rvmaxabs. - destruct H29 as [[? ?] ?]. + destruct H30 as [[? ?] ?]. simpl. replace (vector_nth i pf0 (vecrvabs (δ (x0 + n0)%nat) x1) + -1 * (vector_nth i pf0 (α (x0 + n0)%nat x1) * vector_nth i pf0 (vecrvabs (δ (x0 + n0)%nat) x1))) with @@ -4281,12 +4310,12 @@ Section jaakola_vector2. rewrite Rmult_assoc. apply Rmult_le_compat_l; try lra. apply Rmult_le_compat_l. - + apply H33. - + unfold rvabs, vecrvnth in H32. - specialize (H32 n0). - replace (n0 + x0)%nat with (x0 + n0)%nat in H32 by lia. - unfold rvmaxabs in H32. - rewrite Rabs_Rvector_max_abs in H32. + + apply H34. + + unfold rvabs, vecrvnth in H33. + specialize (H33 n0). + replace (n0 + x0)%nat with (x0 + n0)%nat in H33 by lia. + unfold rvmaxabs in H33. + rewrite Rabs_Rvector_max_abs in H33. apply Rvector_max_abs_le. intros. rewrite Rvector_nth_plus. @@ -4299,7 +4328,7 @@ Section jaakola_vector2. left. eapply Rle_lt_trans. apply Rvector_max_abs_nth_le. - apply H32. + apply H33. * generalize (Rabs_pos (vector_nth i0 pf1 (δ (x0+n0)%nat x1))); intros. generalize (cond_pos eps); intros. lra. @@ -4319,10 +4348,10 @@ Section jaakola_vector2. >= 1 - eps). { intros eps. - specialize (H28 eps). - destruct H28. - specialize (H28 x). - cut_to H28; try lia. + specialize (H29 eps). + destruct H29. + specialize (H29 x). + cut_to H29; try lia. generalize almost_independent_impl; intros HH. assert (gamma_C_pos: 0 < γ * ((C + 1) / C)). { @@ -4417,9 +4446,9 @@ Section jaakola_vector2. intros. now replace (n1 + x)%nat with (x + n1)%nat by lia. } - generalize (lemma3_full_almost αα ββ δδ (mkposreal _ gamma_C_pos) _ _ _ αα_almost ββ_almost αβ_almost l1_div H23 lemma3_eq); intros lemma3. + generalize (lemma3_full_almost αα ββ δδ (mkposreal _ gamma_C_pos) _ _ _ αα_almost ββ_almost αβ_almost l1_div H24 lemma3_eq); intros lemma3. generalize (almost_and _ (almost_and _ H0 H1) (almost_and _ H2 lemma3)); intros. - destruct H29 as [? [??]]. + destruct H30 as [? [??]]. assert (ps_P (event_inter x0 @@ -4439,7 +4468,7 @@ Section jaakola_vector2. now rewrite ps_inter_l1. } eapply Rge_trans; cycle 1. - apply H31. + apply H32. apply Rle_ge. apply ps_sub. intros ??. @@ -4447,28 +4476,28 @@ Section jaakola_vector2. destruct (classic_min_of_sumbool (fun n => Rvector_max_abs (δ (x + n)%nat x1) <= (C * eps))). - destruct s as [? [??]]. - clear H34. + clear H35. assert (forall k, Rvector_max_abs (δ (x + (x2+k))%nat x1) <= C * eps). { induction k. - eapply Rle_trans; cycle 1. - apply H33. + apply H34. replace (x + (x2 + 0))%nat with (x + x2)%nat by lia. lra. - - unfold event_inter, pre_event_inter, inter_of_collection, bounded_inter_of_collection, pre_bounded_inter_of_collection, event_Rle, event_Rge, proj1_sig in H32. - destruct H32. - specialize (H30 x1 H32). - unfold pre_event_inter in H30. - destruct H30 as [[? ?] ?]. + - unfold event_inter, pre_event_inter, inter_of_collection, bounded_inter_of_collection, pre_bounded_inter_of_collection, event_Rle, event_Rge, proj1_sig in H33. + destruct H33. + specialize (H31 x1 H33). + unfold pre_event_inter in H31. + destruct H31 as [[? ?] ?]. rewrite Rvector_max_abs_nth_Rabs_le. intros. - specialize (H34 (x2 + k)%nat i pf0). - apply Rge_le in H34. - unfold rvabs, vecrvnth in H34. - replace (S (x + (x2 + k))) with (x + (x2 + S k))%nat in H34 by lia. + specialize (H35 (x2 + k)%nat i pf0). + apply Rge_le in H35. + unfold rvabs, vecrvnth in H35. + replace (S (x + (x2 + k))) with (x + (x2 + S k))%nat in H35 by lia. eapply Rle_trans. - apply H34. + apply H35. unfold vecrvminus, vecrvmult, vecrvplus, vecrvopp, vecrvabs, vecrvconst, vecrvscale, rvmaxabs, rvscale, rvmult, rvplus. rewrite Rvector_nth_plus, Rvector_nth_scale, Rvector_nth_mult. generalize (cond_pos eps); intros. @@ -4482,62 +4511,62 @@ Section jaakola_vector2. { lra. } - apply Rmult_lt_compat_r with (r := C) in H23; trivial. - rewrite Rmult_1_l in H23. - unfold Rdiv in H23. - rewrite Rmult_assoc in H23. - rewrite Rmult_assoc in H23. - rewrite Rmult_inv_l in H23; try lra. - rewrite Rmult_1_r in H23. - apply Rmult_le_compat_l with (r := γ * (vector_nth i pf0 (β (x + (x2 + k))%nat x1))) in H38. + apply Rmult_lt_compat_r with (r := C) in H24; trivial. + rewrite Rmult_1_l in H24. + unfold Rdiv in H24. + rewrite Rmult_assoc in H24. + rewrite Rmult_assoc in H24. + rewrite Rmult_inv_l in H24; try lra. + rewrite Rmult_1_r in H24. + apply Rmult_le_compat_l with (r := γ * (vector_nth i pf0 (β (x + (x2 + k))%nat x1))) in H39. + assert (γ * vector_nth i pf0 (β (x + (x2 + k))%nat x1) * (Rvector_max_abs (δ (x + (x2 + k))%nat x1) + eps) <= (vector_nth i pf0 (α (x + (x2 + k))%nat x1) * (C * eps))). { eapply Rle_trans. - apply H38. + apply H39. generalize (cond_pos eps); intros. assert (γ * (C + 1) <= C) by lra. - apply Rmult_le_compat_r with (r := eps) in H40; try lra. - apply Rmult_le_compat_l with (r := vector_nth i pf0 (β (x + (x2 + k))%nat x1)) in H40. + apply Rmult_le_compat_r with (r := eps) in H41; try lra. + apply Rmult_le_compat_l with (r := vector_nth i pf0 (β (x + (x2 + k))%nat x1)) in H41. apply Rle_trans with (r2 := vector_nth i pf0 (β (x + (x2 + k))%nat x1) * (C * eps)); try lra. apply Rmult_le_compat_r. apply Rmult_le_pos; lra. + apply H37. apply H36. - apply H35. } - apply Rplus_le_compat_l with (r := (1 - vector_nth i pf0 (α (x + (x2 + k))%nat x1)) * Rabs (vector_nth i pf0 (δ (x + (x2 + k))%nat x1))) in H39. + apply Rplus_le_compat_l with (r := (1 - vector_nth i pf0 (α (x + (x2 + k))%nat x1)) * Rabs (vector_nth i pf0 (δ (x + (x2 + k))%nat x1))) in H40. rewrite <- Rmult_assoc. eapply Rle_trans. - apply H39. + apply H40. assert (Rabs (vector_nth i pf0 (δ (x + (x2 + k))%nat x1)) <= C * eps). { now rewrite Rvector_max_abs_nth_le. } - apply Rmult_le_compat_l with (r := (1 - vector_nth i pf0 (α (x + (x2 + k))%nat x1)) ) in H40. - apply Rplus_le_compat_r with (r := vector_nth i pf0 (α (x + (x2 + k))%nat x1) * (C * eps)) in H40. + apply Rmult_le_compat_l with (r := (1 - vector_nth i pf0 (α (x + (x2 + k))%nat x1)) ) in H41. + apply Rplus_le_compat_r with (r := vector_nth i pf0 (α (x + (x2 + k))%nat x1) * (C * eps)) in H41. eapply Rle_trans. - apply H40. + apply H41. rewrite <- Rmult_plus_distr_r; try lra. - specialize (H30 (x + (x2 + k))%nat i pf0); try lra. + specialize (H31 (x + (x2 + k))%nat i pf0); try lra. + apply Rmult_le_pos; try lra. - apply H35. + apply H36. } exists (x + x2)%nat. intros. - specialize (H34 (n1 + (n0 - (x + x2)))%nat). - replace (x + (x2 + (n1 + (n0 - (x + x2)))))%nat with (n0 + n1)%nat in H34 by lia. - apply H34. + specialize (H35 (n1 + (n0 - (x + x2)))%nat). + replace (x + (x2 + (n1 + (n0 - (x + x2)))))%nat with (n0 + n1)%nat in H35 by lia. + apply H35. - assert (forall n0, Rvector_max_abs (δ (x + n0)%nat x1) > C * eps). { intros. specialize (n0 n1). now apply Rnot_le_gt in n0. } - unfold event_inter, pre_event_inter, inter_of_collection, bounded_inter_of_collection, pre_bounded_inter_of_collection, event_Rle, event_Rge, proj1_sig in H32. - destruct H32. - specialize (H30 x1 H32). - unfold pre_event_inter in H30. - destruct H30 as [[? ?] [? ?]]. + unfold event_inter, pre_event_inter, inter_of_collection, bounded_inter_of_collection, pre_bounded_inter_of_collection, event_Rle, event_Rge, proj1_sig in H33. + destruct H33. + specialize (H31 x1 H33). + unfold pre_event_inter in H31. + destruct H31 as [[? ?] [? ?]]. assert (dd_pos: forall n i pf0, 0 <= vector_nth i pf0 (δδ n x1)). { @@ -4556,13 +4585,13 @@ Section jaakola_vector2. ((1 - (vector_nth i pf0 (α (x + n1)%nat x1))) * vector_nth i pf0 (δδ n1 x1)) by lra. apply Rplus_le_le_0_compat. + apply Rmult_le_pos; trivial. - specialize (H30 (x + n1)%nat i pf0); lra. + specialize (H31 (x + n1)%nat i pf0); lra. + apply Rmult_le_pos. * apply Rvector_max_abs_nonneg. * apply Rmult_le_pos. -- apply Rmult_le_pos; try lra. apply Rdiv_le_0_compat; lra. - -- specialize (H35 (x + n1)%nat i pf0); lra. + -- specialize (H36 (x + n1)%nat i pf0); lra. } assert (forall n i pf, Rabs(vector_nth i pf (δ (x + n)%nat x1)) <= @@ -4577,10 +4606,10 @@ Section jaakola_vector2. now replace (x + 0)%nat with x by lia. - intros. replace (x + S n1)%nat with (S (x + n1)) by lia. - specialize (H34 n1 i pf0). - apply Rge_le in H34. + specialize (H35 n1 i pf0). + apply Rge_le in H35. eapply Rle_trans. - apply H34. + apply H35. simpl. unfold vecrvminus, vecrvplus, vecrvmult, vecrvopp, vecrvscale, vecrvnth. unfold rvplus, rvscale, rvmult. @@ -4603,7 +4632,7 @@ Section jaakola_vector2. ((1 - (vector_nth i pf0 (α (x + n1)%nat x1))) * vector_nth i pf0 (δδ n1 x1)) by lra. apply Rmult_le_compat_l; trivial. - specialize (H30 (x + n1)%nat i pf0); lra. + specialize (H31 (x + n1)%nat i pf0); lra. + unfold rvmaxabs, vecrvabs, vecrvconst, vecrvscalerv. rewrite Rvector_nth_scale. rewrite Rvector_nth_scale. @@ -4613,12 +4642,12 @@ Section jaakola_vector2. rewrite (Rmult_comm _ (vector_nth i pf0 (β (x + n1)%nat x1))). repeat rewrite Rmult_assoc. apply Rmult_le_compat_l. - * specialize (H35 (x + n1)%nat i pf0); lra. - * specialize (H33 n1). - specialize (H24 eps (x + n1)%nat x1 H33). - apply Rmult_le_compat_r with (r := γ) in H24; try lra. + * specialize (H36 (x + n1)%nat i pf0); lra. + * specialize (H34 n1). + specialize (H25 eps (x + n1)%nat x1 H34). + apply Rmult_le_compat_r with (r := γ) in H25; try lra. eapply Rle_trans. - apply H24. + apply H25. rewrite Rmult_comm. rewrite (Rmult_comm (Rvector_max_abs (δδ n1 x1))). rewrite <- Rmult_assoc. @@ -4636,7 +4665,7 @@ Section jaakola_vector2. { intros. eapply Rle_trans. - apply H38. + apply H39. apply Rle_abs. } @@ -4655,33 +4684,33 @@ Section jaakola_vector2. { intros. apply is_lim_seq_incr_n with (N := x). - revert H37. + revert H38. apply is_lim_seq_le_le with (u := const 0). - intros. split. + unfold const. apply Rvector_max_abs_nonneg. + replace (n1 + x)%nat with (x + n1)%nat by lia. - apply H40. + apply H41. - apply is_lim_seq_const. } - apply is_lim_seq_spec in H41. - unfold is_lim_seq' in H41. + apply is_lim_seq_spec in H42. + unfold is_lim_seq' in H42. assert (0 < C * eps). { apply Rmult_lt_0_compat; try lra. apply cond_pos. } - specialize (H41 (mkposreal _ H42)). - destruct H41. + specialize (H42 (mkposreal _ H43)). + destruct H42. exists x2. intros. - specialize (H41 (n1 + n2)%nat). - cut_to H41; try lia. - rewrite Rminus_0_r in H41. - simpl in H41. + specialize (H42 (n1 + n2)%nat). + cut_to H42; try lia. + rewrite Rminus_0_r in H42. + simpl in H42. unfold rvmaxabs. - rewrite Rabs_Rvector_max_abs in H41. + rewrite Rabs_Rvector_max_abs in H42. lra. } assert (epsk: forall (k : nat), @@ -4701,7 +4730,7 @@ Section jaakola_vector2. 1 - (mkposreal _ (epsk k)) ). { intros. - apply H29. + apply H30. } assert (almost prts (fun ω : Ts => is_lim_seq (fun n1 : nat => vector_nth n pf (δ n1 ω)) 0)). @@ -4714,9 +4743,9 @@ Section jaakola_vector2. rewrite <- is_lim_seq_incr_1. apply is_lim_seq_INR. } - apply is_lim_seq_inv in H31. - + replace (Rbar_inv p_infty) with (Finite 0) in H31. - * apply H31. + apply is_lim_seq_inv in H32. + + replace (Rbar_inv p_infty) with (Finite 0) in H32. + * apply H32. * now unfold Rbar_inv. + discriminate. } @@ -4731,8 +4760,8 @@ Section jaakola_vector2. } assert (is_lim_seq (fun k => (C * (mkposreal _ (epsk k)))) 0). { - apply is_lim_seq_scal_l with (a := C) in H31. - now rewrite Rbar_mult_0_r in H31. + apply is_lim_seq_scal_l with (a := C) in H32. + now rewrite Rbar_mult_0_r in H32. } assert (forall k, event_sub @@ -4750,9 +4779,9 @@ Section jaakola_vector2. apply eventually_impl. apply all_eventually. simpl; intros. - specialize (H34 n0). + specialize (H35 n0). eapply Rle_trans. - apply H34. + apply H35. apply Rmult_le_compat_l. - lra. - apply Rinv_le_contravar. @@ -4779,25 +4808,25 @@ Section jaakola_vector2. simpl. unfold pre_event_preimage, pre_event_singleton. split; intros. - - specialize (H35 n0). - destruct H35. + - specialize (H36 n0). + destruct H36. exists x0. intros. - specialize (H35 n1 H36). - specialize (H35 0%nat). - replace (n1 + 0)%nat with n1 in H35 by lia. - apply H35. - - specialize (H35 n0). - destruct H35. + specialize (H36 n1 H37). + specialize (H36 0%nat). + replace (n1 + 0)%nat with n1 in H36 by lia. + apply H36. + - specialize (H36 n0). + destruct H36. exists x0. intros. - specialize (H35 (n1 + n2)%nat). - cut_to H35; try lia. + specialize (H36 (n1 + n2)%nat). + cut_to H36; try lia. eapply Rle_trans. - apply H35. + apply H36. lra. } - generalize (lim_prob_descending _ _ H34 H35); intros. + generalize (lim_prob_descending _ _ H35 H36); intros. assert (forall k, 1 - {| pos := / INR (S k); cond_pos := epsk k |} <= ps_P @@ -4814,8 +4843,8 @@ Section jaakola_vector2. (fun k => (event_eventually (fun n0 : nat => - event_le dom (rvmaxabs (δ n0)) (C * (mkposreal _ (epsk k))))))))) H37 H32 H36); intros. - simpl in H38. + event_le dom (rvmaxabs (δ n0)) (C * (mkposreal _ (epsk k))))))))) H38 H33 H37); intros. + simpl in H39. assert ( ps_P (inter_of_collection (fun k : nat => @@ -4841,35 +4870,34 @@ Section jaakola_vector2. apply is_lim_seq_spec. unfold is_lim_seq'. intros. - simpl in H40. - apply is_lim_seq_spec in H33. - specialize (H33 eps). - destruct H33. - specialize (H40 x0). - revert H40. + simpl in H41. + apply is_lim_seq_spec in H34. + specialize (H34 eps). + destruct H34. + specialize (H41 x0). + revert H41. apply eventually_impl. apply all_eventually. intros. unfold rvmaxabs. rewrite Rminus_0_r, Rabs_Rvector_max_abs. eapply Rle_lt_trans. - apply H40. - specialize (H33 x0). - cut_to H33; try lia. - rewrite Rminus_0_r in H33. - rewrite Rabs_right in H33. - - apply H33. + apply H41. + specialize (H34 x0). + cut_to H34; try lia. + rewrite Rminus_0_r, Rabs_right in H34. + - apply H34. - apply Rle_ge. apply Rmult_le_pos; try lra. left; apply cond_pos. } - revert H31. + revert H32. apply almost_impl. specialize (lim_w_0 n pf). revert lim_w_0. apply almost_impl. apply all_almost; intros ???. - generalize (is_lim_seq_plus' _ _ _ _ H32 H31). + generalize (is_lim_seq_plus' _ _ _ _ H33 H32). rewrite Rplus_0_r. apply is_lim_seq_ext. intros. @@ -4922,7 +4950,9 @@ Section jaakola_vector2. Rbar_le ((FiniteConditionalVariance prts (filt_sub k) (vecrvnth i pf (XF k))) ω) (C * (1 + Rvector_max_abs (X k ω))^2)) -> - (exists (C : R), forall k ω, Rvector_max_abs (X k ω) <= C) -> + (exists (C : Ts -> R), + (RandomVariable (F 0%nat) borel_sa C) /\ + (forall k ω, Rvector_max_abs (X k ω) <= C ω)) -> (forall k, rv_eq (X (S k)) (vecrvplus (vecrvminus (X k) (vecrvmult (α k) (X k))) (vecrvmult (β k) (XF k) ))) -> @@ -4931,6 +4961,14 @@ Section jaakola_vector2. is_lim_seq (fun m => vector_nth i pf (X m ω)) 0). Proof. intros. + assert (Fx_sub: forall x, sa_sub (F 0%nat) (F x)). + { + induction x. + - apply sa_equiv_sub. + reflexivity. + - rewrite IHx. + apply isfilt. + } destruct H2 as [? H2]. destruct H3 as [? H3]. pose (xx := (x + x0)%nat). @@ -4968,7 +5006,7 @@ Section jaakola_vector2. - simpl. rewrite H12. simpl in IHxx. - cut_to IHxx. + cut_to IHxx; trivial. + apply Rvector_plus_rv. * apply Rvector_minus_rv. -- now apply (RandomVariable_sa_sub (isfilt xx)). @@ -4981,8 +5019,6 @@ Section jaakola_vector2. + unfold IsFiltration. intros. apply isfilt. - + intros. - apply filt_sub. + intros ?. apply adapt_alpha. + intros ?. @@ -5138,8 +5174,11 @@ Section jaakola_vector2. apply FiniteConditionalExpectation_ext; reflexivity. - destruct H11. exists x1. - intros. - apply H11. + split. + + replace (0 + xx)%nat with xx by lia. + now apply (RandomVariable_sa_sub (Fx_sub xx)). + + intros. + apply H11. - intros. unfold XX, αα, ββ, XX, XXF. replace (S k + xx)%nat with (S (k + xx))%nat by lia. @@ -5199,7 +5238,9 @@ Section jaakola_vector2. Rbar_le ((FiniteConditionalVariance prts (filt_sub k) (vecrvnth i pf (XF k))) ω) (C * (1 + Rvector_max_abs (X k ω))^2)) -> - (exists (C : R), forall k ω, Rvector_max_abs (X k ω) <= C) -> + (exists (C : Ts -> R), + (RandomVariable (F 0%nat) borel_sa C) /\ + (forall k ω, Rvector_max_abs (X k ω) <= C ω)) -> (forall k, rv_eq (X (S k)) (vecrvplus (vecrvminus (X k) (vecrvmult (α k) (X k))) (vecrvmult (β k) (XF k) ))) ->