FormalConjectures/ErdosProblems/1044.lean

GitHub source file

6 declarations, 4 contain sorry, 0 declared as axioms

1. def Erdos1044.IsAdmissible The polynomials under consideration: those of the form $f(z)=\prod_{i=1}^n(z-z_i)$, for some $n\geq 1$, where $\lvert z_i\rvert\leq 1$ for all $i$ line 42 source

   Source documentation

   The polynomials under consideration: those of the form $f(z)=\prod_{i=1}^n(z-z_i)$, for some $n\geq 1$, where $\lvert z_i\rvert\leq 1$ for all $i$.

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

   Statement uses: Polynomial, Complex

   Proof uses: Exists, Nat, And, LT.lt, OfNat.ofNat, Fin, LE.le, Real, Norm.norm, Eq, Finset.prod, Finset.univ, HSub.hSub, Polynomial.X, RingHom, Polynomial.C

   19 instances, coercions and auxiliary constants left out.

   def IsAdmissible (f : ℂ[X]) : Prop :=
   …

2. def Erdos1044.maxBoundaryLength Documented declaration: maxBoundaryLength line 50 source

   Source documentation

   $\Lambda(f)$, the maximum of the lengths of the boundaries of the connected components of $\{ z: \lvert f(z)\rvert<1\}$, where the length of a subset of $\mathbb{C}$ is its $1$-dimensional Hausdorff measure.

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

   Statement uses: Polynomial, Complex, ENNReal

   Proof uses: iSup, Membership.mem, Set, Set.ofPred, LT.lt, Real, Norm.norm, Polynomial.eval, OfNat.ofNat, Erdos1041.length, frontier, connectedComponentIn

   19 instances, coercions and auxiliary constants left out.

   noncomputable def maxBoundaryLength (f : ℂ[X]) : ℝ≥0∞ :=
   …

3. theorem Erdos1044.erdos_1044 Let $f(z)=\prod_{i=1}^n(z-z_i)\in\mathbb{C}[x]$ where $\lvert z_i\rvert\leq 1$ for all $i$ sorry line 68 source

   Source documentation

   Let $f(z)=\prod_{i=1}^n(z-z_i)\in\mathbb{C}[x]$ where $\lvert z_i\rvert\leq 1$ for all $i$. If $\Lambda(f)$ is the maximum of the lengths of the boundaries of the connected components of $$ \{ z: \lvert f(z)\rvert<1\} $$ then determine the infimum of $\Lambda(f)$.

   A problem of Erdős, Herzog, and Piranian [EHP58].

   This has been resolved by Tang, who proved that the infimum of $\Lambda(f)$ over all such $f$ is $2$.

   depends on sorry what this means

   Statement uses: IsGLB, ENNReal, Set.ofPred, Exists, Polynomial, Complex, And, Erdos1044.IsAdmissible, Eq, Erdos1044.maxBoundaryLength, OfNat.ofNat, Nat

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

   18 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1044 :
       IsGLB {L : ℝ≥0∞ | ∃ f : ℂ[X], IsAdmissible f ∧ maxBoundaryLength f = L} answer(2) := by
   …

   Mentions: Erdos1044.IsAdmissible, Erdos1044.maxBoundaryLength

4. theorem Erdos1044.erdos_1044.variants.infimum_eq_two This has been resolved by Tang, who proved that the infimum of $\Lambda(f)$ over all such $f$ is $2$ sorry line 77 source

   Source documentation

   This has been resolved by Tang, who proved that the infimum of $\Lambda(f)$ over all such $f$ is $2$.

   depends on sorry what this means

   Statement uses: IsGLB, ENNReal, Set.ofPred, Exists, Polynomial, Complex, And, Erdos1044.IsAdmissible, Eq, Erdos1044.maxBoundaryLength, OfNat.ofNat, Nat

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

   18 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1044.variants.infimum_eq_two :
       IsGLB {L : ℝ≥0∞ | ∃ f : ℂ[X], IsAdmissible f ∧ maxBoundaryLength f = L} 2 := by
   …

   Mentions: Erdos1044.IsAdmissible, Erdos1044.maxBoundaryLength

5. theorem Erdos1044.erdos_1044.variants.fixed_degree Tang also suggests that, if the degree $n$ is fixed, then the infimum over all such $f$ of degree $n$ is attained by $f_n(z)=z^n-1$ sorry line 86 source

   Source documentation

   Tang also suggests that, if the degree $n$ is fixed, then the infimum over all such $f$ of degree $n$ is attained by $f_n(z)=z^n-1$.

   depends on sorry what this means

   Statement uses: Nat, LT.lt, OfNat.ofNat, IsLeast, ENNReal, Set.ofPred, Exists, Polynomial, Complex, And, Erdos1044.IsAdmissible, Eq, Polynomial.natDegree, Erdos1044.maxBoundaryLength, HSub.hSub, HPow.hPow, Polynomial.X

   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_1044.variants.fixed_degree (n : ℕ) (hn : 0 < n) :
       IsLeast {L : ℝ≥0∞ | ∃ f : ℂ[X], IsAdmissible f ∧ f.natDegree = n ∧ maxBoundaryLength f = L}
         (maxBoundaryLength (X ^ n - 1)) := by
   …

   Mentions: Erdos1044.IsAdmissible, Erdos1044.maxBoundaryLength

6. theorem Erdos1044.erdos_1044.variants.fixed_degree_of_le_two Tang also suggests that, if the degree $n$ is fixed, then the infimum over all such $f$ of degree $n$ is attained by $f_n(z)=z^n-1$ (and proves this for $n=1$ and $n=2$) sorry line 96 source

   Source documentation

   Tang also suggests that, if the degree $n$ is fixed, then the infimum over all such $f$ of degree $n$ is attained by $f_n(z)=z^n-1$ (and proves this for $n=1$ and $n=2$).

   depends on sorry what this means

   Statement uses: Nat, Or, Eq, OfNat.ofNat, IsLeast, ENNReal, Set.ofPred, Exists, Polynomial, Complex, And, Erdos1044.IsAdmissible, Polynomial.natDegree, Erdos1044.maxBoundaryLength, HSub.hSub, HPow.hPow, Polynomial.X

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

   26 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1044.variants.fixed_degree_of_le_two (n : ℕ) (hn : n = 1 ∨ n = 2) :
       IsLeast {L : ℝ≥0∞ | ∃ f : ℂ[X], IsAdmissible f ∧ f.natDegree = n ∧ maxBoundaryLength f = L}
         (maxBoundaryLength (X ^ n - 1)) := by
   …

   Mentions: Erdos1044.IsAdmissible, Erdos1044.maxBoundaryLength