FormalConjectures/ErdosProblems/349.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

14 declarations, 13 contain sorry, 0 declared as axioms

Erdős Problem 349

Reference: erdosproblems.com/349

Imports (1)
Imported by 1 file
  1. def Erdos349.IsGoodPair This defines the core property of the problem: For what values of $t,\alpha \in (0,\infty)$ is the sequence $\lfloor t\alpha^n\rfloor$ complete? line 36 source

    Source documentation

    This defines the core property of the problem: For what values of $t,\alpha \in (0,\infty)$ is the sequence $\lfloor t\alpha^n\rfloor$ complete?

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

    Statement uses: Real

    Proof uses: IsAddComplete, Int, Set.range, Nat, Int.floor, HMul.hMul, HPow.hPow

    16 instances, coercions and auxiliary constants left out.

    def IsGoodPair (t α : ℝ) : Prop :=
…
  2. theorem Erdos349.erdos_349 Documented declaration: erdos_349 sorry line 44 source

    Source documentation

    For what values of $t,\alpha \in (0,\infty)$ is the sequence $\lfloor t\alpha^n\rfloor$ complete (that is, all sufficiently large integers are the sum of distinct integers of the form $\lfloor t\alpha^n\rfloor$)?

    depends on sorry what this means

    Statement uses: Eq, Set, Prod, Real, Set.ofPred, Erdos349.erdos_349.match_1, And, LT.lt, OfNat.ofNat, Erdos349.IsGoodPair, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_349 :
    {(t, α) | 0 < t ∧ 0 < α ∧ IsGoodPair t α} = answer(sorry) := by
…

    Mentions: Erdos349.IsGoodPair

  3. theorem Erdos349.complete_for_alpha_in_Ioo_one_to_goldenRatio It seems likely that the sequence is complete for all for all $t>0$ and all $1 < \alpha < \frac{1+\sqrt{5}}{2}$ sorry line 53 source

    Source documentation

    It seems likely that the sequence is complete for all for all $t>0$ and all $1 < \alpha < \frac{1+\sqrt{5}}{2}$.

    depends on sorry what this means

    Statement uses: Real, LT.lt, OfNat.ofNat, Membership.mem, Set, Set.Ioo, HDiv.hDiv, HAdd.hAdd, Real.sqrt, Nat, Erdos349.IsGoodPair

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

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem complete_for_alpha_in_Ioo_one_to_goldenRatio (t α : ℝ) (ht : 0 < t)
    (hα : α ∈ Set.Ioo 1 ((1 + √5) / 2)) : IsGoodPair t α := by
…

    Mentions: Erdos349.IsGoodPair

  4. theorem Erdos349.exists_t_for_k_disjoint_segments Documented declaration: exists_t_for_k_disjoint_segments sorry line 63 source

    Source documentation

    For any $k$ there exists some $t_k\in (0,1)$ such that the set of $\alpha > 0$ such that the sequence $\lfloor t_k\alpha^n\rfloor$ is complete consists of at least $k$ disjoint line segments, that is, it has at least $k$ connected components.

    depends on sorry what this means

    Statement uses: Nat, Exists, Real, And, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Set.ofPred, LT.lt, Erdos349.IsGoodPair, LE.le, ENat, Set.encard, Set.image, connectedComponentIn

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

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem exists_t_for_k_disjoint_segments (k : ℕ) :
    ∃ t ∈ Ioo 0 1,
      let S := {α | 0 < α ∧ IsGoodPair t α}
…

    Mentions: Erdos349.IsGoodPair

  5. theorem Erdos349.erdos_349.variants.floor_3_halves_odd Is it true that the terms of the sequence $\lfloor (3/2)^n\rfloor$ are odd infinitely often and even infinitely often? sorry line 74 source

    Source documentation

    Is it true that the terms of the sequence $\lfloor (3/2)^n\rfloor$ are odd infinitely often and even infinitely often?

    depends on sorry what this means

    Statement uses: Iff, True, Set.Infinite, Nat, Set.ofPred, Odd, Int, Int.floor, Real, HPow.hPow, HDiv.hDiv, OfNat.ofNat

    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_349.variants.floor_3_halves_odd :
    answer(sorry) ↔ {n | Odd ⌊(3/2 : ℝ) ^ n⌋}.Infinite := by
…
  6. theorem Erdos349.erdos_349.variants.floor_3_halves_even Is it true that the terms of the sequence $\lfloor (3/2)^n\rfloor$ are even infinitely often? sorry line 82 source

    Source documentation

    Is it true that the terms of the sequence $\lfloor (3/2)^n\rfloor$ are even infinitely often?

    depends on sorry what this means

    Statement uses: Iff, True, Set.Infinite, Nat, Set.ofPred, Even, Int, Int.floor, Real, HPow.hPow, HDiv.hDiv, OfNat.ofNat

    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_349.variants.floor_3_halves_even :
    answer(sorry) ↔ {n | Even ⌊(3/2 : ℝ) ^ n⌋}.Infinite := by
…
  7. theorem Erdos349.alpha_gt_two_not_isGoodPair sorry line 95 source

    depends on sorry what this means

    Statement uses: Real, LT.lt, OfNat.ofNat, Nat, Not, Erdos349.IsGoodPair

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

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  8. theorem Erdos349.alpha_le_one_not_isGoodPair sorry line 106 source

    depends on sorry what this means

    Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, Not, Erdos349.IsGoodPair

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

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  9. theorem Erdos349.exists_finsetSum_two_pow sorry line 117 source

    depends on sorry what this means

    Statement uses: Nat, Exists, Finset, Eq, Finset.sum, HPow.hPow, OfNat.ofNat

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

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  10. theorem Erdos349.one_two_isGoodPair sorry line 126 source

    depends on sorry what this means

    Statement uses: Erdos349.IsGoodPair, OfNat.ofNat, Real, Nat

    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.

  11. theorem Erdos349.dyadic_two_isGoodPair sorry line 136 source

    depends on sorry what this means

    Statement uses: Nat, Erdos349.IsGoodPair, HDiv.hDiv, Real, OfNat.ofNat, HPow.hPow

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

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  12. theorem Erdos349.int_coeff_ge_two_not_isGoodPair sorry line 147 source

    depends on sorry what this means

    Statement uses: Int, LE.le, OfNat.ofNat, Not, Erdos349.IsGoodPair, Real

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

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  13. theorem Erdos349.integer_isGoodPair_iff sorry line 159 source

    depends on sorry what this means

    Statement uses: Int, LE.le, OfNat.ofNat, Iff, Erdos349.IsGoodPair, Real, And, Eq

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

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  14. theorem Erdos349.three_halves_two_not_isGoodPair sorry line 174 source

    depends on sorry what this means

    Statement uses: Not, Erdos349.IsGoodPair, HDiv.hDiv, Real, OfNat.ofNat, Nat

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

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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