Rvector_scale_const

IBM · Dec 22, 2023 · 1bc8357 · 1bc8357
1 parent 718ec65
commit 1bc8357
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 6 deletions.
diff --git a/coq/ProbTheory/RealVectorHilbert.v b/coq/ProbTheory/RealVectorHilbert.v
@@ -513,6 +513,16 @@ Section Rvector_defs.
     lra.
   Qed.
 
+  Lemma Rvector_scale_const (c1 c2 : R) :
+    c1 .* vector_const c2 n = vector_const (c1 * c2)%R n.
+  Proof.
+    apply vector_nth_eq; intros.
+    rewrite vector_nth_const.
+    unfold Rvector_scale.
+    rewrite vector_nth_map, vector_nth_const.
+    lra.
+  Qed.
+
   Lemma Rvector_inner_const_l (x:vector R n) c : vector_const c n ⋅ x = (c * ∑ x)%R.
   Proof.
     now rewrite <- Rvector_scal_one, Rvector_inner_scal, Rvector_inner_one_l.

diff --git a/coq/QLearn/jaakkola_vector.v b/coq/QLearn/jaakkola_vector.v
@@ -699,17 +699,11 @@ Proof.
   rewrite <- Rinv_l_sym in H0; lra.
 Qed.
 
-Lemma Rvector_scale_const {n : nat} (c1 c2 : R) :
-  Rvector_scale c1 (vector_const c2 n) = vector_const (c1 * c2) n.
-Proof.
-  Admitted.
-
 Lemma Rvector_max_abs_const {n : nat} (c : R) :
   Rvector_max_abs (vector_const c n) = Rabs c.
 Proof.
   Admitted.
 
-
 Lemma delta_eps_bound (eps : posreal) (C : posreal) {N} (delta : vector R N) :
   0 < gamma ->
   Rvector_max_abs delta > C * eps ->