RejectionSpace.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.EditApproximation.rejectionStateCells line 11
Source documentation
The stream keeps the current word and one optional accepted value; failed words are overwritten and the failure count belongs only to the probability-space description, not to the machine state.
```
def rejectionStateCells (N bits : ℕ) (state : Option (Fin N)) (word : Fin (2 ^ bits)) : ℕ :=
…
```
theorem OAI.EditApproximation.rejectionStateCells_bound line 14
theorem OAI.EditApproximation.rejectionTransition_cells line 32
Source documentation
This bound holds after every transition, regardless of how many failed trials preceded it.
```
theorem rejectionTransition_cells (N bits : ℕ) (hN : N ≤ 2 ^ bits)
    (state : Option (Fin N)) (word nextWord : Fin (2 ^ bits)) :
    rejectionStateCells N bits (rejectionTransition N (2 ^ bits) state word) nextWord ≤ 2 * bits + 4 :=
…
```
Mentions: OAI.EditApproximation.rejectionStateCells, OAI.EditApproximation.rejectionTransition
theorem OAI.EditApproximation.computedFamilySampler_cells line 37