MovingJointPairRate.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Joint prime-giant idealization of the literal moving kernel

theorem OAI.Ostmann.PublishedProgressionInput.moving_joint_kernelPair_prime_rate_uniform line 15

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_kernelPair_prime_rate_uniform (P : PublishedProgressionInput)
    (n : ℕ) (C : ℝ) (d : ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ (σ : Type u) (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0)
      (childBound pivotBound : ℕ → ℕ) (T : Bool → MovingSlotData σ n) (hf : ∀ b, (T b).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 : ℝ), (∀ b, (T b).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

theorem OAI.Ostmann.PublishedProgressionInput.moving_joint_kernelPair_prime_rate line 80