FormalConjectures/ErdosProblems/1145.lean

GitHub source file

3 declarations, 1 contain sorry, 0 declared as axioms

1. def Erdos1145.Erdos1145Prop Let $A=\{1\leq a_1 < a_2 < \cdots\}$ and $B=\{1\leq b_1 < b_2 < \cdots\}$ be sets of integers with $a_n/b_n\to 1$ line 49 source

   Source documentation

   Let $A=\{1\leq a_1 < a_2 < \cdots\}$ and $B=\{1\leq b_1 < b_2 < \cdots\}$ be sets of integers with $a_n/b_n\to 1$.

   If $A+B$ contains all sufficiently large positive integers then is it true that $\limsup 1_A\ast 1_B(n)=\infty$?

   Formalization note: There's some discussion in the comments of [erdosproblems.com/28] and [erdosproblems.com/1145] about whether or not $0$ should be included in $A$ or $B$ and has been left purposely ambiguous. Problem 1145 was originally written as $A + B = \mathbb{N}$, which would imply that $0$ would need to exist in $A$ or $B$ to include $1$ in $A + B$. However, it's been made more general and rewritten as "sufficiently large positive integers". The formalization below is the version that includes $0$.

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

   Proof uses: Set, Nat, Set.Infinite, Filter.Tendsto, Real, HDiv.hDiv, Nat.nth, Membership.mem, Filter.atTop, nhds, OfNat.ofNat, Filter.Eventually, HAdd.hAdd, Eq, ENat, Filter.limsup, AdditiveCombinatorics.sumConv, Set.indicatorOne, Top.top

   25 instances, coercions and auxiliary constants left out.

   def Erdos1145Prop : Prop :=
   …

2. theorem Erdos1145.erdos_1145 Let $A=\{1\leq a_1 < a_2 < \cdots\}$ and $B=\{1\leq b_1 < b_2 < \cdots\}$ be sets of integers with $a_n/b_n\to 1$ sorry line 65 source

   Source documentation

   Let $A=\{1\leq a_1 < a_2 < \cdots\}$ and $B=\{1\leq b_1 < b_2 < \cdots\}$ be sets of integers with $a_n/b_n\to 1$.

   If $A+B$ contains all sufficiently large positive integers then is it true that $\limsup 1_A\ast 1_B(n)=\infty$?

   A conjecture of Erdős and Sárközy.

   depends on sorry what this means

   Statement uses: Iff, True, Erdos1145.Erdos1145Prop

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

   1 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1145 : answer(sorry) ↔ Erdos1145Prop := by
   …

   Mentions: Erdos1145.Erdos1145Prop

3. theorem Erdos1145.erdos_1145.test_implies_erdos_28 A stronger form of [erdosproblems.com/28] line 72 source

   Source documentation

   A stronger form of [erdosproblems.com/28].

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

   Statement uses: Erdos1145.Erdos1145Prop, Set, Nat, Set.Finite, Compl.compl, HAdd.hAdd, Eq, ENat, Filter.limsup, AdditiveCombinatorics.sumRep, Filter.atTop, Top.top

   Proof uses: id, Membership.mem, LE.le, Exists, AdditiveCombinatorics.sumConv, Set.indicatorOne, Set.Finite.exists_le, dite, Classical.propDecidable, absurd, Set.Finite.infinite_compl, Set.Finite.add, Not, Set.Infinite, Filter.Tendsto.congr', Real, OfNat.ofNat, HDiv.hDiv, Nat.nth, nhds and 22 more

   85 instances, coercions and auxiliary constants left out.

   Tactic trace: 18 steps

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

   theorem erdos_1145.test_implies_erdos_28 : Erdos1145Prop → type_of% Erdos28.erdos_28 := by
   …

   Mentions: Erdos1145.Erdos1145Prop, Erdos28.erdos_28