OAI/NumberTheory/Ostmann/Arithmetic/MovingHarmonicCounterpart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.moving_harmonic_counterpart_le line 12

   Source documentation

   The original giant range and terminal bulk cutoff supply the two exponential denominators in the harmonic product-fibre bound.

   theorem moving_harmonic_counterpart_le (n r m : ℕ)
       (Q : MovingRegularSlot n r m → Finset ℕ) (cg Gmin cb : ℝ)
       (X : ℕ) (y : MovingRegularSlot n r m → ℕ)
       (hX : Real.exp Gmin ≤ (X : ℝ))
       (hy : Real.exp ((2 ^ n : ℕ) * (cb - 1)) ≤ ((∏ i, y i : ℕ) : ℝ)) :
       (Real.exp cg / X) * ((Fintype.card (MovingRegularSlot n r m)).factorial : ℝ) *
           (∏ i, (∑ q ∈ Q i, (q : ℝ)⁻¹)⁻¹) * ((∏ i, y i : ℕ) : ℝ)⁻¹ ≤
         Real.exp (cg - Gmin - (2 ^ n : ℕ) * (cb - 1)) *
           ((Fintype.card (MovingRegularSlot n r m)).factorial : ℝ) *
             (∏ i, (∑ q ∈ Q i, (q : ℝ)⁻¹)⁻¹) := by
   …

   Mentions: OAI.Ostmann.MovingRegularSlot