CoarseChildrenSimulation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EditApproximation.BinaryFraction.coarseBinaryChildren_rep line 10

Source documentation

Child arrays are reused exactly as in the shared rational evaluator. This composition lemma isolates the inductive recursive-call hypothesis.

 theorem coarseBinaryChildren_rep {B d : ℕ} {α : Type*} [DecidableEq α]
    (k q L : ℕ) (frame : List (Option α)) (two allowance : BinaryFraction)
    (children : List (CoarseSourceTree B α d × Fin B × CoarseThresholdDraws B d))
    (htwo : two.value = 2) (ha : allowance.representation.den = two.representation.den)
    (ht : ∀ draw : Fin B,
      (coarseChildThresholdWithWork B q allowance draw).1.value =
        coarseChildThreshold B q allowance.value draw)
    (hs : (coarseChildAllowanceWithWork q allowance).1.value = allowance.value / q)
    (he : ∀ child draw below, (child, draw, below) ∈ children → ∀ start,
      CoarseArrayRep (coarseBinaryEval k q L frame two child below
        (coarseChildAllowanceWithWork L (coarseChildThresholdWithWork B q allowance draw).1).1 start).1
        (coarseArrayEval k q (1 / L) frame child below
…

Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction.coarseChildThresholdWithWork, OAI.EditApproximation.BinaryFraction.value, OAI.EditApproximation.coarseChildThreshold, OAI.EditApproximation.BinaryFraction.coarseChildAllowanceWithWork, OAI.EditApproximation.BinaryFraction.CoarseArrayRep, OAI.EditApproximation.BinaryFraction.coarseBinaryEval, OAI.EditApproximation.coarseArrayEval