OAI/NumberTheory/Ostmann/Construction/SelectedInitialProductWindow.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.selectedInitialLogCenter line 12
2. theorem OAI.Ostmann.selected_initial_center_bounds line 16
3. theorem OAI.Ostmann.selectedInitialCellCenter_sum line 46
4. theorem OAI.Ostmann.selected_initial_product_window line 61

   Source documentation

   The narrow window is centered at the actual selected total. Its width depends only on the number of fixed cell roles, including the giant.

   theorem selected_initial_product_window
       {A B : Set ℕ} {N endpoint top : ℕ} {a C L Y G cb cd target : ℝ}
       {D : Finset ℕ} {centers : List ℕ} {targets : List ℝ}
       (htop : SelectedSmallTailCell A B N a C L Y endpoint D target top)
       (hcenters : List.Forall₂
         (fun j w => SelectedSmallTailCell A B N a C L Y endpoint D (w / 4) j) centers targets)
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (b d : ℕ)
       (μb : Fin b → P → ℝ) (μd : Fin d → P → ℝ) :
       let cells := initialSmallCellList top centers
   …

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