SelectedProductFrequency.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual product schedule satisfies the finite frequency budget

theorem OAI.Ostmann.selectedProductExponent_gap_upper line 10

theorem OAI.Ostmann.selectedProductExponent_gap_budget line 43

Source documentation

Each rounding loss is paid once, in the fixed per-step reserve.

theorem selectedProductExponent_gap_budget
    {A B : Set ℕ} {N hi top : ℕ} {a C L X J G Y cb cd width Dlog BD Bz R : ℝ}
    {D : Finset ℕ} {cs : List ℕ} (k n : ℕ) (hk : 2 ≤ k) (hn : n < k)
    (hL : 1 ≤ L) (hR : 0 ≤ R) (hdef0 : 0 ≤ tailDefectBudget a C X)
    (hdef : tailDefectBudget a C X ≤ R * L)
    (hlarge : 14 * (64 * R + 3) ≤ (k : ℝ) ^ 3)
    (hscale : 4 ≤ (k : ℝ) ^ 4 * L)
    (hm : 4 ≤ (spectatorBulkCount k L : ℝ))
    (hwidth : width = 2 * ((initialSmallCellList top cs).length + 3))
    (hD : 2 * cd - 2 ≤ Dlog)
    (htop : SelectedSmallTailCell A B N a C L X hi D ((J - 2 * cb) / 6) top)
    (hcs : List.Forall₂
…

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

theorem OAI.Ostmann.movingProductFrequency_le_movingCutoff line 81