MovingProductRounding.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Actual cell rounding in the recursive product and frequency budgets

theorem OAI.Ostmann.productExponent_rounding_le line 9
theorem OAI.Ostmann.movingProductExponent_rounding_abs line 22
theorem OAI.Ostmann.movingProductFrequency_rounding_abs line 33

theorem OAI.Ostmann.SelectedSmallTailCell.pivot_exponent_error line 44

Source documentation

The selected integer center is close to its target in the exact pivot exponent used by the product cap, including the lower-edge loss.

theorem SelectedSmallTailCell.pivot_exponent_error
    {A B : Set ℕ} {N hi j : ℕ} {a C L X w : ℝ} {D : Finset ℕ}
    (h : SelectedSmallTailCell A B N a C L X hi D (w / 4) j) (G : ℝ) (n : ℕ) :
    |(G - 1 + ((2 ^ n * 4 : ℕ) : ℝ) * ((j : ℝ) - 1)) -
      (G + (2 : ℝ) ^ n * w)| ≤
        (2 : ℝ) ^ n * (256 * tailDefectBudget a C X + 9) := by
…

Mentions: OAI.Ostmann.SelectedSmallTailCell, OAI.Ostmann.tailDefectBudget

theorem OAI.Ostmann.movingProductFrequency_prescribed_rate line 63

Source documentation

Rounding that fits the existing one-unit reserve preserves the already proved uniform frequency-rate bound.

theorem movingProductFrequency_prescribed_rate (G J Y Bs BD Bz L : ℝ) (k n : ℕ)
    (hn : n ≤ k) (T : ℕ → ℝ) (W C R : ℝ)
    (hbase : 2 * G + J + (movingCompensationTargets J (movingCompensationGaps k BD Bz L)).sum - Y =
      spectatorBaseGap Bs ((k : ℝ) ^ 4) (spectatorBulkCount k L))
    (hW : |W - (2 * G + J + (movingCompensationTargets J (movingCompensationGaps k BD Bz L)).sum)| ≤ C)
    (hT : ∀ j < n, |T j - movingTargetPivotExponent G
      (movingCompensationTargets J (movingCompensationGaps k BD Bz L)) j| ≤ (2 : ℝ) ^ j * R)
    (hbudget : C + n * R ≤ (spectatorBulkCount k L : ℝ))
    (hBs : 0 ≤ Bs) (hBD : 0 ≤ BD) (hBz : 0 ≤ Bz) (hk : 1 ≤ (k : ℝ) ^ 4)
    (hm : 4 ≤ (spectatorBulkCount k L : ℝ)) :
    movingProductFrequencyExponent T W Y (spectatorBulkCount k L) n ≤
      movingFrequencyRate Bs BD Bz ((k : ℝ) ^ 4) n * spectatorBulkCount k L := by
…

Mentions: OAI.Ostmann.movingCompensationTargets, OAI.Ostmann.movingCompensationGaps, OAI.Ostmann.spectatorBaseGap, OAI.Ostmann.spectatorBulkCount, OAI.Ostmann.movingTargetPivotExponent, OAI.Ostmann.movingProductFrequencyExponent, OAI.Ostmann.movingFrequencyRate

theorem OAI.Ostmann.moving_cell_frequency_rounding_budget line 87

Source documentation

The actual initial-cell error and every subsequent pivot-cell error fit the existing one-unit frequency allowance at polynomial bulk scale.

theorem moving_cell_frequency_rounding_budget (k n : ℕ) (R D L : ℝ)
    (hk : 2 ≤ k) (hn : n ≤ k) (hD : 0 ≤ D)
    (hL : 1 ≤ L) (hDL : D ≤ R * L)
    (hlarge : 2 * (704 * R + 26) ≤ (k : ℝ) ^ 3)
    (hscale : 4 ≤ (k : ℝ) ^ 4 * L) :
    (6 + 4 * k) * (64 * D + 1) + 2 * ((3 + 2 * k : ℕ) + 3) +
      n * (256 * D + 9) ≤ (spectatorBulkCount k L : ℝ) := by
…

Mentions: OAI.Ostmann.spectatorBulkCount