'length' in topology

Stream: Is there code for X?

[Success Moses]

Erdős problem 1041:
Let f(z) = ∏ᵢ (z − zᵢ) be a polynomial in ℂ[x] with |zᵢ| < 1 for all i. Must there always exist a path of length less than 2 in {z : |f(z)| < 1} which connects two of the roots of f?

Question about formalization:
In Mathlib.Topology.Path, Path x y is a continuous function f : I → X such that f 0 = x and f 1 = y. Is there a notion of 'length' the way Erdős meant it in this problem already defined in mathlib?

[Aaron Liu]

I guess you could take the 1-dimensional Hausdorff measure of the Set.range of the path

[Success Moses]

@Aaron Liu

import Mathlib.Data.Set.Basic
import Mathlib.Algebra.Polynomial.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Analysis.Complex.Norm
import Mathlib.MeasureTheory.Measure.Hausdorff
-- ℂ is a Measureable space
import Mathlib.MeasureTheory.Constructions.BorelSpace.Complex

open Polynomial MeasureTheory

namespace Erdos1041

variable (n : ℕ) (f : ℂ[X]) (x : Fin n → ℂ)

/--
The length of a subset $s$ of $ℂ$ is defined to be its 1-dimensional
Hausdorff measure `ℋ¹(s)`.
-/
noncomputable def length (s : Set ℂ) : ℝ := ENNReal.toReal <| μH[1] s

/--
Let
$$ f(z) = \prod_{i=1}^{n} (z - z_i) \in \mathbb{C}[x] $$
with $|z_i| < 1$ for all $i$.

Conjecture: Must there always exist a path of length less than 2 in
$$ \{ z \in \mathbb{C} \mid |f(z)| < 1 \} $$
which connects two of the roots of $f$?
-/
theorem erdos_1041
  (hn : n ≥ 2)
  (hx : ∀ i, ‖x i‖ < 1)
  (h : f = ∏ i : Fin n, (X - C (x i))) :
    ∃ (i j : Fin n) (hij : i ≠ j) (γ : Path (x i) (x j)),
    Set.range γ ⊆ { z : ℂ | ‖f.eval z‖ < 1 } ∧
    length (Set.range γ) < 2 := by
  sorry

end Erdos1041

I used Hausdorff measure. Is this good?

[Sébastien Gouëzel]

We have docs#eVariationOn or docs#Manifold.pathELength which are probably better suited for the task.

[Sébastien Gouëzel]

And you should use ENNReal in your statement: otherwise, just take a path with infinite length, thenENNReal.toReal of its length becomes zero, so the statement is true but trivial.

[Junyan Xu]

mathlib3#18375 defines arclength and Path.length in terms of evariationOn but at this moment it probably needs to be manually ported ...

[Success Moses]

namespace Erdos1041

variable (n : ℕ) (f : ℂ[X]) (x : Fin n → ℂ)

noncomputable def length' {α : Type} [PseudoEMetricSpace α] {x y : α}
    (γ : Path x y) : ℝ≥0∞ :=
  eVariationOn γ Set.univ

/--
Let
$$ f(z) = \prod_{i=1}^{n} (z - z_i) \in \mathbb{C}[x] $$
with $|z_i| < 1$ for all $i$.

Conjecture: Must there always exist a path of length less than 2 in
$$ \{ z \in \mathbb{C} \mid |f(z)| < 1 \} $$
which connects two of the roots of $f$?
-/
theorem erdos_1041
  (hn : n ≥ 2)
  (hx : ∀ i, ‖x i‖ < 1)
  (h : f = ∏ i : Fin n, (X - C (x i))) :
    ∃ (i j : Fin n) (hij : i ≠ j) (γ : Path (x i) (x j)),
    Set.range γ ⊆ { z : ℂ | ‖f.eval z‖ < 1 } ∧
    length' γ < 2 := by
  sorry

end Erdos1041

[Success Moses]

mathlib3#18375 defines arclength and Path.length in terms of evariationOn but at this moment it probably needs to be manually ported ...

Should I open issue for this?

[Junyan Xu]

For porting it? That sounds reasonable ...

[Success Moses]

mathlib4#31751

[Kevin Buzzard]

You have opened an issue rather than a pull request. Is this what you meant to do @Success Moses Oh -- maybe? Note that mathlib has hundreds of open issues so you might be waiting a while!

[Success Moses]

I was writing the proofs. Please review #31766 @Junyan Xu and @Kevin Buzzard if you are not too busy.

[Kevin Buzzard]

You can't have sorrys in mathlib, you claim the file is copyright someone else from some other year, and if you're adding a new file you need to run lake exe mk_all to update Mathlib.lean (and then commit it). 400+ lines is quite a long PR from someone new to the ecosystem, is there any way you can make it smaller? I am not competent to review, I don't know the first thing about arc lengths in mathlib.

[Junyan Xu]

It's now sorry-free and apart from some cleanups in https://github.com/SuccessMoses/mathlib4/pull/1, it looks to me (the original author of this part)

[Yan Yablonovskiy 🇺🇦]

Also I recommend considering using the #Formal conjectures channel ! Even though this channel does make perfect sense from another perspective too.