OAI/Combinatorics/EditApproximation/Queries/QueryOnlineSources.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An online random-source range is computed from the gathered mass words before the source is requested. Band construction, dimension, eighty-fold power, and triangular mass are all charged.

  1. theorem OAI.EditApproximation.BinaryFraction.queryOnlineRangeWithWork_value line 18
  2. theorem OAI.EditApproximation.queryOnlineSourceGather_refines line 37