Factors below √(log n)

Bounds on the scale n / √⌊log₂ n⌋ that compare it with n, behind the separations of the counting simulation at time T · h (#1833). The divisor √⌊log₂ n⌋ tends to infinity (Nat.tendsto_sqrt_log_two_atTop), so the scale is o(n): every multiple C * n is eventually at most n * √⌊log₂ n⌋ (Nat.eventually_mul_le_mul_sqrt_log_two).

Multiplying a by a factor b ≥ 1 keeps its scale below a / C as long as C * b ≤ √⌊log₂ a⌋ (Nat.mul_mul_le_mul_sqrt_log_two_mul). The fourth root ⌊√⌊√⌊log₂ n⌋⌋⌋ of the logarithm is such a factor for every C from some n on (Nat.eventually_mul_sqrt_sqrt_log_two_le), and it is positive from n = 2 on (Nat.one_le_sqrt_sqrt_log_two).

Main results

• Nat.tendsto_sqrt_log_two_atTop: √⌊log₂ n⌋ tends to infinity.
• Nat.eventually_mul_le_mul_sqrt_log_two: C * n ≤ n * √⌊log₂ n⌋ eventually.
• Nat.mul_mul_le_mul_sqrt_log_two_mul: C * b ≤ √⌊log₂ a⌋ and 1 ≤ b give C * (a * b) ≤ a * √⌊log₂ (a * b)⌋.
• Nat.eventually_mul_sqrt_sqrt_log_two_le: C * ⌊√⌊√⌊log₂ n⌋⌋⌋ ≤ √⌊log₂ n⌋ eventually.

theorem Nat.tendsto_sqrt_log_two_atTop : Filter.Tendsto (fun (n : ℕ) => (log 2 n).sqrt) Filter.atTop Filter.atTop

The divisor √⌊log₂ n⌋ tends to infinity.

theorem Nat.eventually_mul_le_mul_sqrt_log_two (C : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, C * n ≤ n * (log 2 n).sqrt

The scale n / √⌊log₂ n⌋ is o(n): every multiple C * n is eventually at most n * √⌊log₂ n⌋.

theorem Nat.mul_mul_le_mul_sqrt_log_two_mul {C a b : ℕ} (hb : 1 ≤ b) (h : C * b ≤ (log 2 a).sqrt) : C * (a * b) ≤ a * (log 2 (a * b)).sqrt

A factor below √⌊log₂ a⌋ / C: if b ≥ 1 and C * b ≤ √⌊log₂ a⌋, then C * (a * b) ≤ a * √⌊log₂ (a * b)⌋, so the scale of a * b is at most a / C.

theorem Nat.one_le_sqrt_sqrt_log_two {n : ℕ} (hn : 2 ≤ n) : 1 ≤ (log 2 n).sqrt.sqrt

The fourth root ⌊√⌊√⌊log₂ n⌋⌋⌋ of the logarithm is positive from n = 2 on.

theorem Nat.eventually_mul_sqrt_sqrt_log_two_le (C : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, C * (log 2 n).sqrt.sqrt ≤ (log 2 n).sqrt

The fourth root of the logarithm is o(√log): every multiple of ⌊√⌊√⌊log₂ n⌋⌋⌋ is eventually at most √⌊log₂ n⌋.