FormalConjectures/ErdosProblems/316.lean

GitHub source file

3 declarations, 1 contain sorry, 0 declared as axioms

1. theorem Erdos316.erdos_316 Documented declaration: erdos_316 line 44 source

   Source documentation

   Is it true that if $A \subseteq \mathbb{N}\setminus\{1\}$ is a finite set with $\sum_{n \in A} \frac{1}{n} < 2$ then there is a partition $A=A_1 \sqcup A_2$ such that $\sum_{n \in A_i} \frac{1}{n} < 1$ for $i=1,2$?

   This is not true in general, as shown by Sándor [Sa97].

   The minimal counterexample is $\{2,3,4,5,6,7,10,11,13,14,15\}$, found by Tom Stobart.

   This was formalized in Lean by Mehta.

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

   Statement uses: Iff, False, Finset, Nat, Not, Membership.mem, OfNat.ofNat, LT.lt, Rat, Finset.sum, HDiv.hDiv, Exists, And, Disjoint, Eq, Union.union

   Proof uses: id, Eq.mpr, Inv.inv, LE.le, Eq.trans, congrArg, forall_congr, implies_congr, Eq.refl, congrFun', Finset.sum_congr, one_div, funext, congr, false_iff, propext, exists_prop_congr, Iff.of_eq, Insert.insert, Singleton.singleton and 11 more

   50 instances, coercions and auxiliary constants left out.

   Tactic trace: 14 steps

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

   theorem erdos_316 : answer(False) ↔ ∀ A : Finset ℕ, 0 ∉ A → 1 ∉ A →
       ∑ n ∈ A, (1 / n : ℚ) < 2 → ∃ (A₁ A₂ : Finset ℕ),
         Disjoint A₁ A₂ ∧ A = A₁ ∪ A₂ ∧
         ∑ n ∈ A₁, (1 / n : ℚ) < 1 ∧ ∑ n ∈ A₂, (1 / n : ℚ) <  1 := by
   …

2. lemma Erdos316.erdos_316.variants.multiset This is not true if $A$ is a multiset, for example $2,3,3,5,5,5,5$ line 60 source

   Source documentation

   This is not true if $A$ is a multiset, for example $2,3,3,5,5,5,5$.

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

   Statement uses: Exists, Multiset, Nat, And, Not, Membership.mem, OfNat.ofNat, LT.lt, Rat, Multiset.sum, Multiset.map, HDiv.hDiv, Bind.bind, Pure.pure, Eq, HAdd.hAdd, Or, LE.le

   Proof uses: Insert.insert, Singleton.singleton, Exists.intro, And.intro, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Multiset.powerset, Inv.inv, HSub.hSub, of_eq_true, Eq.trans, True, congrArg, congrFun', add_tsub_cancel_left, eq_self and 12 more

   65 instances, coercions and auxiliary constants left out.

   Tactic trace: 13 steps

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

   lemma erdos_316.variants.multiset : ∃ A : Multiset ℕ, 0 ∉ A ∧ 1 ∉ A ∧
       (A.map ((1 : ℚ) / ·)).sum < 2 ∧ ∀ (A₁ A₂ : Multiset ℕ),
         A = A₁ + A₂ →
           1 ≤ (A₁.map ((1 : ℚ) / ·)).sum ∨ 1 ≤ (A₂.map ((1 : ℚ) / ·)).sum := by
   …

3. theorem Erdos316.erdos_316.variants.generalized This is not true in general, as shown by Sándor [Sa97], who observed that the proper divisors of $120$ form a counterexample sorry line 85 source

   Source documentation

   This is not true in general, as shown by Sándor [Sa97], who observed that the proper divisors of $120$ form a counterexample. More generally, Sándor shows that for any $n\geq 2$ there exists a finite set $A\subseteq \mathbb{N}\backslash\{1\}$ with $\sum_{k\in A}\frac{1}{k} < n$ and no partition into $n$ parts each of which has $\sum_{k\in A_i}\frac{1}{k}<1$.

   A Finpartition has no empty parts, so partitions into at most $n$ parts are tested. Testing exactly $n$ parts would let the singleton $\{2\}$ satisfy the statement vacuously.

   depends on sorry what this means

   Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Finset, And, Finset.Nonempty, Not, Membership.mem, LT.lt, Rat, Finset.sum, HDiv.hDiv, Finpartition, Finset.card, Finpartition.parts

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

   30 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_316.variants.generalized (n : ℕ) (hn : 2 ≤ n) : ∃ A : Finset ℕ,
       A.Nonempty ∧ 0 ∉ A ∧ 1 ∉ A ∧ ∑ k ∈ A, (1 / k : ℚ) < n ∧ ∀ P : Finpartition A,
       P.parts.card ≤ n → ∃ p ∈ P.parts, 1 ≤ ∑ n ∈ p, (1 / n : ℚ) := by
   …