Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2015P3

module

public import Mathlib.Algebra.Order.Star.Basic
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.Fintype.BigOperators
public import Mathlib.Data.Fintype.Powerset

public section


/-!
# USA Mathematical Olympiad 2015, Problem 3

Let S = {1, 2, ..., n}, where n ≥ 1. Each of the 2ⁿ subsets of S is to be colored red or
blue. (The subset itself is assigned a color and not its individual elements.) For any set
T ⊆ S, we then write f(T) for the number of subsets of T that are blue. Determine the number
of colorings that satisfy the following condition: for any subsets T₁ and T₂ of S,

  f(T₁) f(T₂) = f(T₁ ∪ T₂) f(T₁ ∩ T₂).
-/

namespace Usa2015P3

/-- A coloring of the subsets of `Fin n`; `true` means blue, `false` means red. -/
abbrev Coloring (n : ℕ) : Type := Finset (Fin n) → Bool

/-- `blueCard c T` is the number of subsets of `T` that are colored blue by `c`;
this is the function `f` of the problem statement. -/
def blueCard {n : ℕ} (c : Coloring n) (T : Finset (Fin n)) : ℕ :=
  (T.powerset.filter fun W => c W = true).card

/-- A coloring is *valid* if it satisfies the multiplicative condition of the problem. -/
def IsValid {n : ℕ} (c : Coloring n) : Prop :=
  ∀ T₁ T₂ : Finset (Fin n),
    blueCard c T₁ * blueCard c T₂ = blueCard c (T₁ ∪ T₂) * blueCard c (T₁ ∩ T₂)

/-- The colorings that the problem asks to count. -/
def ValidColorings (n : ℕ) : Type := {c : Coloring n // IsValid c}

instance (n : ℕ) : DecidablePred (@IsValid n) := fun _ => Fintype.decidableForallFintype

instance (n : ℕ) : Fintype (ValidColorings n) := Subtype.fintype _

/- determine -/ abbrev NumberOfColorings (n : ℕ) : ℕ := sorry

theorem usa2015_p3 (n : ℕ) :
    Fintype.card (ValidColorings n) = NumberOfColorings n := sorry

end Usa2015P3

File author(s): Kimi K3

This problem has a complete formalized solution.