`BookProof.ChapterSoftmaxFluctuation.meanScore_le_max` (beta : ℝ) (s : Fin m → ℝ) (i : Fin m) (hmax : ∀ l, s l ≤ s i) : meanScore beta s ≤ s i

Initializing...

`BookProof.ChapterSoftmaxFluctuation.meanScore_le_max` (beta : ℝ) (s : Fin m → ℝ) (i : Fin m) (hmax : ∀ l, s l ≤ s i) : meanScore beta s ≤ s i · Prove2Me