FormalConjectures/ErdosProblems/269.lean

GitHub source file

7 declarations, 3 contain sorry, 0 declared as axioms

1. def Erdos269.HasPrimeFactorsIn A positive integer $n$ has all its prime factors in the set $P$ line 33 source

   Source documentation

   A positive integer $n$ has all its prime factors in the set $P$. By convention, $1$ satisfies this for any $P$ as it has no prime divisors.

   standard axioms: propext what this means

   Statement uses: Set, Nat

   Proof uses: And, GT.gt, OfNat.ofNat, Nat.Prime, Dvd.dvd, Membership.mem

   4 instances, coercions and auxiliary constants left out.

   def HasPrimeFactorsIn (P : Set ℕ) (n : ℕ) : Prop :=
   …

2. def Erdos269.a The infinite, strictly increasing sequence $\{a_0, a_1, \dots\}$ of integers whose prime factors all belong to $P$ line 40 source

   Source documentation

   The infinite, strictly increasing sequence $\{a_0, a_1, \dots\}$ of integers whose prime factors all belong to $P$.

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

   Statement uses: Set, Nat

   Proof uses: Nat.nth, Erdos269.HasPrimeFactorsIn

   noncomputable def a (P : Set ℕ) : ℕ → ℕ := Nat.nth <| HasPrimeFactorsIn P

   Mentions: Erdos269.HasPrimeFactorsIn

3. def Erdos269.partialLcm The $n$-th partial least common multiple, $[a_0, \dots, a_{n-1}]$, which is the LCM of the first $n$ integers in the sequence line 46 source

   Source documentation

   The $n$-th partial least common multiple, $[a_0, \dots, a_{n-1}]$, which is the LCM of the first $n$ integers in the sequence.

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

   Statement uses: Set, Nat

   Proof uses: Finset.lcm, Finset.range, Erdos269.a

   3 instances, coercions and auxiliary constants left out.

   noncomputable def partialLcm (P : Set ℕ) (n : ℕ) : ℕ :=
   …

4. def Erdos269.series The sum $\sum_{n=1}^\infty \frac{1}{[a_0,\ldots,a_{n - 1}]}$ line 53 source

   Source documentation

   The sum $\sum_{n=1}^\infty \frac{1}{[a_0,\ldots,a_{n - 1}]}$.

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

   Statement uses: Set, Nat, Real

   Proof uses: tsum, HDiv.hDiv, OfNat.ofNat, Erdos269.partialLcm, SummationFilter.unconditional

   11 instances, coercions and auxiliary constants left out.

   noncomputable def series (P : Set ℕ) : ℝ :=  ∑' n, (1 : ℝ) / (partialLcm P n)
   …

   Mentions: Erdos269.partialLcm

5. theorem Erdos269.erdos_269.variants.rational Let $P$ be a finite set of primes with $|P| \ge 2$ and let $\{a_1 < a_2 < \dots\}$ be the set of positive integers whose prime factors are all in $P$ sorry line 63 source

   Source documentation

   Let $P$ be a finite set of primes with $|P| \ge 2$ and let $\{a_1 < a_2 < \dots\}$ be the set of positive integers whose prime factors are all in $P$. Is the sum $$ \sum_{n=1}^\infty \frac{1}{[a_1,\ldots,a_n]} $$ rational?

   depends on sorry what this means

   Statement uses: Iff, True, Finset, Nat, Membership.mem, Nat.Prime, GE.ge, Finset.card, OfNat.ofNat, Exists, Rat, Eq, Real, Erdos269.series

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

   14 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_269.variants.rational : answer(sorry) ↔
       ∀ᵉ (P : Finset ℕ) (h : ∀ p ∈ P, p.Prime) (h_card : P.card ≥ 2),
       ∃ (q : ℚ), q = (series (P : Set ℕ)) := by
   …

   Mentions: Erdos269.series

6. theorem Erdos269.erdos_269.variants.irrational Let $P$ be a finite set of primes with $|P| \ge 2$ and let $\{a_1 < a_2 < \dots\}$ be the set of positive integers whose prime factors are all in $P$ sorry line 76 source

   Source documentation

   Let $P$ be a finite set of primes with $|P| \ge 2$ and let $\{a_1 < a_2 < \dots\}$ be the set of positive integers whose prime factors are all in $P$. Is the sum $$ \sum_{n=1}^\infty \frac{1}{[a_1,\ldots,a_n]} $$ irrational?

   depends on sorry what this means

   Statement uses: Iff, True, Finset, Nat, Membership.mem, Nat.Prime, GE.ge, Finset.card, OfNat.ofNat, Irrational, Erdos269.series

   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_269.variants.irrational : answer(sorry) ↔
       ∀ᵉ (P : Finset ℕ) (h : ∀ p ∈ P, p.Prime) (h_card : P.card ≥ 2),
       Irrational (series (P : Set ℕ)) := by
   …

   Mentions: Erdos269.series

7. theorem Erdos269.erdos_269.variants.infinite This theorem addresses the case where the set of primes $P$ is infinite sorry line 86 source

   Source documentation

   This theorem addresses the case where the set of primes $P$ is infinite. In this case the sum is irrational.

   depends on sorry what this means

   Statement uses: Set, Nat, Membership.mem, Nat.Prime, Set.Infinite, Irrational, Erdos269.series

   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.

   theorem erdos_269.variants.infinite (P : Set ℕ) (h : ∀ p ∈ P, p.Prime) (h_inf : P.Infinite) :
     Irrational (series P) := by
   …

   Mentions: Erdos269.series