OAI/Combinatorics/ParityLifts/FixedETH.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ParityWL.Complexity.rate_parameters line 7
2. theorem OAI.ParityWL.Complexity.fixed_dimension_eth line 55

   Source documentation

   Positive-rate ETH: one absolute slope and one threshold, uniform over both refinements and both histogram implementations.

   theorem fixed_dimension_eth : FixedDimensionETHStatement := by
   …

   Mentions: OAI.ParityWL.Complexity.FixedDimensionETHStatement