Named quantities in the determinant and auxiliary-polynomial bounds for a hypersurface of degree d in ℙ^(n+2), and the bracket auxDegreeBound of the coefficient-sensitive auxiliary theorem (CCDN Theorem 3.1.1).

@[reducible, inline]

noncomputable abbrev CCDN.degreeRoot (n d : ℕ) : ℝ

The root d ^ (1 / (n + 1)) of the degree.

Equations

• CCDN.degreeRoot n d = ↑d ^ (1 / (↑n + 1))

@[reducible, inline]

noncomputable abbrev CCDN.factorialRoot (n : ℕ) : ℝ

The root ((n + 1)!) ^ (1 / (n + 1)).

Equations

• CCDN.factorialRoot n = ↑(n + 1).factorial ^ (1 / (↑n + 1))

@[reducible, inline]

noncomputable abbrev CCDN.heightExponent (n d : ℕ) : ℝ

The coefficient-height exponent 1 / ((n + 1) d d ^ (1 / (n + 1))).

Equations

• CCDN.heightExponent n d = 1 / ((↑n + 1) * ↑d * CCDN.degreeRoot n d)

@[reducible, inline]

noncomputable abbrev CCDN.boxExponent (n d : ℕ) : ℝ

The radius exponent (n + 2) / ((n + 1) d ^ (1 / (n + 1))).

Equations

• CCDN.boxExponent n d = (↑n + 2) / ((↑n + 1) * CCDN.degreeRoot n d)

@[reducible, inline]

noncomputable abbrev CCDN.primeSetFactor (bad : Finset ℕ) : ℝ

The bad-prime factor exp (∑ p ∈ bad, log p / p) of a finite set of primes.

Equations

• CCDN.primeSetFactor bad = Real.exp (∑ p ∈ bad, Real.log ↑p / ↑p)

noncomputable def CCDN.auxMainTerm (n d : ℕ) (B b H : ℝ) : ℝ

The main term d^(4 - 1/(n+1)) b B^boxExponent / H^heightExponent of the coefficient-sensitive auxiliary degree bound, for points of height at most B on an equation with coefficient height H and bad-prime factor b.

Equations

• CCDN.auxMainTerm n d B b H = ↑d ^ (4 - 1 / (↑n + 1)) * b * B ^ CCDN.boxExponent n d / H ^ CCDN.heightExponent n d

noncomputable def CCDN.auxDegreeBound (n d : ℕ) (B b H : ℝ) : ℝ

The bracket auxMainTerm + d^(1 - 1/(n+1)) log B + d^(4 - 1/(n+1)) of the coefficient-sensitive auxiliary degree bound.

Equations

• CCDN.auxDegreeBound n d B b H = CCDN.auxMainTerm n d B b H + ↑d ^ (1 - 1 / (↑n + 1)) * Real.log B + ↑d ^ (4 - 1 / (↑n + 1))

theorem CCDN.le_rpow_four_sub_inv {n d : ℕ} (hd : 0 < d) : ↑d ≤ ↑d ^ (4 - 1 / (↑n + 1))

d ≤ d ^ (4 - 1 / (n + 1)) for a positive degree.