Parameters lying in intermediate fields of degree at most one quarter of the ambient degree have a uniform fourth-root contribution at the balanced discriminant radius.

def CCDN.boundedSmallSubfieldIntegers (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : Set (NumberField.RingOfIntegers K)

The algebraic integers of K bounded by B at every infinite place that lie in an intermediate field L with 4 * [L : ℚ] ≤ [K : ℚ].

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.boundedSmallSubfieldIntegers_finite (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : (boundedSmallSubfieldIntegers K B).Finite

The set boundedSmallSubfieldIntegers K B is finite.

noncomputable def CCDN.smallSubfieldIntegerCountConstant (n : ℕ) : ℝ

The constant 2 ^ n * (2 * √n + 1) ^ n in the count of bounded integers in small subfields of a number field of degree n.

Equations

• CCDN.smallSubfieldIntegerCountConstant n = 2 ^ n * (2 * √↑n + 1) ^ n

theorem CCDN.smallSubfieldIntegerCountConstant_pos (n : ℕ) : 0 < smallSubfieldIntegerCountConstant n

The constant smallSubfieldIntegerCountConstant n is positive.

theorem CCDN.boundedSmallSubfieldIntegers_balanced_count (K : Type u_1) [Field K] [NumberField K] {D : ℝ} (hD : 1 ≤ D) : ↑(boundedSmallSubfieldIntegers K (9 * D ^ (1 / ↑(Module.finrank ℚ K)))).ncard ≤ smallSubfieldIntegerCountConstant (Module.finrank ℚ K) * 9 ^ (↑(Module.finrank ℚ K) / 4) * D ^ (1 / 4)

At the balanced radius 9 * D ^ (1 / n) with D ≥ 1 and n = [K : ℚ], the number of bounded integers in small subfields is at most a constant depending only on n times D ^ (1 / 4).