OAI/NumberTheory/Ostmann/Arithmetic/MovingProductRigidity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingProductFrequency_gap line 8
2. theorem OAI.Ostmann.movingProductFrequency_rigidity_margin line 16

   Source documentation

   The initial center error cancels from this margin. Only the current pivot-cell error remains, twice.

   theorem movingProductFrequency_rigidity_margin (T U : ℕ → ℝ) (W Z Y m R : ℝ) (n : ℕ)
       (hT : T n ≤ U n + (2 : ℝ) ^ n * R) (hR : R ≤ m / 40)
       (hideal : (3 / 20 : ℝ) * (2 : ℝ) ^ n * m ≤
         (movingProductExponent U Z n - 2 * U n) -
           movingProductFrequencyExponent U Z Y m n) :
       (1 / 10 : ℝ) * (2 : ℝ) ^ n * m ≤
         (movingProductExponent T W n - 2 * T n) -
           movingProductFrequencyExponent T W Y m n := by
   …

   Mentions: OAI.Ostmann.movingProductExponent, OAI.Ostmann.movingProductFrequencyExponent

3. theorem OAI.Ostmann.movingProductFrequency_prescribed_margin line 28
4. theorem OAI.Ostmann.movingProductNaturalCutoff_rigidity line 61