English
For all a, k, n, the inequality holds: the number of x in Ico k (k+n) with gcd(a,x)=1 is bounded by φ(a)·(n/a+1).
Русский
Для всех a, k, n: количество x в Ico k (k+n), с gcd(a,x)=1, ограничено φ(a)·(n/a+1).
LaTeX
$$$$\#\{x ∈ Ico(k, k+n) : a\perp x\} ≤ φ(a) \cdot \left(\frac{n}{a} + 1\right).$$$$
Lean4
theorem Ico_filter_coprime_le {a : ℕ} (k n : ℕ) (a_ne_zero : a ≠ 0) :
#({x ∈ Ico k (k + n) | a.Coprime x}) ≤ totient a * (n / a + 1) :=
by
conv_lhs => rw [← Nat.mod_add_div n a]
induction n / a with
| zero =>
rw [← filter_coprime_Ico_eq_totient a k]
simp only [add_zero, mul_one, mul_zero, zero_add]
gcongr
exact le_of_lt (mod_lt n (pos_iff_ne_zero.mpr a_ne_zero))
| succ i ih => ?_
simp only [mul_succ]
simp_rw [← add_assoc] at ih ⊢
calc
#({x ∈ Ico k (k + n % a + a * i + a) | a.Coprime x}) ≤
#({x ∈ Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x}) :=
by
gcongr
apply Ico_subset_Ico_union_Ico
_ ≤ #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) + a.totient :=
by
rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]
apply card_union_le
_ ≤ a.totient * i + a.totient + a.totient := add_le_add_right ih (totient a)
