FormalConjectures/ErdosProblems/513.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

4 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 513

Reference:

Imports (1)
Imported by 1 file
  1. def Erdos513.ratio line 36 source

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

    Statement uses: Real, Complex

    Proof uses: HDiv.hDiv, iSup, Nat, Norm.norm, HMul.hMul, iteratedDeriv, OfNat.ofNat, Inv.inv, Nat.factorial, HPow.hPow, Subtype, Eq

    26 instances, coercions and auxiliary constants left out.

  2. theorem Erdos513.erdos_513 Let f be a transcendental entire function sorry line 42 source

    Source documentation

    Let f be a transcendental entire function. What is the greatest possible value of liminf (fun r : ℝ => ratio r f) atTop?

    depends on sorry what this means

    Statement uses: Eq, Real, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat, iSup, Subtype, Complex, And, Transcendental, Polynomial, Differentiable, Filter.liminf, Erdos513.ratio, Filter.atTop

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_513 : answer(sorry) =
    ⨆ f : {f : ℂ → ℂ // Transcendental ℂ[X] f ∧ Differentiable ℂ f},
    (liminf (fun r : ℝ => ratio r f) atTop) := by
…

    Mentions: Erdos513.ratio

  3. theorem Erdos513.erdos_513.variants.upper_bound For all transcendental entire function f, liminf (fun r : ℝ => ratio r f) atTop ≤ 2 / π - c for some c > 0 sorry line 50 source

    Source documentation

    For all transcendental entire function f, liminf (fun r : ℝ => ratio r f) atTop ≤ 2 / π - c for some c > 0. This is proved in [ClHa64].

    depends on sorry what this means

    Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, LE.le, iSup, Subtype, Complex, Transcendental, Polynomial, Differentiable, Filter.liminf, Erdos513.ratio, Filter.atTop, HSub.hSub, HDiv.hDiv, Nat, Real.pi

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

    86 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_513.variants.upper_bound : ∃ c > 0,
    ⨆ f : {f : ℂ → ℂ // Transcendental ℂ[X] f ∧ Differentiable ℂ f},
    (liminf (fun r : ℝ => ratio r f) atTop) ≤ 2 / π - c := by
…

    Mentions: c, Erdos513.ratio

  4. theorem Erdos513.erdos_513.variants.lower_bound For all transcendental entire function f, liminf (fun r : ℝ => ratio r f) atTop > 1 / 2 sorry line 57 source

    Source documentation

    For all transcendental entire function f, liminf (fun r : ℝ => ratio r f) atTop > 1 / 2.

    depends on sorry what this means

    Statement uses: GT.gt, Real, iSup, Subtype, Complex, And, Transcendental, Polynomial, Differentiable, Filter.liminf, Erdos513.ratio, Filter.atTop, HDiv.hDiv, OfNat.ofNat, Nat

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

    80 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_513.variants.lower_bound :
    ⨆ f : {f : ℂ → ℂ // Transcendental ℂ[X] f ∧ Differentiable ℂ f},
    (liminf (fun r : ℝ => ratio r f) atTop) > 1 / 2 := by
…

    Mentions: Erdos513.ratio