Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2022P5

module

public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.Order.Archimedean.Real.Basic
public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.Fintype.BigOperators
public import Mathlib.Data.Nat.Bitwise
public import Mathlib.Data.Nat.Log
public import Mathlib.Data.Nat.SuccPred
public import Mathlib.Tactic.IntervalCases

public section


/-!
# USA Mathematical Olympiad 2022, Problem 5

A function f : ℝ → ℝ is essentially increasing if f(s) ≤ f(t) holds
whenever s ≤ t are real numbers such that f(s) ≠ 0 and f(t) ≠ 0.

Find the smallest integer k such that for any 2022 real numbers
x₁, x₂, ..., x₂₀₂₂, there exist k essentially increasing functions
f₁, f₂, ..., fₖ such that

  f₁(n) + f₂(n) + ⋯ + fₖ(n) = xₙ

for every n = 1, 2, ..., 2022.
-/

namespace Usa2022P5

/-- A function `f : ℝ → ℝ` is *essentially increasing* if `f s ≤ f t`
whenever `s ≤ t` are real numbers such that `f s ≠ 0` and `f t ≠ 0`. -/
def EssentiallyIncreasing (f : ℝ → ℝ) : Prop :=
  ∀ s t : ℝ, s ≤ t → f s ≠ 0 → f t ≠ 0 → f s ≤ f t

/-- The property of the natural number `k` occurring in the problem:
every `2022`-tuple `(x₁, …, x₂₀₂₂)` of real numbers is the pointwise sum
of `k` essentially increasing functions at the points `1, …, 2022`. -/
def Good (k : ℕ) : Prop :=
  ∀ x : Fin 2022 → ℝ, ∃ f : Fin k → ℝ → ℝ,
    (∀ i, EssentiallyIncreasing (f i)) ∧
    ∀ n : Fin 2022, ∑ i, f i (n.val + 1) = x n

/- determine -/ abbrev solution : ℕ := sorry

theorem usa2022_p5 : IsLeast {k | Good k} solution := sorry

end Usa2022P5

File author(s): Kimi K3

This problem has a complete formalized solution.