FormalConjectures/ErdosProblems/434.lean

GitHub source file

4 declarations, 2 contain sorry, 0 declared as axioms

1. abbrev Erdos434.Nat.IsRepresentableAs A natural $n$ is representable as a set $A$ if it can be written as the sum of finitely many elements of $A$ (with repetition allowed) line 40 source

   Source documentation

   A natural $n$ is representable as a set $A$ if it can be written as the sum of finitely many elements of $A$ (with repetition allowed).

   standard axioms: propext what this means

   Statement uses: Nat, Set

   Proof uses: Exists, Multiset, And, Membership.mem, Eq, Multiset.sum

   3 instances, coercions and auxiliary constants left out.

   abbrev Nat.IsRepresentableAs (n : ℕ) (A : Set ℕ) :=
   …

2. abbrev Erdos434.Nat.NcardUnrepresentable The number of naturals that cannot be written as the sum of finitely many elements of the set $A$, with repetition allowed line 47 source

   Source documentation

   The number of naturals that cannot be written as the sum of finitely many elements of the set $A$, with repetition allowed.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Set, Nat

   Proof uses: Set.ncard, Set.ofPred, Not, Erdos434.Nat.IsRepresentableAs

   noncomputable abbrev Nat.NcardUnrepresentable (A : Set ℕ) :=
   …

3. theorem Erdos434.erdos_434.parts.i Let $k \le n$ sorry line 62 source

   Source documentation

   Let $k \le n$. What choice of $A\subseteq\{1, \dots, n\}$ (with $\text{gcd}(A) = 1$) of size $|A| = k$ maximises the number of integers not representable as the sum of finitely many elements from $A$ (with repetitions allowed)? Is it $\{n, n - 1, \dots, n - k + 1\}$?

   The maximal choice is indeed $\{n, \dots, n - k + 1\}$, as proved by Kiss [Ki02].

   The Lean theorem assumes $2 \le k$. When $k = 1 < n$, the proposed singleton $\{n\}$ does not have gcd $1$; the gcd condition instead forces the unique admissible choice $A = \{1\}$.

   depends on sorry what this means

   Statement uses: Nat, LE.le, OfNat.ofNat, IsGreatest, Set.ofPred, Exists, Finset, Finset.Icc, Eq, Finset.card, Finset.gcd, id, Erdos434.Nat.NcardUnrepresentable, Set.Icc, HAdd.hAdd, HSub.hSub

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   32 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_434.parts.i (n k : ℕ) (hn : 1 ≤ n) (hk : 2 ≤ k) (h : k ≤ n) :
       IsGreatest
         { Nat.NcardUnrepresentable S | (S : Finset ℕ) (_ : S ⊆ Finset.Icc 1 n)
           (_ : #S = k) (_ : S.gcd id = 1) }
         (Nat.NcardUnrepresentable <| answer(Set.Icc (n - k + 1 : ℕ) n)) := by
   …

   Mentions: Erdos434.Nat.NcardUnrepresentable

4. theorem Erdos434.erdos_434.parts.ii Documented declaration: ii sorry line 75 source

   Source documentation

   For $2 \le k \le n$, the interval $A = \{n, n - 1, \dots, n - k + 1\}$ maximises the number of integers not representable as the sum of finitely many elements from $A$ (with repetitions allowed), as proved by Kiss [Ki02].

   depends on sorry what this means

   Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, LE.le, IsGreatest, Set.ofPred, Exists, Finset, Finset.Icc, Eq, Finset.card, Finset.gcd, id, Erdos434.Nat.NcardUnrepresentable, Set.Icc, HAdd.hAdd, HSub.hSub

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   32 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_434.parts.ii : answer(True) ↔ ∀ᵉ (n ≥ 1) (k ≥ 2), k ≤ n →
       IsGreatest
         { Nat.NcardUnrepresentable S | (S : Finset ℕ) (_ : S ⊆ Finset.Icc 1 n)
           (_ : #S = k) (_ : S.gcd id = 1)}
         (Nat.NcardUnrepresentable <| Set.Icc (n - k + 1 : ℕ) n) := by
   …

   Mentions: Erdos434.Nat.NcardUnrepresentable