OAI/NumberTheory/Ostmann/Construction/SelectedScheduledProduct.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.nat_cell_drop_sum line 11
2. theorem OAI.Ostmann.selected_cell_pivot_exponent line 21
3. theorem OAI.Ostmann.selectedProductExponent_eq line 27
4. theorem OAI.Ostmann.selectedProductExponent_gap line 43
5. theorem OAI.Ostmann.selectedProductExponent_gap_from_diagonal line 53
6. theorem OAI.Ostmann.selectedProductExponent_budget line 74
7. theorem OAI.Ostmann.selectedProductExponent_budget_of_cells line 98

   Source documentation

   The chosen compensation cells give the actual recursive product budget.

   theorem selectedProductExponent_budget_of_cells
       {A B : Set ℕ} {N hi top : ℕ} {a C L X J G Y cb cd width Dlog BD Bz : ℝ}
       {D : Finset ℕ} {cs : List ℕ} (k : ℕ)
       (hk0 : 1 ≤ k) (hL : 1 ≤ L) (hX : 0 < X) (hXupper : X ≤ Real.exp L)
       (hk : 1024 * tailCellLinearRate a C + 52 ≤ (k : ℝ) ^ 4)
       (hcount : (8 + 4 * cs.length : ℕ) ≤ L)
       (hcb : 0 ≤ cb) (hD : Dlog ≤ 2 * cd + 2) (hwidth : 0 ≤ width)
       (hBD : 1 ≤ BD) (hBz : 0 ≤ Bz)
       (htop : SelectedSmallTailCell A B N a C L X hi D ((J - 2 * cb) / 6) top)
       (hcs : List.Forall₂
         (fun j t => SelectedSmallTailCell A B N a C L X hi D (t / 4) j)
         cs (movingCompensationTargets J (movingCompensationGaps k BD Bz L))) :
   …

   Mentions: OAI.Ostmann.tailCellLinearRate, OAI.Ostmann.SelectedSmallTailCell, OAI.Ostmann.movingCompensationTargets, OAI.Ostmann.movingCompensationGaps

8. theorem OAI.Ostmann.selected_cell_pivot_nonneg line 132