English
For all a, k with a ≠ 0 and a < k, and all n, π'(k+n) ≤ π'(k) + φ(a) · (n/a + 1).
Русский
Для всех a, k с a ≠ 0 и a < k и для всех n выполняется неравенство: π'(k+n) ≤ π'(k) + φ(a) · (n/a + 1).
LaTeX
$$$\forall \{a,k:\mathbb{N}\}, a \neq 0 \to a < k \to \forall n, \\pi'(k+n) \le \pi'(k) + \varphi(a) \left(\frac{n}{a} + 1\right)$$$
Lean4
/-- A linear upper bound on the size of the `primeCounting'` function -/
theorem primeCounting'_add_le {a k : ℕ} (h0 : a ≠ 0) (h1 : a < k) (n : ℕ) :
π' (k + n) ≤ π' k + Nat.totient a * (n / a + 1) :=
calc
π' (k + n) ≤ #({p ∈ range k | p.Prime}) + #({p ∈ Ico k (k + n) | p.Prime}) :=
by
rw [primeCounting', count_eq_card_filter_range, range_eq_Ico, ← Ico_union_Ico_eq_Ico (zero_le k) le_self_add,
filter_union]
apply card_union_le
_ ≤ π' k + #({p ∈ Ico k (k + n) | p.Prime}) := by rw [primeCounting', count_eq_card_filter_range]
_ ≤ π' k + #({b ∈ Ico k (k + n) | a.Coprime b}) :=
by
refine add_le_add_left (card_le_card ?_) k.primeCounting'
simp only [subset_iff, and_imp, mem_filter, mem_Ico]
intro p succ_k_le_p p_lt_n p_prime
constructor
· exact ⟨succ_k_le_p, p_lt_n⟩
· rw [coprime_comm]
exact coprime_of_lt_prime h0 (lt_of_lt_of_le h1 succ_k_le_p) p_prime
_ ≤ π' k + totient a * (n / a + 1) := by
rw [add_le_add_iff_left]
exact Ico_filter_coprime_le k n h0
