OAI/NumberTheory/Ostmann/Arithmetic/MovingProductPrescribedCutoff.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.headD_drop_ofFn line 11
2. theorem OAI.Ostmann.movingProductExponent_sum_gaps line 23
3. theorem OAI.Ostmann.movingProductFrequency_prescribed line 32
4. theorem OAI.Ostmann.movingProductNaturalCutoff_prescribed line 62

   Source documentation

   Consequently this construction retains the original floor cutoffs when there is no cell-center error.

   theorem movingProductNaturalCutoff_prescribed (G J Y Bs BD Bz L : ℝ) (k n : ℕ)
       (hn : n ≤ k)
       (hbase : 2 * G + J + (movingCompensationTargets J (movingCompensationGaps k BD Bz L)).sum - Y =
         spectatorBaseGap Bs ((k : ℝ) ^ 4) (spectatorBulkCount k L)) :
       let ws := movingCompensationTargets J (movingCompensationGaps k BD Bz L)
   …

   Mentions: OAI.Ostmann.movingCompensationTargets, OAI.Ostmann.movingCompensationGaps, OAI.Ostmann.spectatorBaseGap, OAI.Ostmann.spectatorBulkCount