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 : ℕ → ℝ) (k : ℕ →₀ ℕ) : ℝ

A Beurling integer is a number of the form ∏ i, (a i) ^ (k i) for a given sequence a and a finitely-supported sequence of naturals k.

Equations

• beurlingInteger a k = k.prod fun (x y : ℕ) => a x ^ y

@[simp]

theorem beurlingInteger_def (a : ℕ → ℝ) (k : ℕ →₀ ℕ) : beurlingInteger a k = k.prod fun (x y : ℕ) => a x ^ y

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

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

Equations

• BeurlingIntegers a = Set.range (beurlingInteger a)

theorem beurlingInteger_mem (a : ℕ → ℝ) (k : ℕ →₀ ℕ) : beurlingInteger a k ∈ BeurlingIntegers a

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

Every element of the sequence a is a Beurling integer.

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

The set of Beurling integers is closed under multiplication.

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

The set of Beurling integers is closed under taking powers.