FormalConjectures/ErdosProblems/206.lean

GitHub source file

5 declarations, 1 contain sorry, 0 declared as axioms

1. def Erdos206.egyptianSum The Egyptian fraction sum: ∑_{m ∈ S} 1/m for a finset of natural numbers line 59 source

   Source documentation

   The Egyptian fraction sum: ∑_{m ∈ S} 1/m for a finset of natural numbers.

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

   Statement uses: Finset, Nat, Real

   Proof uses: Finset.sum, HDiv.hDiv, OfNat.ofNat

   8 instances, coercions and auxiliary constants left out.

   noncomputable def egyptianSum (S : Finset ℕ) : ℝ :=
   …

2. def Erdos206.IsUnderapprox S is an Egyptian underapproximation of x: valid denominators (all positive) and sum < x line 63 source

   Source documentation

   S is an Egyptian underapproximation of x: valid denominators (all positive) and sum < x.

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

   Statement uses: Finset, Nat, Real

   Proof uses: And, Membership.mem, LT.lt, OfNat.ofNat, Erdos206.egyptianSum

   5 instances, coercions and auxiliary constants left out.

   def IsUnderapprox (S : Finset ℕ) (x : ℝ) : Prop :=
   …

3. def Erdos206.IsBestNTerm S achieves the best n-term Egyptian underapproximation of x, i.e. egyptianSum S realises $R_n(x)$ line 68 source

   Source documentation

   S achieves the best n-term Egyptian underapproximation of x, i.e. egyptianSum S realises $R_n(x)$.

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

   Statement uses: Finset, Nat, Real

   Proof uses: And, Eq, Finset.card, Erdos206.IsUnderapprox, LE.le, Erdos206.egyptianSum

   1 instances, coercions and auxiliary constants left out.

   def IsBestNTerm (S : Finset ℕ) (n : ℕ) (x : ℝ) : Prop :=
   …

4. def Erdos206.EventuallyGreedy Documented declaration: EventuallyGreedy line 76 source

   Source documentation

   x has eventually greedy best Egyptian underapproximations: from some n₀ on, the best n-term underapproximations of x are the prefixes of a single strictly increasing sequence of denominators, so each is obtained from the previous by appending the minimal admissible denominator.

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

   Statement uses: Real

   Proof uses: And, GT.gt, OfNat.ofNat, Exists, Nat, StrictMono, LT.lt, GE.ge, Erdos206.IsBestNTerm, Finset.image, Finset.range

   8 instances, coercions and auxiliary constants left out.

   def EventuallyGreedy (x : ℝ) : Prop :=
   …

5. theorem Erdos206.erdos_206 Let $x>0$ be a real number sorry line 97 source

   Source documentation

   Let $x>0$ be a real number. For any $n\geq 1$ let $$R_n(x) = \sum_{i=1}^n\frac{1}{m_i}<x$$ be the maximal sum of $n$ distinct unit fractions which is $<x$.

   Is it true that, for almost all $x$, for sufficiently large $n$, we have $$R_{n+1}(x)=R_n(x)+\frac{1}{m},$$ where $m$ is minimal such that $m$ does not appear in $R_n(x)$ and the right-hand side is $<x$? (That is, are the best underapproximations eventually always constructed in a 'greedy' fashion?)

   Kovač [Ko24b] has proved that this is false - in fact as false as possible: the set of $x\in (0,\infty)$ for which the best underapproximations are eventually 'greedy' has Lebesgue measure zero.

   depends on sorry what this means

   Statement uses: Iff, False, Filter.Eventually, Real, Erdos206.EventuallyGreedy, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat

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

   15 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_206 : answer(False) ↔
       ∀ᵐ x ∂(volume.restrict (Set.Ioi (0 : ℝ))), EventuallyGreedy x := by
   …

   Mentions: Erdos206.EventuallyGreedy