MovingJointGiantRate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Joint prime-giant idealization of the literal moving kernel

theorem OAI.Ostmann.PublishedProgressionInput.moving_joint_prime_rate line 13

Source documentation

Both original 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_prime_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 → a.Coprime q → b.Coprime q →
      Real.log (4 * (Q : ℝ)) ≤ 2 * Real.exp ((12 / 1000 : ℝ) * L) →
      ∀ u v r s : ℝ,
      Real.exp ((49 / 1000 : ℝ) * L) ≤ u → u ≤ v → v ≤ u + 1 →
…

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