Least prime powers exceeding a real threshold

noncomputable def NairTenenbaum.firstPowerAbove (p : ℕ) (T : ℝ) : ℕ

The least exponent whose prime power exceeds the real threshold.

Equations

• NairTenenbaum.firstPowerAbove p T = if hp : 1 < p then Nat.find ⋯ else 0

theorem NairTenenbaum.firstPowerAbove_spec {p : ℕ} (hp : 1 < p) (T : ℝ) : T < ↑p ^ firstPowerAbove p T

theorem NairTenenbaum.firstPowerAbove_le {p e : ℕ} (hp : 1 < p) {T : ℝ} (he : T < ↑p ^ e) : firstPowerAbove p T ≤ e

theorem NairTenenbaum.firstPowerAbove_pos {p : ℕ} (hp : 1 < p) {T : ℝ} (hT : 1 ≤ T) : 0 < firstPowerAbove p T

theorem NairTenenbaum.firstPowerAbove_upper {p : ℕ} (hp : 1 < p) {T : ℝ} (hT : 1 ≤ T) : ↑p ^ firstPowerAbove p T ≤ ↑p * T

theorem NairTenenbaum.firstPowerAbove_dvd {p e n : ℕ} (hp : 1 < p) {T : ℝ} (he : T < ↑p ^ e) (hd : p ^ e ∣ n) : p ^ firstPowerAbove p T ∣ n

Minimality preserves divisibility whenever an available prime power already exceeds the threshold.

theorem NairTenenbaum.PolynomialSystem.sum_totalExponent_le_degree {k r : ℕ} (P : PolynomialSystem k r) : ∑ i : Fin r, totalExponent P.exponent i ≤ P.total.natDegree

The total multiplicities of the irreducible factors are bounded by degree.

theorem NairTenenbaum.PolynomialSystem.exists_large_coordinate_primePower {k r : ℕ} (P : PolynomialSystem k r) (n : Tuple r) {p : ℕ} {T : ℝ} (hT : 1 ≤ T) (hlarge : T ^ P.total.natDegree < ↑p ^ ∑ i : Fin r, totalExponent P.exponent i * (↑(n i)).factorization p) : ∃ (i : Fin r), T < ↑p ^ (↑(n i)).factorization p

A large weighted prime part forces a large prime power in one coordinate. The exponent loss is the total degree, accounting for repeated factors.

theorem NairTenenbaum.PolynomialSystem.exists_large_primePower_of_crossing {k r : ℕ} (P : PolynomialSystem k r) (n : Tuple r) {p : ℕ} (hp : Nat.Prime p) {T : ℝ} (hT : 1 ≤ T) (hsmall : ↑(weightedMass P.exponent (primeSelect n (Finset.range p))) ≤ T ^ P.total.natDegree) (hcross : (T ^ P.total.natDegree) ^ 2 < ↑(weightedMass P.exponent (primeSelect n (Finset.range (p + 1))))) : ∃ (i : Fin r), T < ↑p ^ (↑(n i)).factorization p

The gap between two prefix thresholds forces a large coordinate prime power at the crossing prime.