theorem AnalyticNumberTheory.LargeSieve.sum_Ioc_nat_eq_sum_Icc_int (M : ℤ) (a b : ℕ) (f : ℤ → ℂ) : ∑ n ∈ Finset.Ioc a b, f (M + ↑n) = ∑ n ∈ Finset.Icc (M + ↑a + 1) (M + ↑b), f n

theorem AnalyticNumberTheory.LargeSieve.sum_Ioc_telescope_eq (y L : ℕ) (f : ℕ → ℂ) : ∑ k ∈ Finset.range L, ∑ n ∈ Finset.Ioc (y / 2 ^ (k + 1) * 2 ^ (k + 1)) (y / 2 ^ k * 2 ^ k), f n = ∑ n ∈ Finset.Ioc (y / 2 ^ L * 2 ^ L) y, f n

theorem AnalyticNumberTheory.LargeSieve.div_mod_two_eq (y k : ℕ) : y / 2 ^ k = 2 * (y / 2 ^ (k + 1)) + y / 2 ^ k % 2

theorem AnalyticNumberTheory.LargeSieve.decomp_eq (y N : ℕ) (hy : y ≤ N) (f : ℕ → ℂ) : ∑ n ∈ Finset.Ioc 0 y, f n = ∑ k ∈ Finset.range (N.log2 + 1) with y / 2 ^ k % 2 = 1, ∑ n ∈ Finset.Ioc (2 * (y / 2 ^ (k + 1)) * 2 ^ k) (2 * (y / 2 ^ (k + 1)) * 2 ^ k + 2 ^ k), f n

theorem AnalyticNumberTheory.LargeSieve.decomp_j_lt (y N k : ℕ) (hy : y ≤ N) : 2 * (y / 2 ^ (k + 1)) < N + 1

theorem AnalyticNumberTheory.LargeSieve.Ioc_disjoint (a b c d : ℤ) (h : b ≤ c) : Disjoint (Finset.Ioc a b) (Finset.Ioc c d)

theorem AnalyticNumberTheory.LargeSieve.sum_biUnion_le {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (S : ι → Finset ℤ) (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) (T : Finset ℤ) (h_sub : ∀ i ∈ s, S i ⊆ T) (c : ℤ → ℝ) (hc : ∀ n ∈ T, 0 ≤ c n) : ∑ i ∈ s, ∑ n ∈ S i, c n ≤ ∑ n ∈ T, c n

theorem AnalyticNumberTheory.LargeSieve.weighted_primitive_prefix_maximal (b : ℤ → ℂ) (M : ℤ) (N Q : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, primitiveCharacterPrefixMaxSquare b M N q χ ≤ ↑(N.log2 + 1) ^ 2 * primitiveLargeSieveConstant N Q * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2