From 51e44f80434d0899494b4105dc588a5a78168520 Mon Sep 17 00:00:00 2001 From: Barry Trager Date: Thu, 5 Dec 2024 16:34:25 -0500 Subject: [PATCH] cleanup --- coq/QLearn/jaakkola_vector.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/coq/QLearn/jaakkola_vector.v b/coq/QLearn/jaakkola_vector.v index e01470ed..e28b835a 100644 --- a/coq/QLearn/jaakkola_vector.v +++ b/coq/QLearn/jaakkola_vector.v @@ -7027,13 +7027,13 @@ Proof. (**r sum of α^2 converges almost always uniformly *) (forall i pf, - is_lim_seq'_uniform_almost (fun n ω => sum_n (fun k => rvsqr (vecrvnth i pf (α k)) ω) n) - (fun ω => Lim_seq (sum_n (fun k => rvsqr (vecrvnth i pf (α k)) ω)))) -> + is_lim_seq'_uniform_almost (fun n ω => sum_n (fun k => (vector_nth i pf (α k ω))²) n) + (fun ω => Lim_seq (sum_n (fun k => (vector_nth i pf (α k ω))²)))) -> (**r sum of β^2 converges almost always uniformly *) (forall i pf, - is_lim_seq'_uniform_almost (fun n ω => sum_n (fun k => rvsqr (vecrvnth i pf (β k)) ω) n) - (fun ω => Lim_seq (sum_n (fun k => rvsqr (vecrvnth i pf (β k)) ω)))) -> + is_lim_seq'_uniform_almost (fun n ω => sum_n (fun k => (vector_nth i pf (β k ω))²) n) + (fun ω => Lim_seq (sum_n (fun k => (vector_nth i pf (β k ω))² )))) -> (**r exists C, such that conditional variance of XF is almost always bounded by C * (1 + W_scaled norm X)^2 *) (exists (C : R),