Choosing an integer moment order

Rounding a sqrt(u/log u) upward preserves the leading normalized cost a/2+t/a. Choosing a=sqrt(2t) gives the sharp coefficient sqrt(2t).

noncomputable def NairTenenbaum.momentOrderScale (a u : ℝ) : ℝ

The real scale used to select the Hooley moment order.

Equations

• NairTenenbaum.momentOrderScale a u = a * √(u / Real.log u)

noncomputable def NairTenenbaum.roundedMomentOrder (a u : ℝ) : ℕ

The integral moment order obtained by rounding the chosen scale.

Equations

• NairTenenbaum.roundedMomentOrder a u = ⌈NairTenenbaum.momentOrderScale a u⌉₊

theorem NairTenenbaum.tendsto_div_log_atTop : Filter.Tendsto (fun (u : ℝ) => u / Real.log u) Filter.atTop Filter.atTop

theorem NairTenenbaum.tendsto_momentOrderScale {a : ℝ} (ha : 0 < a) : Filter.Tendsto (momentOrderScale a) Filter.atTop Filter.atTop

theorem NairTenenbaum.tendsto_roundedMomentOrder {a : ℝ} (ha : 0 < a) : Filter.Tendsto (roundedMomentOrder a) Filter.atTop Filter.atTop

theorem NairTenenbaum.tendsto_roundedMomentOrder_div_scale {a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (u : ℝ) => ↑(roundedMomentOrder a u) / momentOrderScale a u) Filter.atTop (nhds 1)

theorem NairTenenbaum.momentOrderScale_pos {a u : ℝ} (ha : 0 < a) (hu : 1 < u) : 0 < momentOrderScale a u

theorem NairTenenbaum.momentOrderScale_log_identity {a u : ℝ} (hu : 1 < u) : momentOrderScale a u * Real.log u = a * √(u * Real.log u)

theorem NairTenenbaum.momentOrderScale_sqrt_identity {a u : ℝ} (hu : 1 < u) : momentOrderScale a u * √(u * Real.log u) = a * u

theorem NairTenenbaum.log_momentOrderScale {a u : ℝ} (ha : 0 < a) (hu : 1 < u) : Real.log (momentOrderScale a u) = Real.log a + (Real.log u - Real.log (Real.log u)) / 2

theorem NairTenenbaum.tendsto_log_roundedMomentOrder_div_log {a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (u : ℝ) => Real.log ↑(roundedMomentOrder a u) / Real.log u) Filter.atTop (nhds (1 / 2))

theorem NairTenenbaum.tendsto_momentOrderCost {a K t : ℝ} (ha : 0 < a) (hK : 0 < K) : Filter.Tendsto (fun (u : ℝ) => (↑(roundedMomentOrder a u) * Real.log (K * ↑(roundedMomentOrder a u)) + t * u / ↑(roundedMomentOrder a u)) / √(u * Real.log u)) Filter.atTop (nhds (a / 2 + t / a))

theorem NairTenenbaum.eventually_exists_momentOrderCost_le {K t η : ℝ} (hK : 0 < K) (ht : 0 < t) (hη : √(2 * t) < η) (N : ℕ) : ∀ᶠ (u : ℝ) in Filter.atTop, ∃ (q : ℕ), N ≤ q ∧ ↑q * Real.log (K * ↑q) + t * u / ↑q ≤ η * √(u * Real.log u)