OAI/NumberTheory/Ostmann/Construction/InitialCellPriors.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.initialRegularPrimeRange line 10
2. theorem OAI.Ostmann.initialRegularPrimeRange_prime line 13
3. theorem OAI.Ostmann.mem_initialRegularPrimeRange line 16
4. theorem OAI.Ostmann.initial_broad_cell_subset line 20
5. theorem OAI.Ostmann.SelectedSmallTailCell.subset_initialRegularPrimeRange line 30
6. theorem OAI.Ostmann.initialSmallCellList_property line 40
7. theorem OAI.Ostmann.initial_selected_cells_valid line 50
8. theorem OAI.Ostmann.initial_selected_cells_balanced_mass line 70

   Source documentation

   Append every actual top/compensation cell to the two already chosen cutoff weights. The cells are not conditioned on any new event.

   theorem initial_selected_cells_balanced_mass
       {A B : Set ℕ} {N hi top : ℕ} {a C L Y target : ℝ} {D : Finset ℕ}
       {centers : List ℕ} {targets : List ℝ}
       (htop : SelectedSmallTailCell A B N a C L Y hi D target top)
       (hcenters : List.Forall₂
         (fun j w => SelectedSmallTailCell A B N a C L Y hi D (w / 4) j) centers targets)
       (P : Finset ℕ) (hsmallP : initialRegularPrimeRange L ⊆ P)
       (b d m : ℕ) (Qb Qd : Finset ℕ) (cb cd : ℝ)
       (hb : Real.exp (-(Real.log 2 + 2) * m) ≤
         ∑ x ∈ balancedTupleSet b (fun _ (p : P) =>
           (1 / 3 : ℝ) ≤ residueDensity (tailDensityMask A N p) ∧
             residueDensity (tailDensityMask A N p) ≤ 2 / 3),
   …

   Mentions: OAI.Ostmann.SelectedSmallTailCell, OAI.Ostmann.initialRegularPrimeRange, OAI.Ostmann.balancedTupleSet, OAI.Ostmann.residueDensity, OAI.Ostmann.tailDensityMask