Skip to content

Commit

Permalink
cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@bmtrager
bmtrager committed Jan 25, 2025
1 parent 3392667 commit 5594b07
Showing 1 changed file with 14 additions and 36 deletions.
50 changes: 14 additions & 36 deletions coq/QLearn/Tsitsiklis.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1927,10 +1927,7 @@ Lemma lemma2_beta (W : nat -> nat -> Ts -> R) (ω : Ts)
(forall t,
Rabs (x t ω) <= Rabs (W t ω) + (Y t ω)) ->
is_lim_seq (fun t => Y t ω) (β * D) ->
(exists (T : nat),
forall t,
(t >= T)%nat ->
Rabs (W t ω) <= β * eps * D) ->
eventually (fun t => Rabs (W t ω) <= β * eps * D) ->
Rbar_le (LimSup_seq (fun t => Rabs (x t ω))) (β * (1 + eps) * D).
Proof.
intros.
Expand Down Expand Up @@ -1974,10 +1971,7 @@ Lemma lemma2_beta (W : nat -> nat -> Ts -> R) (ω : Ts)
(forall t,
Rabs (x t ω) <= Rabs (W t ω) + (Y t ω)) ->
(forall C, Rbar_le (LimSup_seq (fun t => C + Y t ω)) (C + (b * D))) ->
(exists (T : nat),
forall t,
(t >= T)%nat ->
Rabs (W t ω) <= b * eps * D) ->
eventually (fun t => Rabs (W t ω) <= b * eps * D) ->
Rbar_le (LimSup_seq (fun t => Rabs (x t ω))) (b * (1 + eps) * D).
Proof.
intros.
Expand Down Expand Up @@ -2036,10 +2030,7 @@ Lemma lemma2_beta (W : nat -> nat -> Ts -> R) (ω : Ts)
(forall t,
Rabs (x t ω) <= D) ->
is_lim_seq (fun t => Y t ω) (β * D) ->
(exists (T : nat),
forall t,
(t >= T)%nat ->
Rabs (W t ω) <= β * eps * D) ->
eventually (fun t => Rabs (W t ω) <= β * eps * D) ->
eventually (fun t => Rabs (x t ω) <= (β * (1 + 2 * eps) * D)).
Proof.
intros.
Expand Down Expand Up @@ -2081,10 +2072,7 @@ Lemma lemma2_beta (W : nat -> nat -> Ts -> R) (ω : Ts)
(forall t,
Rabs (x t ω) <= D) ->
(forall C, Rbar_le (LimSup_seq (fun t => C + Y t ω)) (C + (b * D))) ->
(exists (T : nat),
forall t,
(t >= T)%nat ->
Rabs (W t ω) <= b * eps * D) ->
eventually (fun t => Rabs (W t ω) <= b * eps * D) ->
eventually (fun t => Rabs (x t ω) <= (b * (1 + 2 * eps) * D)).
Proof.
intros.
Expand Down Expand Up @@ -2128,10 +2116,7 @@ Lemma lemma2_beta (W : nat -> nat -> Ts -> R) (ω : Ts)
Rabs (x t ω) <= D ω)) ->
(forall ω, is_lim_seq (fun t => Y t ω) (β * D ω)) ->
almost prts (fun ω =>
exists (T : nat),
forall t,
(t >= T)%nat ->
Rabs (W t ω) <= β * eps * D ω) ->
eventually (fun t => Rabs (W t ω) <= β * eps * D ω)) ->
exists (N : Ts -> nat),
almost prts (fun ω =>
forall (t : nat),
Expand Down Expand Up @@ -2187,10 +2172,8 @@ Lemma lemma2_beta (W : nat -> nat -> Ts -> R) (ω : Ts)
almost prts (fun ω => forall C,
Rbar_le (LimSup_seq (fun t => C + Y t ω)) (C + (b * D ω))) ->
almost prts (fun ω =>
exists (T : nat),
forall t,
(t >= T)%nat ->
Rabs (W t ω) <= b * eps * D ω) ->
eventually (fun t =>
Rabs (W t ω) <= b * eps * D ω)) ->
exists (N : Ts -> nat),
almost prts (fun ω =>
forall (t : nat),
Expand Down Expand Up @@ -2234,9 +2217,7 @@ Lemma lemma2_beta (W : nat -> nat -> Ts -> R) (ω : Ts)
(exists (T : Ts -> nat),
(almost prts
(fun ω =>
forall t,
(t >= T ω)%nat ->
Rabs (W t ω) <= β * eps * D ω))) ->
eventually (fun t => Rabs (W t ω) <= β * eps * D ω)))) ->
almost prts (fun ω =>
Rbar_le (LimSup_seq (fun t => Rabs (x t ω))) (β * (1 + eps) * D ω)).
Proof.
Expand All @@ -2245,8 +2226,7 @@ Lemma lemma2_beta (W : nat -> nat -> Ts -> R) (ω : Ts)
revert H4; apply almost_impl.
revert H5; apply almost_impl.
apply all_almost; intros ???.
apply lemma8_abs_part2 with (Y := Y) (W := W) (α := α) (w := w); try easy.
now exists (x0 x1).
now apply lemma8_abs_part2 with (Y := Y) (W := W) (α := α) (w := w).
Qed.

Lemma lemma8_abs_part2_almost_beta (x Y W : nat -> Ts -> R)
Expand All @@ -2265,9 +2245,8 @@ Lemma lemma2_beta (W : nat -> nat -> Ts -> R) (ω : Ts)
(exists (T : Ts -> nat),
(almost prts
(fun ω =>
forall t,
(t >= T ω)%nat ->
Rabs (W t ω) <= b * eps * D ω))) ->
eventually (fun t =>
Rabs (W t ω) <= b * eps * D ω)))) ->
almost prts (fun ω =>
Rbar_le (LimSup_seq (fun t => Rabs (x t ω))) (b * (1 + eps) * D ω)).
Proof.
Expand All @@ -2276,8 +2255,7 @@ Lemma lemma2_beta (W : nat -> nat -> Ts -> R) (ω : Ts)
revert H5; apply almost_impl.
revert H6; apply almost_impl.
apply all_almost; intros ???.
apply lemma8_abs_part2_beta with (Y := Y) (W := W) (α := α) (β := β) (w := w); try easy.
now exists (x0 x1).
now apply lemma8_abs_part2_beta with (Y := Y) (W := W) (α := α) (β := β) (w := w).
Qed.

Lemma Y_prod (Y : nat -> Ts -> R) (D : Ts -> R) (β : R)
Expand Down Expand Up @@ -6770,7 +6748,7 @@ Qed.
exists (N2 x).
intros.
unfold Wtau.
specialize (H14 (tauk x) t).
specialize (H14 (tauk x) n0).
apply H14.
unfold tauk.
lia.
Expand Down Expand Up @@ -7270,7 +7248,7 @@ Qed.
exists (N2 x).
intros.
unfold Wtau.
specialize (H14 (tauk x) t).
specialize (H14 (tauk x) n0).
apply H14.
unfold tauk.
lia.
Expand Down

0 comments on commit 5594b07

Please sign in to comment.