FormalConjectures/ErdosProblems/1026.lean

GitHub source file

7 declarations, 5 contain sorry, 0 declared as axioms

1. def Erdos1026.monotonicSubsequenceSums The set of sums $\sum x_{i_r}$, where $x_{i_1},\ldots,x_{i_r}$ ranges over the monotonic subsequences of the sequence $x_1,\ldots,x_n$ line 47 source

   Source documentation

   The set of sums $\sum x_{i_r}$, where $x_{i_1},\ldots,x_{i_r}$ ranges over the monotonic subsequences of the sequence $x_1,\ldots,x_n$.

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

   Statement uses: Nat, Fin, Real, Set

   Proof uses: Set.ofPred, Exists, Finset, And, Or, MonotoneOn, AntitoneOn, Eq, Finset.sum

   6 instances, coercions and auxiliary constants left out.

   def monotonicSubsequenceSums {n : ℕ} (x : Fin n → ℝ) : Set ℝ :=
   …

2. def Erdos1026.admissibleConstants The set of constants line 62 source

   Source documentation

   The set of constants $c$ such that, for all sequences of $n$ distinct positive real numbers $x_1,\ldots,x_n$, $$ \max\left(\sum x_{i_r}\right) > (c-o(1))\frac{1}{\sqrt{n}}\sum x_i $$ (where the maximum is taken over all monotonic subsequences).

   The source reduces to positive sequences. With signed sequences the condition is not a vanishing error term: for $\varepsilon > |c|$ and $x_i = -i$ the right-hand side is positive while every subsequence sum is nonpositive, so no constant would be admissible.

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

   Statement uses: Set, Real

   Proof uses: Set.ofPred, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, Fin, Function.Injective, Exists, And, Membership.mem, Erdos1026.monotonicSubsequenceSums, LE.le, HMul.hMul, HDiv.hDiv, HSub.hSub, Real.sqrt, Finset.sum, Finset.univ, Filter.atTop

   17 instances, coercions and auxiliary constants left out.

   def admissibleConstants : Set ℝ :=
   …

3. theorem Erdos1026.erdos_1026 Let $x_1,\ldots,x_n$ be a sequence of distinct real numbers sorry line 94 source

   Source documentation

   Let $x_1,\ldots,x_n$ be a sequence of distinct real numbers. Determine $$ \max\left(\sum x_{i_r}\right), $$ where the maximum is taken over all monotonic subsequences.

   This is as Erdős posed the problem in [Er71], which is rather ambiguous. Discussion between several users in the comments section has led to the following precise possible question, as posed by van Doorn:

   What is the largest constant $c$ such that, for all sequences of $n$ real numbers $x_1,\ldots,x_n$, $$ \max\left(\sum x_{i_r}\right) > (c-o(1))\frac{1}{\sqrt{n}}\sum x_i $$ (where again the maximum is taken over all monotonic subsequences)?

   Cambie makes the stronger conjecture that if $x_1,\ldots,x_{k^2}$ are distinct positive real numbers with $\sum x_i=1$ then there is always a monotonic subsequence with sum at least $1/k$.

   This stronger conjecture appears to have been first proved by Tidor, Wang, and Yang [TWY16], and is also implicit in work of Wagner [Wa17]. A proof was given and formalised by Aristotle (see the comments), with an alternative proof provided by Chan. In particular, this shows that $c=1$.

   depends on sorry what this means

   Statement uses: IsGreatest, Real, Erdos1026.admissibleConstants, OfNat.ofNat

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

   7 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1026 : IsGreatest admissibleConstants 1 := by
   …

   Mentions: Erdos1026.admissibleConstants

4. theorem Erdos1026.erdos_1026.variants.upper_bound A construction of Cambie in the comments shows that $c\leq 1$ sorry line 101 source

   Source documentation

   A construction of Cambie in the comments shows that $c\leq 1$.

   depends on sorry what this means

   Statement uses: Membership.mem, Real, Set, upperBounds, Erdos1026.admissibleConstants, OfNat.ofNat

   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.

   theorem erdos_1026.variants.upper_bound : 1 ∈ upperBounds admissibleConstants := by
   …

   Mentions: Erdos1026.admissibleConstants

5. theorem Erdos1026.erdos_1026.variants.lower_bound Hanani [Ha57] showed that every sequence is the disjoint union of at most $(\sqrt{2}+o(1))\sqrt{n}$ many monotonic subsequences, whence $c\geq 1/\sqrt{2}$ sorry line 109 source

   Source documentation

   Hanani [Ha57] showed that every sequence is the disjoint union of at most $(\sqrt{2}+o(1))\sqrt{n}$ many monotonic subsequences, whence $c\geq 1/\sqrt{2}$.

   depends on sorry what this means

   Statement uses: Membership.mem, Real, Set, Erdos1026.admissibleConstants, HDiv.hDiv, OfNat.ofNat, Real.sqrt, Nat

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

   22 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1026.variants.lower_bound : 1 / Real.sqrt 2 ∈ admissibleConstants := by
   …

   Mentions: Erdos1026.admissibleConstants

6. theorem Erdos1026.erdos_1026.variants.hanani Hanani [Ha57] showed that every sequence is the disjoint union of at most $(\sqrt{2}+o(1))\sqrt{n}$ many monotonic subsequences sorry line 117 source

   Source documentation

   Hanani [Ha57] showed that every sequence is the disjoint union of at most $(\sqrt{2}+o(1))\sqrt{n}$ many monotonic subsequences.

   depends on sorry what this means

   Statement uses: Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, Fin, Function.Injective, Exists, Finset, And, Or, MonotoneOn, AntitoneOn, Pairwise, Disjoint, Eq, Finset.biUnion, Finset.univ, LE.le, HMul.hMul and 3 more

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

   48 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1026.variants.hanani (ε : ℝ) (hε : 0 < ε) :
       ∀ᶠ n : ℕ in atTop, ∀ x : Fin n → ℝ, Function.Injective x →
         ∃ (m : ℕ) (I : Fin m → Finset (Fin n)),
           (∀ j, MonotoneOn x ↑(I j) ∨ AntitoneOn x ↑(I j)) ∧
           (Pairwise fun j k => Disjoint (I j) (I k)) ∧
           (Finset.univ : Finset (Fin m)).biUnion I = Finset.univ ∧
           (m : ℝ) ≤ (Real.sqrt 2 + ε) * Real.sqrt (n : ℝ) := by
   …

7. theorem Erdos1026.erdos_1026.variants.weighted_erdos_szekeres Documented declaration: weighted_erdos_szekeres sorry line 137 source

   Source documentation

   Cambie makes the stronger conjecture that if $x_1,\ldots,x_{k^2}$ are distinct positive real numbers with $\sum x_i=1$ then there is always a monotonic subsequence with sum at least $1/k$. This is a weighted-form of the Erdős-Szekeres theorem, and is also mentioned (as an open question) in a survey on the latter by Steele [St95].

   This stronger conjecture appears to have been first proved by Tidor, Wang, and Yang [TWY16], and is also implicit in work of Wagner [Wa17]. A proof was given and formalised by Aristotle (see the comments), with an alternative proof provided by Chan.

   depends on sorry what this means

   Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, HPow.hPow, Real, Function.Injective, Eq, Finset.sum, Finset.univ, Exists, And, Membership.mem, Set, Erdos1026.monotonicSubsequenceSums, LE.le, HDiv.hDiv

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

   40 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1026.variants.weighted_erdos_szekeres (k : ℕ) (hk : 0 < k) (x : Fin (k ^ 2) → ℝ)
       (hx : Function.Injective x) (hx' : ∀ i, 0 < x i) (hsum : (∑ i, x i) = 1) :
       ∃ S ∈ monotonicSubsequenceSums x, 1 / (k : ℝ) ≤ S := by
   …

   Mentions: Erdos1026.monotonicSubsequenceSums