OAI/Combinatorics/EditApproximation/Geometry/DomainExponential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exponential form of the actual domain bound used in amplification.

  1. theorem OAI.EditApproximation.computed_labeledStateCount_exp line 9