Theorems · Definition · number theory

liouvilleNumber

ℝ → ℝ

For a real number m, Liouville's constant is $$ \sum_{i=0}^\infty\frac{1}{m^{i!}}. $$ The series converges only for 1 < m. However, there is no restriction on m, since, if the series does not converge, then the sum of the series is defined to be zero.

Defined in

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Cited by

3 results in Mathlib

Foundations

Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound