OAI/Combinatorics/EditApproximation/Geometry/RoundedGroupStates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Enumerating rounded endpoints with a length-gap guard costs only one wide coordinate and one envelope coordinate.

  1. theorem OAI.EditApproximation.gridGapStates_complete line 16
  2. theorem OAI.EditApproximation.gridGapStates_length_le line 32
  3. theorem OAI.EditApproximation.lengthGap_guard_distance line 44
  4. theorem OAI.EditApproximation.wide_firstEndpoint_near_cell line 60
  5. theorem OAI.EditApproximation.gridGapStates_rounded_count line 84

    Source documentation

    The spacing dominates h/K and one. This includes the spacing-one case for fractional envelopes. No success or accuracy event is needed.

    theorem gridGapStates_rounded_count (n g anchor sourceLength b : ℕ) (h K : ℚ)
    (hg : 0 < g) (hh : 0 < h) (hK : 1 ≤ K) (hspacing : h ≤ K * g) :
    ((gridGapStates n g anchor (12 * b) sourceLength ⌈2 * h⌉₊).length : ℚ) ≤
      208 * K ^ 2 * (1 + b / h) := by
…

    Mentions: OAI.EditApproximation.gridGapStates

  6. theorem OAI.EditApproximation.shared_rounded_inputs_bound line 124