diff --git a/coq/QLearn/Dvoretzky.v b/coq/QLearn/Dvoretzky.v index d96da093..77f831a5 100644 --- a/coq/QLearn/Dvoretzky.v +++ b/coq/QLearn/Dvoretzky.v @@ -3959,5 +3959,475 @@ Proof. - apply all_almost; intros. apply ex_series_const0. - trivial. - Qed. +Qed. + +(* +Lemma Dvoretzky_converge_W_alpha_beta (W w α β: nat -> Ts -> R) + {F : nat -> SigmaAlgebra Ts} (isfilt : IsFiltration F) (filt_sub : forall n, sa_sub (F n) dom) + {adaptZ : IsAdapted borel_sa W F} (adapt_alpha : IsAdapted borel_sa α F) + (adapt_beta : IsAdapted borel_sa β F) + {rvw : forall n, RandomVariable dom borel_sa (w n)} + + {rvalpha : forall n, RandomVariable dom borel_sa (α n)} + {rvbeta : forall n, RandomVariable dom borel_sa (β n)} +(* + (alpha_pos:forall n x, 0 <= α n x) + (alpha_one:forall n x, 0 <= 1 - α n x ) +*) + (apos: forall (n:nat), almostR2 prts Rle (const 0) (α n)) + (aone: forall (n:nat), almostR2 prts Rle (α n) (const 1)) + (bpos: forall (n:nat), almostR2 prts Rle (const 0) (β n)) + (bone: forall (n:nat), almostR2 prts Rle (β n) (const 1)) : + (forall n, + almostR2 prts eq + (ConditionalExpectation prts (filt_sub n) (w n)) + (const 0)) -> + (exists (C: R), + (forall n, + almostR2 prts Rbar_le + (ConditionalExpectation prts (filt_sub n) (rvsqr (w n))) + (const (Rsqr C)))) -> + almost prts (fun ω : Ts => is_lim_seq (sum_n(fun n : nat => α n ω)) p_infty) -> + almost prts (fun ω : Ts => is_lim_seq (sum_n (fun n : nat => β n ω)) p_infty) -> + (exists (A2 : R), + almost prts (fun ω => Rbar_lt (Lim_seq (sum_n (fun n : nat => rvsqr (α n) ω))) (Finite A2))) -> + +(* (exists (A3 : R), + almost prts (fun ω => Rbar_lt (Lim_seq (sum_n (fun n : nat => rvsqr (β n) ω))) (Finite A3))) -> + *) + almost prts (fun ω => ex_series (fun n => Rsqr (β n ω))) -> + (forall n, rv_eq (W (S n)) (rvplus (rvmult (rvminus (const 1) (α n)) (W n)) (rvmult (w n) (β n)))) -> + almost _ (fun ω => is_lim_seq (fun n => W n ω) (Finite 0)). +Proof. + intros condexpw condexpw2 alpha_inf beta_inf alpha_sqr beta_sqr (* W0 *) Wrel. + + assert (svy1b: forall n : nat, IsFiniteExpectation prts (rvsqr (β n))). + { + intros. + now apply isfe_sqr_X_almost_01. + } + + assert (isfew2: forall n : nat, IsFiniteExpectation prts (rvsqr (w n) )). + { + intros. + destruct condexpw2 as [C ?]. + specialize (H n). + eapply isfe_almost_condexp_sqr_bounded with (sub2 := filt_sub n). + apply H. + } + + assert (isfew : forall n, IsFiniteExpectation prts (w n)). + { + intros. + now apply isfe_rsqr. + } + + assert (isfemult : forall n, IsFiniteExpectation prts (rvmult (w n) (β n))). + { + intros. + now apply isfe_rvmult_almost_01. + } + + assert (svy2b : forall n : nat, IsFiniteExpectation prts (rvsqr (rvmult (w n) (β n)))). + { + intros. + now apply isfe_rvsqr_rvmult_almost_01. + } + + assert (forall (n:nat) (x:Ts), 0 <= (fun n x => 0) n x). + { + intros. + lra. + } + assert (forall n, RandomVariable dom borel_sa (rvmult (w n) (β n))). + { + intros. + typeclasses eauto. + } + assert (HH: forall n : nat, almostR2 prts Rle (const 0) (const 0)). + { + intros. + apply all_almost. + intros; unfold const; lra. + } + generalize (Dvoretzky_DS_extended_alt_almost W (fun n => rvmult (w n) (β n)) + (fun n => rvmult (rvminus (const 1) (α n)) (W n)) + isfilt filt_sub HH HH apos H0 Wrel); intros. + apply H1. + - intros. + assert (RandomVariable (F n) borel_sa (β n)) by apply adapt_beta. + generalize (ConditionalExpectation.Condexp_factor_out prts (filt_sub n) (w n) (β n)); intros. + apply almost_prob_space_sa_sub_lift with (sub := filt_sub n) in H3. + specialize (condexpw n). + revert condexpw. + apply almost_impl. + revert H3. + unfold almostR2. + apply almost_impl, all_almost. + intros; red; intros; red; intros. + rewrite H3. + unfold Rbar_rvmult. + replace (Finite (const 0 x)) with (Rbar_mult (Finite (β n x)) (Finite (const 0 x))). + + f_equal. + rewrite <- H4. + apply ConditionalExpectation.ConditionalExpectation_ext. + now intro z. + + unfold const. + now rewrite Rbar_mult_0_r. + - intros. + specialize (apos n). + revert apos. + apply almost_impl. + specialize (aone n). + revert aone. + apply almost_impl. + apply all_almost; unfold impl; intros omega ??. + rv_unfold. + rewrite Rplus_0_r. + unfold Rabs, Rmax. + match_destr; match_destr. + + match_destr; try lra. + + match_destr_in n0; try lra. + assert (0 <= (1 + -1 * α n omega)). + { + lra. + } + apply Rge_le in r0. + generalize (Rmult_le_pos _ _ H4 r0). + lra. + + match_destr; try lra. + + match_destr_in n0; try lra. + assert (0 <= (1 + -1 * α n omega)). + { + lra. + } + apply Rlt_gt in r0. + assert (W n omega <= 0) by lra. + generalize (Rmult_le_ge_compat_neg_l _ _ _ H5 H4); intros. + rewrite Rmult_0_r in H6. + rewrite Rmult_comm in H6. + lra. + - destruct condexpw2 as [C ?]. + assert (forall n, + FiniteExpectation prts (rvsqr (rvmult (w n) (β n))) + <= C^2 * FiniteExpectation prts (rvsqr (β n))). + { + intros. + assert (RandomVariable (F n) borel_sa (rvsqr (β n))). + { + now apply rvsqr_rv. + } + assert (almostR2 prts Rbar_le + (ConditionalExpectation prts (filt_sub n) (rvmult (rvsqr (w n)) (rvsqr (β n)))) + (Rbar_rvmult (rvsqr (β n)) (const (Rsqr C)))). + + { + specialize (H2 n). + revert H2. + apply almost_impl. + generalize (NonNegCondexp_factor_out prts (filt_sub n) (rvsqr (w n)) (rvsqr (β n))); intros. + apply almost_prob_space_sa_sub_lift with (sub := filt_sub n) in H2. + revert H2. + apply almost_impl, all_almost. + unfold impl; intros. + rewrite <- Condexp_nneg_simpl in H2. + rewrite H2. + unfold Rbar_rvmult, const. + apply Rbar_le_pos_compat_l. + - apply nnfsqr. + - rewrite <- Condexp_nneg_simpl. + apply H4. + } + assert (almostR2 prts Rbar_le + (ConditionalExpectation prts (filt_sub n) (rvsqr (rvmult (w n) (β n)))) + (Rbar_rvmult (rvsqr (β n)) (const (Rsqr C)))). + + { + + generalize (NonNegCondexp_factor_out prts (filt_sub n) (rvsqr (w n)) (rvsqr (β n))); intros. + apply almost_prob_space_sa_sub_lift with (sub := filt_sub n) in H5. + revert H5. + apply almost_impl. + specialize (H2 n). + revert H2. + apply almost_impl, all_almost. + unfold impl; intros. + assert (rv_eq (rvsqr (rvmult (w n) (β n))) + (rvmult (rvsqr (w n)) (rvsqr (β n)))). + { + intros ?. + rv_unfold. + unfold Rsqr. + lra. + } + rewrite (ConditionalExpectation_ext prts (filt_sub n) _ _ H6). + rewrite <- Condexp_nneg_simpl in H5. + rewrite H5. + unfold Rbar_rvmult, const. + apply Rbar_le_pos_compat_l. + - apply nnfsqr. + - rewrite <- Condexp_nneg_simpl. + apply H2. + } + assert (IsFiniteExpectation prts + (FiniteConditionalExpectation prts (filt_sub n) + (rvsqr (rvmult (w n) (β n))))). + { + apply FiniteCondexp_isfe. + } + rewrite <- (FiniteCondexp_FiniteExpectation prts (filt_sub n)) with (isfe' := H6). + rewrite <- Rsqr_pow2. + rewrite <- FiniteExpectation_scale. + apply FiniteExpectation_ale. + - apply (RandomVariable_sa_sub (filt_sub n)). + apply FiniteCondexp_rv. + - typeclasses eauto. + - revert H5. + apply almost_impl, all_almost. + unfold impl; intros. + assert (Rbar_le (FiniteConditionalExpectation prts (filt_sub n) (rvsqr (rvmult (w n) (β n))) + x) + (rvscale C² (rvsqr (β n)) x)). + { + generalize (FiniteCondexp_eq prts (filt_sub n) (rvsqr (rvmult (w n) (β n)))); intros. + apply (f_equal (fun a => a x)) in H7. + rewrite <- H7. + eapply Rbar_le_trans. + apply H5. + unfold Rbar_rvmult, rvscale, rvsqr, const, Rsqr. + simpl. + lra. + } + now simpl in H7. + } + apply (@ex_series_le R_AbsRing R_CompleteNormedModule ) with + (b := fun n => C^2 * FiniteExpectation prts (rvsqr (β n))). + + intros. + unfold norm; simpl. + unfold abs; simpl. + rewrite Rabs_right. + * eapply Rle_trans. + apply H3. + unfold pow; lra. + * apply Rle_ge, (FiniteExpectation_sq_nneg prts (rvmult (w n) (β n)) (svy2b n)). + + apply (@ex_series_scal R_AbsRing). + rewrite <- ex_finite_lim_series. + rewrite ex_finite_lim_seq_correct. + split. + * apply ex_lim_seq_incr. + intros. + apply sum_n_pos_incr; try lia. + intros. + apply FiniteExpectation_pos. + typeclasses eauto. + * generalize (sum_expectation prts (fun n => rvsqr (β n))); intros. + assert (forall n, RandomVariable dom borel_sa (rvsqr (β n))). + { + intros. + typeclasses eauto. + } + specialize (H4 H5 svy1b). + rewrite (Lim_seq_ext _ _ H4). + generalize (Dominated_convergence_almost + prts + (fun n omega => Finite (rvsum (fun n0 => rvsqr (β n0)) n omega)) + (Rbar_rvlim (fun n omega => Finite (rvsum (fun n0 => rvsqr (β n0)) n omega))) + ); intros. + pose (A3' ω := Series (fun n : nat => (β n ω)²)). + assert (A3'rv : RandomVariable dom borel_sa A3'). + { + unfold A3'. + unfold Series. + apply Rbar_real_rv. + cut (RandomVariable dom Rbar_borel_sa (fun omega : Ts => ELim_seq (sum_n (fun n : nat => (β n omega)²)))). + { + apply RandomVariable_proper; try reflexivity; intros ?. + now rewrite <- Elim_seq_fin. + } + typeclasses eauto. + } + + assert (A3'rv' : RandomVariable dom Rbar_borel_sa (fun ω : Ts => A3' ω)). + { + now apply Real_Rbar_rv. + } + + destruct (beta_sqr) as [p [pone beta_sqr_all]]. + pose (A3 := + (rvchoice (fun x => if Req_EM_T (((EventIndicator (classic_dec p))) x) 0 then false else true) + (A3') + (const 0) + )). + + assert (A3rv : RandomVariable dom borel_sa A3). + { + apply rvchoiceb_rv; trivial. + cut (RandomVariable dom (discrete_sa bool) + (fun x0 : Ts => if classic_dec p x0 then true else false)). + { + apply RandomVariable_proper; try reflexivity. + intros ?. + unfold EventIndicator. + destruct (classic_dec p a); simpl + ; destruct (Req_dec_T _ _); trivial; lra. + } + + Existing Instance FiniteRange_FiniteRangeFunction. + apply (frf_singleton_rv _ _). + intros [|] _; unfold pre_event_singleton, pre_event_singleton, pre_event_preimage; simpl. + - generalize (sa_sigma_event_pre p). + apply sa_proper; intros ?. + match_destr; intuition. + - generalize (sa_complement _ (sa_sigma_event_pre p)). + apply sa_proper; intros ?; unfold pre_event_none. + match_destr; intuition. + - apply rvconst. + } + assert (A3eq : almostR2 prts eq A3 A3'). + { + exists p. + split; trivial. + intros pp ppp. + specialize (beta_sqr_all pp ppp). + unfold A3, rvchoice, EventIndicator. + destruct (classic_dec p pp); try tauto. + destruct (Req_dec_T _ _); lra. + } + + assert (A3rv' : RandomVariable dom Rbar_borel_sa (fun ω : Ts => A3 ω)). + { + now apply Real_Rbar_rv. + } + assert (A3isfe' : Rbar_IsFiniteExpectation prts (fun ω : Ts => A3' ω)). + { + unfold A3', Series. + apply IsFiniteExpectation_Rbar. + unfold IsFiniteExpectation. + assert (A3'nnf:NonnegativeFunction (fun ω : Ts => Lim_seq (sum_n (fun n : nat => (β n ω)²)))). + { + admit. + } + rewrite (Expectation_pos_pofrf _ (nnf:=A3'nnf)). + + + +(* assert (A3isfe : Rbar_IsFiniteExpectation prts (fun ω : Ts => A3 ω)). + { + + (* I think I can prove this *) + admit. + (* + cut (Rbar_IsFiniteExpectation prts (fun ω : Ts => Lim_seq (sum_n (fun n : nat => (β n ω)²))) + + almost prts (fun ω : Ts => ex_series (fun n : nat => (β n ω)²)) + eapply Rbar_IsFiniteExpectation_proper_almostR2; try eapply (isfefn n). +*) + } + *) + assert (leA3lim : + almostR2 prts Rbar_le + (Rbar_rvlim (fun (n : nat) (omega : Ts) => rvsum (fun n0 : nat => rvsqr (β n0)) n omega)) + (fun omega : Ts => A3 omega)). + { + revert A3eq. + apply almost_impl. + revert beta_sqr. + apply almost_impl, all_almost. + intros ???. + rewrite H8. + unfold Rbar_rvlim, A3'. + rewrite Elim_seq_fin. + rewrite <- ex_series_Lim_seq; trivial. + unfold rvsum, rvsqr. + apply Rbar_le_refl. + } + + assert (leA3 : forall n : nat, + almostR2 prts Rbar_le + (Rbar_rvabs (fun omega : Ts => rvsum (fun n0 : nat => rvsqr (β n0)) n omega)) + (fun omega : Ts => A3 omega)). + { + intros n. + revert leA3lim. + apply almost_impl; apply all_almost; intros ??. + eapply Rbar_le_trans; try eapply H7. + unfold Rbar_rvabs, const. + unfold rvsum. + simpl Rbar_abs. + rewrite Rabs_right. + - unfold Rbar_rvlim. + rewrite Elim_seq_fin. + apply (Lim_seq_increasing_le (sum_n (fun n0 : nat => rvsqr (β n0) x))); intros. + apply sum_n_pos_incr; try lia. + intros. + apply nnfsqr. + - apply Rle_ge, sum_n_nneg. + intros. + apply nnfsqr. + } + specialize (H6 A3). + cut_to H6. + -- assert (isfefn : forall n : nat, + Rbar_IsFiniteExpectation prts + (fun omega : Ts => + (rvsum (fun n0 : nat => rvsqr (β n0)) n omega))). + { + intros. + apply IsFiniteExpectation_Rbar. + now apply IsFiniteExpectation_sum. + } + assert + (isfe : Rbar_IsFiniteExpectation prts + (Rbar_rvlim + (fun (n : nat) (omega : Ts) => + (rvsum (fun n0 : nat => rvsqr (β n0)) n omega)))). + { + apply Rbar_IsFiniteExpectation_nnf_bounded_almost with + (g := A3). + - typeclasses eauto. + - trivial. + - typeclasses eauto. + - trivial. + - trivial. + } + specialize (H6 isfefn isfe). + apply is_lim_seq_unique in H6. + ++ rewrite Lim_seq_ext with + (v := (fun n : nat => + Rbar_FiniteExpectation + prts + (fun omega : Ts => + Finite (rvsum (fun n0 : nat => rvsqr (β n0)) n omega)))). + ** rewrite H6. + now simpl. + ** intros. + rewrite <- FinExp_Rbar_FinExp. + --- apply Rbar_FiniteExpectation_ext. + now intro z. + --- apply rvsum_rv. + intros. + typeclasses eauto. + ++ trivial. + ++ trivial. + ++ apply all_almost. + intros. + unfold Rbar_rvlim. + apply ELim_seq_correct. + rewrite ex_Elim_seq_fin. + apply ex_lim_seq_incr. + intros. + apply sum_n_pos_incr; try lia. + intros. + apply nnfsqr. + -- intros. + typeclasses eauto. + -- typeclasses eauto. + -- trivial. + - apply all_almost; intros. + apply is_lim_seq_const. + - apply all_almost; intros. + apply ex_series_const0. + - trivial. +Qed. +*) End Dvoretzky_alpha_beta.