OAI/Combinatorics/EditApproximation/Geometry/LocalCells.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Direct bounded-range enumeration of the cells meeting a query square.

  1. theorem OAI.EditApproximation.localCellCoordinates_complete line 13
  2. theorem OAI.EditApproximation.localCellCoordinates_length_le line 25
  3. theorem OAI.EditApproximation.localTargetCells_complete line 52
  4. theorem OAI.EditApproximation.localTargetCells_length_le line 60
  5. theorem OAI.EditApproximation.localTargetCells_query_length line 72

    Source documentation

    Every retained query scale has only polynomially many nearby cells, even when the initial seed is inaccurate.

    theorem localTargetCells_query_length {n : ℕ} (F b exponent : ℕ)
    (q : TargetInterval n) (w : ℚ) (hF : 1 ≤ F) (hb : 1 ≤ b)
    (hw : 0 ≤ w) (hwindow : w / (16 * F) ≤ b) :
    (localTargetCells ((2 : ℚ) ^ (-(exponent : ℤ)) * b) ⌈w⌉₊ q).length ≤
      ((32 * F + 2) * 2 ^ exponent + 2) ^ 2 := by
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.localTargetCells