OAI/NumberTheory/Ostmann/Arithmetic/MovingCellChoice.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.integer_cell_center_avoiding line 12

   Source documentation

   At most card D failures move an integer center by at most card D + 1. This one-sided choice also preserves every lower endpoint target.

   theorem integer_cell_center_avoiding (D : Finset ℤ) (T : ℝ) :
       ∃ c : ℤ, c ∉ D ∧ T ≤ (c : ℝ) ∧ (c : ℝ) ≤ T + D.card + 1 := by
   …

2. theorem OAI.Ostmann.nat_cell_center_avoiding line 37
3. theorem OAI.Ostmann.compensation_cell_center_avoiding line 60
4. theorem OAI.Ostmann.protected_cell_center_avoiding line 68

   Source documentation

   All six protected top slots may use one good cell; the resulting error is upward and does not weaken the protected lower bound.

   theorem protected_cell_center_avoiding (D : Finset ℤ) (J cb : ℝ) :
       ∃ c : ℤ, c ∉ D ∧ J ≤ 6 * (c : ℝ) + cb ∧
         6 * ((c : ℝ) + 1) + cb ≤ J + 6 * (D.card + 2) := by
   …