# Documentation

Mathlib.Data.BinaryHeap

structure BinaryHeap (α : Type u_1) (lt : ααBool) :
Type u_1
• arr :

A max-heap data structure.

Instances For
def BinaryHeap.heapifyDown {α : Type u_1} (lt : ααBool) (a : ) (i : Fin ()) :
{ a' // }

Core operation for binary heaps, expressed directly on arrays. Given an array which is a max-heap, push item i down to restore the max-heap property.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem BinaryHeap.size_heapifyDown {α : Type u_1} (lt : ααBool) (a : ) (i : Fin ()) :
Array.size ↑() =
def BinaryHeap.mkHeap {α : Type u_1} (lt : ααBool) (a : ) :
{ a' // }

Core operation for binary heaps, expressed directly on arrays. Construct a heap from an unsorted array, by heapifying all the elements.

Equations
def BinaryHeap.mkHeap.loop {α : Type u_1} (lt : ααBool) (i : ) (a : ) :
i { a' // }
Equations
• One or more equations did not get rendered due to their size.
• BinaryHeap.mkHeap.loop lt 0 x x_1 = { val := x, property := (_ : ) }
@[simp]
theorem BinaryHeap.size_mkHeap {α : Type u_1} (lt : ααBool) (a : ) :
Array.size ↑() =
def BinaryHeap.heapifyUp {α : Type u_1} (lt : ααBool) (a : ) (i : Fin ()) :
{ a' // }

Core operation for binary heaps, expressed directly on arrays. Given an array which is a max-heap, push item i up to restore the max-heap property.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem BinaryHeap.size_heapifyUp {α : Type u_1} (lt : ααBool) (a : ) (i : Fin ()) :
Array.size ↑() =
def BinaryHeap.empty {α : Type u_1} (lt : ααBool) :

O(1). Build a new empty heap.

Equations
• = { arr := #[] }
instance BinaryHeap.instInhabitedBinaryHeap {α : Type u_1} (lt : ααBool) :
Equations
• = { default := }
instance BinaryHeap.instEmptyCollectionBinaryHeap {α : Type u_1} (lt : ααBool) :
Equations
• = { emptyCollection := }
def BinaryHeap.singleton {α : Type u_1} (lt : ααBool) (x : α) :

O(1). Build a one-element heap.

Equations
• = { arr := #[x] }
def BinaryHeap.size {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) :

O(1). Get the number of elements in a BinaryHeap.

Equations
def BinaryHeap.get {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) (i : Fin (BinaryHeap.size self)) :
α

O(1). Get an element in the heap by index.

Equations
def BinaryHeap.insert {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) (x : α) :

O(log n). Insert an element into a BinaryHeap, preserving the max-heap property.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem BinaryHeap.size_insert {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) (x : α) :
def BinaryHeap.max {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) :

O(1). Get the maximum element in a BinaryHeap.

Equations
def BinaryHeap.popMaxAux {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) :
{ a' // = BinaryHeap.size self - 1 }

Auxiliary for popMax.

Equations
• One or more equations did not get rendered due to their size.
def BinaryHeap.popMax {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) :

O(log n). Remove the maximum element from a BinaryHeap. Call max first to actually retrieve the maximum element.

Equations
• = ↑()
@[simp]
theorem BinaryHeap.size_popMax {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) :
def BinaryHeap.extractMax {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) :
× BinaryHeap α lt

O(log n). Return and remove the maximum element from a BinaryHeap.

Equations
theorem BinaryHeap.size_pos_of_max {α : Type u_1} {x : α} {lt : ααBool} {self : BinaryHeap α lt} (e : BinaryHeap.max self = some x) :
def BinaryHeap.insertExtractMax {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) (x : α) :
α × BinaryHeap α lt

O(log n). Equivalent to extractMax (self.insert x), except that extraction cannot fail.

Equations
• One or more equations did not get rendered due to their size.
def BinaryHeap.replaceMax {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) (x : α) :
× BinaryHeap α lt

O(log n). Equivalent to (self.max, self.popMax.insert x).

Equations
• One or more equations did not get rendered due to their size.
def BinaryHeap.decreaseKey {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) (i : Fin (BinaryHeap.size self)) (x : α) :

O(log n). Replace the value at index i by x. Assumes that x ≤ self.get i≤ self.get i.

Equations
def BinaryHeap.increaseKey {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) (i : Fin (BinaryHeap.size self)) (x : α) :

O(log n). Replace the value at index i by x. Assumes that self.get i ≤ x≤ x.

Equations
def Array.toBinaryHeap {α : Type u_1} (lt : ααBool) (a : ) :

O(n). Convert an unsorted array to a BinaryHeap.

Equations
• = { arr := ↑() }
@[specialize #[]]
def Array.heapSort {α : Type u_1} (a : ) (lt : ααBool) :

O(n log n). Sort an array using a BinaryHeap.

Equations
def Array.heapSort.loop {α : Type u_1} (lt : ααBool) (a : BinaryHeap α fun y x => lt x y) (out : ) :
Equations
• One or more equations did not get rendered due to their size.