OAI/NumberTheory/Ostmann/Arithmetic/MovingProductFrequency.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingProductFrequencyExponent line 11

   Source documentation

   Centering at the measured terminal product avoids charging its rounding error again at each subsequent transfer.

   noncomputable def movingProductFrequencyExponent (T : ℕ → ℝ)
       (W Y m : ℝ) (n : ℕ) : ℝ :=
   …

2. def OAI.Ostmann.movingProductNaturalCutoff line 15
3. theorem OAI.Ostmann.movingProductExponent_monotone line 19
4. theorem OAI.Ostmann.movingProductNaturalCutoff_monotone line 27
5. theorem OAI.Ostmann.movingProductFrequency_reserve line 39
6. theorem OAI.Ostmann.movingProductNaturalCutoff_scale line 48

   Source documentation

   The full ceiling product cap satisfies the next integer-frequency bound. Only the actual lower bound on the inserted pivot product is needed.

   theorem movingProductNaturalCutoff_scale (T : ℕ → ℝ) (W Y m : ℝ) (n : ℕ)
       (hm : 64 ≤ m) (hY : Y ≤ W)
       (hgap : ∀ j, 2 * T j ≤ movingProductExponent T W j)
       (hH : 0 ≤ movingProductExponent T W n - T n)
       (M : ℕ) (hM : Real.exp (T n) ≤ (M : ℝ)) :
       2 * movingProductNaturalCutoff T W Y m n *
           ⌈Real.exp (movingProductExponent T W n - T n)⌉₊ ≤
         movingProductNaturalCutoff T W Y m (n + 1) * M := by
   …

   Mentions: OAI.Ostmann.movingProductExponent, OAI.Ostmann.movingProductNaturalCutoff