Equilibrium points of logarithmic potentials

AbbreviationCharge sequences#✓fully proved

A charge sequence is an arbitrary sequence \((z_n)_{n \in \mathbb{N}}\) of complex numbers, read as the positions of the charges.

abbrev ChargeSeq := ℕ → ℂ

Used by 4

Used byEquilibrium-free logarithmic potential conjecture · Field of a charge sequence · Summable charge sequences · Distinct charge positions

DefinitionDistinct charge positions#✓fully proved

A charge sequence \((z_n)\) has distinct positions when its terms are pairwise distinct: \(z_m \neq z_n\) whenever \(m \neq n\).

def PointsDistinct (c : ChargeSeq) : Prop :=
  Function.Injective c

Uses 1 · Used by 1

Statement usesCharge sequences

Used byEquilibrium-free logarithmic potential conjecture

DefinitionSummable charge sequences#✓fully proved

A charge sequence \((z_n)\) is summable when \(z_n \neq 0\) for every \(n\) and \(\sum_n 1/|z_n| < \infty\).

def IsSummable (c : ChargeSeq) : Prop :=
  (∀ n, c n ≠ 0) ∧ Summable (fun n => 1 / ‖c n‖)

Uses 1 · Used by 1

Statement usesCharge sequences

Used byEquilibrium-free logarithmic potential conjecture

DefinitionField of a charge sequence#✓fully proved

For a charge sequence \((z_n)\) and a point \(z \in \mathbb{C}\), the field at \(z\) is the sum \(\sum_n 1/(z - z_n)\), where a term with \(z_n = z\) counts as \(0\) and the sum is taken to be \(0\) when the family \(\bigl(1/(z - z_n)\bigr)_n\) is not summable.

The sum converges absolutely when \(z_n \neq 0\) for every \(n\) and \(\sum_n 1/|z_n| < \infty\).

noncomputable def FieldSum (c : ChargeSeq) (z : ℂ) : ℂ :=
  ∑' n, 1 / (z - c n)

Uses 1 · Used by 1

Statement usesCharge sequences

Used byEquilibrium-free logarithmic potential conjecture

DefinitionEquilibrium-free logarithmic potential conjecture#✓fully proved

The conjecture states that there exists a charge sequence \((z_n)\) whose positions are pairwise distinct, which is summable (\(z_n \neq 0\) for every \(n\) and \(\sum_n 1/|z_n| < \infty\)), and whose field \(\sum_n 1/(z - z_n)\) is nonzero at every point \(z \in \mathbb{C}\) that is not one of the \(z_n\).

def conjecture : Prop :=
  ∃ c : ChargeSeq, PointsDistinct c ∧ IsSummable c ∧
    ∀ z : ℂ, (∀ n, z ≠ c n) → FieldSum c z ≠ 0

Sources

• record AMR-022-7078 (Problem 7.78, Rubel).

Uses 4 · Used by 1

Statement usesCharge sequences · Field of a charge sequence · Summable charge sequences · Distinct charge positions

Used byThe equilibrium-free logarithmic potential conjecture is false

TheoremThe equilibrium-free logarithmic potential conjecture is false#●ready to prove

There is no charge sequence \((z_n)\) whose positions are pairwise distinct, which is summable (\(z_n \neq 0\) for every \(n\) and \(\sum_n 1/|z_n| < \infty\)), and whose field \(\sum_n 1/(z - z_n)\) is nonzero at every point \(z \in \mathbb{C}\) that is not one of the \(z_n\).

Clunie, Eremenko and Rossi proved more: under these hypotheses the field has infinitely many zeros.

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

• J. Clunie, A. Eremenko and J. Rossi, On equilibrium points of logarithmic and Newtonian potentials, J. London Math. Soc. (2) 47 (1993), 309-320.

Uses 1

Statement usesEquilibrium-free logarithmic potential conjecture

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.