matrix_norm_inf_sub_mult

IBM · Dec 1, 2023 · 6b6927b · 6b6927b
1 parent e220793
commit 6b6927b
Showing 1 changed file with 18 additions and 20 deletions.
diff --git a/coq/FHE/encode.v b/coq/FHE/encode.v
@@ -2329,27 +2329,25 @@ Section norms.
       + apply /RlebP.
         apply sum_le => j0.
         apply normc_triang_sum.
-      + replace  (\sum_(i < p) \sum_(j0 < m) normc (R:=R_rcfType) (mat1 j j0 * mat2 j0 i)) with
-          (\sum_(j0 < m) \sum_(i < p) normc (R:=R_rcfType) (mat1 j j0 * mat2 j0 i)).
-        * generalize (@sum_mult_distr); intros.
-          rewrite /mul /= in H0.
-          rewrite H0.
-          apply /RlebP.
-          apply sum_le => j0.
-          replace  (\sum_(i < p) normc (R:=R_rcfType) (mat1 j j0 * mat2 j0 i)) with
-            ((normc (R:=R_rcfType) (mat1 j j0)) * 
-               (\sum_(i < p) normc (R:=R_rcfType) (mat2 j0 i))).
+      + rewrite nested_sums_comm.
+        generalize (@sum_mult_distr); intros.
+        rewrite /mul /= in H0.
+        rewrite H0.
+        apply /RlebP.
+        apply sum_le => j0.
+        replace  (\sum_(i < p) normc (R:=R_rcfType) (mat1 j j0 * mat2 j0 i)) with
+          ((normc (R:=R_rcfType) (mat1 j j0)) * 
+             (\sum_(i < p) normc (R:=R_rcfType) (mat2 j0 i))).
+        * apply /RlebP.
+          apply Rmult_le_compat_l.
+          -- apply normc_nnegR.
           -- apply /RlebP.
-             apply Rmult_le_compat_l.
-             ++ apply normc_nnegR.
-             ++ apply /RlebP.
-                generalize (@bigmaxr_le_alt m
-                              (fun j0 => (\sum_(i < p) normc (R:=R_rcfType) (mat2 j0 i))) 0 j0); intros.
-                apply H1.
-          -- rewrite mulrC sum_mult_distr.
-             apply eq_bigr => i _.
-             by rewrite mulrC ComplexField.Normc.normcM.
-        * by rewrite nested_sums_comm.
+             generalize (@bigmaxr_le_alt m
+                           (fun j0 => (\sum_(i < p) normc (R:=R_rcfType) (mat2 j0 i))) 0 j0); intros.
+             apply H1.
+        * rewrite mulrC sum_mult_distr.
+          apply eq_bigr => i _.
+          by rewrite mulrC ComplexField.Normc.normcM.
     - apply /RlebP.
       apply bigmax_nneg => i.
       apply sum_nneg => k.