ComputedQueryMemo.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EditApproximation.computed_small_word_pos line 11
theorem OAI.EditApproximation.computedQueryBase_value line 20
Source documentation
The same materialized binary constants are shared by all requests of a pass.
```
theorem computedQueryBase_value (N : ℕ) :
    bitWordValue (computedQueryBase N) = inputSmallLog N ^ 10 + 1 := by
…
```
Mentions: OAI.EditApproximation.bitWordValue, OAI.EditApproximation.computedQueryBase, OAI.EditApproximation.inputSmallLog
theorem OAI.EditApproximation.computedQueryBase_pos line 24
def OAI.EditApproximation.computedQueryMemoRaw line 34
Source documentation
Coarse words here are the stored outputs of the separately charged coarse initializer. The adaptive mixed memo consumes them on demand.
```
def computedQueryMemoRaw (source target : List ℕ) (N : ℕ)
    (occurrence : BinaryMemo PositionCounts) (symbolBits positionBits : ℕ)
    (input : ComputedFamilyInput source target N) (key : ComputedFamilyMemoKey source target N) :=
…
```
Mentions: OAI.EditApproximation.BinaryMemo, OAI.EditApproximation.PositionCounts, OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.ComputedFamilyMemoKey
def OAI.EditApproximation.computedQueryMemoNormalized line 47