ComputedQueryCorrect.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EditApproximation.computedQueryParameters_values line 10
def OAI.EditApproximation.computedQueryReference line 19
theorem OAI.EditApproximation.computedQueryMemoNormalized_correct line 33

theorem OAI.EditApproximation.computedQueryMemoNormalized_width_bound line 73

Source documentation

Width of the actual stored word.

theorem computedQueryMemoNormalized_width_bound (source target : List ℕ) (N : ℕ)
    (occurrence : BinaryMemo PositionCounts) (symbolBits positionBits : ℕ)
    (input : ComputedFamilyInput source target N) (hf : 3 ≤ smallLogExponent N)
    (hs : ∀ z ∈ source, z < 2 ^ symbolBits) (ht : ∀ z ∈ target, z < 2 ^ symbolBits)
    (hp : target.length ≤ 2 ^ positionBits)
    (htable : occurrence = occurrenceBuild symbolBits positionBits target.zipIdx)
    (key : ComputedFamilyMemoKey source target N) (V : ℕ)
    (hV : |computedFamilyExpectedValue source target N input key| ≤ (V : ℚ)) :
    (rankedBitProgramValue (SourceRanked.rank ChargedPhysicalRequest.rank)
      (computedQueryMemoNormalized source target N occurrence symbolBits positionBits input) key).width ≤
      Nat.size V + 2 * (queryFamilyMemoRemaining target N (integerParameters N).P (inputSmallLog N)
        (40 * smallLogExponent N) (inputHeight N) (inputSmallLog N ^ 80) key *
…