BinaryRoundedKernel.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Exact rounded canonical actions from their computed binary envelopes. Rounding spacing is obtained by a natural ceiling, since the dyadic product is either below one or an integer. No logarithm is evaluated.

theorem OAI.EditApproximation.interval_eq_of_endpoints line 19
theorem OAI.EditApproximation.roundStateWithWork_value line 30
Source documentation
A binary interval output, with its order/range proofs erased.
```
@[simp] theorem roundStateWithWork_value {n : ℕ} (spacing : ℕ) (hspacing : 0 < spacing)
    (q : TargetInterval n) : (roundStateWithWork spacing hspacing q).1 = roundInterval spacing q := by
…
```
Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.roundStateWithWork, OAI.EditApproximation.roundInterval
theorem OAI.EditApproximation.actionEqualWithWork_value line 38
theorem OAI.EditApproximation.actionMemberWithWork_value line 54
Source documentation
A literal membership scan, preserving the wide-list definition on inaccurate as well as accurate input seeds.
```
@[simp] theorem actionMemberWithWork_value {n M : ℕ} (a : Fin M → TargetInterval n)
    (actions : List (Fin M → TargetInterval n)) :
    (actionMemberWithWork a actions).1 = true ↔ a ∈ actions := by
…
```
Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.actionMemberWithWork
theorem OAI.EditApproximation.BinaryFraction.roundedSpacingWithWork_value line 66
theorem OAI.EditApproximation.BinaryFraction.roundedSpacingWithWork_pos line 71
theorem OAI.EditApproximation.BinaryFraction.roundedSpacingWithWork_band_value line 76
def OAI.EditApproximation.BinaryFraction.roundedBandWithWork line 85
theorem OAI.EditApproximation.BinaryFraction.roundedBandWithWork_value line 96

def OAI.EditApproximation.BinaryFraction.unskippedGuardWithWork line 107

Source documentation

All numerical acceptance tests after a nonempty band has been built.

def unskippedGuardWithWork {nx ny M : ℕ} (parent : TargetInterval nx) (_center : TargetInterval ny)
    (b thetaExponent : ℕ) (F : BinaryFraction) (band wide : List (Fin M → TargetInterval ny))
    (hne : band ≠ []) (initial : Fin M → TargetInterval ny → BinaryFraction) : Bool × ℕ :=
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.BinaryFraction

theorem OAI.EditApproximation.BinaryFraction.unskippedGuardWithWork_value line 126