OAI/NumberTheory/Ostmann/Arithmetic/MovingCellGap.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.spectatorStepGap_sub_one line 11
2. theorem OAI.Ostmann.moving_cell_diagonal_gap line 18

   Source documentation

   J + tail is the protected and surviving compensation target in (7.4). The two cell errors are paid by one unit of the coefficient of the step gap.

   theorem moving_cell_diagonal_gap (BD Bz z r m J tail w b cb small cg ec es : ℝ)
       (hr : 0 ≤ r)
       (hbalance : r * w = r * (J + tail) - spectatorStepGap BD Bz z r m)
       (hupper : 4 * b ≤ w + ec)
       (hlower : r * (J + tail) - es * r ≤ small + r * (cb - 1))
       (hcost : 2 * cg + 1 + (ec + es) * r ≤ r * m) :
       2 * cg + 1 + (r * 4) * b - (small + r * (cb - 1)) ≤
         -spectatorStepGap (BD - 1) Bz z r m := by
   …

   Mentions: OAI.Ostmann.spectatorStepGap

3. theorem OAI.Ostmann.eventual_moving_cell_error_budget line 30
4. theorem OAI.Ostmann.moving_linear_cell_error_budget line 53

   Source documentation

   The centers may each have an error proportional to L. Since the bulk size is k^4 L + O(1), the same one-unit gap reserve pays these errors.

   theorem moving_linear_cell_error_budget (k n : ℕ) (C L cg ec es : ℝ)
       (hC : 0 ≤ C) (hk : 4 * C + 16 ≤ (k : ℝ) ^ 4) (hL : 1 ≤ L)
       (hcg : cg ≤ (91 / 100 : ℝ) * L) (he : ec + es ≤ C * L) :
       2 * cg + 1 + (ec + es) * (2 ^ n : ℕ) ≤
         (2 ^ n : ℕ) * (spectatorBulkCount k L : ℝ) := by
   …

   Mentions: OAI.Ostmann.spectatorBulkCount