Master Theorem

Stream: Is there code for X?

[Andrew Carter]

Is there a proof of the math part of the master theorem (https://en.wikipedia.org/wiki/Master_theorem_(analysis_of_algorithms))?
The semantic search (http://mathlib-search.edayers.com/?query=master+theorem) seems to have turned up

theorem master_theorem {a b c : ℕ} (h : a ≥ 1) (h₁ : b > 1) (h₂ : c ≥ 0)
  (h₃ : a * b ^ c ≤ b ^ (c + 1)) : ∃ (k : ℕ), a = b ^ k

which might be equivalent (its got the right sort of feel to it except it deals in powers instead of logs - also I'm not quite sure how the extra log components are handled when f(n) is close to n^ccrit), but I also can't figure out where that is defined in mathlib (I resorted to grep and still couldn't find it).

[Eric Wieser]

Note that that generated theorem is false witha=2, b=3, c=1

[Eric Wieser]

So I think the answer is "that doesn't exist in mathlib, it was generated by the language model"

[Andrew Carter]

Well that makes me feel better about not finding it even with grep. Although is the answer in general the master theorem (or some variant thereof doesn't exist?) I feel like some forms of it almost feel trivial. For example the critical definition could look something like:

(∃ c < a, θ(f) ≤ θ(c^n)) → θ(∑ i : fin n, f(n-i) * a^i) = θ(a^n)
θ(f) = θ(a^n) → θ(∑ i : fin n, f(n-i) * a^i) = θ(n a^n)

Which is just saying that in the first case the first term dominates, and in the second case they all contribute equally.

[Eric Wieser]

Can you write those statements as full #mwe s, where you define the types and quantifiers for all the variables

[Andrew Carter]

The problem is I don't think I understand asymptotic filters enough to be able to write it I think, but I think I can write the exists form.

[Andrew Carter]

Ok, I could be wrong, but I think it would look something like (assuming we are sticking to the power version):

open_locale big_operators
theorem master_theorem_leaf_heavy (f: ℕ → ℕ) (a n: ℕ) (ha_pos: 0 < a):
  (∃ (c < a) k, ∀ i, f i ≤ k * c ^ i) → ∃ k, (∑ i : fin n.succ, f (n - i) * a ^ (i:ℕ)) ≤ k * a ^ n := sorry

theorem master_theorem_critical (f: ℕ → ℕ) (a n: ℕ) (ha_pos: 0 < a):
  (∃ k, ∀ i, f i ≤ k * a ^ i) → ∃ k, (∑ i : fin n.succ, f (n - i) * a ^ (i:ℕ)) ≤ k * n * a ^ n := sorry

I'm not sure about the root heavy case since I'm not exactly sure how the regularity condition translates.

[Andrew Carter]

But I'm not quite sure what the nicest form of the Master Theorem would look like from a mathematical perspective (CS likes to think about it from a divide and conquer perspective, which might not be preferrable in most other situations).

[Martin Dvořák]

I suspect your quantification ∃ (c < a), something(c) means ∃ c : ℕ, c + 1 ≤ a ∧ something(c) which is not what you wanted probably.

[Andrew Carter]

It is what I want, but actually I think I might need to be in ℝ instead (or at least ℚ). Basically there needs to be some separation in the exponent rather than just a polynomial factor.

[Andrew Carter]

Without actually dipping into Q I can fake it with

theorem master_theorem_leaf_heavy (f: ℕ → ℕ) (a n: ℕ) (ha_pos: 0 < a):
  (∃ cn cd k, cn ≤ a * cd ∧ ∀ i, f i ≤ k * cn ^ i / cd ^ i) → ∃ k, (∑ i : fin n.succ, f (n - i) * a ^ (i:ℕ)) ≤ k * a ^ n := sorry

[Martin Dvořák]

Interesting...
Are you reïmplementing rationals in order to be sure that negative numbers cannot appear there?
Do you want to have an explicit encoding of c for the sake of using it as a number in your computations later?

[Andrew Carter]

At the moment I'm not doing anything, I was hoping there was a form that already existed so I can just head towards that, right now I just have:

def divide_and_conquer_cost (p: program α) (fc: ℕ → ℕ): ℕ → ℕ
| 0 := internal_cost_bound p + fc 0
| (n+1) := internal_cost_bound p + fc (n + 1) + divide_and_conquer_cost n * recurse_count p

this is essentially the above sum

(∑ i : fin n.succ, f (n - i) * a ^ (i:ℕ))

except in a slightly different form.

a =  recurse_count p
``` and
```lean
f(i) = fc(i) + internal_cost_bound p

where p is held constant so the functions are constants.

And I've shown

theorem divide_and_conquer_cost_sound {p: program α}
  {fr: bank α → ℕ} (hfr: ∀ inp arg, recurse_arg p inp arg → fr arg < fr inp)
  {fc: ℕ → ℕ} (hfc: ∀ inp, call_cost_le ⟨p, p, inp⟩ (fc (fr inp))):
  ∀ inp, p.cost_le inp (divide_and_conquer_cost p fc (fr inp))

So basically all the computational complexity work is done as far as the model goes, and the only thing left is the asymptotics.

[Martin Dvořák]

If asymptotics is the only thing left, you should celebrate!

[Andrew Carter]

I am pretty happy, the proofs a very ugly though