OAI/Combinatorics/EditApproximation/Refinement/ComputedPreparedInputBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.precision_power_bound line 10
2. theorem OAI.EditApproximation.prepared_loop_caps line 12
3. theorem OAI.EditApproximation.computedPreparedNumericBounds line 48

   Source documentation

   Every numeric premise of the prepared kernel follows from the computed parameters. Width assumptions here concern only the five actual parameter words; cached data are added by physicalPreparedStep_inputBounds.

   theorem computedPreparedNumericBounds :
       ∀ᶠ N : ℕ in atTop, ∀ nx ny : ℕ, nx + ny ≤ N → ∀ t : ℕ, t ≤ inputHeight N ^ 2 →
         ∀ tau a eta kappa delta : BinaryFraction,
         tau.width ≤ inputHeight N ^ 8 → a.width ≤ inputHeight N ^ 8 →
         eta.width ≤ inputHeight N ^ 8 → kappa.width ≤ inputHeight N ^ 8 →
         delta.width ≤ inputHeight N ^ 8 → |eta.value| ≤ ((inputHeight N ^ 5 : ℕ) : ℚ) →
         (0 ≤ kappa.value ∧ kappa.value ≤ 1) →
         ∀ integer : ℕ → TargetInterval ny → ℕ,
         (∀ b r, Nat.size (integer b r) ≤ inputHeight N) →
         BinaryFraction.PreparedKernelNumericBounds (nx := nx) (M := (integerParameters N).M)
   …

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