Finite ideal sums bounded by geometric Euler products

noncomputable def NairTenenbaum.idealNormWeightHom {K : Type u_1} [Field K] [NumberField K] (σ : ℝ) : Ideal (NumberField.RingOfIntegers K) →* ℝ

The multiplicative weight obtained by raising ideal norms to a real power.

Equations

• NairTenenbaum.idealNormWeightHom σ = { toFun := fun (I : Ideal (NumberField.RingOfIntegers K)) => ↑(Ideal.absNorm I) ^ (-σ), map_one' := ⋯, map_mul' := ⋯ }

theorem NairTenenbaum.ideal_eq_prod_factor_counts {K : Type u_1} [Field K] [NumberField K] {I : Ideal (NumberField.RingOfIntegers K)} (hI : I ≠ ⊥) (S : Finset (Ideal (NumberField.RingOfIntegers K))) (hS : (UniqueFactorizationMonoid.normalizedFactors I).toFinset ⊆ S) : I = ∏ P ∈ S, P ^ Multiset.count P (UniqueFactorizationMonoid.normalizedFactors I)

theorem NairTenenbaum.idealNorm_prime_gt_one {K : Type u_1} [Field K] [NumberField K] {P : Ideal (NumberField.RingOfIntegers K)} (hP : Prime P) : 1 < Ideal.absNorm P

theorem NairTenenbaum.finite_idealNorm_sum_le_prod {K : Type u_1} [Field K] [NumberField K] (T S : Finset (Ideal (NumberField.RingOfIntegers K))) (hT : ∀ I ∈ T, I ≠ ⊥) (hS : ∀ P ∈ S, Prime P) (hsupport : ∀ I ∈ T, (UniqueFactorizationMonoid.normalizedFactors I).toFinset ⊆ S) {σ : ℝ} (hσ : 0 < σ) : ∑ I ∈ T, ↑(Ideal.absNorm I) ^ (-σ) ≤ ∏ P ∈ S, (1 - ↑(Ideal.absNorm P) ^ (-σ))⁻¹

theorem NairTenenbaum.idealNorm_prime_weight_le_half {K : Type u_1} [Field K] [NumberField K] {P : Ideal (NumberField.RingOfIntegers K)} (hP : Prime P) {σ : ℝ} (hσ : 1 ≤ σ) : ↑(Ideal.absNorm P) ^ (-σ) ≤ 1 / 2

theorem NairTenenbaum.finite_idealNorm_sum_le_exp {K : Type u_1} [Field K] [NumberField K] (T S : Finset (Ideal (NumberField.RingOfIntegers K))) (hT : ∀ I ∈ T, I ≠ ⊥) (hS : ∀ P ∈ S, Prime P) (hsupport : ∀ I ∈ T, (UniqueFactorizationMonoid.normalizedFactors I).toFinset ⊆ S) {σ : ℝ} (hσ : 1 ≤ σ) : ∑ I ∈ T, ↑(Ideal.absNorm I) ^ (-σ) ≤ Real.exp (∑ P ∈ S, (↑(Ideal.absNorm P) ^ (-σ) + 2 * (↑(Ideal.absNorm P) ^ (-σ)) ^ 2))