OAI/Combinatorics/EditApproximation/Queries/QueryGroupSources.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Complete scalar-source key generation uses the original dyadic query window, cell order, scale order, and sample order.

  1. theorem OAI.EditApproximation.BinaryFraction.queryGroupSourceKeysWithWork_value line 16
  2. theorem OAI.EditApproximation.queryGroupSourceGather_refines line 33