FormalConjectures/ErdosProblems/318.lean

GitHub source file

8 declarations, 6 contain sorry, 0 declared as axioms

1. def Erdos318.P₁ Documented declaration: P₁ line 43 source

   Source documentation

   A set A : Set ℕ is said to have property P₁ if for any nonconstant sequence f : A → {-1, 1}, one can always select a finite, nonempty subset S ⊆ A \ {0} such that ∑ n ∈ S, fₙ / n = 0. This is defined in [Sa82b].

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

   Statement uses: Set, Nat

   Proof uses: Real, Ne, Subtype, Membership.mem, SDiff.sdiff, Singleton.singleton, OfNat.ofNat, Function.comp, Neg.neg, LE.le, Set.range, Insert.insert, Exists, Finset, And, Finset.Nonempty, Eq, Finset.sum, HDiv.hDiv

   20 instances, coercions and auxiliary constants left out.

   def P₁ (A : Set ℕ) : Prop := ∀ (f : ℕ → ℝ),
   …

2. theorem Erdos318.erdos_318.variants.univ sorry line 52 source

   depends on sorry what this means

   Statement uses: Erdos318.P₁, Set.univ, Nat

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

   1 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

3. theorem Erdos318.erdos_318.variants.odd sorry line 58 source

   depends on sorry what this means

   Statement uses: Erdos318.P₁, Set.ofPred, Nat, Odd

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

   3 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

4. theorem Erdos318.erdos_318.variants.squares The set of squares does not have property P₁ line 63 source

   Source documentation

   The set of squares does not have property P₁.

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

   Statement uses: Not, Erdos318.P₁, Set.ofPred, Nat, IsSquare

   Proof uses: Eq.mpr, Exists, Real, Ne, Subtype, Membership.mem, Set, SDiff.sdiff, Singleton.singleton, OfNat.ofNat, Function.comp, Neg.neg, LE.le, Set.range, Insert.insert, Finset, Finset.Nonempty, Eq, Finset.sum, HDiv.hDiv and 204 more

   254 instances, coercions and auxiliary constants left out.

   Tactic trace: 58 steps

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

   theorem erdos_318.variants.squares : ¬ P₁ ({n | IsSquare n}) := by
   …

   Mentions: Erdos318.P₁

5. theorem Erdos318.erdos_318.variants.contain_single_even For any infinite set A containing exactly one positive even number, A does not have property P₁ sorry line 112 source

   Source documentation

   For any infinite set A containing exactly one positive even number, A does not have property P₁. Sattler [Sa82] credits this observation to Erdős, who presumably found this after [ErGr80]. The element 0 is not counted, since P₁ ignores it, and the infinitude hypothesis excludes degenerate sets such as {2}, on which P₁ holds vacuously.

   depends on sorry what this means

   Statement uses: Set, Nat, Set.Infinite, Eq, Set.ncard, Set.ofPred, And, Membership.mem, SDiff.sdiff, Singleton.singleton, OfNat.ofNat, Even, Not, Erdos318.P₁

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

   10 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_318.variants.contain_single_even {A : Set ℕ} (hA : A.Infinite)
       (hA' : {n | n ∈ A \ {0} ∧ Even n}.ncard = 1) : ¬ P₁ A := by
   …

   Mentions: Erdos318.P₁

6. theorem Erdos318.erdos_318.parts.i There exists a set A with positive density that does not have property P₁ sorry line 125 source

   Source documentation

   There exists a set A with positive density that does not have property P₁. #TODO: prove this lemma by assuming erdos_318.contain_single_even.

   The density sits in an existential, so HasPosDensity is the stronger reading here and weakening it to positive lower density would claim less, which is the opposite of the usual situation for Erdős' "positive density". It also costs nothing: by erdos_318.variants.contain_single_even a witness only needs exactly one even element, and the odd numbers together with one even number have density 1 / 2 on the nose.

   depends on sorry what this means

   Statement uses: Exists, Set, Nat, And, Set.HasPosDensity, Set.univ, Not, Erdos318.P₁

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

   9 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_318.parts.i : ∃ A : Set ℕ, HasPosDensity A ∧ ¬ P₁ A := by
   …

   Mentions: Erdos318.P₁

7. theorem Erdos318.erdos_318.variants.infinite_AP sorry line 131 source

   depends on sorry what this means

   Statement uses: Set, Nat, Set.IsAPOfLength, Top.top, ENat, Erdos318.P₁

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

   5 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

8. theorem Erdos318.erdos_318.parts.ii Does the set of squares excluding 1 have property P₁? sorry line 140 source

   Source documentation

   Does the set of squares excluding 1 have property P₁?

   Larsen [La26] proved that this set does have property P₁.

   depends on sorry what this means

   Statement uses: Iff, True, Erdos318.P₁, SDiff.sdiff, Set, Nat, Set.ofPred, IsSquare, Singleton.singleton, OfNat.ofNat

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

   8 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_318.parts.ii : answer(True) ↔  P₁ ({n | IsSquare n} \ {1}) := by
   …

   Mentions: Erdos318.P₁