OAI/NumberTheory/Ostmann/Construction/RepeatFactorBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.doubledRole_normalizers line 13
2. theorem OAI.Ostmann.bulk_top_normalizers line 20
3. theorem OAI.Ostmann.bulk_top_normalizers_le line 33
4. theorem OAI.Ostmann.repeated_positions_power line 62

   Source documentation

   Extra roles cost only a fixed power of the number of bulk positions.

   theorem repeated_positions_power (m b : ℕ) (L z : ℝ) (hL : 0 < L)
       (hn : ((2 * m + b : ℕ) : ℝ) ≤ z * L) :
       L⁻¹ ^ (2 * m) * ((2 * m + b : ℕ) : ℝ) ^ (2 * m + b) ≤
         z ^ (2 * m) * ((2 * m + b : ℕ) : ℝ) ^ b := by
   …

5. theorem OAI.Ostmann.eventual_fixed_role_cost line 76

   Source documentation

   A fixed polynomial loss is absorbed before the gap is chosen.

   theorem eventual_fixed_role_cost (b : ℕ) (ε : ℝ) (hε : 0 < ε) :
       ∀ᶠ m : ℕ in atTop, ((2 * m + b : ℕ) : ℝ) ^ b ≤ Real.exp (ε * m) := by
   …

6. theorem OAI.Ostmann.eventual_repeat_multiplicity_cost line 93

   Source documentation

   The bulk normalizers cancel the powers of L in the ordered-tuple cost.

   theorem eventual_repeat_multiplicity_cost (b : ℕ) (a z : ℝ) (ha : 0 < a) (hz : 0 < z) :
       ∀ᶠ m : ℕ in atTop, ∀ L : ℝ, 0 < L → (m : ℝ) ≤ z * L → b ≤ m →
         (a * L)⁻¹ ^ (2 * m) * ((2 * m + b : ℕ) : ℝ) ^ (2 * m + b) ≤
           Real.exp ((2 * Real.log (3 * z / a) + 1) * m) := by
   …