Prove2Me

`BookProof.ChapterAttentionTopK.isTopWeight_of_isTopScore` {beta : ℝ} (hbeta : 0 < beta) (s : Fin m → ℝ) {S : Finset (Fin m)} (hS : ∀ x ∈ S, ∀ y ∉ S, s y ≤ s x) : IsTop (scoreSoftm

Proved
BookProof.ChapterAttentionTopK.isTopWeight_of_isTopScore

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterAttentionTopK.

BookProof.ChapterAttentionTopK.isTopWeight_of_isTopScore {beta : ℝ} (hbeta : 0 < beta) (s : Fin m → ℝ) {S : Finset (Fin m)} (hS : ∀ x ∈ S, ∀ y ∉ S, s y ≤ s x) : IsTop (scoreSoftmax beta s) S

Formalization note: Lean 4 identifier BookProof.ChapterAttentionTopK.isTopWeight_of_isTopScore.

Preamble
-- Generated from ChapterAttentionTopK.lean — theorem BookProof.ChapterAttentionTopK.isTopWeight_of_isTopScore
import Definitions.Def_ChapterSoftmaxOrder
import Mathlib
import Definitions.Def_ChapterAttentionTopK
import Definitions.Def_ChapterSoftmaxSharpness
open BookProof.ChapterSoftmaxSharpness
open BookProof.ChapterAttentionTopK


open scoped BigOperators

noncomputable section


open BookProof.ChapterSoftmaxSharpness BookProof.ChapterSoftmaxOrder

variable {m : ℕ} {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
Formal statement
theorem BookProof.ChapterAttentionTopK.isTopWeight_of_isTopScore {beta : ℝ} (hbeta : 0 < beta) (s : Fin m → ℝ)
    {S : Finset (Fin m)} (hS : ∀ x ∈ S, ∀ y ∉ S, s y ≤ s x) :
    IsTop (scoreSoftmax beta s) S := by sorry

View graph