少し複雑な関数の極限として
$$\lim_{x\to 0}x\,\sin{\frac1{x}}=0$$
を証明します。$x$が$\sin$の引数の分母にあるので$x=0$では定義されませんが$x\to 0$での極限は存在して$0$になる、という命題です。
今回は関数の絶対値を取ってから挟み撃ち論法で証明する方針です。そのための道具として$x\to 0$で、関数の極限が0になることと関数の絶対値の極限が0になることが同値であることを示しておきます。
$$\lim_{x\to 0}f(x)=0 \iff \lim_{x\to 0}|f(x)|=0\hspace{20cm}$$
theorem real_tendsto_zero_iff_abs_tendsto_zero (f:ℝ→ℝ) : Tendsto (abs ∘ f) (𝓝 0) (𝓝 0) ↔ Tendsto f (𝓝 0) (𝓝 0) := by
exact Iff.symm (tendsto_zero_iff_abs_tendsto_zero f)
同じ内容だが非常に一般化された定理tendsto_zero_iff_abs_tendsto_zeroがmathlib4で証明されており、これをそのまま使って１行で証明は終了します。
早速証明を見ていきましょう。まず１行目で今示した定理を使って証明のゴールを書き換えます。ゴールは、
$$\lim_{x\to 0}|x\,\sin{\frac1{x}}|=0\hspace{20cm}$$
⊢ Tendsto (abs ∘ fun x ↦ x * Real.sin (1 / x)) (𝓝 0) (𝓝 0)
になります。
example : Tendsto (fun x:ℝ => x * (Real.sin (1/x))) (𝓝 0) (𝓝 0) := by
refine (real_tendsto_zero_iff_abs_tendsto_zero fun x => x * (Real.sin (1/x))).mp ?_
-- ⊢ Tendsto (abs ∘ fun x ↦ x * Real.sin (1 / x)) (𝓝 0) (𝓝 0)have h1 : (abs ∘ fun x => x * (Real.sin (1 / x))) = fun x => |x| * |(Real.sin (1 / x))| := by calc
(abs ∘ fun x => x * (Real.sin (1 / x)))
= fun x => |x*(Real.sin (1 / x))| := by rfl
_= fun x => |x| * |Real.sin (1 / x)| := by
refine funext ?h
intro x
exact abs_mul x (Real.sin (1 / x))
rw [h1] -- ⊢ Tendsto (fun x ↦ |x| * |Real.sin (1 / x)|) (𝓝 0) (𝓝 0)
上記の前半部分では簡単な絶対値の計算を使ってさらに書き換えています。結果rw [h1]後のゴールはこうなります。
⊢ Tendsto (fun x ↦ |x| * |Real.sin (1 / x)|) (𝓝 0) (𝓝 0)
ここからは挟み撃ちです。$\lim_{x\to 0}|x|\,|\sin{\frac1{x}}|=0$を次のように挟み撃ちします。
$$ 0 \le |x|\,|\sin{\frac1{x}}| \le |x| $$
have h3 : Tendsto (fun x:ℝ => |x|) (𝓝 0) (𝓝 0) := by
exact Continuous.tendsto' continuous_abs 0 0 abs_zero
have h4 : (fun x:ℝ => 0) ≤ (fun x:ℝ => |x| * |Real.sin (1 / x)|) := by
intro x
simp
refine mul_nonneg (abs_nonneg x) ?_
exact abs_nonneg (Real.sin x⁻¹)
have h5 : (fun x:ℝ => |x| * |Real.sin (1 / x)|) ≤ (fun x:ℝ => |x|) := by
intro x
simp
refine mul_le_of_le_one_right (abs_nonneg x) ?_
apply Real.abs_sin_le_one
exact squeeze_zero h4 h5 h3
後半の形式証明で補題h3は$\lim_{x\to 0}|x|=0$で、絶対値が連続関数であることを使って１行で証明が終わります。
補題h4は挟み撃ち不等式の前半部分ですね。絶対値の積は非負ということで証明が終わります。
補題h5は挟み撃ち不等式の後半部分です。サイン関数の絶対値は引数に関わらず1以下という定理がmathlib4で証明済みなのでそれを使って証明が終わります。
挟み撃ちの定理はsqueeze_zeroという名前でmathlib4の中で証明済みです。この定理にすでに証明した補題h3, h4, h5を組み込むと全体の証明が終わりました。
