Gauss–Kuzmin–Wirsing operator

DefinitionTerms of the Gauss–Kuzmin–Wirsing series#✓fully proved

For a function \(f : \mathbb{R} \to \mathbb{R}\), a real number \(x\) and a natural number \(k\), the \(k\)-th term of the Gauss–Kuzmin–Wirsing series of \(f\) at \(x\) is \(\frac{1}{(x+k+1)^2} f\left(\frac{1}{x+k+1}\right)\), with the convention \(1/0 = 0\).

Summing these terms over \(k \ge 0\) gives the Gauss–Kuzmin–Wirsing operator, whose value at \(x\) is \(\sum_{k \ge 1} (x+k)^{-2} f(1/(x+k))\) when this series converges absolutely and \(0\) otherwise; for \(x \in [0, 1]\) the series converges absolutely whenever \(f\) is bounded on \([0, 1]\).

noncomputable def gkwTerm (f : ℝ → ℝ) (x : ℝ) (k : ℕ) : ℝ :=
  (1 / (x + (k + 1 : ℝ)) ^ 2) * f (1 / (x + (k + 1 : ℝ)))

Used by 2

Used byEigenvalues of the Gauss–Kuzmin–Wirsing operator on continuous functions · The Gauss–Kuzmin–Wirsing operator has eigenvalue one

DefinitionEigenvalues of the Gauss–Kuzmin–Wirsing operator on continuous functions#✓fully proved

A real number \(\lambda\) is an eigenvalue of the Gauss–Kuzmin–Wirsing operator in the continuous model when there is a function \(f : \mathbb{R} \to \mathbb{R}\), continuous on \([0, 1]\), bounded on \([0, 1]\) and not identically zero on \([0, 1]\), such that for every \(x \in [0, 1]\)

\[\sum_{k \ge 1} \frac{1}{(x+k)^2} f\left(\frac{1}{x+k}\right) = \lambda f(x).\]

Boundedness follows from continuity on \([0, 1]\) and is recorded explicitly; it makes the series converge on \([0, 1]\). This continuous model is not the source's spectral space: it admits eigenvalues that the holomorphic theory excludes (for example \(1/3\), from eigenfunction lifts under inversion), so it is kept only as a pointwise model exhibiting the dominant eigenvalue \(1\). The Wirsing constant is defined over holomorphic eigenfunctions instead.

def IsEigenvalue (lam : ℝ) : Prop :=
  ∃ f : ℝ → ℝ, ContinuousOn f (Set.Icc 0 1) ∧
    (∃ x ∈ Set.Icc (0 : ℝ) 1, f x ≠ 0) ∧
    (∃ M : ℝ, ∀ y ∈ Set.Icc (0 : ℝ) 1, |f y| ≤ M) ∧
    ∀ x ∈ Set.Icc (0 : ℝ) 1, gkwOperator f x = lam * f x

Uses 1 · Used by 1

Statement usesTerms of the Gauss–Kuzmin–Wirsing series

Used byThe Gauss–Kuzmin–Wirsing operator has eigenvalue one

TheoremThe Gauss–Kuzmin–Wirsing operator has eigenvalue one#✓fully proved

There is a function \(f : \mathbb{R} \to \mathbb{R}\) that is continuous on \([0, 1]\), bounded on \([0, 1]\) and not identically zero on \([0, 1]\), such that \(\sum_{k \ge 1} \frac{1}{(x+k)^2} f\left(\frac{1}{x+k}\right) = f(x)\) for every \(x \in [0, 1]\); that is, \(1\) is an eigenvalue of the Gauss–Kuzmin–Wirsing operator in the continuous model.

An eigenfunction is the Gauss density \(x \mapsto 1/(1+x)\), for which the series telescopes.

theorem isEigenvalue_one : IsEigenvalue 1

Uses 2

Statement usesEigenvalues of the Gauss–Kuzmin–Wirsing operator on continuous functions

Proof usesTerms of the Gauss–Kuzmin–Wirsing series

DefinitionTerms of the complex Gauss–Kuzmin–Wirsing series#✓fully proved

For a function \(f : \mathbb{C} \to \mathbb{C}\), a complex number \(z\) and a natural number \(k\), the \(k\)-th term of the Gauss–Kuzmin–Wirsing series of \(f\) at \(z\) is \(\frac{1}{(z+k+1)^2} f\left(\frac{1}{z+k+1}\right)\), with the convention \(1/0 = 0\).

noncomputable def gkwTermHol (f : ℂ → ℂ) (z : ℂ) (k : ℕ) : ℂ :=
  (1 / (z + (k + 1 : ℂ)) ^ 2) * f (1 / (z + (k + 1 : ℂ)))

Used by 1

Used byHolomorphic eigenvalues of the Gauss–Kuzmin–Wirsing operator

DefinitionHolomorphic eigenvalues of the Gauss–Kuzmin–Wirsing operator#✓fully proved

Let \(D = \{z \in \mathbb{C} : |z - 1| < 3/2\}\) be the Mayer disk. A complex number \(\lambda\) is a holomorphic eigenvalue of the Gauss–Kuzmin–Wirsing operator when there is a function \(f : \mathbb{C} \to \mathbb{C}\), holomorphic on \(D\) and not identically zero on \(D\), such that for every \(z \in D\)

\[\sum_{k \ge 1} \frac{1}{(z+k)^2} f\left(\frac{1}{z+k}\right) = \lambda f(z).\]

This is the function space of Mayer and Roepstorff, on which the spectrum of the operator below the dominant eigenvalue \(1\) is the source's spectral data.

def IsHolomorphicEigenvalue (lam : ℂ) : Prop :=
  ∃ f : ℂ → ℂ, DifferentiableOn ℂ f (Metric.ball 1 (3 / 2)) ∧
    (∃ z ∈ Metric.ball (1 : ℂ) (3 / 2 : ℝ), f z ≠ 0) ∧
    ∀ z ∈ Metric.ball (1 : ℂ) (3 / 2 : ℝ), gkwOperatorHol f z = lam * f z

Uses 1 · Used by 1

Statement usesTerms of the complex Gauss–Kuzmin–Wirsing series

Used byWirsing constant

DefinitionWirsing constant#✓fully proved

The Wirsing constant is the supremum in \(\mathbb{R}\) of \(|\lambda|\) over all holomorphic eigenvalues \(\lambda \ne 1\) of the Gauss–Kuzmin–Wirsing operator on the Mayer disk \(\{z \in \mathbb{C} : |z - 1| < 3/2\}\), with the convention that the supremum is \(0\) when there is no such \(\lambda\) or when these absolute values are unbounded.

The source's spectral theorem, that this supremum is attained at the negative eigenvalue \(\lambda_2\) and that no other holomorphic eigenvalue lies between it and \(1\) in absolute value, is not asserted here.

noncomputable def wirsingConstant : ℝ :=
  sSup { r : ℝ | ∃ lam : ℂ, IsHolomorphicEigenvalue lam ∧ lam ≠ 1 ∧
    r = ‖lam‖ }

Uses 1 · Used by 2

Statement usesHolomorphic eigenvalues of the Gauss–Kuzmin–Wirsing operator

Used byMayer–Roepstorff lower bound for the Wirsing constant · Mayer–Roepstorff upper bound for the Wirsing constant

TheoremMayer–Roepstorff lower bound for the Wirsing constant#●ready to prove

The Wirsing constant is at least \(0.30366299\).

theorem_wanted mayerRoepstorffLowerBound_wanted :
    (30366299 / 100000000 : ℝ) ≤ wirsingConstant

Sources

• Mayer and Roepstorff (1987), eq. (5.20), catalogue lower bound 0.30366299, certified via generalized Temple inequalities.

Uses 1

Statement usesWirsing constant

TheoremMayer–Roepstorff upper bound for the Wirsing constant#●ready to prove

The Wirsing constant is at most \(0.30366327\).

theorem_wanted mayerRoepstorffUpperBound_wanted :
    wirsingConstant ≤ (30366327 / 100000000 : ℝ)

Sources

• Mayer and Roepstorff (1987), eq. (5.20), catalogue upper bound 0.30366327.

Uses 1

Statement usesWirsing constant

6 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.