diff --git a/coq/QLearn/Tsitsiklis.v b/coq/QLearn/Tsitsiklis.v index 7a34486b..294f7188 100644 --- a/coq/QLearn/Tsitsiklis.v +++ b/coq/QLearn/Tsitsiklis.v @@ -4648,9 +4648,6 @@ Qed. forall i pf, almost prts (fun ω => Rbar_le (Lim_seq (sum_n (fun k : nat => Rsqr (vector_nth i pf (beta k ω))))) (Finite C))) -> - -(* (forall i pf, (almost prts (fun ω => is_lim_seq (sum_n (fun k => vector_nth i pf (α k ω))) p_infty))) -> -*) almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (α k ω))) p_infty) -> (exists (C : R), @@ -5645,6 +5642,1027 @@ Qed. lia. Qed. + Theorem Tsitsiklis1_Jaakkola_beta_uniform {n} (β : R) (X w α beta : nat -> Ts -> vector R (S n)) + (XF : nat -> Ts -> vector R (S n)) + {F : nat -> SigmaAlgebra Ts} + (isfilt : IsFiltration F) + (filt_sub : forall k, sa_sub (F k) dom) + (adapt_alpha : IsAdapted (Rvector_borel_sa (S n)) α F) + (adapt_beta : IsAdapted (Rvector_borel_sa (S n)) beta F) + {rvX0 : RandomVariable (F 0%nat) (Rvector_borel_sa (S n)) (X 0%nat)} + (adapt_w : IsAdapted (Rvector_borel_sa (S n)) w (fun k => F (S k))) + {rvXF : forall k, RandomVariable (F (S k)) (Rvector_borel_sa (S n)) (XF k)} + {rvw : forall k i pf, RandomVariable dom borel_sa (fun ω : Ts => vector_nth i pf (w k ω))} + {iscond : forall k i pf, is_conditional_expectation prts (F k) (vecrvnth i pf (w k)) (ConditionalExpectation prts (filt_sub k) (vecrvnth i pf (w k)))} : + + almost prts (fun ω => forall k i pf, 0 <= vector_nth i pf (α k ω) <= 1) -> + almost prts (fun ω => forall k i pf, 0 <= vector_nth i pf (beta k ω) <= 1) -> + almost prts (fun ω => forall k i pf, vector_nth i pf (beta k ω) <= vector_nth i pf (α k ω)) -> + almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (beta k ω))) p_infty) -> + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (beta n ω))))) -> + (exists epsilon : posreal, + eventually (fun n => forall i pf, + almostR2 prts Rbar_lt (fun ω => Lim_seq (sum_n (fun nn => rvsqr (vecrvnth i pf (beta (nn+n)%nat)) ω))) (const epsilon))) -> + almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (α k ω))) p_infty) -> + + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (α n ω))))) -> + (forall k i pf, almostR2 prts eq (ConditionalExpectation _ (filt_sub k) (vecrvnth i pf (w k))) (const 0)) -> + (exists (A B : R), + 0 < A /\ 0 < B /\ + forall k i pf, + almostR2 prts Rbar_le (ConditionalExpectation + _ (filt_sub k) + (rvsqr (vecrvnth i pf (w k)))) + (rvplus (const A) + (rvscale B (rvmaxlist + (fun j ω => rvsqr (rvmaxabs (X j)) ω) + k)))) -> + 0 <= β < 1 -> + (exists (D : nonnegreal), + almost prts (fun ω => + forall k, + Rvector_max_abs (XF k ω) <= β * Rvector_max_abs (X k ω) + D)) -> + (forall k, rv_eq (X (S k)) + (vecrvplus (vecrvminus (X k) (vecrvmult (α k) (X k))) (vecrvmult (beta k) (vecrvplus (XF k) (w k))))) -> + + exists (D0 : Ts -> R), forall k, almostR2 prts Rle (rvmaxabs (X k)) D0. + Proof. + intros H beta_prop alpha_beta_prop beta_inf beta_fin beta_eps. + intros. + assert (exists γ,β < γ < 1). + { + exists (β + (1 - β)/2). + lra. + } + destruct H5 as [D ?]. + destruct H7 as [γ ?]. + assert (exists G0, + 1 < G0 /\ + β * G0 + D <= γ * G0). + { + exists ((D + 1) / (γ - β)). + split. + - generalize (cond_nonneg D); intros. + rewrite <- Rlt_div_r; lra. + - field_simplify; try lra. + unfold Rdiv. + apply Rmult_le_compat_r; try lra. + left. + apply Rinv_0_lt_compat. + lra. + } + destruct H8 as [G0 [? ?]]. + assert (almost prts (fun ω => forall k i pf, + Rabs (vector_nth i pf (XF k ω)) <= + γ * Rmax (Rvector_max_abs (X k ω)) G0)). + { + revert H5; apply almost_impl. + apply all_almost; intros ω?. + intros. + eapply Rle_trans. + - apply Rvector_max_abs_nth_le. + - eapply Rle_trans. + apply H5. + unfold Rmax. + match_destr. + + apply Rle_trans with (r2 := β * G0 + D); try lra. + apply Rplus_le_compat_r. + apply Rmult_le_compat_l; try lra. + + assert (Rvector_max_abs (X k ω) > G0) by lra. + pose (G1 := Rvector_max_abs (X k ω) - G0). + replace (Rvector_max_abs (X k ω)) with (G0 + G1). + * assert (β * G1 <= γ * G1). + { + apply Rmult_le_compat_r; try lra. + unfold G1; lra. + } + lra. + * unfold G1; lra. + } + assert (exists ε, + 0 < ε /\ + γ * (1 + ε) = 1). + { + exists (1/γ - 1). + split. + - field_simplify; try lra. + apply Rdiv_lt_0_compat; lra. + - field_simplify; lra. + } + destruct H11 as [ε [? ?]]. + pose (M := fun t ω => Rmax_list_map (seq 0 (S t)) + (fun n0 : nat => rvmaxabs (X n0) ω)). + pose (G := fix G t := + match t with + | 0%nat => rvmax (M 0%nat) (const G0) + | S t' => rvchoice + (fun ω => + if Rle_dec (M t ω) ((1+ε)*(G t' ω)) then true else false) + (G t') + (rvscale G0 (fun ω => powerRZ_ge_fun (1 + ε) ((M t ω)/G0))) + end). + assert (forall t, rv_le (M t) (rvscale (1 + ε) (G t))). + { + intros ??. + destruct t. + - simpl. + unfold rvscale, rvmax, const. + apply Rle_trans with (r2 := 1 * Rmax (M 0%nat a) G0). + + rewrite Rmult_1_l. + apply Rmax_l. + + apply Rmult_le_compat_r. + * apply Rle_trans with (r2 := G0); try lra. + apply Rmax_r. + * lra. + - simpl. + unfold rvscale, rvchoice. + match_case; intros. + + match_destr_in H13. + + apply Rle_trans with (r2 := (1 + ε) * (M (S t) a)). + * rewrite <- (Rmult_1_l (M (S t) a)) at 1. + apply Rmult_le_compat_r; try lra. + unfold M. + apply Rmax_list_map_seq_ge; try lia. + exists (0%nat). + split; try lia. + apply rvmaxabs_pos. + * generalize (powerRZ_ge_scale (1 + ε) (M (S t) a) G0); intros. + cut_to H14; try lra. + apply Rmult_le_compat_l; try lra. + } + assert (forall t ω, + (G t ω < G (S t) ω) -> + (M (S t) ω <= G (S t) ω)). + { + intros ???. + simpl in H14; simpl. + unfold rvmax, const, rvchoice, rvscale in H14. + unfold rvmax, const, rvchoice, rvscale. + match_destr_in H14; try lra. + apply powerRZ_ge_scale; try lra. + } + assert (adaptX : IsAdapted (Rvector_borel_sa (S n)) X F). + { + intros ?. + induction n0. + - easy. + - rewrite H6. + apply Rvector_plus_rv. + + apply Rvector_minus_rv. + * now apply (RandomVariable_sa_sub (isfilt n0)). + * apply Rvector_mult_rv. + -- now apply (RandomVariable_sa_sub (isfilt n0)). + -- now apply (RandomVariable_sa_sub (isfilt n0)). + + apply Rvector_mult_rv. + * now apply (RandomVariable_sa_sub (isfilt n0)). + * apply Rvector_plus_rv; try easy. + } + assert (adaptM : IsAdapted borel_sa M F). + { + intros ?. + unfold M. + induction n0. + - unfold Rmax_list_map; simpl. + now apply Rvector_max_abs_rv. + - unfold Rmax_list_map. + assert (rv_eq + (fun ω : Ts => Max_{ seq 0 (S (S n0))}(fun n1 : nat => rvmaxabs (X n1) ω)) + (fun ω : Ts => Rmax (Max_{ seq 0 (S n0)}(fun n1 : nat => rvmaxabs (X n1) ω)) + (rvmaxabs (X (S n0)) ω))). + { + intros ?. + rewrite Rmax_list_Sn; try lia. + now replace (0 + S n0)%nat with (S n0) by lia. + } + assert (RandomVariable (F (S n0)) borel_sa + (fun ω : Ts => Rmax (Max_{ seq 0 (S n0)}(fun n1 : nat => rvmaxabs (X n1) ω)) + (rvmaxabs (X (S n0)) ω))). + { + apply rvmax_rv. + - now apply (RandomVariable_sa_sub (isfilt n0)). + - now apply Rvector_max_abs_rv. + } + revert H16. + apply RandomVariable_proper; try easy. + } + + assert (Mnneg:forall t ω, 0 <= M t ω). + { + intros. + unfold M. + apply Rmax_list_map_seq_ge; try lia. + exists (0%nat). + split; try lia. + apply rvmaxabs_pos. + } + + assert (Gnneg:forall t ω, 0 <= G t ω). + { + intros. + induction t. + - simpl. + unfold rvmax, const. + apply Rle_trans with (r2 := G0); try lra. + apply Rmax_r. + - simpl. + unfold rvchoice, rvscale. + match_destr. + generalize (powerRZ_ge_scale (1 + ε) (M (S t) ω) G0); intros. + cut_to H15; try lra. + specialize (Mnneg (S t) ω). + lra. + } + + assert (Gincr: forall t, rv_le (G t) (G (S t))). + { + intros ??. + simpl. + unfold rvchoice, rvscale. + match_case; intros; try lra. + match_destr_in H15. + assert (M (S t) a > (1 + ε) * G t a) by lra. + generalize (powerRZ_ge_scale (1 + ε) (M (S t) a) G0); intros. + cut_to H17; try lra. + apply Rle_trans with (r2 := (M (S t) a)); try lra. + apply Rle_trans with (r2 := (1 + ε) * G t a); try lra. + rewrite <- Rmult_1_l at 1. + apply Rmult_le_compat_r; try lra. + apply Gnneg. + } + + assert (Gpos1:forall t ω, 1 < G t ω). + { + intros. + induction t. + - simpl. + unfold rvmax, const. + apply Rlt_le_trans with (r2 := G0); try lra. + apply Rmax_r. + - specialize (Gincr t ω). + lra. + } + assert (Gpos:forall t ω, 0 < G t ω). + { + intros. + specialize (Gpos1 t ω);lra. + } + assert (adaptG : IsAdapted borel_sa G F). + { + intros ?. + induction n0. + - simpl. + typeclasses eauto. + - simpl. + assert (rvc:RandomVariable (F (S n0)) (discrete_sa bool) + (fun x : Ts => if Rle_dec (M (S n0) x) ((1 + ε) * G n0 x) then true else false)). + { + Existing Instance FiniteRange_FiniteRangeFunction. + apply (frf_singleton_rv _ _). + intros [|] _; unfold pre_event_singleton, pre_event_singleton, pre_event_preimage; simpl. + * apply sa_proper with + (x := (fun ω => (rvminus (M (S n0)) + (rvscale (1 + ε) (G n0)) ω) <= 0)). + -- intros ?. + rv_unfold'. + match_destr. + ++ assert (M (S n0) x - (1 + ε) * G n0 x <= 0) by lra. + try easy. + ++ assert (~(M (S n0) x - (1 + ε) * G n0 x <= 0)) by lra. + try easy. + -- apply sa_le_le_rv. + apply rvminus_rv; try easy. + apply (RandomVariable_sa_sub (isfilt n0)). + now apply rvscale_rv. + * apply sa_proper with + (x := (fun ω => (rvminus (M (S n0)) + (rvscale (1 + ε) (G n0)) ω) > 0)). + -- intros ?. + rv_unfold'. + match_destr. + ++ assert (~ (M (S n0) x - (1 + ε) * G n0 x > 0)) by lra. + try easy. + ++ assert ((M (S n0) x - (1 + ε) * G n0 x > 0)) by lra. + try easy. + -- apply sa_le_gt_rv. + apply rvminus_rv; try easy. + apply (RandomVariable_sa_sub (isfilt n0)). + now apply rvscale_rv. + } + apply rvchoiceb_rv; try easy. + + now apply (RandomVariable_sa_sub (isfilt n0)). + + apply rvscale_rv. + apply (@compose_rv Ts R R (F (S n0)) borel_sa borel_sa + (fun ω => M (S n0) ω / G0) + (fun z => powerRZ_ge_fun (1 + ε) z)). + * assert (RandomVariable (F (S n0)) borel_sa + (rvscale (/ G0) (M (S n0)))). + { + apply rvscale_rv. + apply adaptM. + } + revert H15. + apply RandomVariable_proper; try easy. + intros ?. + unfold rvscale; lra. + * apply powerRZ_ge_fun_rv. + } + + pose (ww := fun t => vecrvscalerv (rvinv (G t)) (w t)). + + assert (rvww : forall (k i : nat) (pf : (i < (S n))%nat), RandomVariable dom borel_sa (vecrvnth i pf (ww k))). + { + intros. + unfold ww. + apply vecrvnth_rv. + apply Rvector_scale_rv_rv. + - apply rvinv_rv. + now apply (RandomVariable_sa_sub (filt_sub k)). + - apply rv_vecrvnth. + apply rvw. + } + + assert (expw0 : forall k i pf, Expectation (vecrvnth i pf (w k)) = Some (Finite 0)). + { + intros. + specialize (H2 k i pf). + specialize (iscond k i pf). + generalize (@is_conditional_expectation_Expectation Ts dom prts (F k) (vecrvnth i pf (w k))); intros. + specialize (H15 _ _ _ iscond). + assert (RandomVariable dom Rbar_borel_sa + (ConditionalExpectation prts (filt_sub k) (vecrvnth i pf (w k)))). + { + apply (RandomVariable_sa_sub (filt_sub k)). + apply Condexp_rv. + } + generalize (Rbar_Expectation_almostR2_proper prts (ConditionalExpectation prts (filt_sub k) (vecrvnth i pf (w k))) (fun x : Ts => const 0 x) H2); intros. + rewrite H17 in H15. + now rewrite Rbar_Expectation_finite_const in H15. + } + assert (isfef : forall k i pf, IsFiniteExpectation prts (vecrvnth i pf (w k))). + { + intros. + unfold IsFiniteExpectation. + now rewrite expw0. + } + assert (isfefg: forall k i pf, IsFiniteExpectation prts (rvmult (vecrvnth i pf (w k)) (rvinv (G k)))). + { + intros. + destruct (IsFiniteExpectation_parts prts _ (isfef k i pf)). + assert (forall t ω, 0 < rvinv (G t) ω < 1). + { + intros. + specialize (Gpos1 t ω). + rewrite rvinv_Rinv; try lra. + split. + - apply Rinv_0_lt_compat; lra. + - replace 1 with (/ 1) by lra. + apply Rinv_lt_contravar; lra. + } + apply IsFiniteExpectation_from_parts. + - apply IsFiniteExpectation_bounded with + (rv_X1 := const 0) (rv_X3 := pos_fun_part (vecrvnth i pf (w k))); trivial. + + apply IsFiniteExpectation_const. + + apply positive_part_nnf. + + assert (rv_eq (fun x : Ts => nonneg (pos_fun_part (rvmult (vecrvnth i pf (w k)) (rvinv (G k))) x)) + (rvmult (fun x : Ts => nonneg (pos_fun_part (vecrvnth i pf (w k)) x)) + (rvinv (G k)))). + { + intros ?. + unfold rvmult. + unfold pos_fun_part. + simpl. + rewrite Rmax_mult. + - now rewrite Rmult_0_l. + - specialize (H17 k a); lra. + } + rewrite H18. + intros ?. + unfold rvmult. + rewrite <- Rmult_1_r. + apply Rmult_le_compat_l. + * apply positive_part_nnf. + * specialize (H17 k a); lra. + - apply IsFiniteExpectation_bounded with + (rv_X1 := const 0) (rv_X3 := neg_fun_part (vecrvnth i pf (w k))); trivial. + + apply IsFiniteExpectation_const. + + apply negative_part_nnf. + + assert (rv_eq (fun x : Ts => nonneg (neg_fun_part (rvmult (vecrvnth i pf (w k)) (rvinv (G k))) x)) + (rvmult (fun x : Ts => nonneg (neg_fun_part (vecrvnth i pf (w k)) x)) + (rvinv (G k)))). + { + intros ?. + unfold rvmult. + unfold neg_fun_part. + simpl. + rewrite Rmax_mult. + - rewrite Rmult_0_l. + f_equal. + lra. + - specialize (H17 k a); lra. + } + rewrite H18. + intros ?. + unfold rvmult. + rewrite <- Rmult_1_r. + apply Rmult_le_compat_l. + * apply negative_part_nnf. + * specialize (H17 k a); lra. + } + assert (forall k i pf, + almostR2 prts eq (ConditionalExpectation prts (filt_sub k) (vecrvnth i pf (ww k))) + (fun x : Ts => const 0 x)). + { + intros. + assert (RandomVariable (F k) borel_sa (rvinv (G k))). + { + now apply rvinv_rv. + } + assert (RandomVariable dom borel_sa (rvmult (vecrvnth i pf (w k)) (rvinv (G k)))). + { + apply rvmult_rv. + - apply rvw. + - apply rvinv_rv. + now apply (RandomVariable_sa_sub (filt_sub k)). + } + generalize (Condexp_factor_out prts (filt_sub k) (vecrvnth i pf (w k)) (rvinv (G k))); intros. + apply almost_prob_space_sa_sub_lift in H17. + revert H17; apply almost_impl. + specialize (H2 k i pf). + revert H2. + apply almost_impl, all_almost; intros ???. + unfold ww. + assert (rv_eq + (vecrvnth i pf (vecrvscalerv (rvinv (G k)) (w k))) + (rvmult (vecrvnth i pf (w k)) (rvinv (G k)))). + { + intros ?. + unfold vecrvnth, vecrvscalerv. + unfold rvmult. + rewrite Rvector_nth_scale. + lra. + } + erewrite (ConditionalExpectation_ext _ (filt_sub k) _ _ H18). + rewrite H17. + unfold Rbar_rvmult. + rewrite H2. + unfold const. + apply Rbar_mult_0_r. + } + + assert (exists (K : R), + forall k i pf, + almostR2 prts Rbar_le + (ConditionalExpectation prts (filt_sub k) (rvsqr (vecrvnth i pf (ww k)))) + (const K)). + { + destruct H3 as [A [B [? [? ?]]]]. + assert (exists (K : R), + forall t ω, + (A + B * Rsqr (M t ω))/(Rsqr (G t ω)) <= K). + { + exists ((A / Rsqr G0) + B * (Rsqr (1 + ε))). + intros. + assert (0 < (Rsqr (G t ω))). + { + unfold Rsqr. + now apply Rmult_lt_0_compat. + } + + assert (0 < Rsqr G0). + { + unfold Rsqr. + apply Rmult_lt_0_compat; lra. + } + + assert (A / (Rsqr (G t ω)) <= A / Rsqr G0). + { + unfold Rdiv. + apply Rmult_le_compat_l; try lra. + apply Rle_Rinv; try lra. + apply Rsqr_incr_1; try lra. + induction t. + - simpl. + unfold rvmax, const. + apply Rmax_r. + - cut_to IHt. + + eapply Rle_trans. + apply IHt. + apply Gincr. + + unfold Rsqr. + now apply Rmult_lt_0_compat. + - now left. + } + assert (0 <> (Rsqr (G t ω))). + { + now apply Rlt_not_eq. + } + assert ((B * Rsqr (M t ω))/(Rsqr (G t ω)) <= B * Rsqr (1 + ε)). + { + specialize (H13 t ω). + unfold rvscale in H13. + apply Rmult_le_reg_r with (r := Rsqr (G t ω)); try lra. + field_simplify; try lra. + rewrite Rmult_assoc. + apply Rmult_le_compat_l; try lra. + apply Rsqr_incr_1 in H13. + - rewrite Rsqr_mult in H13; try lra. + - apply Mnneg. + - apply Rle_trans with (r2 := (G t ω)). + + now left. + + rewrite <- Rmult_1_l at 1. + apply Rmult_le_compat_r; try lra. + now left. + } + generalize (Rplus_le_compat _ _ _ _ H20 H22); intros. + assert (0 <> Rsqr G0). + { + now apply Rlt_not_eq. + } + field_simplify in H23; try lra. + } + destruct H18 as [K ?]. + exists K. + intros. + specialize (H15 k i pf). + unfold ww. + generalize (is_conditional_expectation_factor_out_nneg_both_Rbar prts (filt_sub k) (rvsqr (vecrvnth i pf (w k))) (rvsqr (rvinv (G k)))); intros. + specialize (H19 (ConditionalExpectation prts (filt_sub k) (rvsqr (vecrvnth i pf (w k))))). + assert (RandomVariable dom borel_sa (rvsqr (rvinv (G k)))). + { + apply rvsqr_rv, rvinv_rv. + now apply (RandomVariable_sa_sub (filt_sub k)). + } + generalize (NonNegCondexp_cond_exp prts (filt_sub k) (rvmult (rvsqr (vecrvnth i pf (w k))) (rvsqr (rvinv (G k))))); intros. + assert (Rbar_NonnegativeFunction (ConditionalExpectation prts (filt_sub k) (rvsqr (vecrvnth i pf (w k)))) ). + { + apply Condexp_nneg. + typeclasses eauto. + } + assert (RandomVariable (F k) borel_sa (rvsqr (rvinv (G k)))). + { + now apply rvsqr_rv, rvinv_rv. + } + specialize (H19 _ _ _ _ _ _ _ ). + assert (rvgce : RandomVariable (F k) Rbar_borel_sa + (Rbar_rvmult (fun x : Ts => rvsqr (rvinv (G k)) x) + (ConditionalExpectation prts (filt_sub k) (rvsqr (vecrvnth i pf (w k)))))). + { + apply Rbar_rvmult_rv. + - apply Real_Rbar_rv. + typeclasses eauto. + - apply Condexp_rv. + } + specialize (H19 _). + cut_to H19. + - revert H15; apply almost_impl. + generalize (is_conditional_expectation_nneg_unique prts (filt_sub k) _ _ _ H19 H21); intros. + apply almost_prob_space_sa_sub_lift in H15. + revert H15; apply almost_impl. + specialize (H17 k i pf). + revert H17; apply almost_impl. + apply all_almost; intros ????. + erewrite Condexp_nneg_simpl. + assert (rv_eq + (rvsqr (vecrvnth i pf (vecrvscalerv (rvinv (G k)) (w k)))) + (rvmult (rvsqr (vecrvnth i pf (w k))) (rvsqr (rvinv (G k))))). + { + intros ?. + rv_unfold. + unfold vecrvscalerv, vecrvnth. + rewrite Rvector_nth_scale. + rewrite Rsqr_mult. + now apply Rmult_comm. + } + erewrite (NonNegCondexp_ext prts (filt_sub k) _ _ H25). + rewrite <- H17. + assert (rvmaxlist (fun (j : nat) (ω : Ts) => rvsqr (rvmaxabs (X j)) ω) k x <= Rsqr (M k x)). + { + unfold M, rvmaxlist, rvsqr. + unfold Rmax_list_map. + apply Rmax_list_le_iff. + - apply map_not_nil, seq_not_nil; lia. + - intros. + apply in_map_iff in H26. + destruct H26 as [? [? ?]]. + rewrite <- H26. + apply Rsqr_le_abs_1. + rewrite Rabs_pos_eq. + + rewrite Rabs_pos_eq. + apply (Rmax_spec_map (seq 0 (S k)) (fun n0 : nat => rvmaxabs (X n0) x) x1 H27). + apply Rmax_list_ge with (x := rvmaxabs (X x1) x). + * apply in_map_iff. + exists x1; split; trivial. + * apply rvmaxabs_pos. + + apply rvmaxabs_pos. + } + assert (Rbar_le (ConditionalExpectation prts (filt_sub k) (rvsqr (vecrvnth i pf (w k))) x) + (rvplus (const (Rabs A)) (rvscale (Rabs B) (rvsqr (M k))) x)). + { + eapply Rbar_le_trans. + apply H15. + rv_unfold. + simpl. + rewrite Rabs_right; try lra. + rewrite Rabs_right; try lra. + apply Rplus_le_compat_l. + apply Rmult_le_compat_l. + - lra. + - apply H26. + } + unfold Rbar_rvmult, const. + assert (0 < rvsqr (rvinv (G k)) x). + { + unfold rvsqr. + apply Rsqr_pos_lt. + apply Rgt_not_eq. + unfold rvinv, rvpower, const. + apply power_pos. + apply Gpos. + } + rewrite Rbar_mult_comm. + rewrite Rbar_mult_pos_le with (z := mkposreal _ H28) in H27. + simpl in H27. + rewrite Rbar_mult_mult_pos in H27. + eapply Rbar_le_trans. + apply H27. + rv_unfold. + simpl. + rewrite Rabs_right; try lra. + rewrite Rabs_right; try lra. + specialize (H18 k x). + unfold Rdiv in H18. + replace (Rsqr (rvinv (G k) x)) with (/ Rsqr (G k x)); trivial. + assert (G k x <> 0). + { + apply Rgt_not_eq, Gpos. + } + rewrite rvinv_Rinv; trivial. + rewrite Rsqr_inv; trivial. + - apply Condexp_cond_exp_nneg. + typeclasses eauto. + } + destruct + (classic + (exists D0 : Ts -> R, forall k : nat, almostR2 prts Rle (rvmaxabs (X k)) D0)); trivial. + push_neg_in H17. + assert (forall x : Ts -> R, exists x0 : nat, exists pt : Ts, Rgt (rvmaxabs (X x0) pt) (x pt)). + { + intros x. + specialize (H17 x). + destruct H17 as [x0 HH]. + exists x0. + unfold almostR2,almost in HH. + push_neg_in HH. + specialize (HH Ω ps_one). + destruct HH as [pt [_ HH]]. + exists pt. + lra. + } + pose (WW := fix WW i pf t' t0 := + match t' with + | 0%nat => const 0 + | (S t) => + rvplus + (rvmult + (rvminus (const 1) (vecrvnth i pf (α (t + t0)%nat))) + (WW i pf t t0)) + (rvmult (vecrvnth i pf (beta (t + t0)%nat)) + (vecrvnth i pf (ww (t + t0)%nat))) + end). + assert (forall i pf, + almost prts (fun ω => is_lim_seq (fun k => WW i pf k 0%nat ω) 0)). + { + intros. +(* + destruct H1 as [Ca ?]. + destruct beta_fin as [Cb ?]. +*) + destruct H16 as [K ?]. + + apply lemma1_alpha_beta_uniform with + (α := fun k => vecrvnth i pf (α k)) + (β := fun k => vecrvnth i pf (beta k)) + (w := fun k => vecrvnth i pf (ww k)) + (filt_sub := filt_sub) + (rv := fun k => rvww k i pf) + (B := fun _ => const K); try easy. + - simpl. + apply rvconst. + - unfold IsAdapted; intros. + apply rvconst. + - unfold IsAdapted; intros. + unfold ww. + apply vecrvnth_rv. + apply Rvector_scale_rv_rv. + + apply rvinv_rv. + now apply (RandomVariable_sa_sub (isfilt n0)). + + apply adapt_w. + - unfold IsAdapted. + intros. + now apply vecrvnth_rv. + - unfold IsAdapted. + intros. + now apply vecrvnth_rv. + - intros. + apply Condexp_cond_exp. + unfold ww. + specialize (isfefg n0 i pf). + revert isfefg. + apply IsFiniteExpectation_proper. + intros ?. + unfold vecrvnth, vecrvscalerv, rvmult, Rvector_scale. + rewrite vector_nth_map. + apply Rmult_comm. + - intros. + revert H. + apply almost_impl. + apply all_almost. + intros ??. + apply H. + - intros. + revert beta_prop. + apply almost_impl. + apply all_almost. + intros ??. + apply H19. + - intros. + revert H. + apply almost_impl. + apply all_almost. + intros ??. + apply H. + - intros. + revert beta_prop. + apply almost_impl. + apply all_almost. + intros ??. + apply H19. + - revert H0; apply almost_impl. + apply all_almost; intros ??. + specialize (H0 i pf). + now unfold vecrvnth. + - revert beta_inf; apply almost_impl. + apply all_almost; intros ??. + apply H19. + - apply beta_fin. + - destruct beta_eps as [eps ?]. + exists eps. + revert H19. + apply eventually_impl. + apply all_eventually. + intros. + specialize (H19 i pf). + revert H19. + apply almost_impl, all_almost. + intros ??. + now unfold rvsqr, vecrvnth. + - intros. + simpl. + rv_unfold. + replace (n0 + 0)%nat with n0 by lia. + lra. + - exists (const K). + apply all_almost. + intros. + apply Rle_abs. + } + + assert (almost prts (fun ω => + forall i pf, + is_lim_seq (fun k => WW i pf k 0%nat ω) 0)). + { + apply almost_bounded_forall. + intros. + - apply lt_dec. + - intros. + apply is_lim_seq_ext with (u := (fun k : nat => WW i pf1 k 0%nat x)); trivial. + intros. + now rewrite (digit_pf_irrel _ _ pf2 pf1). + - apply H19. + } + + assert (almost prts (fun ω => + is_lim_seq (fun k : nat => M k ω) p_infty -> + exists t0 : nat, + forall t, + (G t0 ω = G (t + t0)%nat ω))). + { + generalize (lemma3_almost_Jaakkola_beta WW ε G0 α beta X ww M G XF); intros. + cut_to H21; try easy. + - assert (almost prts (fun ω : Ts => is_lim_seq (fun k : nat => M k ω) p_infty -> exists t0 : nat, M t0 ω <= G t0 ω /\ (forall (t i : nat) (pf : (i < S n)%nat), Rabs (WW i pf t t0 ω) <= ε))). + { + revert H; apply almost_impl. + revert beta_prop; apply almost_impl. + revert H20; apply almost_impl, all_almost; intros ?????. + generalize (lemma3_pre0 x (mkposreal _ H11) G M H23); intros. + cut_to H24; try easy. + - generalize (lemma3_pre1_beta WW x (mkposreal _ H11) α beta ww ); intros. + cut_to H25; try easy. + + destruct H25. + specialize (H24 x0). + destruct H24 as [? [? ?]]. + exists x1. + split; trivial. + intros. + specialize (H25 i pf x1 t H24). + apply H25. + + intros. + apply H22. + + intros. + apply H20. + + intros. + simpl. + rv_unfold. + lra. + - intros. + simpl. + apply H13. + - intros. + apply Gincr. + - intros. + now apply H14. + } + specialize (H21 H22). + revert H21. + apply almost_impl, all_almost; intros ???. + destruct (H21 H23). + exists x0. + intros. + symmetry. + apply H24. + - intros. + simpl. + unfold rvchoice. + match_case; intros. + now match_destr_in H23. + - intros. + apply H13. + - intros. + unfold M. + unfold Rmax_list_map. + rewrite Rmax_list_Sn; try lia. + now simpl. + - intros. + unfold M. + apply Rle_trans with (r2 := rvmaxabs (X t) ω). + + apply Rvector_max_abs_nth_le. + + unfold Rmax_list_map. + apply Rmax_spec. + apply in_map_iff. + exists t. + split; trivial. + apply in_seq. + lia. + - intros. + simpl. + rv_unfold. + lra. + - intros. + rewrite H6. + intros ?. + unfold ww, vecrvscalerv. + unfold vecrvminus, vecrvplus, vecrvmult, vecrvopp, vecrvscale. + do 3 f_equal. + rewrite Rvector_scale_scale. + specialize (Gpos k a). + rewrite rvinv_Rinv; trivial. + rewrite <- Rinv_r_sym; try lra. + now rewrite Rvector_scale1. + - revert H10; apply almost_impl. + apply all_almost; intros a?. + intros. + eapply Rle_trans. + apply H10. + assert (Rvector_max_abs (X k a) <= (1 + ε) * G k a). + { + apply Rle_trans with (r2 := M k a). + - unfold M. + unfold Rmax_list_map, rvmaxabs. + apply Rmax_spec. + apply in_map_iff. + exists k. + split; trivial. + apply in_seq. + lia. + - apply H13. + } + replace (G k a) with (γ * ((1 + ε) * G k a)). + + apply Rmult_le_compat_l; try lra. + apply Rle_Rmax. + split; trivial. + apply Rle_trans with (r2 := G k a). + * clear H22. + induction k. + -- simpl. + unfold rvmax, const. + apply Rmax_r. + -- eapply Rle_trans. + apply IHk. + apply Gincr. + * rewrite <- Rmult_1_l at 1. + apply Rmult_le_compat_r; try lra. + left; apply Gpos. + + rewrite <- Rmult_assoc. + rewrite H12. + lra. + } + assert (almost prts (fun ω => + is_lim_seq (fun k : nat => M k ω) p_infty -> + exists D0 : R, + forall t, + M t ω <= D0)). + { + revert H21. + apply almost_impl, all_almost; intros ???. + destruct (H21 H22). + exists ((1 + ε) * (G x0 x)). + intros. + destruct (le_dec t x0). + - apply Rle_trans with (r2 := M x0 x). + + unfold M. + apply Rmax_seq_map_monotone. + lia. + + apply H13. + - specialize (H23 (t - x0)%nat). + replace (t - x0 + x0)%nat with t in H23 by lia. + rewrite H23. + apply H13. + } + assert (almost prts + (fun ω => exists D0 : R, + forall t, + M t ω <= D0)). + { + revert H22. + apply almost_impl, all_almost; intros ??. + destruct (classic (is_lim_seq (fun k : nat => M k x) p_infty)). + - specialize (H22 H23). + destruct H22. + exists x0. + intros. + apply H22. + - assert (ex_finite_lim_seq (fun k => M k x)). + { + assert (forall k, M k x <= M (S k) x). + { + intros. + unfold M. + apply Rmax_seq_map_monotone. + lia. + } + generalize (ex_lim_seq_incr _ H24); intros. + apply ex_finite_lim_seq_correct. + split; trivial. + case_eq (Lim_seq (fun k : nat => M k x)); intros. + - now simpl. + - apply Lim_seq_correct in H25. + now rewrite H26 in H25. + - generalize (Lim_seq_pos (fun k => M k x)); intros. + cut_to H27. + + now rewrite H26 in H27. + + intros. + apply Mnneg. + } + destruct H24. + apply is_lim_seq_bounded in H24. + destruct H24. + exists x1. + intros. + specialize (H24 t). + eapply Rle_trans. + shelve. + apply H24. + Unshelve. + apply Rle_abs. + } + assert (exists D0 : Ts -> R, + forall k, almostR2 prts Rle (M k) D0). + { + apply exists_almost in H23. + destruct H23 as [??]. + exists x. + now apply forall_almost. + } + destruct H24. + exists x. + intros. + specialize (H24 k). + revert H24. + apply almost_impl, all_almost; intros ??. + unfold M in H24. + unfold Rmax_list_map in H24. + eapply Rle_trans. + shelve. + apply H24. + Unshelve. + apply Rmax_spec. + apply in_map_iff. + exists k. + split; trivial. + apply in_seq. + lia. + Qed. + Theorem Tsitsiklis3_beta_pos {n} (X w α : nat -> Ts -> vector R n) (β : R) (D0' : Ts -> R) diff --git a/coq/QLearn/jaakkola_vector.v b/coq/QLearn/jaakkola_vector.v index 6aca62ca..9602dae5 100644 --- a/coq/QLearn/jaakkola_vector.v +++ b/coq/QLearn/jaakkola_vector.v @@ -3648,7 +3648,6 @@ Section jaakola_vector2. - apply Lim_seq_const. Qed. - Theorem Jaakkola_alpha_beta_bounded (γ : R) (X XF α β : nat -> Ts -> vector R (S N)) @@ -3672,14 +3671,8 @@ Section jaakola_vector2. almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (α k ω))) p_infty) -> almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (β k ω))) p_infty) -> - - (exists (C : R), - forall i pf, - almost prts (fun ω => Rbar_le (Lim_seq (sum_n (fun k : nat => Rsqr (vector_nth i pf (α k ω))))) (Finite C))) -> - (exists (C : R), - forall i pf, - almost prts (fun ω => Rbar_le (Lim_seq (sum_n (fun k : nat => Rsqr (vector_nth i pf (β k ω))))) (Finite C))) -> - + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (α n ω))))) -> + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (β n ω))))) -> (almost prts (fun ω => forall k i pf, @@ -3696,6 +3689,9 @@ Section jaakola_vector2. almost prts (fun ω => 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)))) -> + (exists epsilon : posreal, + eventually (fun n => forall i pf, + almostR2 prts Rbar_lt (fun ω => Lim_seq (sum_n (fun nn => rvsqr (vecrvnth i pf (β (nn+n)%nat)) ω))) (const epsilon))) -> almost prts (fun ω => forall i pf, is_lim_seq (fun m => vector_nth i pf (X m ω)) 0). @@ -3773,14 +3769,14 @@ Section jaakola_vector2. destruct H9 as [? ?]. exists (rvscale x (rvsqr (rvplus (const 1) x0))). intros. - revert H12; apply almost_impl. + revert H13; apply almost_impl. revert H9; apply almost_impl. apply all_almost; intros ???. intros. - specialize (H12 k i pf). + specialize (H13 k i pf). eapply Rle_trans. - simpl in H12. - apply H12. + simpl in H13. + apply H13. unfold rvmult, rvsqr, rvplus, const. apply Rmult_le_compat_l; try lra. unfold Rsqr. @@ -3848,14 +3844,14 @@ Section jaakola_vector2. generalize (condexp_condexp_diff_0 (vecrvnth i pf (XF k)) (filt_sub k)). apply almost_impl. apply all_almost; intros ??. - rewrite <- H18. + rewrite <- H19. now apply ConditionalExpectation_ext. } - revert H17. + revert H18. apply almost_impl. apply all_almost. intros ??. - rewrite <- H17. + rewrite <- H18. apply ConditionalExpectation_ext. intros ?. unfold vecrvminus, vecrvplus, vecrvopp, vecrvscale, vector_FiniteConditionalExpectation. @@ -3870,8 +3866,6 @@ Section jaakola_vector2. rewrite vector_dep_zip_nth_proj1. now rewrite vector_nth_fun_to_vector. } - destruct H5 as [Ca ?]. - destruct H6 as [Cb ?]. assert (eqvec: forall k i pf, rv_eq (vecrvnth i pf @@ -3912,16 +3906,16 @@ Section jaakola_vector2. forall k i pf, (FiniteConditionalExpectation prts (filt_sub k) (rvsqr (vecrvnth i pf (r k)))) ω <= (B ω))). { - unfold FiniteConditionalVariance in H12. - destruct H12 as [C H12]. + unfold FiniteConditionalVariance in H13. + destruct H13 as [C H13]. exists C. - revert H12; apply almost_impl. + revert H13; apply almost_impl. apply all_almost; intros ??. intros. - specialize (H12 k i pf). + specialize (H13 k i pf). unfold r. eapply Rle_trans; cycle 1. - apply H12. + apply H13. right. apply FiniteConditionalExpectation_ext. intros ?. @@ -3929,18 +3923,18 @@ Section jaakola_vector2. f_equal. now rewrite eqvec. } - destruct H18 as [B ?]. + destruct H19 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_alpha_beta_alt + generalize (fun i pf => lemma1_alpha_beta_alt_uniform (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 ω))); intros. - apply (H19 n1 pf Ca Cb F isfilt filt_sub _ _); clear H19; trivial. + apply (H20 n1 pf isfilt filt_sub _ _); clear H20; trivial. - unfold IsAdapted; intros. apply vecrvnth_rv. unfold r. @@ -3958,7 +3952,7 @@ Section jaakola_vector2. apply adapt_beta. - intros. apply Condexp_cond_exp. - apply H15. + apply H16. - intros. revert H0. apply almost_impl. @@ -3985,7 +3979,13 @@ Section jaakola_vector2. - revert H4. apply almost_impl. now apply all_almost; intros ??. - - apply H6. + - destruct H11 as [eps H11]. + exists eps. + revert H11. + apply eventually_impl. + apply all_eventually. + intros. + apply H11. - intros. simpl. unfold vecrvminus, vecrvmult, vecrvplus, vecrvopp, vecrvscale. @@ -3994,13 +3994,13 @@ Section jaakola_vector2. repeat rewrite Rvector_nth_mult. lra. - exists B. - revert H18; apply almost_impl. + revert H19; apply almost_impl. apply all_almost; intros ??. intros. - specialize (H18 n n1 pf). + specialize (H19 n n1 pf). generalize (FiniteCondexp_eq prts (filt_sub n)); intros. - specialize (H19 (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))). + specialize (H20 (rvsqr (fun ω : Ts => vector_nth n1 pf (r n ω))) + (@rvsqr_rv Ts dom (@vecrvnth Ts R (S N) n1 pf (r n)) (H14 n n1 pf))). assert (IsFiniteExpectation prts (rvsqr (fun ω : Ts => vector_nth n1 pf (r n ω)))). { generalize (isfe2 n n1 pf). @@ -4012,20 +4012,20 @@ Section jaakola_vector2. rewrite <- eqvec. reflexivity. } - specialize (H19 H20). - unfold vecrvnth in H18. + specialize (H20 H21). unfold vecrvnth in H19. - rewrite H19. + unfold vecrvnth in H20. + rewrite H20. simpl. unfold const. - eapply Rle_trans; [| apply H18]. + eapply Rle_trans; [| apply H19]. right. apply FiniteConditionalExpectation_ext. reflexivity. } apply almost_bounded_forall; intros. - apply lt_dec. - - revert H19. + - revert H20. apply is_lim_seq_ext. intros. apply vector_nth_ext. @@ -4062,7 +4062,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 -> @@ -4135,7 +4135,7 @@ Section jaakola_vector2. apply Rmult_le_compat_l; try lra. rewrite vector_FiniteConditionalExpectation_nth. specialize (H7 n0 i pf0). - rewrite H11 in H7. + rewrite H12 in H7. eapply Rle_trans; cycle 1. assert ( γ * Rvector_max_abs (vecrvplus (δ n0) (w n0) ω) <= γ * Rvector_max_abs (Rvector_plus (Rvector_abs (δ n0 ω)) (Rvector_abs (w n0 ω)))). @@ -4152,7 +4152,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. @@ -4242,10 +4242,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 ??. @@ -4259,25 +4259,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 @@ -4289,12 +4289,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. @@ -4307,7 +4307,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. @@ -4327,10 +4327,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)). { @@ -4425,9 +4425,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 @@ -4447,7 +4447,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 ??. @@ -4455,28 +4455,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. @@ -4490,62 +4490,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)). { @@ -4564,13 +4564,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)) <= @@ -4585,10 +4585,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. @@ -4611,7 +4611,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. @@ -4621,12 +4621,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. @@ -4644,7 +4644,7 @@ Section jaakola_vector2. { intros. eapply Rle_trans. - apply H38. + apply H39. apply Rle_abs. } @@ -4663,33 +4663,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), @@ -4709,7 +4709,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)). @@ -4722,9 +4722,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. } @@ -4739,8 +4739,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 @@ -4758,9 +4758,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. @@ -4787,25 +4787,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 @@ -4822,8 +4822,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 => @@ -4849,38 +4849,38 @@ 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, 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. - rewrite H11. + rewrite H12. unfold vecrvplus. now rewrite Rvector_nth_plus. Qed. @@ -4911,12 +4911,8 @@ Section jaakola_vector2. almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (α k ω))) p_infty) -> almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (β k ω))) p_infty) -> - (exists (C : R), - forall i pf, - almost prts (fun ω => Rbar_le (Lim_seq (sum_n (fun k : nat => Rsqr (vector_nth i pf (α k ω))))) (Finite C))) -> - (exists (C : R), - forall i pf, - almost prts (fun ω => Rbar_le (Lim_seq (sum_n (fun k : nat => Rsqr (vector_nth i pf (β k ω))))) (Finite C))) -> + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (α n ω))))) -> + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (β n ω))))) -> (almost prts (fun ω => forall k i pf, @@ -4934,6 +4930,9 @@ Section jaakola_vector2. almost prts (fun ω => 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) ))) -> + (exists epsilon : posreal, + eventually (fun n => forall i pf, + almostR2 prts Rbar_lt (fun ω => Lim_seq (sum_n (fun nn => rvsqr (vecrvnth i pf (β (nn+n)%nat)) ω))) (const epsilon))) -> almost prts (fun ω => forall i pf, is_lim_seq (fun m => vector_nth i pf (X m ω)) 0). @@ -5028,7 +5027,7 @@ Section jaakola_vector2. intros. unfold XXF. generalize (isfe2 (k + xx)%nat i pf); intros. - revert H13. + revert H14. apply IsFiniteExpectation_proper. intros ?. unfold rvsqr; f_equal. @@ -5040,12 +5039,33 @@ Section jaakola_vector2. generalize (Jaakkola_alpha_beta_bounded γ XX XXF αα ββ isfilt_FF (fun k => filt_sub (k + xx)%nat) adapt_aa adapt_bb H); intros jak_bound. cut_to jak_bound; trivial. + cut_to jak_bound. - revert jak_bound; apply almost_impl. apply all_almost; intros ??. intros. - specialize (H13 i pf). - unfold XX in H13. + specialize (H14 i pf). + unfold XX in H14. now apply is_lim_seq_incr_n with (N := xx). + - destruct H13 as [eps H13]. + exists eps. + unfold ββ. + destruct H13 as [NN ?]. + exists NN. + intros. + specialize (H13 (n + xx)%nat). + cut_to H13; try lia. + specialize (H13 i pf). + revert H13. + apply almost_impl. + apply all_almost; intros ??. + eapply Rbar_le_lt_trans; cycle 1. + apply H13. + apply slln.eq_Rbar_le. + apply Lim_seq_ext. + intros. + apply sum_n_ext. + intros. + now replace (n1 + (n + xx))%nat with (n1 + n + xx)%nat by lia. - unfold αα. apply almost_forall. intros. @@ -5089,45 +5109,26 @@ Section jaakola_vector2. intros. specialize (H6 i pf). now apply is_lim_seq_sum_shift_inf with (N := xx) in H6. - - destruct H7. - exists x1. - intros. + - intros. specialize (H7 i pf). revert H7; apply almost_impl. apply all_almost; intros ??. unfold αα. - rewrite <- (Lim_seq_incr_n (sum_n (fun k : nat => (vector_nth i pf (α k x2))²)) xx) in H7. - unfold sum_n in H7. - erewrite Lim_seq_ext; cycle 1. - { intros. - rewrite <- (sum_n_m_shift (fun k : nat => (vector_nth i pf (α (k)%nat x2))²) xx n). - reflexivity. - } - eapply Rbar_le_trans; try apply H7. - apply Lim_seq_le; intros. - destruct xx; [reflexivity |]. - rewrite (sum_split (fun k : nat => (vector_nth i pf (α k x2))²) 0 (n + S xx) xx); unfold plus; simpl; try lia. - cut (0 <= sum_n_m (fun k : nat => (vector_nth i pf (α k x2))²) 0 xx); try lra. - apply nneg_sum_n_m_sq. - - destruct H8. - exists x1. - - unfold ββ; intros i pf. - generalize (H8 i pf). - apply almost_impl; apply all_almost; intros ? HH. - rewrite <- (Lim_seq_incr_n (sum_n (fun k : nat => (vector_nth i pf (β k x2))²)) xx) in HH. - unfold sum_n in HH. - erewrite Lim_seq_ext; cycle 1. - { intros. - rewrite <- (sum_n_m_shift (fun k : nat => (vector_nth i pf (β (k)%nat x2))²) xx n). - reflexivity. - } - eapply Rbar_le_trans; try apply HH. - apply Lim_seq_le; intros. - destruct xx; [reflexivity |]. - rewrite (sum_split (fun k : nat => (vector_nth i pf (β k x2))²) 0 (n + S xx) xx); unfold plus; simpl; try lia. - cut (0 <= sum_n_m (fun k : nat => (vector_nth i pf (β k x2))²) 0 xx); try lra. - apply nneg_sum_n_m_sq. + rewrite ex_series_incr_n with (n := xx) in H7. + revert H7. + apply ex_series_ext. + intros. + now replace (xx + n)%nat with (n + xx)%nat by lia. + - intros. + specialize (H8 i pf). + revert H8; apply almost_impl. + apply all_almost; intros ??. + unfold ββ. + rewrite ex_series_incr_n with (n := xx) in H8. + revert H8. + apply ex_series_ext. + intros. + now replace (xx + n)%nat with (n + xx)%nat by lia. - revert H9; apply almost_impl. apply all_almost; intros ??. intros. @@ -5141,21 +5142,21 @@ Section jaakola_vector2. - destruct H10 as [? [??]]. exists x1. split; trivial. - revert H13; apply almost_impl. + revert H14; apply almost_impl. apply all_almost; intros ??. intros. unfold XX, XXF. - specialize (H13 (k + xx)%nat i pf). + specialize (H14 (k + xx)%nat i pf). eapply Rle_trans; cycle 1. - apply H13. + apply H14. simpl. right. apply FiniteConditionalExpectation_ext; intros ?. unfold rvsqr, rvminus, rvplus, rvopp, rvscale. do 3 f_equal. apply FiniteConditionalExpectation_ext; reflexivity. - - destruct H11 as [? ?]. - clear jak_bound. + - clear jak_bound. + destruct H11 as [? ?]. exists x1. revert H11; apply almost_impl. apply all_almost; intros ??. @@ -5198,12 +5199,8 @@ Section jaakola_vector2. almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (α k ω))) p_infty) -> almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (β k ω))) p_infty) -> - (exists (C : R), - forall i pf, - almost prts (fun ω => Rbar_le (Lim_seq (sum_n (fun k : nat => Rsqr (vector_nth i pf (α k ω))))) (Finite C))) -> - (exists (C : R), - forall i pf, - almost prts (fun ω => Rbar_le (Lim_seq (sum_n (fun k : nat => Rsqr (vector_nth i pf (β k ω))))) (Finite C))) -> + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (α n ω))))) -> + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (β n ω))))) -> (almost prts (fun ω => forall k i pf, @@ -5289,7 +5286,73 @@ Section jaakola_vector2. + intros. erewrite vector_nth_ext; try apply H14. + apply H13. - Qed. + - assert (forall i pf, + exists epsilon : posreal, + eventually + (fun n : nat => + almostR2 prts Rbar_lt + (fun ω : Ts => + Lim_seq + (sum_n (fun nn : nat => rvsqr (vecrvnth i pf (β (nn + n)%nat)) ω))) + (fun x : Ts => const epsilon x))). + { + intros. + specialize (H9 i pf). + generalize (uniform_converge_sum_sq_tails _ (H6 i pf)); intros. + assert (0 < 2) by lra. + exists (mkposreal _ H14). + assert (0 < 1) by lra. + simpl in H13. + specialize (H13 H9 (mkposreal _ H15)). + destruct H13. + exists (S x). + intros. + specialize (H13 (n-1)%nat). + cut_to H13; try lia. + revert H13. + apply almost_impl. + apply all_almost; intros ??. + simpl. + simpl in H13. + assert (Rbar_lt 1 2) by (simpl; lra). + eapply Rbar_le_lt_trans; cycle 1. + apply H17. + eapply Rbar_le_trans; cycle 1. + apply H13. + apply slln.eq_Rbar_le. + apply Lim_seq_ext; intros. + apply sum_n_ext; intros. + unfold rvsqr. + now replace (S (n - 1 + n1)) with (n1 + n)%nat by lia. + } + generalize + (bounded_nat_ex_choice_vector + (A := R) (n := S N) + (fun i pf eps => + 0 < eps /\ + eventually + (fun n : nat => + almostR2 prts Rbar_lt + (fun ω : Ts => + Lim_seq + (sum_n (fun nn : nat => rvsqr (vecrvnth i pf (β (nn + n)%nat)) ω))) + (fun x : Ts => const eps x)))); intros. + cut_to H14. + + destruct H14. + pose (eps := Rvector_max_abs x). + assert (0 < eps). + { + assert (forall i pf, 0 < vector_nth i pf x). + { + intros. + specialize (H14 i pf). + apply H14. + } + admit. + } + exists (mkposreal _ H15). + admit. + Admitted. Lemma Binomial_C_2_1 : Binomial.C 2 1 = 2. Proof. @@ -5367,13 +5430,8 @@ Section jaakola_vector2. almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (α k ω))) p_infty) -> almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (β k ω))) p_infty) -> - - (exists (C : R), - forall i pf, - almost prts (fun ω => Rbar_le (Lim_seq (sum_n (fun k : nat => Rsqr (vector_nth i pf (α k ω))))) (Finite C))) -> - (exists (C : R), - forall i pf, - almost prts (fun ω => Rbar_le (Lim_seq (sum_n (fun k : nat => Rsqr (vector_nth i pf (β k ω))))) (Finite C))) -> + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (α n ω))))) -> + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (β n ω))))) -> (almost prts (fun ω => forall k i pf, @@ -5393,13 +5451,16 @@ Section jaakola_vector2. *) (forall k, rv_eq (X (S k)) (vecrvplus (vecrvminus (X k) (vecrvmult (α k) (X k))) (vecrvmult (β k) (XF k)))) -> + (exists epsilon : posreal, + eventually (fun n => forall i pf, + almostR2 prts Rbar_lt (fun ω => Lim_seq (sum_n (fun nn => rvsqr (vecrvnth i pf (β (nn+n)%nat)) ω))) (const epsilon))) -> almost prts (fun ω => forall i pf, is_lim_seq (fun m => vector_nth i pf (X m ω)) 0). Proof. intros. apply (Jaakkola_alpha_beta_bounded γ X XF α β isfilt filt_sub _ _); trivial. - generalize (Tsitsiklis1_Jaakkola_beta γ X); intros Tsit1. + generalize (Tsitsiklis1_Jaakkola_beta_uniform γ X); intros Tsit1. assert (rvXF2 : forall k, RandomVariable dom (Rvector_borel_sa (S N)) (XF k)). { intros. @@ -5438,16 +5499,16 @@ Section jaakola_vector2. } specialize (Tsit1 w α β XF2 F isfilt filt_sub _ _ _ _ _ _). cut_to Tsit1; trivial; try lra. - cut_to Tsit1. + cut_to Tsit1; try lra. - destruct Tsit1. exists x. - apply almost_forall in H10. - revert H10; apply almost_impl. + apply almost_forall in H11. + revert H11; apply almost_impl. apply all_almost; intros ??. intros. - apply H10. + apply H11. - assert (0 <= 0) by lra. - exists (mknonnegreal _ H10). + exists (mknonnegreal _ H11). revert H7; apply almost_impl. apply all_almost; intros ??. intros. @@ -5478,7 +5539,7 @@ Section jaakola_vector2. rewrite Rvector_plus_inv. now rewrite Rvector_plus_zero. } - now rewrite H10. + now rewrite H11. - intros. apply Condexp_cond_exp. unfold w. @@ -5496,7 +5557,7 @@ Section jaakola_vector2. rewrite vector_FiniteConditionalExpectation_nth'. apply FiniteCondexp_isfe. } - revert H10. + revert H11. apply IsFiniteExpectation_proper. unfold vecrvnth, vecrvminus, vecrvplus, vecrvopp, vecrvscale. intros ?. @@ -5511,7 +5572,7 @@ Section jaakola_vector2. generalize (condexp_condexp_diff_0 (vecrvnth i pf (XF k)) (filt_sub k)). apply almost_impl. apply all_almost; intros ??. - rewrite <- H11. + rewrite <- H12. apply ConditionalExpectation_ext. intros ?. unfold vecrvminus, vecrvplus, vecrvopp, vecrvscale. @@ -5590,7 +5651,7 @@ Section jaakola_vector2. + revert HH; apply almost_impl. apply all_almost; intros ??. simpl. - apply H10. + apply H11. Qed. Theorem Jaakkola_alpha_beta_unbounded_eventually_almost @@ -5618,12 +5679,8 @@ Section jaakola_vector2. almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (α k ω))) p_infty) -> almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (β k ω))) p_infty) -> - (exists (C : R), - forall i pf, - almost prts (fun ω => Rbar_le (Lim_seq (sum_n (fun k : nat => Rsqr (vector_nth i pf (α k ω))))) (Finite C))) -> - (exists (C : R), - forall i pf, - almost prts (fun ω => Rbar_le (Lim_seq (sum_n (fun k : nat => Rsqr (vector_nth i pf (β k ω))))) (Finite C))) -> + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (α n ω))))) -> + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (β n ω))))) -> (almost prts (fun ω => forall k i pf, @@ -5642,6 +5699,9 @@ Section jaakola_vector2. *) (forall k, rv_eq (X (S k)) (vecrvplus (vecrvminus (X k) (vecrvmult (α k) (X k))) (vecrvmult (β k) (XF k) ))) -> + (exists epsilon : posreal, + eventually (fun n => forall i pf, + almostR2 prts Rbar_lt (fun ω => Lim_seq (sum_n (fun nn => rvsqr (vecrvnth i pf (β (nn+n)%nat)) ω))) (const epsilon))) -> almost prts (fun ω => forall i pf, is_lim_seq (fun m => vector_nth i pf (X m ω)) 0). @@ -5736,7 +5796,7 @@ Section jaakola_vector2. intros. unfold XXF. generalize (isfe2 (k + xx)%nat i pf); intros. - revert H12. + revert H13. apply IsFiniteExpectation_proper. intros ?. unfold rvsqr; f_equal. @@ -5751,8 +5811,8 @@ Section jaakola_vector2. - revert jak_bound; apply almost_impl. apply all_almost; intros ??. intros. - specialize (H12 i pf). - unfold XX in H12. + specialize (H13 i pf). + unfold XX in H13. now apply is_lim_seq_incr_n with (N := xx). - unfold αα. apply almost_forall. @@ -5797,45 +5857,26 @@ Section jaakola_vector2. intros. specialize (H6 i pf). now apply is_lim_seq_sum_shift_inf with (N := xx) in H6. - - destruct H7. - exists x1. - intros. + - intros. specialize (H7 i pf). revert H7; apply almost_impl. apply all_almost; intros ??. unfold αα. - rewrite <- (Lim_seq_incr_n (sum_n (fun k : nat => (vector_nth i pf (α k x2))²)) xx) in H7. - unfold sum_n in H7. - erewrite Lim_seq_ext; cycle 1. - { intros. - rewrite <- (sum_n_m_shift (fun k : nat => (vector_nth i pf (α (k)%nat x2))²) xx n). - reflexivity. - } - eapply Rbar_le_trans; try apply H7. - apply Lim_seq_le; intros. - destruct xx; [reflexivity |]. - rewrite (sum_split (fun k : nat => (vector_nth i pf (α k x2))²) 0 (n + S xx) xx); unfold plus; simpl; try lia. - cut (0 <= sum_n_m (fun k : nat => (vector_nth i pf (α k x2))²) 0 xx); try lra. - apply nneg_sum_n_m_sq. - - destruct H8. - exists x1. - - unfold ββ; intros i pf. - generalize (H8 i pf). - apply almost_impl; apply all_almost; intros ? HH. - rewrite <- (Lim_seq_incr_n (sum_n (fun k : nat => (vector_nth i pf (β k x2))²)) xx) in HH. - unfold sum_n in HH. - erewrite Lim_seq_ext; cycle 1. - { intros. - rewrite <- (sum_n_m_shift (fun k : nat => (vector_nth i pf (β (k)%nat x2))²) xx n). - reflexivity. - } - eapply Rbar_le_trans; try apply HH. - apply Lim_seq_le; intros. - destruct xx; [reflexivity |]. - rewrite (sum_split (fun k : nat => (vector_nth i pf (β k x2))²) 0 (n + S xx) xx); unfold plus; simpl; try lia. - cut (0 <= sum_n_m (fun k : nat => (vector_nth i pf (β k x2))²) 0 xx); try lra. - apply nneg_sum_n_m_sq. + rewrite ex_series_incr_n with (n := xx) in H7. + revert H7. + apply ex_series_ext. + intros. + now replace (xx + n)%nat with (n + xx)%nat by lia. + - intros. + specialize (H8 i pf). + revert H8; apply almost_impl. + apply all_almost; intros ??. + unfold ββ. + rewrite ex_series_incr_n with (n := xx) in H8. + revert H8. + apply ex_series_ext. + intros. + now replace (xx + n)%nat with (n + xx)%nat by lia. - revert H9; apply almost_impl. apply all_almost; intros ??. intros. @@ -5849,13 +5890,13 @@ Section jaakola_vector2. - destruct H10 as [? [??]]. exists x1. split; trivial. - revert H12; apply almost_impl. + revert H13; apply almost_impl. apply all_almost; intros ??. intros. unfold XX, XXF. - specialize (H12 (k + xx)%nat i pf). + specialize (H13 (k + xx)%nat i pf). eapply Rle_trans; cycle 1. - apply H12. + apply H13. simpl. right. apply FiniteConditionalExpectation_ext; intros ?. @@ -5866,6 +5907,26 @@ Section jaakola_vector2. unfold XX, αα, ββ, XX, XXF. replace (S k + xx)%nat with (S (k + xx))%nat by lia. now rewrite H11. + - destruct H12 as [eps H12]. + exists eps. + unfold ββ. + destruct H12 as [NN ?]. + exists NN. + intros. + specialize (H12 (n + xx)%nat). + cut_to H12; try lia. + specialize (H12 i pf). + revert H12. + apply almost_impl. + apply all_almost; intros ??. + eapply Rbar_le_lt_trans; cycle 1. + apply H12. + apply slln.eq_Rbar_le. + apply Lim_seq_ext. + intros. + apply sum_n_ext. + intros. + now replace (n1 + (n + xx))%nat with (n1 + n + xx)%nat by lia. Qed. Theorem Jaakkola_alpha_beta_unbounded_uniformly @@ -5896,12 +5957,8 @@ Section jaakola_vector2. almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (α k ω))) p_infty) -> almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (β k ω))) p_infty) -> - (exists (C : R), - forall i pf, - almost prts (fun ω => Rbar_le (Lim_seq (sum_n (fun k : nat => Rsqr (vector_nth i pf (α k ω))))) (Finite C))) -> - (exists (C : R), - forall i pf, - almost prts (fun ω => Rbar_le (Lim_seq (sum_n (fun k : nat => Rsqr (vector_nth i pf (β k ω))))) (Finite C))) -> + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (α n ω))))) -> + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (β n ω))))) -> (almost prts (fun ω => forall k i pf, @@ -5983,7 +6040,73 @@ Section jaakola_vector2. + intros. erewrite vector_nth_ext; try apply H13. + apply H12. - Qed. + - assert (forall i pf, + exists epsilon : posreal, + eventually + (fun n : nat => + almostR2 prts Rbar_lt + (fun ω : Ts => + Lim_seq + (sum_n (fun nn : nat => rvsqr (vecrvnth i pf (β (nn + n)%nat)) ω))) + (fun x : Ts => const epsilon x))). + { + intros. + specialize (H9 i pf). + generalize (uniform_converge_sum_sq_tails _ (H6 i pf)); intros. + assert (0 < 2) by lra. + exists (mkposreal _ H13). + assert (0 < 1) by lra. + simpl in H12. + specialize (H12 H9 (mkposreal _ H14)). + destruct H12. + exists (S x). + intros. + specialize (H12 (n-1)%nat). + cut_to H12; try lia. + revert H12. + apply almost_impl. + apply all_almost; intros ??. + simpl. + simpl in H12. + assert (Rbar_lt 1 2) by (simpl; lra). + eapply Rbar_le_lt_trans; cycle 1. + apply H16. + eapply Rbar_le_trans; cycle 1. + apply H12. + apply slln.eq_Rbar_le. + apply Lim_seq_ext; intros. + apply sum_n_ext; intros. + unfold rvsqr. + now replace (S (n - 1 + n1)) with (n1 + n)%nat by lia. + } + generalize + (bounded_nat_ex_choice_vector + (A := R) (n := S N) + (fun i pf eps => + 0 < eps /\ + eventually + (fun n : nat => + almostR2 prts Rbar_lt + (fun ω : Ts => + Lim_seq + (sum_n (fun nn : nat => rvsqr (vecrvnth i pf (β (nn + n)%nat)) ω))) + (fun x : Ts => const eps x)))); intros. + cut_to H13. + + destruct H13. + pose (eps := Rvector_max_abs x). + assert (0 < eps). + { + assert (forall i pf, 0 < vector_nth i pf x). + { + intros. + specialize (H13 i pf). + apply H13. + } + admit. + } + exists (mkposreal _ H14). + admit. + Admitted. Definition Scaled_Rvector_max_abs {n} (x y :vector R n) : R := Rvector_max_abs (Rvector_mult x y). @@ -6335,12 +6458,8 @@ Section jaakola_vector2. almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (α k ω))) p_infty) -> almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (β k ω))) p_infty) -> - (exists (C : R), - forall i pf, - almost prts (fun ω => Rbar_le (Lim_seq (sum_n (fun k : nat => Rsqr (vector_nth i pf (α k ω))))) (Finite C))) -> - (exists (C : R), - forall i pf, - almost prts (fun ω => Rbar_le (Lim_seq (sum_n (fun k : nat => Rsqr (vector_nth i pf (β k ω))))) (Finite C))) -> + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (α n ω))))) -> + (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (β n ω))))) -> almost prts (fun ω => (forall k, @@ -6712,6 +6831,7 @@ Proof. unfold XF'. unfold vecrvnth, pos_Rvector_mult, rvscale. now rewrite Rvector_nth_mult, vector_nth_map, Rmult_comm. + } generalize (bounded_nat_ex_choice_vector