OAI/Combinatorics/EditApproximation/Queries/QueryNumericInteger.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.PreparedKernelNumericBounds.with_integer line 8

   Source documentation

   Changing the sampled integers changes only their explicit width premise.

   theorem PreparedKernelNumericBounds.with_integer {nx ny M : ℕ}
       {N P F exponent H Q eM eF B E S t : ℕ}
       {tau a eta kappa delta : BinaryFraction} {integer : ℕ → TargetInterval ny → ℕ}
       (hn : PreparedKernelNumericBounds (nx := nx) (M := M)
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.BinaryFraction.PreparedKernelNumericBounds