Polynomial-time numbers and tests — division, powers and logarithms

The arithmetic behind the division, power and logarithm rules of Complexitylib.Classes.P.Unary. Each of those functions is computed as a count of the indices below a bound at which a comparison holds, or, for a capped power, as a loop; the identities here say that the count or the loop gives the intended value.

Contents

• card_filter_range_of_iff — a count of the indices below a mark
• div_eq_card_filter_range — division as a count
• min_mul_iterate — capped multiplication, iterated, is a capped power
• size_eq_card_filter_range, clog_eq_card_filter_range, log_eq_card_filter_range — binary length and logarithms as counts

theorem Complexity.card_filter_range_of_iff {n m : ℕ} (hm : m ≤ n) (p : ℕ → Prop) [DecidablePred p] (h : ∀ i < n, p i ↔ i < m) : (Finset.filter p (Finset.range n)).card = m

If a test holds at exactly the indices below m ≤ n, then m of the indices below n pass it.

theorem Complexity.div_eq_card_filter_range (a b : ℕ) : a / b = {i ∈ Finset.range a | 0 < b ∧ (i + 1) * b ≤ a}.card

Division as a count: a / b is the number of i < a with (i + 1) * b ≤ a, or 0 when b = 0.

theorem Complexity.min_mul_iterate (b c j : ℕ) : (fun (x : ℕ) => min (b * x) c)^[j] (min 1 c) = min (b ^ j) c

Multiplying by b and capping at c, j times from min 1 c, gives the capped power min (b ^ j) c.

theorem Complexity.size_eq_card_filter_range (n : ℕ) : n.size = {i ∈ Finset.range n | min (2 ^ i) (n + 1) ≤ n}.card

Binary length as a count: Nat.size n is the number of i < n with 2 ^ i ≤ n, the power capped at n + 1.

theorem Complexity.clog_eq_card_filter_range (b n : ℕ) : Nat.clog b n = {i ∈ Finset.range n | 1 < b ∧ min (b ^ i) n < n}.card

The ceiling logarithm as a count: for 1 < b, Nat.clog b n is the number of i < n with b ^ i < n, the power capped at n; and it is 0 otherwise.

theorem Complexity.log_eq_card_filter_range (b n : ℕ) : Nat.log b n = {i ∈ Finset.range n | 1 < b ∧ min (b ^ (i + 1)) (n + 1) ≤ n}.card

The floor logarithm as a count: for 1 < b, Nat.log b n is the number of i < n with b ^ (i + 1) ≤ n, the power capped at n + 1; and it is 0 otherwise.