The scale n / √(log n)

Natural-number estimates for the scale n / Nat.sqrt (Nat.log 2 n), that is ⌊n / ⌊√⌊log₂ n⌋⌋⌋, in which the deterministic simulations of nondeterministic and probabilistic time by blocking and tensor contraction are stated (#1833). From n = 2 on the divisor is positive (Nat.one_le_sqrt_log_two), and so is the scale (Nat.one_le_div_sqrt_log_two).

The scale dominates the logarithm (Nat.log_two_le_div_sqrt_log_two), hence every polynomial in the exponent, and the number ⌈n / ⌈log₂ (n + 2)⌉⌉ of time blocks of length ⌈log₂ (n + 2)⌉ (Nat.ceilDiv_clog_two_le). Scaling n by a constant scales it by at most that constant, up to an additive constant (Nat.mul_div_sqrt_log_two_le). The scale is not monotone, since the divisor jumps, but it is monotone up to constants (Nat.div_sqrt_log_two_le_of_le), so a bound in a smaller size, such as the number of edges of a network, transfers to the clock. Together these give the exponent arithmetic of the simulation: for t = c * T, with q = ⌈t / ⌈log₂ (t + 2)⌉⌉ blocks, the cost 3 ^ (K * q) * (t + 1) ^ d * 2 ^ (e * t / √⌊log₂ t⌋) of enumerating the movement schedules, building the networks and contracting them is 2 ^ O(T / √⌊log₂ T⌋) (Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two).

The floors cost only constant factors: the natural scale is between the real scale n / √(log₂ n) minus one and three times it, which is checked in the test suite.

Main results

• Nat.log_two_le_div_sqrt_log_two: ⌊log₂ n⌋ ≤ n / √⌊log₂ n⌋.
• Nat.sqrt_log_two_le_sqrt_clog_two_sub_one_add_one: ⌊√⌊log₂ n⌋⌋ ≤ ⌊√(⌈log₂ n⌉ - 1)⌋ + 1, which is ⌈√⌈log₂ n⌉⌉ for n ≥ 2.
• Nat.ceilDiv_clog_two_le: ⌈n / ⌈log₂ (n + 2)⌉⌉ ≤ n / √⌊log₂ n⌋ + 1.
• Nat.mul_div_sqrt_log_two_le: the scale of c * n is at most c times that of n, plus c.
• Nat.div_sqrt_log_two_le_of_le: the scale is monotone up to constants.
• Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two: the cost of the counting simulation.
• Nat.mul_two_pow_add_le_two_pow, Nat.mul_two_pow_div_sqrt_log_two_add_le, Nat.mul_add_one_pow_add_le_pow: absorbing constants into exponential and polynomial bounds.

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

The divisor √⌊log₂ n⌋ is positive from n = 2 on.

theorem Nat.sqrt_log_two_mono : Monotone fun (n : ℕ) => (log 2 n).sqrt

The divisor √⌊log₂ n⌋ is monotone.

theorem Nat.sqrt_log_two_le_sqrt_clog_two_sub_one_add_one (n : ℕ) : (log 2 n).sqrt ≤ (clog 2 n - 1).sqrt + 1

⌊√⌊log₂ n⌋⌋ ≤ ⌊√(⌈log₂ n⌉ - 1)⌋ + 1, with truncated subtraction. The right-hand side is ⌈√⌈log₂ n⌉⌉ for n ≥ 2 and is 1 for n ≤ 1, so from n = 2 on the divisor of the scale is at most the ceiling convention for the square root of the ceiling logarithm.

theorem Nat.log_two_mul_sqrt_log_two_le (n : ℕ) : log 2 n * (log 2 n).sqrt ≤ n

⌊log₂ n⌋ * √⌊log₂ n⌋ ≤ n: with L = ⌊log₂ n⌋, (L √L) ^ 2 ≤ L ^ 3 ≤ 4 ^ L ≤ n ^ 2.

theorem Nat.log_two_le_div_sqrt_log_two (n : ℕ) : log 2 n ≤ n / (log 2 n).sqrt

The scale dominates the logarithm: ⌊log₂ n⌋ ≤ n / √⌊log₂ n⌋.

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

The scale is positive from n = 2 on.

theorem Nat.ceilDiv_clog_two_le (n : ℕ) : n ⌈/⌉ clog 2 (n + 2) ≤ n / (log 2 n).sqrt + 1

Time blocks. There are at most n / √⌊log₂ n⌋ + 1 blocks of length ⌈log₂ (n + 2)⌉ in n steps, since √⌊log₂ n⌋ ≤ ⌈log₂ (n + 2)⌉.

theorem Nat.mul_div_le_mul_div_add (c n r : ℕ) : c * n / r ≤ c * (n / r) + c

Multiplying before dividing gains less than the multiplier: c * n / r ≤ c * (n / r) + c.

theorem Nat.mul_div_sqrt_log_two_le (c n : ℕ) : c * n / (log 2 (c * n)).sqrt ≤ c * (n / (log 2 n).sqrt) + c

Scaling. The scale of c * n is at most c times the scale of n, plus c: the divisor only grows.

theorem Nat.div_sqrt_log_two_le_of_le {m n : ℕ} (h : m ≤ n) : m / (log 2 m).sqrt ≤ 2 * (n / (log 2 n).sqrt) + 2

The scale is monotone up to constants: m ≤ n gives m / √⌊log₂ m⌋ ≤ 2 * (n / √⌊log₂ n⌋) + 2. When the divisors are within a factor 2 of each other this is division by the smaller divisor; otherwise m is so much smaller than n that m * √⌊log₂ n⌋ ≤ n.

theorem Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two (K c d e : ℕ) : ∃ (C : ℕ), ∀ (T : ℕ), 2 ≤ T → 3 ^ (K * (c * T ⌈/⌉ clog 2 (c * T + 2))) * (c * T + 1) ^ d * 2 ^ (e * (c * T) / (log 2 (c * T)).sqrt) ≤ 2 ^ (C * T / (log 2 T).sqrt)

The cost of the counting simulation is 2 ^ O(T / √(log T)) (#1833). For t = c * T, time blocks of length b = ⌈log₂ (t + 2)⌉ and q = ⌈t / b⌉ blocks, the number 3 ^ (K * q) of movement schedules of K heads, a polynomial (t + 1) ^ d and a contraction cost 2 ^ (e * t / √⌊log₂ t⌋) multiply to at most 2 ^ (C * T / √⌊log₂ T⌋) from T = 2 on, for a constant C depending only on K, c, d and e.

theorem Nat.mul_two_pow_add_le_two_pow {a b c x : ℕ} (hx : 1 ≤ x) : a * 2 ^ (c * x) + b ≤ 2 ^ ((a + b + c) * x)

A constant factor and an additive constant are absorbed by a positive exponent: a * 2 ^ (c * x) + b ≤ 2 ^ ((a + b + c) * x) for 1 ≤ x.

theorem Nat.mul_two_pow_div_sqrt_log_two_add_le {a b C T : ℕ} (hT : 2 ≤ T) : a * 2 ^ (C * T / (log 2 T).sqrt) + b ≤ 2 ^ ((a + b + 1) * (C + 1) * T / (log 2 T).sqrt)

A constant factor and an additive constant are absorbed into the constant of 2 ^ O(T / √⌊log₂ T⌋) from T = 2 on.

theorem Nat.mul_add_one_pow_add_le_pow {a b d n : ℕ} (hn : 2 ≤ n) : a * (n + 1) ^ d + b ≤ n ^ (a + b + 2 * d)

A constant factor and an additive constant are absorbed by the degree from n = 2 on: a * (n + 1) ^ d + b ≤ n ^ (a + b + 2 * d).