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

3 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 1041

Reference: erdosproblems.com/1041

Imports (1)
Imported by 1 file
  1. def Erdos1041.length The length of a subset $s$ of $\mathbb{C}$ is defined to be its 1-dimensional Hausdorff measure $\mathcal{H}^1(s)$ line 43 source

    Source documentation

    The length of a subset $s$ of $\mathbb{C}$ is defined to be its 1-dimensional Hausdorff measure $\mathcal{H}^1(s)$.

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

    Statement uses: Set, Complex, ENNReal

    Proof uses: MeasureTheory.Measure, MeasureTheory.Measure.hausdorffMeasure, OfNat.ofNat, Real

    9 instances, coercions and auxiliary constants left out.

    noncomputable def length (s : Set ℂ) : ℝ≥0∞ := μH[1] s
…
  2. theorem Erdos1041.exists_connected_component_contains_two_roots Documented declaration: exists_connected_component_contains_two_roots sorry line 57 source

    Source documentation

    Erdős–Herzog–Piranian Component Lemma (Metric Properties of Polynomials, 1958): If $f$ is a monic degree $n$ polynomial with all roots in the unit disk, then some connected component of $\{z \mid |f(z)| < 1\}$ contains at least two roots with multiplicity.

    See p. 139, above Problem 5: [EHP58] Erdős, P. and Herzog, F. and Piranian, G., Metric properties of polynomials. J. Analyse Math. (1958), 125-148.

    depends on sorry what this means

    Statement uses: Nat, Polynomial, Complex, GE.ge, OfNat.ofNat, Eq, Polynomial.natDegree, Polynomial.Monic, LE.le, Set, Polynomial.rootSet, Metric.ball, Real, Exists, And, Set.ofPred, LT.lt, Norm.norm, Polynomial.eval, IsConnected and 5 more

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

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem exists_connected_component_contains_two_roots :
    ∃ C, C ⊆ {z | ‖f.eval z‖ < 1} ∧ IsConnected C ∧
      2 ≤ (f.roots.filter (· ∈ C)).card := by
…
  3. theorem Erdos1041.erdos_1041 sorry line 81 source

    depends on sorry what this means

    Statement uses: Iff, False, Nat, Polynomial, Complex, GE.ge, OfNat.ofNat, Eq, Polynomial.natDegree, Polynomial.Monic, LE.le, Set, Polynomial.rootSet, Metric.ball, Real, Exists, Multiset, Insert.insert, Singleton.singleton, Polynomial.roots and 10 more

    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.