OAI/Combinatorics/EditApproximation/Queries/QueryRoundedCounts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.groupRoundSpacing_endpoint_counts line 9

   Source documentation

   Every envelope queried by a shared group bounds both endpoint loops, including the fractional-envelope, unit-spacing case.

   theorem groupRoundSpacing_endpoint_counts (M b exponent : ℕ) (h : ℚ)
       (hM : 0 < M) (_hh : 0 ≤ h) (hfloor : (b : ℚ) / M ≤ h) :
       2 * (12 * b) / groupRoundSpacing exponent h + 2 ≤ 24 * 2 ^ exponent * M + 2 ∧
       2 * ⌈2 * h⌉₊ / groupRoundSpacing exponent h + 2 ≤ 4 * 2 ^ exponent + 4 := by
   …

   Mentions: OAI.EditApproximation.groupRoundSpacing