Beurling primes

References:

• Wikipedia
• Beurling Zeta Functions, Generalised Primes, and Fractal Membranes

noncomputable def IsBeurlingPrimes (a : ℕ → ℝ) : Prop

A sequence of real numbers 1 < a 0 < a 1 < ... is called a set of Beurling prime numbers if it tends to infinity.

Equations

• IsBeurlingPrimes a = (1 < a 0 ∧ StrictMono a ∧ Filter.Tendsto a Filter.atTop Filter.atTop)

def BeurlingInteger (a : ℕ → ℝ) : Set ℝ

The set of Beurling integers are numbers of the form ∏ i, (a i) ^ (k i), where k has finite support.

Equations

• BeurlingInteger a = Set.range fun (k : ℕ →₀ ℕ) => k.prod fun (x y : ℕ) => a x ^ y

theorem generator_mem_beurling (a : ℕ → ℝ) (i : ℕ) : a i ∈ BeurlingInteger a

Every element of the sequence a is a Beurling integer.

theorem mul_mem_beurling {a : ℕ → ℝ} {x y : ℝ} (hx : x ∈ BeurlingInteger a) (hy : y ∈ BeurlingInteger a) : x * y ∈ BeurlingInteger a

The set of Beurling integers is closed under multiplication.

theorem pow_mem_beurling {a : ℕ → ℝ} {x : ℝ} (k : ℕ) (hx : x ∈ BeurlingInteger a) : x ^ k ∈ BeurlingInteger a

The set of Beurling integers is closed under taking powers.