`BookProof.ChapterSoftmaxTemperatureMonotone.min_le_meanScore` (beta : ℝ) (s : Fin m → ℝ) (i : Fin m) (hmin : ∀ l, s i ≤ s l) : s i ≤ meanScore beta s

Initializing...

`BookProof.ChapterSoftmaxTemperatureMonotone.min_le_meanScore` (beta : ℝ) (s : Fin m → ℝ) (i : Fin m) (hmin : ∀ l, s i ≤ s l) : s i ≤ meanScore beta s · Prove2Me