Largest-term bound from two finite-sequence moments
ProvedWorkbookCorrected.plus_32724corrected-formalizationinequalitieslean-workbooksource-checked
Let a₁ ≤ a₂ ≤ ⋯ ≤ a₁₀₀ be real numbers with sum 67 and sum of squares 45. Then a₁₀₀ ≤ 1.
Formalization Note: Restores the source’s summation indices 1 through 100, and restricts its sortedness assumption to that same finite sequence.
Source: InternLM Lean-Workbook, record lean_workbook_plus_32724 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_32724 (a : ℕ → ℝ)
(h1 : ∑ k ∈ Finset.Icc 1 100, a k = 67)
(h2 : ∑ k ∈ Finset.Icc 1 100, (a k)^2 = 45)
(hs : MonotoneOn a (Set.Icc 1 100)) : a 100 ≤ 1 := by sorrySource