OAI/Combinatorics/ParityLifts/UniformETH.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ParityWL.Complexity.uniform_eth line 9

   Source documentation

   Uniform exclusion under the weaker, single-machine subexponential hypothesis; no positive forbidden rate and no convergence modulus are assumed.

   theorem uniform_eth : UniformETHStatement := by
   …

   Mentions: OAI.ParityWL.Complexity.UniformETHStatement