theorem AnalyticNumberTheory.LargeSieve.PanLow.low_harmonic_le {N A₁ A₂ : ℕ} (hA : A₂ ≤ N) : ∑ a ∈ Finset.Ioc A₁ A₂, (↑a)⁻¹ ≤ 1 + Real.log ↑N

theorem AnalyticNumberTheory.LargeSieve.PanLow.nonprincipalLow_le_prime_budget (g : ℕ → ℂ) (N A₁ A₂ Q m : ℕ) (K s : ℝ) (hN : 3 ≤ N) (hA : A₂ ≤ N) (hm : 0 < m) (hK : 0 ≤ K) (hg : ∀ a ∈ Finset.Ioc A₁ A₂, ‖g a‖ ≤ 1) (hprefix : ∀ a ∈ Finset.Ioc A₁ A₂, ∀ q ∈ Finset.Icc 2 Q, ∀ (χ : PrimitiveCharacter q), ‖primePrefix (↑χ) (N / a)‖ ≤ K * ↑N / Real.log ↑N ^ s / ↑a) : nonprincipalLow g (fun (n : ℕ) => if Nat.Prime n ∧ n.Coprime m then 1 else 0) N A₁ A₂ Q ≤ ↑Q * (K * ↑N / Real.log ↑N ^ s * (1 + Real.log ↑N) + ↑A₂ * ↑m.primeFactors.card)

Low-lane only: the whole-a norm is kept until triangle is paid by the explicit actual-prime prefix premise. No SW transport is asserted here.