OAI/NumberTheory/Ostmann/Construction/SelectedProductSchedule.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingProductExponent_gap_of_constant_tail line 10
2. theorem OAI.Ostmann.selectedCompensation_pivot_tail line 28
3. theorem OAI.Ostmann.selectedCompensation_pivot_nonneg line 33
4. theorem OAI.Ostmann.selectedCompensation_product_gaps line 42

   Source documentation

   Every finite selected pivot gap is positive, and the unused constant tail preserves that inequality. Hence the constructed frequencies are monotone on all natural indices, as required by the original sampled-history recursion.

   theorem selectedCompensation_product_gaps
       {A B : Set ℕ} {N hi : ℕ} {a C L X G J W E : ℝ} {D : Finset ℕ}
       {centers : List ℕ} (k : ℕ) (BD Bz : ℝ)
       (hcenters : List.Forall₂
         (fun j w => SelectedSmallTailCell A B N a C L X hi D (w / 4) j) centers
         (movingCompensationTargets J (movingCompensationGaps k BD Bz L)))
       (hW : |W - (2 * G + J +
         (movingCompensationTargets J (movingCompensationGaps k BD Bz L)).sum)| ≤ E)
       (hbudget : E + k * (256 * tailDefectBudget a C X + 9) ≤
         (spectatorBulkCount k L : ℝ))
       (hD : 0 ≤ tailDefectBudget a C X)
       (hR : 256 * tailDefectBudget a C X + 9 ≤ (spectatorBulkCount k L : ℝ) / 40)
   …

   Mentions: OAI.Ostmann.SelectedSmallTailCell, OAI.Ostmann.movingCompensationTargets, OAI.Ostmann.movingCompensationGaps, OAI.Ostmann.tailDefectBudget, OAI.Ostmann.spectatorBulkCount