Prove2Me

`BookProof.ChapterAttentionCapacity.tendsto_capacityError` {r C : ℝ} (hr : 0 < r) (M : ℝ) : Tendsto (fun b : ℝ => 2 * C * (M * Real.exp (-(b * r ^ 2)))) atTop (𝓝 0)

Proved
BookProof.ChapterAttentionCapacity.tendsto_capacityError

by leonardopedro Β· Oct 7, 2026 Β· Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterAttentionCapacity.

BookProof.ChapterAttentionCapacity.tendsto_capacityError {r C : ℝ} (hr : 0 < r) (M : ℝ) : Tendsto (fun b : ℝ => 2 * C * (M * Real.exp (-(b * r ^ 2)))) atTop (𝓝 0)

Formalization note: Lean 4 identifier BookProof.ChapterAttentionCapacity.tendsto_capacityError.

Preamble
-- Generated from ChapterAttentionCapacity.lean β€” theorem BookProof.ChapterAttentionCapacity.tendsto_capacityError
import Definitions.Def_ChapterSoftmaxSharpness
import Definitions.Def_ChapterSoftmaxOrder
import Mathlib
import Definitions.Def_ChapterAttentionCapacity
open BookProof.ChapterAttentionCapacity


open scoped BigOperators

open Filter Topology

noncomputable section


open BookProof.ChapterSoftmaxSharpness BookProof.ChapterSoftmaxOrder

variable {m n : β„•} {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
Formal statement
theorem BookProof.ChapterAttentionCapacity.tendsto_capacityError {r C : ℝ} (hr : 0 < r) (M : ℝ) :
    Tendsto (fun b : ℝ => 2 * C * (M * Real.exp (-(b * r ^ 2)))) atTop (𝓝 0) := by sorry

View graph