Rvector_max_abs_const

IBM · Dec 22, 2023 · 96c7048 · 96c7048
1 parent 1bc8357
commit 96c7048
Showing 1 changed file with 7 additions and 4 deletions.
diff --git a/coq/QLearn/jaakkola_vector.v b/coq/QLearn/jaakkola_vector.v
@@ -700,14 +700,17 @@ Proof.
 Qed.
 
 Lemma Rvector_max_abs_const {n : nat} (c : R) :
-  Rvector_max_abs (vector_const c n) = Rabs c.
+  Rvector_max_abs (vector_const c (S n)) = Rabs c.
 Proof.
-  Admitted.
+  destruct (Rvector_max_abs_nth_in (vector_const c (S n))) as [?[? eqq]].
+  rewrite eqq.
+  now rewrite vector_nth_const.
+Qed.
 
-Lemma delta_eps_bound (eps : posreal) (C : posreal) {N} (delta : vector R N) :
+Lemma delta_eps_bound (eps : posreal) (C : posreal) {N} (delta : vector R (S N)) :
   0 < gamma ->
   Rvector_max_abs delta > C * eps ->
-  gamma * Rvector_max_abs (Rvector_plus delta (vector_const (pos eps) N)) <=
+  gamma * Rvector_max_abs (Rvector_plus delta (vector_const (pos eps) (S N))) <=
     gamma * (C + 1)/ C * Rvector_max_abs delta.
 Proof.
   intros.