CoarseIndexedCompare.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.EditApproximation.BinaryFraction.coarseIndexAdditionalWork line 8

theorem OAI.EditApproximation.BinaryFraction.coarseIndexChildren_value_congr line 18

Source documentation

Local arithmetic depends only on returned arrays, so replacing a child by a representation-equivalent implementation preserves every parent array.

theorem coarseIndexChildren_value_congr {B : ℕ} (k q L : ℕ) (two : BinaryFraction)
    (width : Fin B → ℕ) (draw : Fin B → Fin B)
    (evaluate other : Fin B → BinaryFraction → ℕ → CoarseBinaryArray × ℕ)
    (he : ∀ i a start, (evaluate i a start).1 = (other i a start).1)
    (allowance : BinaryFraction) (indices : List (Fin B)) (start : ℕ) :
    (coarseIndexChildren k q L two width evaluate draw allowance indices start).1 =
      (coarseIndexChildren k q L two width other draw allowance indices start).1 := by
…

Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.width, OAI.EditApproximation.BinaryFraction.CoarseBinaryArray, OAI.EditApproximation.BinaryFraction.coarseIndexChildren

theorem OAI.EditApproximation.BinaryFraction.coarseIndexChildren_cost_compare line 32

Source documentation

Extra costs compose along the same child traversal; no child arithmetic or array allocation is charged twice by this comparison.

theorem coarseIndexChildren_cost_compare {B : ℕ} (k q L : ℕ) (two : BinaryFraction)
    (width : Fin B → ℕ) (draw : Fin B → Fin B)
    (evaluate other : Fin B → BinaryFraction → ℕ → CoarseBinaryArray × ℕ)
    (extra : Fin B → BinaryFraction → ℕ → ℕ)
    (he : ∀ i a start, (evaluate i a start).1 = (other i a start).1)
    (hc : ∀ i a start, (evaluate i a start).2 ≤ (other i a start).2 + extra i a start)
    (allowance : BinaryFraction) (indices : List (Fin B)) (start : ℕ) :
    (coarseIndexChildren k q L two width evaluate draw allowance indices start).2 ≤
      (coarseIndexChildren k q L two width other draw allowance indices start).2 +
        coarseIndexAdditionalWork q L width draw extra allowance indices start := by
…

theorem OAI.EditApproximation.BinaryFraction.arithmeticMapWithWork_add_cost line 58