伊莎貝爾矩陣算術：det_linear_row_setsum在庫中有不同的符號

Question

我最近開始使用Isabelle定理證明。因爲我想證明另一個引理，所以我想使用與在「HOL庫」中找到的引理「det_linear_row_setsum」中使用的不同的符號。更具體地說，我想用「χi j notation」而不是「χi」。我一直在嘗試制定一個等價的表達式，但還沒有弄明白。

(* ORIGINAL lemma from library *) 
(* from HOL/Multivariate_Analysis/Determinants.thy *) 
lemma det_linear_row_setsum: 
    assumes fS: "finite S" 
    shows "det ((χ i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n) = setsum (λj. det ((χ i. if i = k then a i j else c i)::'a^'n^'n)) S" 
proof(induct rule: finite_induct[OF fS]) 
    case 1 thus ?case apply simp unfolding setsum_empty det_row_0[of k] .. 
next 
    case (2 x F) 
    then show ?case by (simp add: det_row_add cong del: if_weak_cong) 
qed 

..

(* My approach to rewrite the above lemma in χ i j matrix notation *) 
lemma mydet_linear_row_setsum: 
    assumes fS: "finite S" 
    fixes A :: "'a::comm_ring_1^'n^'n" and k :: "'n" and vec1 :: "'vec1 ⇒ ('a, 'n) vec" 
    shows "det (χ r c . if r = k then (setsum (λj .vec1 j $ c) S) else A $ r $ c) = 
    (setsum (λj . (det(χ r c . if r = k then vec1 j $ c else A $ r $ c))) S)" 
proof- 
    show ?thesis sorry 
qed 

Answer 1

首先，讓自己清楚原來引理說：a是i和j，c索引向量的家庭是i索引向量的家庭。左側矩陣的第k行是來自集S的所有j範圍內的矢量a k j的總和。 其他行取自c。在右邊，矩陣是相同的，除了行k現在是a k j並且j被綁定在外部總和中。

正如你已經意識到，矢量a的家庭僅用於索引，這樣你就可以通過%_ j. vec1 $ j代替a。您的矩陣A產生行的族，即c變爲%r. A $ r。然後，您只需要利用該(χ n. x $ n) = x（定理vec_nth_inverse）並通過if和setsum推送$。結果如下所示：

lemma mydet_linear_row_setsum: 
    assumes fS: "finite S" 
    fixes A :: "'a::comm_ring_1^'n^'n" and k :: "'n" and vec1 :: "'vec1 => 'a^'n" 
    shows "det (χ r c . if r = k then setsum (%j. vec1 j $ c) S else A $ r $ c) = 
    (setsum (%j. (det(χ r c . if r = k then vec1 j $ c else A $ r $ c))) S)" 

爲了證明這一點，你就必須撤消擴張，並通過推搡，引理if_distrib，cond_application_beta和setsum_component可能會幫助你這樣做。