Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2024P6

module

public import Mathlib.Algebra.BigOperators.Field
public import Mathlib.Algebra.EuclideanDomain.Basic
public import Mathlib.Algebra.EuclideanDomain.Field
public import Mathlib.Algebra.Order.Chebyshev
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.Analysis.Normed.Field.Basic

public section


/-!
# USA Mathematical Olympiad 2024, Problem 6

Let n > 2 be an integer and let ℓ ∈ {1, 2, ..., n}. A collection A₁, ..., Aₖ
of (not necessarily distinct) subsets of {1, 2, ..., n} is called ℓ-large if
|Aᵢ| ≥ ℓ for all 1 ≤ i ≤ k. Find, in terms of n and ℓ, the largest real
number c such that the inequality

  ∑ᵢ ∑ⱼ xᵢ xⱼ |Aᵢ ∩ Aⱼ|²/(|Aᵢ|·|Aⱼ|) ≥ c (∑ᵢ xᵢ)²

holds for all positive integers k, all nonnegative real numbers x₁, ..., xₖ,
and all ℓ-large collections A₁, ..., Aₖ of subsets of {1, ..., n}.
-/

namespace Usa2024P6

/-- The answer: `c = (n + ℓ² - 2ℓ)/(n(n-1))`. -/
noncomputable /- determine -/ abbrev solution : ℕ → ℕ → ℝ := sorry

/-- `Works n ℓ c` says that the inequality of the problem holds with constant
`c`: for every positive integer `k`, all nonnegative weights `x₁, ..., xₖ` and
every ℓ-large collection `A₁, ..., Aₖ` of subsets of `{1, ..., n}`. -/
noncomputable def Works (n ℓ : ℕ) (c : ℝ) : Prop :=
  ∀ (k : ℕ), 0 < k → ∀ (x : Fin k → ℝ), (∀ i, 0 ≤ x i) →
    ∀ (A : Fin k → Finset (Fin n)), (∀ i, ℓ ≤ (A i).card) →
      c * (∑ i, x i) ^ 2 ≤
        ∑ i, ∑ j, x i * x j *
          (((A i ∩ A j).card : ℝ) ^ 2 / ((A i).card : ℝ) / ((A j).card : ℝ))

theorem usa2024_p6 (n ℓ : ℕ) (hn : 2 < n) (hℓ : 1 ≤ ℓ ∧ ℓ ≤ n) :
    IsGreatest {c : ℝ | Works n ℓ c} (solution n ℓ) := sorry

end Usa2024P6

File author(s): Kimi K3

This problem has a complete formalized solution.