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

7 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 509

Reference: erdosproblems.com/509

Imports (1)
  1. structure Erdos509.BoundedDiscCover An $r$-bounded disc cover of a subset of a metric space $M$ is an indexed family of closed discs whose radii sum to at most $r$ line 41 source

    Source documentation

    An $r$-bounded disc cover of a subset of a metric space $M$ is an indexed family of closed discs whose radii sum to at most $r$.

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

    Statement uses: MetricSpace, Set, Real

    structure BoundedDiscCover (S : Set M) (r : ℝ) (ι : Type v) where
…
  2. def Erdos509.boundedDiscCover_empty line 51 source

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

    Statement uses: MetricSpace, Nonempty, Real, LT.lt, OfNat.ofNat, Erdos509.BoundedDiscCover, EmptyCollection.emptyCollection, Set, PUnit

    Proof uses: Erdos509.BoundedDiscCover.mk, Classical.ofNonempty

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  3. lemma Erdos509.BoundedDiscCover.bound_nonneg_of_nonempty line 65 source

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

    Statement uses: MetricSpace, Set, Set.Nonempty, Real, Erdos509.BoundedDiscCover, LT.lt, OfNat.ofNat

    Proof uses: lt_of_lt_of_le, tsum, Erdos509.BoundedDiscCover.R, SummationFilter.unconditional, Nonempty, Classical.byContradiction, Not, Set.Nonempty.ne_empty, Set.eq_empty_of_subset_empty, Eq.mpr, LE.le, EmptyCollection.emptyCollection, Set.iUnion, Metric.closedBall, Erdos509.BoundedDiscCover.C, eq_of_heq, LE, Eq, HEq, Eq.refl and 17 more

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  4. theorem Erdos509.erdos_509 Let $f(z) ∈ ℂ[z]$ be a monic non-constant polynomial sorry line 85 source

    Source documentation

    Let $f(z) ∈ ℂ[z]$ be a monic non-constant polynomial. Can the set $\{z ∈ ℂ : |f(z)| ≤ 1\}$ be covered by a set of closed discs the sum of whose radii is $≤ 2$?

    depends on sorry what this means

    Statement uses: Iff, True, Polynomial, Complex, Polynomial.Monic, Ne, Nat, Polynomial.natDegree, OfNat.ofNat, Exists, Nonempty, Erdos509.BoundedDiscCover, Set.ofPred, LE.le, Real, Norm.norm, Polynomial.eval

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

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_509 : answer(sorry) ↔ ∀ (f : ℂ[X]), f.Monic → f.natDegree ≠ 0 →
    ∃ (ι : Type), Nonempty (BoundedDiscCover {z | ‖f.eval z‖ ≤ 1} 2 ι) := by
…

    Mentions: Erdos509.BoundedDiscCover

  5. theorem Erdos509.erdos_509.variants.Cartan_bound Let $f(z) ∈ ℂ[z]$ be a monic non-constant polynomial sorry line 99 source

    Source documentation

    Let $f(z) ∈ ℂ[z]$ be a monic non-constant polynomial. Can the set $\{z ∈ ℂ : |f(z)| ≤ 1\}$ be covered by a set of closed discs the sum of whose radii is $≤ 2e$? Solution: True. This is due to Cartan. See Sur les systèmes de fonctions holomorphes à variétés linéaires lacunaires et leurs applications, Henri Cartan, http://www.numdam.org/article/ASENS_1928_3_45__255_0.pdf

    L4DEL explanation

    Let $f(z) ∈ ℂ[z]$ be a monic non-constant polynomial. Can the set $\{z ∈ ℂ : |f(z)| ≤ 1\}$ be covered by a set of closed discs the sum of whose radii is $≤ 2e$? Solution: True. This is due to Cartan. See Sur les systèmes de fonctions holomorphes à variétés linéaires lacunaires et leurs applications, Henri Cartan, http://www.numdam.org/article/ASENS_1928_3_45__255_0.pdf

    Sources and attribution: Pinned Lean source (1646ca16afd6)

    depends on sorry what this means

    Statement uses: Iff, True, Polynomial, Complex, Polynomial.Monic, Ne, Nat, Polynomial.natDegree, OfNat.ofNat, Exists, Nonempty, Erdos509.BoundedDiscCover, Set.ofPred, LE.le, Real, Norm.norm, Polynomial.eval, HMul.hMul, Real.exp

    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.

    theorem erdos_509.variants.Cartan_bound : answer(True) ↔ ∀ (f : ℂ[X]), f.Monic → f.natDegree ≠ 0 →
    ∃ (ι : Type), Nonempty (BoundedDiscCover {z | ‖f.eval z‖ ≤ 1} (2*rexp 1) ι) := by
…

    Mentions: Erdos509.BoundedDiscCover

  6. theorem Erdos509.erdos_509.variants.Pommerenke_bound Let $f(z) ∈ ℂ[z]$ be a monic non-constant polynomial sorry line 109 source

    Source documentation

    Let $f(z) ∈ ℂ[z]$ be a monic non-constant polynomial. Can the set $\{z ∈ ℂ : |f(z)| ≤ 1\}$ be covered by a set of closed discs the sum of whose radii is $≤ 2.59$? Solution: True. This is due to Pommerenke.

    depends on sorry what this means

    Statement uses: Iff, True, Polynomial, Complex, Polynomial.Monic, Ne, Nat, Polynomial.natDegree, OfNat.ofNat, Exists, Nonempty, Erdos509.BoundedDiscCover, Set.ofPred, LE.le, Real, Norm.norm, Polynomial.eval, OfScientific.ofScientific, Bool.true

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

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_509.variants.Pommerenke_bound : answer(True) ↔ ∀ (f : ℂ[X]), f.Monic → f.natDegree ≠ 0 →
    ∃ (ι : Type), Nonempty (BoundedDiscCover {z | ‖f.eval z‖ ≤ 1} 2.59 ι) := by
…

    Mentions: Erdos509.BoundedDiscCover

  7. theorem Erdos509.erdos_509.variants.Pommerenke_connected Let $f(z) ∈ ℂ[z]$ be a monic non-constant polynomial sorry line 120 source

    Source documentation

    Let $f(z) ∈ ℂ[z]$ be a monic non-constant polynomial. If it is connected, can the set $\{z ∈ ℂ : |f(z)| ≤ 1\}$ be covered by a set of circles the sum of whose radii is $≤ 2$? Solution: True. This is due to Pommerenke.

    depends on sorry what this means

    Statement uses: Iff, True, Polynomial, Complex, Polynomial.Monic, Ne, Nat, Polynomial.natDegree, OfNat.ofNat, IsConnected, Set.ofPred, LE.le, Real, Norm.norm, Polynomial.eval, Exists, Nonempty, Erdos509.BoundedDiscCover

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

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_509.variants.Pommerenke_connected : answer(True) ↔ ∀ (f : ℂ[X]), f.Monic → f.natDegree ≠ 0 →
    IsConnected {z | ‖f.eval z‖ ≤ 1} →
    ∃ (ι : Type), Nonempty (BoundedDiscCover {z | ‖f.eval z‖ ≤ 1} 2 ι) := by
…

    Mentions: Erdos509.BoundedDiscCover