1

最近、イザベルの定理証明器を使い始めました。別の補題を証明したいので、HOL ライブラリにある補題「det_linear_row_setsum」で使用されているものとは異なる表記法を使用したいと思います。より具体的には、「χ i 」ではなく「χ ij 表記」を使用したいと考えています。しばらくの間、同等の式を定式化しようとしてきましたが、まだわかりませんでした。

(* 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
4

1 に答える 1

2

最初に、元の補題が何を言っているのかを明確にしてaください。左側の行列の - 番目の行は、セットからすべての範囲にわたるベクトルの合計です。他の行は から取得されます。右側の行列は同じですが、行が現在、外側の合計にバインドされている点が異なります。ijcika k jjScka k jj

お気づきのとおり、ベクトルのファミリはaindex にのみ使用されるため、 に置き換えるi = kことができます。あなたの行列は、行のファミリーを生成します。つまり、 になります。次に、それ(定理) を利用して、とをプッシュするだけです。結果は次のようになります。a%_ j. vec1 $ jAc%r. A $ r(χ n. x $ n) = xvec_nth_inverse$ifsetsum

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がそうするのに役立つかもしれません。

于 2013-06-26T11:25:28.110 に答える