A finite sum bounded by a product of truncated terms

Proved

WorkbookSource.plus_50180

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

inequalitieslean-workbooksource-checked

For any sequence of positive real numbers $a_0,\ldots,a_{94}$ ,

\sum_{k=0}^{94}a_k\leq94+\prod_{k=0}^{94}\max\{1,a_k\}.

This compares an additive total with the product obtained by replacing factors below one by one. The indexing is shifted by one from the source's list of 95 positive numbers.

Formalization Note: The source proposition is retained; obsolete summation notation is updated for Lean 4.33.1.

Preamble

import Mathlib
open scoped BigOperators

Formal statement

theorem WorkbookSource.plus_50180 (a : ℕ → ℝ) (ha : ∀ k, 0 < a k) : ∑ k ∈ Finset.range 95, a k ≤ 94 + ∏ k ∈ Finset.range 95, max 1 (a k)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_50180; Apache-2.0

View graph