/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import Mathlib.Algebra.BigOperators.Finsupp.Basic
public import Mathlib.Data.Real.Basic
public import Mathlib.Order.Filter.AtTopBot.Defs@[expose] public sectionBeurling primes
References:
open Filter
A sequence of real numbers 1 < a 0 < a 1 < ... is called a set of Beurling prime numbers if
it tends to infinity.
noncomputable def IsBeurlingPrimes (a : ℕ → ℝ) : Prop :=
1 < a 0 ∧ StrictMono a ∧ Tendsto a atTop atTop
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.
def 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 := rfl
The set of Beurling integers are numbers of the form ∏ i, (a i) ^ (k i), where k has
finite support.
def BeurlingIntegers (a : ℕ → ℝ) : Set ℝ := .range (beurlingInteger a)theorem beurlingInteger_mem (a k) : beurlingInteger a k ∈ BeurlingIntegers a := a:ℕ → ℝk:ℕ →₀ ℕ⊢ beurlingInteger a k ∈ BeurlingIntegers a
All goals completed! 🐙
Every element of the sequence a is a Beurling integer.
lemma generator_mem_beurling (a : ℕ → ℝ) (i : ℕ) : a i ∈ BeurlingIntegers a :=
⟨Finsupp.single i 1, a:ℕ → ℝi:ℕ⊢ beurlingInteger a (Finsupp.single i 1) = a i All goals completed! 🐙⟩The set of Beurling integers is closed under multiplication.
lemma mul_mem_beurling {a : ℕ → ℝ} {x y : ℝ} (hx : x ∈ BeurlingIntegers a)
(hy : y ∈ BeurlingIntegers a) : x * y ∈ BeurlingIntegers a := a:ℕ → ℝx:ℝy:ℝhx:x ∈ BeurlingIntegers ahy:y ∈ BeurlingIntegers a⊢ x * y ∈ BeurlingIntegers a
a:ℕ → ℝy:ℝhy:y ∈ BeurlingIntegers ak:ℕ →₀ ℕ⊢ beurlingInteger a k * y ∈ BeurlingIntegers a
a:ℕ → ℝk:ℕ →₀ ℕl:ℕ →₀ ℕ⊢ beurlingInteger a k * beurlingInteger a l ∈ BeurlingIntegers a
exact ⟨k + l, a:ℕ → ℝk:ℕ →₀ ℕl:ℕ →₀ ℕ⊢ beurlingInteger a (k + l) = beurlingInteger a k * beurlingInteger a l All goals completed! 🐙⟩The set of Beurling integers is closed under taking powers.
lemma pow_mem_beurling {a : ℕ → ℝ} {x : ℝ} (k : ℕ) (hx : x ∈ BeurlingIntegers a) :
x ^ k ∈ BeurlingIntegers a := a:ℕ → ℝx:ℝk:ℕhx:x ∈ BeurlingIntegers a⊢ x ^ k ∈ BeurlingIntegers a
induction k with
a:ℕ → ℝx:ℝhx:x ∈ BeurlingIntegers a⊢ x ^ 0 ∈ BeurlingIntegers a exact ⟨0, a:ℕ → ℝx:ℝhx:x ∈ BeurlingIntegers a⊢ beurlingInteger a 0 = x ^ 0 All goals completed! 🐙⟩
a:ℕ → ℝx:ℝhx:x ∈ BeurlingIntegers ak:ℕih:x ^ k ∈ BeurlingIntegers a⊢ x ^ (k + 1) ∈ BeurlingIntegers a All goals completed! 🐙