Bottom-up heap construction costs

TheoremCost bound for one adjacent merging pass#✓fully proved

One adjacent pass costs at most the number of pairs times the merge bound.

theorem fdsa_chap15_ex02
    (Itree : α → Prop) (sz : α → ℕ)
    (Tmerge : α → α → ℕ)
    (ts : List α) (n : ℕ)
    (hItree : ∀ t ∈ ts, Itree t)
    (hsize : ∀ t ∈ ts, sz t = n)
    (hTmerge_bound : ∀ t1 t2, Itree t1 → Itree t2 → sz t1 = n → sz t2 = n → Tmerge t1 t2 ≤
        mergeCostBound n) :
    mergeAdjacentCost Tmerge ts ≤ (ts.length / 2) * mergeCostBound n

Used by 1

Used byMulti-pass cost bound for equally sized heaps

TheoremMulti-pass cost bound for equally sized heaps#✓fully proved

The multi-pass cost bound (15.2) for equally sized heaps.

theorem fdsa_chap15_ex01
    (Itree : α → Prop) (sz : α → ℕ)
    (merge : α → α → α) (Tmerge : α → α → ℕ)
    (ts : List α) (n k : ℕ)
    (hItree : ∀ t ∈ ts, Itree t)
    (hsize : ∀ t ∈ ts, sz t = n)
    (hlen : ts.length = 2 ^ k)
    (hmerge_size : ∀ a b, sz (merge a b) = sz a + sz b)
    (hmerge_Itree : ∀ a b, Itree a → Itree b → Itree (merge a b))
    (hTmerge_bound : ∀ a b m, Itree a → Itree b → sz a = m → sz b = m → Tmerge a b ≤
        mergeCostBound m) :
    mergeAllCost merge Tmerge ts ≤ ∑ i ∈ Finset.Icc 1 k, 2 ^ (k - i) * mergeCostBound (2 ^ (i -
        1) * n)

Uses 1

Proof usesCost bound for one adjacent merging pass

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.