Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2005P6

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.Analysis.SpecialFunctions.Log.Base
public import Mathlib.Data.Nat.Digits.Lemmas

public section


/-!
# USA Mathematical Olympiad 2005, Problem 6

For a positive integer m, let s(m) denote the sum of the decimal digits of m.
A set S of positive integers is k-stable if s(∑_{x∈X} x) = k for any nonempty
subset X ⊆ S. For each integer n ≥ 2 let f(n) be the minimal k for which there
exists a k-stable set with n integers. Prove that there are constants
0 < C₁ < C₂ with C₁ log₁₀ n ≤ f(n) ≤ C₂ log₁₀ n.
-/

namespace Usa2005P6

/-- The sum of the decimal digits of `m`. -/
def s (m : ℕ) : ℕ := (Nat.digits 10 m).sum

/-- A set `S` of positive integers is `k`-stable if the sum of the elements of
any nonempty subset `X ⊆ S` has digit sum equal to `k`. -/
def IsStable (k : ℕ) (S : Finset ℕ) : Prop :=
  (∀ x ∈ S, 0 < x) ∧ ∀ X ∈ S.powerset, X.Nonempty → s (∑ x ∈ X, x) = k

/-- `f n` is the minimal `k` for which there exists a `k`-stable set with `n`
integers. (That the defining set is nonempty is proved in `stable_exists`. -/
noncomputable def f (n : ℕ) : ℕ := sInf {k | ∃ S : Finset ℕ, IsStable k S ∧ S.card = n}

theorem usa2005_p6 : ∃ C₁ C₂ : ℝ, 0 < C₁ ∧ C₁ < C₂ ∧
    ∀ n : ℕ, 2 ≤ n → C₁ * Real.logb 10 n ≤ (f n : ℝ) ∧ (f n : ℝ) ≤ C₂ * Real.logb 10 n := sorry

File author(s): Kimi K3

This problem has a complete formalized solution.