604604 (sum_n_m (fun n0 : nat => -2 * a n0) (S n0) (n + S n0))).
605605 {
606606 intros.
607- rewrite <- sum_split; trivial; lia.
607+ rewrite <- (@ sum_split R_AbelianGroup) ; trivial; lia.
608608 }
609609 unfold plus in H13; simpl in H13.
610610 exists (-2*x1 - sum_n_m (fun n0 : nat => -2 * a n0) 0 n0 ).
@@ -994,15 +994,15 @@ Section Derman_Sacks.
994994 - rewrite is_lim_seq_incr_n with (N := N).
995995 apply is_lim_seq_ext with
996996 (u := fun n =>
997- (sum_n_m (fun j : nat => (delta j - c j) / B j) 0 (n + N)) -
998- (sum_n_m (fun j : nat => (delta j - c j) / B j) 0 (N-1))).
997+ (@ sum_n_m R_AbelianGroup (fun j : nat => (delta j - c j) / B j) 0 (n + N)) -
998+ (@ sum_n_m R_AbelianGroup (fun j : nat => (delta j - c j) / B j) 0 (N-1))).
999999 intros.
1000- rewrite sum_split with (m := (N-1)%nat); try lia.
1000+ rewrite (@ sum_split R_AbelianGroup) with (m := (N-1)%nat); try lia.
10011001 unfold plus; simpl; ring_simplify.
10021002 replace (S (N-1))%nat with N by lia; trivial.
10031003 apply is_lim_seq_minus with
10041004 (l1 := m_infty)
1005- (l2 := sum_n_m (fun j : nat => (delta j - c j) / B j) 0 (N - 1)).
1005+ (l2 := @ sum_n_m R_AbelianGroup (fun j : nat => (delta j - c j) / B j) 0 (N - 1)).
10061006 + now rewrite is_lim_seq_incr_n with (N := N) in H13.
10071007 + apply is_lim_seq_const.
10081008 + now unfold is_Rbar_minus, is_Rbar_plus; simpl.
@@ -3776,23 +3776,25 @@ Lemma Dvoretzky_converge_W_alpha_beta_uniform (W w α β: nat -> Ts -> R)
37763776 almostR2 prts Rbar_le
37773777 (ConditionalExpectation prts (filt_sub n) (rvsqr (w n)))
37783778 (const (Rsqr C)))) ->
3779- almost prts (fun ω : Ts => is_lim_seq (sum_n(fun n : nat => α n ω)) p_infty) ->
3780- almost prts (fun ω : Ts => is_lim_seq (sum_n (fun n : nat => β n ω)) p_infty) ->
3779+ almost prts (fun ω : Ts => is_lim_seq (@ sum_n R_AbelianGroup (fun n : nat => α n ω)) p_infty) ->
3780+ almost prts (fun ω : Ts => is_lim_seq (@ sum_n R_AbelianGroup (fun n : nat => β n ω)) p_infty) ->
37813781 almost prts (fun ω => ex_series (fun n => Rsqr (β n ω))) ->
3782- (exists epsilon : posreal, eventually (fun n => almostR2 prts Rbar_lt (fun ω => Lim_seq (sum_n (fun nn => rvsqr (β (nn+n)%nat) ω))) (const epsilon))) ->
3782+ (exists epsilon : posreal, eventually (fun n => almostR2 prts Rbar_lt (fun ω => Lim_seq (@ sum_n R_AbelianGroup (fun nn => rvsqr (β (nn+n)%nat) ω))) (const epsilon))) ->
37833783 (forall n, rv_eq (W (S n)) (rvplus (rvmult (rvminus (const 1) (α n)) (W n)) (rvmult (w n) (β n)))) ->
37843784 almost _ (fun ω => is_lim_seq (fun n => W n ω) (Finite 0)).
37853785Proof .
37863786 intros condexpw condexpw2 alpha_inf beta_inf beta_sqr [ϵ beta_bounded] (* W0 *) Wrel.
3787-
37883787 assert (svy1b: forall n : nat, IsFiniteExpectation prts (rvsqr (β n))).
37893788 {
37903789 intros.
37913790 now apply isfe_sqr_X_almost_01.
37923791 }
37933792
37943793 eapply (@Dvoretzky_converge_W_alpha_beta_isf_seq_sum W w α β F isfilt filt_sub adaptZ adapt_alpha adapt_beta rvw); eauto.
3795-
3794+ change (is_finite
3795+ (Lim_seq
3796+ (@sum_n R_AbelianGroup
3797+ (fun n : nat => @FiniteExpectation Ts dom prts (@rvsqr Ts (β n)) (svy1b n))))).
37963798 generalize (sum_expectation prts (fun n => rvsqr (β n))); intros HH.
37973799 assert (rv2 : forall n, RandomVariable dom borel_sa (rvsqr (β n))).
37983800 {
@@ -3812,7 +3814,7 @@ Proof.
38123814 unfold A3'.
38133815 unfold Series.
38143816 apply Rbar_real_rv.
3815- cut (RandomVariable dom Rbar_borel_sa (fun omega : Ts => ELim_seq (sum_n (fun n : nat => (β n omega)²)))).
3817+ cut (RandomVariable dom Rbar_borel_sa (fun omega : Ts => ELim_seq (@ sum_n R_AbelianGroup (fun n : nat => (β n omega)²)))).
38163818 {
38173819 apply RandomVariable_proper; try reflexivity; intros ?.
38183820 now rewrite <- Elim_seq_fin.
@@ -3878,7 +3880,7 @@ Proof.
38783880 specialize (betaN (S N)).
38793881 cut_to betaN; try lia.
38803882
3881- pose (btail := (rvplus (fun ω => sum_n (fun nn : nat => rvsqr (β nn) ω) N)
3883+ pose (btail := (rvplus (fun ω => @ sum_n R_AbelianGroup (fun nn : nat => rvsqr (β nn) ω) N)
38823884 (const (pos ϵ)))).
38833885
38843886 assert (btail_rv : RandomVariable dom Rbar_borel_sa btail).
@@ -3892,7 +3894,7 @@ Proof.
38923894 apply IsFiniteExpectation_Rbar.
38933895 apply Rbar_finexp_finexp.
38943896 {
3895- cut (RandomVariable dom Rbar_borel_sa (fun omega : Ts => ELim_seq (sum_n (fun n : nat => (β n omega)²)))).
3897+ cut (RandomVariable dom Rbar_borel_sa (fun omega : Ts => ELim_seq (@ sum_n R_AbelianGroup (fun n : nat => (β n omega)²)))).
38963898 {
38973899 apply RandomVariable_proper; try reflexivity; intros ?.
38983900 now rewrite <- Elim_seq_fin.
@@ -3901,7 +3903,7 @@ Proof.
39013903 }
39023904 apply (Rbar_IsFiniteExpectation_nnf_bounded_almost _ _ btail).
39033905 - intros ?.
3904- generalize (Lim_seq_le (fun _ => 0) (sum_n (fun n : nat => (β n x)²)))
3906+ generalize (Lim_seq_le (fun _ => 0) (@ sum_n R_AbelianGroup (fun n : nat => (β n x)²)))
39053907 ; intros HHH.
39063908 cut_to HHH.
39073909 + rewrite Lim_seq_const in HHH.
@@ -3916,13 +3918,13 @@ Proof.
39163918 apply almost_impl.
39173919 apply all_almost; intros ω bsqr_ex bsqr_bound.
39183920 rewrite <- (Lim_seq_incr_n _ (S N)).
3919- assert (eqq:Lim_seq (fun n : nat => sum_n (fun n0 : nat => (β n0 ω)²) (n + S N)) =
3921+ assert (eqq:Lim_seq (fun n : nat => @ sum_n R_AbelianGroup (fun n0 : nat => (β n0 ω)²) (n + S N)) =
39203922
3921- (Lim_seq (fun n => sum_n (fun nn : nat => rvsqr (β nn) ω) N +
3922- (sum_n (fun nn : nat => rvsqr (β (nn + S N)%nat) ω) n)))).
3923+ (Lim_seq (fun n => @ sum_n R_AbelianGroup (fun nn : nat => rvsqr (β nn) ω) N +
3924+ (@ sum_n R_AbelianGroup (fun nn : nat => rvsqr (β (nn + S N)%nat) ω) n)))).
39233925 {
39243926 apply Lim_seq_ext; intros n.
3925- generalize (sum_split (fun n0 : nat => (β n0 ω)²) 0 ((n + S N)%nat) N)
3927+ generalize (@ sum_split R_AbelianGroup (fun n0 : nat => (β n0 ω)²) 0 ((n + S N)%nat) N)
39263928 ; intros HHH.
39273929 cut_to HHH; try lia.
39283930 unfold sum_n.
@@ -3931,12 +3933,19 @@ Proof.
39313933 f_equal.
39323934 now rewrite sum_shift.
39333935 }
3936+ change ( Rbar_le (Lim_seq (fun n : nat => @sum_n R_AbelianGroup (fun n0 : nat => (β n0 ω)²) (n + S N)))
3937+ (rvplus (fun ω0 : Ts => @sum_n R_AbelianGroup (fun nn : nat => rvsqr (β nn) ω0) N) (const ϵ) ω)).
39343938 rewrite eqq.
39353939 rewrite Lim_seq_plus.
39363940 + unfold rvplus.
39373941 rewrite Lim_seq_const.
3938- replace (Finite (sum_n (fun nn : nat => rvsqr (β nn) ω) N + const (pos ϵ) ω)) with
3939- (Rbar_plus (sum_n (fun nn : nat => rvsqr (β nn) ω) N) (const (pos ϵ) ω)) by reflexivity.
3942+ replace (Finite
3943+ (Rplus
3944+ (@sum_n (AbelianGroup.AbelianMonoid R_AbelianGroup)
3945+ (fun nn : nat => @rvsqr Ts (β nn) ω) N)
3946+ (pos (@const posreal Ts ϵ ω))))
3947+ with
3948+ (Rbar_plus (@sum_n R_AbelianGroup (fun nn : nat => rvsqr (β nn) ω) N) (const (pos ϵ) ω)) by reflexivity.
39403949 apply Rbar_plus_le_compat.
39413950 { apply Rbar_le_refl. }
39423951 now apply Rbar_lt_le.
@@ -4139,16 +4148,18 @@ Proof.
41394148 + destruct n; [lia |].
41404149 rewrite <- (Lim_seq_incr_n (sum_n (fun n0 : nat => rvsqr (β n0) ω)) (S n)).
41414150 apply Lim_seq_le; intros.
4142- generalize (sum_split (fun n0 : nat => (β n0 ω)²) 0 ((n0 + S n)%nat) n)
4151+ generalize (@ sum_split R_AbelianGroup (fun n0 : nat => (β n0 ω)²) 0 ((n0 + S n)%nat) n)
41434152 ; intros HHH.
4144- cut_to HHH; try lia.
4145- unfold sum_n, rvsqr.
4146- rewrite HHH.
4147- unfold plus, rvsqr; simpl.
4148- rewrite sum_shift.
4149- cut (0 <= sum_n_m (fun n1 : nat => (β n1 ω)²) 0 n); try lra.
4150- apply sum_n_m_pos; intros.
4151- apply Rle_0_sqr.
4153+ cut_to HHH; try lia.
4154+ unfold sum_n, rvsqr.
4155+ etransitivity; [| right; symmetry; apply HHH].
4156+ unfold plus, rvsqr; simpl.
4157+ rewrite sum_shift.
4158+ change (@sum_n_m R_AbelianGroup (fun nn : nat => (β (nn + S n)%nat ω)²) 0 n0 <=
4159+ @sum_n_m R_AbelianGroup (fun n1 : nat => (β n1 ω)²) 0 n + @sum_n_m R_AbelianGroup (fun n1 : nat => (β (n1 + S n)%nat ω)²) 0 n0).
4160+ cut (0 <= @sum_n_m R_AbelianGroup (fun n1 : nat => (β n1 ω)²) 0 n); try lra.
4161+ apply sum_n_m_pos; intros.
4162+ apply Rle_0_sqr.
41524163 + simpl.
41534164 apply Rmax_r.
41544165Qed .
0 commit comments