이사벨 행렬 산술 : 다른 표기법을 사용한 라이브러리의 det_linear_row_setsum

Question

최근에 이사벨 이론 정리자를 사용하기 시작했습니다. 다른 보조 정리를 증명하기 위해 HOL 라이브러리에서 찾을 수있는 보조 정리 "det_linear_row_setsum"과 다른 표기법을 사용하고 싶습니다. 더 구체적으로, 나는 "χ i"대신에 "χ i j 표기법"을 사용하고자합니다. 나는 얼마 동안 동등한 표현을 공식화하려고 노력했지만 아직 이해할 수 없었다. a이 i 및 j, c 색인 벡터의 가족 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

첫째, 원래의 보조 정리의 말씀 자신을 명확하게. 왼쪽의 행렬의 k 번째 행은 집합 S에서 이 모두 j에있는 벡터의 합계입니다. 다른 행은 c에서 가져옵니다. 오른쪽의 행은 k이 이제 a k j이고 j이 외부 합계에 바인딩된다는 것을 제외하고는 행렬이 동일합니다. 당신이 실현 것처럼 당신이 %_ j. vec1 $ j에 의해 a 교체 할 수 있도록

는 벡터 a의 가족은, 인덱스 i = k에 사용됩니다. 행렬 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는 그렇게 당신을 도울 수 있습니다 결과는 다음과 같습니다.