OAI/NumberTheory/Ostmann/Arithmetic/MovingJointMixedRate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.PublishedProgressionInput.moving_joint_mixed_rate line 14

   Source documentation

   The original integer and prime sums are replaced jointly. The Page factors remain inside their actual measures and the threshold is uniform in the small data.

   theorem PublishedProgressionInput.moving_joint_mixed_rate (P : PublishedProgressionInput)
       {σ : Type*} (n : ℕ) (C : ℝ) (d : ℕ) :
       ∀ᶠ L : ℝ in atTop, ∀ (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0)
         (childBound pivotBound : ℕ → ℕ) (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0))
         (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
         (φ : ℝ → ℝ) (G : ℕ → ℝ) (B D : ℝ) (_hB : 0 ≤ B) (_hD : 0 ≤ D)
         (_hφ : ∀ x, |φ x| ≤ B) (_hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|)
         (_hout : ∀ x, 1 ≤ |x| → φ x = 0) (V : ℝ), T.Frequencies (fun s => |(s : ℝ)| ≤ V) →
         ∀ Q q a b : ℕ, 2 ≤ Q → 1 ≤ q → q ≤ Q → b.Coprime q →
         Real.log (4 * (Q : ℝ)) ≤ 2 * Real.exp ((12 / 1000 : ℝ) * L) →
         ∀ u v r s J : ℝ,
         Real.exp ((49 / 1000 : ℝ) * L) ≤ J → u ≤ v → v ≤ u + 1 →
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.MovingSlotData