OAI/Combinatorics/EditApproximation/Refinement/ComputedQueryRegisters.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.EditApproximation.ComputedQueryRegisters line 11

   Source documentation

   The remaining scalar premises of the concrete table dispatcher.

   structure ComputedQueryRegisters (N ny J : ℕ)
       (request : PhysicalTableRequest (integerParameters N).M J ny) : Prop where
   …

   Mentions: OAI.EditApproximation.PhysicalTableRequest, OAI.EditApproximation.integerParameters

2. theorem OAI.EditApproximation.computedQueryRegisters line 28

   Source documentation

   None of these register bounds assumes a successful random draw.

   theorem computedQueryRegisters (N ny J : ℕ) (hN : 0 < N)
       (hell : 2 ^ 1000 ≤ inputSmallLog N) (hny : ny ≤ N) (hJ : J ≤ inputHeight N)
       (request : PhysicalTableRequest (integerParameters N).M J ny)
       (hr : request.Bounded (computedSeedPassCount N + 1) (inputHeight N ^ 2)
         (integerParameters N).T (integerParameters N).S) : ComputedQueryRegisters N ny J request := by
   …

   Mentions: OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.inputHeight, OAI.EditApproximation.PhysicalTableRequest, OAI.EditApproximation.integerParameters, OAI.EditApproximation.computedSeedPassCount, OAI.EditApproximation.ComputedQueryRegisters