`BookProof.ChapterAttentionPrior.priorDenom_pos` {w : Fin m → ℝ} (hw : ∀ j, 0 < w j) (beta : ℝ) (s : Fin m → ℝ) (i : Fin m) : 0 < ∑ l, w l * Real.exp (beta * s l)
ProvedBookProof.ChapterAttentionPrior.priorDenom_postheoremstimepiece
Prove the following Lean 4 theorem from ChapterAttentionPrior.
BookProof.ChapterAttentionPrior.priorDenom_pos {w : Fin m → ℝ} (hw : ∀ j, 0 < w j) (beta : ℝ) (s : Fin m → ℝ) (i : Fin m) : 0 < ∑ l, w l * Real.exp (beta * s l)
Formalization note: Lean 4 identifier BookProof.ChapterAttentionPrior.priorDenom_pos.
Preamble
-- Generated from ChapterAttentionPrior.lean — theorem BookProof.ChapterAttentionPrior.priorDenom_pos
import Definitions.Def_ChapterSoftmaxSharpness
import Definitions.Def_ChapterSoftmaxOrder
import Mathlib
import Definitions.Def_ChapterAttentionPrior
open BookProof.ChapterAttentionPrior
open scoped BigOperators
noncomputable section
open BookProof.ChapterSoftmaxSharpness BookProof.ChapterSoftmaxOrder
variable {m : ℕ}Formal statement
theorem BookProof.ChapterAttentionPrior.priorDenom_pos {w : Fin m → ℝ} (hw : ∀ j, 0 < w j) (beta : ℝ) (s : Fin m → ℝ)
(i : Fin m) : 0 < ∑ l, w l * Real.exp (beta * s l) := by sorry