LeanPool.LatticeTriangle.Solution

def largestPrimeFactor (n : ℕ) : ℕ

The largest prime factor of n, or 0 if n has no prime factors (i.e. n ≤ 1).

Equations

• largestPrimeFactor n = WithBot.unbotD 0 n.primeFactors.max

def truncatedObtuseRegion (n : ℕ) (η : ℝ) : Set (ℤ × ℤ)

The truncated obtuse region H_n(η): integer pairs (p, q) with η * n ≤ p, η * n ≤ q, p + q < n / 2, and gcd(p, q, n) = 1.

Equations

• truncatedObtuseRegion n η = {pq : ℤ × ℤ | η * ↑n ≤ ↑pq.1 ∧ η * ↑n ≤ ↑pq.2 ∧ ↑pq.1 + ↑pq.2 < ↑n / 2 ∧ (↑(pq.1.gcd pq.2)).gcd ↑n = 1}

def intervalSet (n m : ℕ) : Set (ZMod n)

The image in ZMod n of the integer interval {1, …, m}.

Equations

• intervalSet n m = {x : ZMod n | 1 ≤ x.val ∧ x.val ≤ m}

@[instance_reducible]

instance intervalSetDecidableMem (n m : ℕ) : DecidablePred fun (x : ZMod n) => x ∈ intervalSet n m

Equations

• intervalSetDecidableMem n m x✝ = instDecidableAnd

def countingFunctionS (n : ℕ) (p q : ℤ) : ℕ

The counting function S(p, q): the number of units a ∈ (ZMod n)ˣ for which both a * p and a * q land in the initial intervals intervalSet n (2p-1) and intervalSet n (2q-1).

Equations

• One or more equations did not get rendered due to their size.

def badPairsSet (n : ℕ) (η : ℝ) : Set (ℤ × ℤ)

The bad pairs: pairs of truncatedObtuseRegion n η with gcd(q, P⁺(n)) = 1 and countingFunctionS n p q < 5, where P⁺(n) = largestPrimeFactor n.

Equations

• badPairsSet n η = {pq : ℤ × ℤ | pq ∈ truncatedObtuseRegion n η ∧ pq.2.gcd ↑(largestPrimeFactor n) = 1 ∧ countingFunctionS n pq.1 pq.2 < 5}

theorem truncatedObtuseRegion_subset_box (n : ℕ) (η : ℝ) : truncatedObtuseRegion n η ⊆ Set.Icc (⌈η * ↑n⌉ - 1) ⌊↑n / 2 - η * ↑n⌋ ×ˢ Set.Icc (⌈η * ↑n⌉ - 1) ⌊↑n / 2 - η * ↑n⌋

theorem truncatedObtuseRegion_finite (n : ℕ) (η : ℝ) : (truncatedObtuseRegion n η).Finite

theorem coprime_triangle_subset_truncatedObtuseRegion (n : ℕ) (η : ℝ) : {pq : ℤ × ℤ | η * ↑n ≤ ↑pq.1 ∧ η * ↑n ≤ ↑pq.2 ∧ ↑pq.1 + ↑pq.2 < ↑n / 2 ∧ pq.1.gcd pq.2 = 1} ⊆ truncatedObtuseRegion n η

theorem coprime_triangle_finite (n : ℕ) (η : ℝ) : {pq : ℤ × ℤ | η * ↑n ≤ ↑pq.1 ∧ η * ↑n ≤ ↑pq.2 ∧ ↑pq.1 + ↑pq.2 < ↑n / 2 ∧ pq.1.gcd pq.2 = 1}.Finite

theorem sum_lt_half_zero_case (p q : ℤ) (hp : p ≤ ⌊↑0 / 6⌋) (hq : q ≤ ⌊↑0 / 6⌋) (hgcd : p.gcd q = 1) : ↑p + ↑q < ↑0 / 2

theorem sum_lt_half_pos_case (n : ℕ) (p q : ℤ) (hn : 1 ≤ n) (hp : p ≤ ⌊↑n / 6⌋) (hq : q ≤ ⌊↑n / 6⌋) : ↑p + ↑q < ↑n / 2

theorem sum_lt_half_of_le_floor_sixth (n : ℕ) (p q : ℤ) (hp : p ≤ ⌊↑n / 6⌋) (hq : q ≤ ⌊↑n / 6⌋) (hgcd : p.gcd q = 1) : ↑p + ↑q < ↑n / 2

theorem rectangle_coprime_subset_target (n : ℕ) (η : ℝ) : {pq : ℤ × ℤ | ⌈η * ↑n⌉ ≤ pq.1 ∧ pq.1 ≤ ⌊↑n / 6⌋ ∧ ⌈η * ↑n⌉ ≤ pq.2 ∧ pq.2 ≤ ⌊↑n / 6⌋ ∧ pq.1.gcd pq.2 = 1} ⊆ {pq : ℤ × ℤ | η * ↑n ≤ ↑pq.1 ∧ η * ↑n ≤ ↑pq.2 ∧ ↑pq.1 + ↑pq.2 < ↑n / 2 ∧ pq.1.gcd pq.2 = 1}

theorem Int_Icc_ncard (a b : ℤ) : (Set.Icc a b).ncard = (b + 1 - a).toNat

theorem eta_n_plus_one_le_n_div_six (η : ℝ) (_hη_pos : 0 < η) (hη_lt : η < 1 / 6) : ∃ (N₀ : ℕ), ∀ (n : ℕ), N₀ ≤ n → η * ↑n + 1 ≤ ↑n / 6

theorem int_expr_real_lower_bound (η : ℝ) (n : ℕ) : ↑n / 6 - η * ↑n - 1 < ↑(⌊↑n / 6⌋ + 1 - ⌈η * ↑n⌉)

theorem ceil_le_floor_for_large_n (η : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) : ∃ (N₀ : ℕ), ∀ (n : ℕ), N₀ ≤ n → ⌈η * ↑n⌉ ≤ ⌊↑n / 6⌋

theorem int_expr_nonneg_for_large_n (η : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) : ∃ (N₀ : ℕ), ∀ (n : ℕ), N₀ ≤ n → 0 ≤ ⌊↑n / 6⌋ + 1 - ⌈η * ↑n⌉

theorem half_bound_for_large_n (η : ℝ) (_hη_pos : 0 < η) (hη_lt : η < 1 / 6) : ∃ (N₀ : ℕ), ∀ (n : ℕ), N₀ ≤ n → (1 / 6 - η) / 2 * ↑n ≤ (1 / 6 - η) * ↑n - 1

theorem interval_toNat_lower_bound (η : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) : ∃ (N₀ : ℕ), ∀ (n : ℕ), N₀ ≤ n → (1 / 6 - η) / 2 * ↑n ≤ ↑(⌊↑n / 6⌋ + 1 - ⌈η * ↑n⌉).toNat

theorem interval_ncard_lower_bound (η : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) : ∃ (N₀ : ℕ), ∀ (n : ℕ), N₀ ≤ n → (1 / 6 - η) / 2 * ↑n ≤ ↑(Set.Icc ⌈η * ↑n⌉ ⌊↑n / 6⌋).ncard

theorem coprime_pairs_subset_product (A B : ℤ) : {pq : ℤ × ℤ | A ≤ pq.1 ∧ pq.1 ≤ B ∧ A ≤ pq.2 ∧ pq.2 ≤ B ∧ pq.1.gcd pq.2 = 1} ⊆ Set.Icc A B ×ˢ Set.Icc A B

theorem sq_add_one_le (a : ℝ) : (a + 1) ^ 2 ≤ 5 / 4 * a ^ 2 + 5

theorem inv_sq_le_inv_pred_mul (k : ℕ) (hk : 2 ≤ k) : 1 / ↑k ^ 2 ≤ 1 / ((↑k - 1) * ↑k)

theorem telescoping_sum_eq (N : ℕ) (hN : 3 ≤ N) : ∑ k ∈ Finset.Icc 3 N, 1 / ((↑k - 1) * ↑k) = 1 / 2 - 1 / ↑N

theorem tail_sum_le_half (N : ℕ) : ∑ k ∈ Finset.Icc 3 N, 1 / ↑k ^ 2 ≤ 1 / 2

theorem sum_Icc_split (N : ℕ) (hN : 2 ≤ N) (f : ℕ → ℝ) : ∑ k ∈ Finset.Icc 2 N, f k = f 2 + ∑ k ∈ Finset.Icc 3 N, f k

theorem sum_inv_sq_le_three_fourths (N : ℕ) : ∑ k ∈ Finset.Icc 2 N, 1 / ↑k ^ 2 ≤ 3 / 4

theorem multiples_finite (A B : ℤ) (m : ℕ) : {x : ℤ | A ≤ x ∧ x ≤ B ∧ ↑m ∣ x}.Finite

theorem toNat_inj_of_nonneg (a b : ℤ) (ha : 0 ≤ a) (hb : 0 ≤ b) (h : a.toNat = b.toNat) : a = b

theorem emod_eq_of_dvd (x₁ x₂ A m : ℤ) (h₁ : m ∣ x₁) (h₂ : m ∣ x₂) : (x₁ - A) % m = (x₂ - A) % m

theorem eq_of_ediv_eq_emod_eq (a b m : ℤ) (_hm : m ≠ 0) (hdiv : a / m = b / m) (hmod : a % m = b % m) : a = b

theorem shift_div_toNat_injOn (A B : ℤ) (m : ℕ) (hm : 0 < m) : Set.InjOn (fun (x : ℤ) => ((x - A) / ↑m).toNat) {x : ℤ | A ≤ x ∧ x ≤ B ∧ ↑m ∣ x}

theorem shift_div_toNat_le (A B : ℤ) (m : ℕ) (hm : 0 < m) (x : ℤ) (hxA : A ≤ x) (hxB : x ≤ B) : ((x - A) / ↑m).toNat ≤ (B + 1 - A).toNat / m

theorem shift_div_image_subset_range (A B : ℤ) (m : ℕ) (hm : 0 < m) : (fun (x : ℤ) => ((x - A) / ↑m).toNat) '' {x : ℤ | A ≤ x ∧ x ≤ B ∧ ↑m ∣ x} ⊆ ↑(Finset.range ((Set.Icc A B).ncard / m + 1))

theorem ncard_multiples_le (A B : ℤ) (m : ℕ) (hm : 0 < m) : {x : ℤ | A ≤ x ∧ x ≤ B ∧ ↑m ∣ x}.ncard ≤ (Set.Icc A B).ncard / m + 1

theorem exists_prime_dvd_both (A B : ℤ) (B' : ℕ) (hB' : ∀ (p : ℤ), A ≤ p → p ≤ B → ∀ (ℓ : ℕ), Nat.Prime ℓ → ↑ℓ ∣ p → ℓ ≤ B') (p q : ℤ) (hAp : A ≤ p) (hpB : p ≤ B) (_hAq : A ≤ q) (_hqB : q ≤ B) (hgcd : p.gcd q ≠ 1) : ∃ (ℓ : ℕ), Nat.Prime ℓ ∧ 2 ≤ ℓ ∧ ℓ ≤ B' ∧ ↑ℓ ∣ p ∧ ↑ℓ ∣ q

theorem non_coprime_subset_union (A B : ℤ) (_hAB : A ≤ B) (B' : ℕ) (hB' : ∀ (p : ℤ), A ≤ p → p ≤ B → ∀ (ℓ : ℕ), Nat.Prime ℓ → ↑ℓ ∣ p → ℓ ≤ B') : have S := Set.Icc A B ×ˢ Set.Icc A B; have C := {pq : ℤ × ℤ | A ≤ pq.1 ∧ pq.1 ≤ B ∧ A ≤ pq.2 ∧ pq.2 ≤ B ∧ pq.1.gcd pq.2 = 1}; S \ C ⊆ ⋃ ℓ ∈ Finset.filter Nat.Prime (Finset.Icc 2 B'), {x : ℤ | A ≤ x ∧ x ≤ B ∧ ↑ℓ ∣ x} ×ˢ {x : ℤ | A ≤ x ∧ x ≤ B ∧ ↑ℓ ∣ x}

theorem ncard_multiples_prod_le (A B : ℤ) (ℓ : ℕ) (hℓ : Nat.Prime ℓ) : have L := (Set.Icc A B).ncard; have Mℓ := {x : ℤ | A ≤ x ∧ x ≤ B ∧ ↑ℓ ∣ x}; (Mℓ ×ˢ Mℓ).ncard ≤ (L / ℓ + 1) ^ 2

theorem non_coprime_ncard_le_sum (A B : ℤ) (hAB : A ≤ B) (B' : ℕ) (hB' : ∀ (p : ℤ), A ≤ p → p ≤ B → ∀ (ℓ : ℕ), Nat.Prime ℓ → ↑ℓ ∣ p → ℓ ≤ B') : have L := (Set.Icc A B).ncard; have S := Set.Icc A B ×ˢ Set.Icc A B; have C := {pq : ℤ × ℤ | A ≤ pq.1 ∧ pq.1 ≤ B ∧ A ≤ pq.2 ∧ pq.2 ≤ B ∧ pq.1.gcd pq.2 = 1}; (S \ C).ncard ≤ ∑ ℓ ∈ Finset.Icc 2 B' with Nat.Prime ℓ, (L / ℓ + 1) ^ 2

theorem card_primes_le_B' (B' : ℕ) : (Finset.filter Nat.Prime (Finset.Icc 2 B')).card ≤ B'

theorem sum_inv_sq_primes_le (B' : ℕ) : ∑ ℓ ∈ Finset.Icc 2 B' with Nat.Prime ℓ, 1 / ↑ℓ ^ 2 ≤ 3 / 4

theorem term_sq_bound (L ℓ : ℕ) (hℓ : 2 ≤ ℓ) : ↑(L / ℓ + 1) ^ 2 ≤ 5 / 4 * ↑L ^ 2 / ↑ℓ ^ 2 + 5

theorem sum_sq_bound_real (L B' : ℕ) : ∑ ℓ ∈ Finset.Icc 2 B' with Nat.Prime ℓ, ↑(L / ℓ + 1) ^ 2 ≤ 15 / 16 * ↑L ^ 2 + 5 * ↑B'

theorem non_coprime_pairs_upper_bound (A B : ℤ) (hAB : A ≤ B) (B' : ℕ) (hB' : ∀ (p : ℤ), A ≤ p → p ≤ B → ∀ (ℓ : ℕ), Nat.Prime ℓ → ↑ℓ ∣ p → ℓ ≤ B') : have L := (Set.Icc A B).ncard; have S := Set.Icc A B ×ˢ Set.Icc A B; have C := {pq : ℤ × ℤ | A ≤ pq.1 ∧ pq.1 ≤ B ∧ A ≤ pq.2 ∧ pq.2 ≤ B ∧ pq.1.gcd pq.2 = 1}; ↑(S \ C).ncard ≤ 15 / 16 * ↑L ^ 2 + 5 * ↑B'

theorem coprime_lower_bound_from_complement (L C_card NC_card B' : ℕ) (h_partition : C_card + NC_card = L * L) (h_NC_bound : ↑NC_card ≤ 15 / 16 * ↑L ^ 2 + 5 * ↑B') : ↑L ^ 2 / 16 - 5 * ↑B' ≤ ↑C_card

theorem coprime_pairs_sieve_lower_bound (A B : ℤ) (hAB : A ≤ B) (B' : ℕ) (hB' : ∀ (p : ℤ), A ≤ p → p ≤ B → ∀ (ℓ : ℕ), Nat.Prime ℓ → ↑ℓ ∣ p → ℓ ≤ B') : have L := (Set.Icc A B).ncard; ↑L ^ 2 / 16 - 5 * ↑B' ≤ ↑{pq : ℤ × ℤ | A ≤ pq.1 ∧ pq.1 ≤ B ∧ A ≤ pq.2 ∧ pq.2 ≤ B ∧ pq.1.gcd pq.2 = 1}.ncard

theorem quadratic_dominates_linear (δ L n B' : ℝ) (hδ : 0 < δ) (hn : 0 ≤ n) (hL : δ * n ≤ L) (hB' : 5 * B' ≤ 5 * n) (hn_large : 160 / δ ^ 2 ≤ n) : δ ^ 2 / 32 * n ^ 2 ≤ L ^ 2 / 16 - 5 * B'

theorem ceil_eta_n_pos (η : ℝ) (hη_pos : 0 < η) (n : ℕ) (hn : 1 ≤ n) : 1 ≤ ⌈η * ↑n⌉

theorem floor_div_six_le_n (n : ℕ) : ⌊↑n / 6⌋ ≤ ↑n

theorem interval_ncard_le_n (η : ℝ) (hη_pos : 0 < η) (n : ℕ) (hn : ⌈1 / η⌉₊ ≤ n) : (Set.Icc ⌈η * ↑n⌉ ⌊↑n / 6⌋).ncard ≤ n

theorem interval_ncard_upper_bound (η : ℝ) (hη_pos : 0 < η) : ∃ (N₀ : ℕ), ∀ (n : ℕ), N₀ ≤ n → ↑(Set.Icc ⌈η * ↑n⌉ ⌊↑n / 6⌋).ncard ≤ ↑n

theorem prime_dvd_le_of_pos (p : ℤ) (hp : 0 < p) (ℓ : ℕ) (_hprime : Nat.Prime ℓ) (hdvd : ↑ℓ ∣ p) : ↑ℓ ≤ p

theorem prime_divisor_bound (η : ℝ) (hη_pos : 0 < η) (n : ℕ) (hn : 1 ≤ n) (p : ℤ) : ⌈η * ↑n⌉ ≤ p → p ≤ ⌊↑n / 6⌋ → ∀ (ℓ : ℕ), Nat.Prime ℓ → ↑ℓ ∣ p → ℓ ≤ n

theorem rectangle_coprime_ncard_lower_bound (η : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) : ∃ (c : ℝ) (N₁ : ℕ), 0 < c ∧ ∀ (n : ℕ), N₁ ≤ n → c * ↑n ^ 2 ≤ ↑{pq : ℤ × ℤ | ⌈η * ↑n⌉ ≤ pq.1 ∧ pq.1 ≤ ⌊↑n / 6⌋ ∧ ⌈η * ↑n⌉ ≤ pq.2 ∧ pq.2 ≤ ⌊↑n / 6⌋ ∧ pq.1.gcd pq.2 = 1}.ncard

theorem coprime_triangle_ncard_lower_bound (η : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) : ∃ (c : ℝ) (N₁ : ℕ), 0 < c ∧ ∀ (n : ℕ), N₁ ≤ n → c * ↑n ^ 2 ≤ ↑{pq : ℤ × ℤ | η * ↑n ≤ ↑pq.1 ∧ η * ↑n ≤ ↑pq.2 ∧ ↑pq.1 + ↑pq.2 < ↑n / 2 ∧ pq.1.gcd pq.2 = 1}.ncard

theorem truncatedObtuseRegion_ncard_lower_bound (η : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) : ∃ (c : ℝ) (N₁ : ℕ), 0 < c ∧ ∀ (n : ℕ), N₁ ≤ n → c * ↑n ^ 2 ≤ ↑(truncatedObtuseRegion n η).ncard

noncomputable def badPairsE (n : ℕ) (η : ℝ) : Set (ℤ × ℤ)

A relaxed family of bad pairs, replacing countingFunctionS n p q < 5 by (countingFunctionS n p q : ℝ) < η ^ 2 / 2 * φ(n).

Equations

• badPairsE n η = {pq : ℤ × ℤ | pq ∈ truncatedObtuseRegion n η ∧ pq.2.gcd ↑(largestPrimeFactor n) = 1 ∧ ↑(countingFunctionS n pq.1 pq.2) < η ^ 2 / 2 * ↑n.totient}

noncomputable def pdivPairs (n : ℕ) (η : ℝ) : Set (ℤ × ℤ)

Pairs of truncatedObtuseRegion n η with gcd(q, P⁺(n)) = 1 and P⁺(n) ∣ p.

Equations

• pdivPairs n η = {pq : ℤ × ℤ | pq ∈ truncatedObtuseRegion n η ∧ pq.2.gcd ↑(largestPrimeFactor n) = 1 ∧ ↑(largestPrimeFactor n) ∣ pq.1}

noncomputable def residueBadPairs (n : ℕ) (η : ℝ) : Set (ℤ × ℤ)

The pairs in badPairsE n η whose first coordinate is not divisible by the largest prime factor of n.

Equations

• residueBadPairs n η = {pq : ℤ × ℤ | pq ∈ badPairsE n η ∧ ¬↑(largestPrimeFactor n) ∣ pq.1}

theorem div_toNat_mem_range (B : ℤ) (P : ℕ) (_hP : 0 < P) (hB : 0 ≤ B) (x : ℤ) (hx0 : 0 ≤ x) (hxB : x ≤ B) : (x / ↑P).toNat < B.toNat / P + 1

theorem inj_div_toNat (B : ℤ) (P : ℕ) (hP : 0 < P) : Set.InjOn (fun (x : ℤ) => (x / ↑P).toNat) {x : ℤ | 0 ≤ x ∧ x ≤ B ∧ ↑P ∣ x}

theorem ncard_nonneg_multiples_le (B : ℤ) (P : ℕ) (hP : 0 < P) (hB : 0 ≤ B) : {x : ℤ | 0 ≤ x ∧ x ≤ B ∧ ↑P ∣ x}.ncard ≤ B.toNat / P + 1

theorem nonneg_multiples_finite (B : ℤ) (P : ℕ) : {x : ℤ | 0 ≤ x ∧ x ≤ B ∧ ↑P ∣ x}.Finite

theorem mul_P_mem_set (B : ℤ) (P : ℕ) (_hP : 0 < P) (hB : 0 ≤ B) (k : ℕ) (hk : k ≤ B.toNat / P) : ↑k * ↑P ∈ {x : ℤ | 0 ≤ x ∧ x ≤ B ∧ ↑P ∣ x}

theorem ncard_nonneg_multiples_ge (B : ℤ) (P : ℕ) (hP : 0 < P) (hB : 0 ≤ B) : B.toNat / P + 1 ≤ {x : ℤ | 0 ≤ x ∧ x ≤ B ∧ ↑P ∣ x}.ncard

theorem real_sq_div_mono (n P : ℕ) (θ : ℝ) (hn : 2 ≤ n) (_hP_pos : 0 < P) (hP : ↑P ≥ ↑n ^ θ) : ↑n ^ 2 / ↑P ≤ ↑n ^ 2 / ↑n ^ θ

theorem residueBadPairs_finite (n : ℕ) (η : ℝ) : (residueBadPairs n η).Finite

theorem largestPrimeFactor_pos_helper (n : ℕ) (hn : 2 ≤ n) : ∃ (a : ℕ), n.primeFactors.max = ↑a ∧ 0 < a

theorem largestPrimeFactor_pos (n : ℕ) (hn : 2 ≤ n) : 0 < largestPrimeFactor n

theorem fiber_empty_of_gcd_ne_one (n : ℕ) (η : ℝ) (q : ℤ) (hq : q.gcd ↑(largestPrimeFactor n) ≠ 1) : {p : ℤ | (p, q) ∈ residueBadPairs n η} = ∅

theorem snd_lt_half_of_mem_truncatedObtuseRegion_fb (n : ℕ) (η : ℝ) (pq : ℤ × ℤ) (h : pq ∈ truncatedObtuseRegion n η) (hp_pos : 0 < pq.1) : ↑pq.2 < ↑n / 2

theorem intLe_half_of_real_lt_half_fb (n : ℕ) (q : ℤ) (hq : ↑q < ↑n / 2) : q ≤ ↑n / 2

theorem pos_of_mem_truncatedObtuseRegion_fst_fb (n : ℕ) (η : ℝ) (hη_pos : 0 < η) (pq : ℤ × ℤ) (h : pq ∈ truncatedObtuseRegion n η) : 0 < pq.1

theorem pos_of_mem_truncatedObtuseRegion_snd_fb (n : ℕ) (η : ℝ) (hη_pos : 0 < η) (pq : ℤ × ℤ) (h : pq ∈ truncatedObtuseRegion n η) : 0 < pq.2

theorem fiber_subset_range (n : ℕ) (η : ℝ) (hη_pos : 0 < η) (q : ℤ) : {p : ℤ | (p, q) ∈ residueBadPairs n η} ⊆ Set.Ico 0 (↑n / 2)

theorem fiber_finite (n : ℕ) (η : ℝ) (hη_pos : 0 < η) (q : ℤ) : {p : ℤ | (p, q) ∈ residueBadPairs n η}.Finite

theorem counting_large_implies_not_badPairsE (n : ℕ) (η : ℝ) (p q : ℤ) (h : η ^ 2 / 2 * ↑n.totient ≤ ↑(countingFunctionS n p q)) : (p, q) ∉ badPairsE n η

theorem fiber_div_injOn (n d : ℕ) (hd_pos : 0 < d) (b : ℕ) (S : Set ℤ) (hS_sub : S ⊆ Set.Ico 0 (↑n / 2)) : Set.InjOn (fun (x : ℤ) => (x / ↑d).toNat) {x : ℤ | x ∈ S ∧ (x % ↑d).toNat = b}

theorem int_ediv_eq_natCast_div (n : ℤ) (m : ℕ) (_hm : 0 < m) (hn : 0 ≤ n) : n / ↑m = ↑(n.toNat / m)

theorem int_toNat_ediv_eq (n : ℤ) (m : ℕ) (hm : 0 < m) (hn : 0 ≤ n) : (n / ↑m).toNat = n.toNat / m

theorem int_ediv_toNat_le (a b : ℤ) (m : ℕ) (_hm : 0 < m) (ha : 0 ≤ a) (hab : a ≤ b) : (a / ↑m).toNat ≤ (b / ↑m).toNat

theorem div_toNat_le_half_div (n d : ℕ) (hd_pos : 0 < d) (x : ℤ) (hx0 : 0 ≤ x) (hx_lt : x < ↑n / 2) : (x / ↑d).toNat ≤ n / (2 * d)

theorem fiber_div_mem_range (n d : ℕ) (hd_pos : 0 < d) (b : ℕ) (S : Set ℤ) (hS_sub : S ⊆ Set.Ico 0 (↑n / 2)) (x : ℤ) (hx : x ∈ {x : ℤ | x ∈ S ∧ (x % ↑d).toNat = b}) : (x / ↑d).toNat ∈ Finset.range (n / (2 * d) + 1)

theorem product_ge_eta_sq_n_sq (η : ℝ) (hη_pos : 0 < η) (n : ℕ) (hn : 2 ≤ n) (p q : ℤ) (hp : η * ↑n ≤ ↑p) (hq : η * ↑n ≤ ↑q) : (η * ↑n) ^ 2 ≤ (2 * ↑p - 1) * (2 * ↑q - 1)

theorem rearrange_ineq (η : ℝ) (n : ℕ) (hn : 2 ≤ n) (p q : ℤ) (h : (η * ↑n) ^ 2 ≤ (2 * ↑p - 1) * (2 * ↑q - 1)) : η ^ 2 * ↑n.totient ≤ (2 * ↑p - 1) * (2 * ↑q - 1) * ↑n.totient / ↑n ^ 2

theorem main_term_lower_bound (η : ℝ) (hη_pos : 0 < η) (n : ℕ) (hn : 2 ≤ n) (p q : ℤ) (hpq : (p, q) ∈ truncatedObtuseRegion n η) : η ^ 2 * ↑n.totient ≤ (2 * ↑p - 1) * (2 * ↑q - 1) * ↑n.totient / ↑n ^ 2

noncomputable def intervalIndicator (n m : ℕ) : ZMod n → ℂ

The complex-valued indicator function of intervalSet n m on ZMod n.

Equations

• intervalIndicator n m = (intervalSet n m).indicator fun (x : ZMod n) => 1

noncomputable def normalizedDFT (n : ℕ) [NeZero n] (f : ZMod n → ℂ) (k : ZMod n) : ℂ

The normalised discrete Fourier transform of f : ZMod n → ℂ, scaled by (n : ℂ)⁻¹.

Equations

• normalizedDFT n f k = (↑n)⁻¹ * ZMod.dft f k

noncomputable def ramanujanSum (n : ℕ) [NeZero n] (t : ℤ) : ℂ

The Ramanujan sum c_n(t), written via the standard additive character of ZMod n.

Equations

• ramanujanSum n t = ∑ a : (ZMod n)ˣ, ZMod.stdAddChar (↑a * ↑t)

theorem toNat_two_mul_sub_one (p : ℤ) (hp : 1 ≤ p) : ↑(2 * p - 1).toNat = 2 * ↑p - 1

theorem indicator_product_eq_ite (n mp mq : ℕ) (x y : ZMod n) : intervalIndicator n mp x * intervalIndicator n mq y = if x ∈ intervalSet n mp ∧ y ∈ intervalSet n mq then 1 else 0

theorem counting_as_indicator_product (n : ℕ) (p q : ℤ) (hn : 2 ≤ n) (_hp : 1 ≤ p) (_hq : 1 ≤ q) (_hpq : ↑p + ↑q < ↑n / 2) : ↑(countingFunctionS n p q) = ∑ a : (ZMod n)ˣ, intervalIndicator n (2 * p - 1).toNat (↑a * ↑p) * intervalIndicator n (2 * q - 1).toNat (↑a * ↑q)

theorem fourier_inversion (n : ℕ) [NeZero n] (f : ZMod n → ℂ) (x : ZMod n) : f x = ∑ k : ZMod n, normalizedDFT n f k * ZMod.stdAddChar (k * x)

theorem three_sum_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : Type u_4} [Fintype α] [Fintype β] [Fintype γ] [AddCommMonoid R] (f : α → β → γ → R) : ∑ a : α, ∑ b : β, ∑ c : γ, f a b c = ∑ b : β, ∑ c : γ, ∑ a : α, f a b c

theorem sum_product_interchange_units (n : ℕ) [NeZero n] (c d : ZMod n → ℂ) (f g : ZMod n → (ZMod n)ˣ → ℂ) : ∑ a : (ZMod n)ˣ, (∑ k : ZMod n, c k * f k a) * ∑ l : ZMod n, d l * g l a = ∑ k : ZMod n, ∑ l : ZMod n, c k * d l * ∑ a : (ZMod n)ˣ, f k a * g l a

theorem interchange_and_factor (n : ℕ) (p q : ℤ) (hn : 2 ≤ n) : 1 ≤ p → 1 ≤ q → ↑p + ↑q < ↑n / 2 → ∑ a : (ZMod n)ˣ, intervalIndicator n (2 * p - 1).toNat (↑a * ↑p) * intervalIndicator n (2 * q - 1).toNat (↑a * ↑q) = ∑ k : ZMod n, ∑ l : ZMod n, normalizedDFT n (intervalIndicator n (2 * p - 1).toNat) k * normalizedDFT n (intervalIndicator n (2 * q - 1).toNat) l * ∑ a : (ZMod n)ˣ, ZMod.stdAddChar (k * (↑a * ↑p)) * ZMod.stdAddChar (l * (↑a * ↑q))

theorem character_product_simplify (n : ℕ) [NeZero n] (k l : ZMod n) (p q : ℤ) : ∑ a : (ZMod n)ˣ, ZMod.stdAddChar (k * (↑a * ↑p)) * ZMod.stdAddChar (l * (↑a * ↑q)) = ramanujanSum n (↑k.val * p + ↑l.val * q)

theorem counting_eq_fourier_ramanujan_sum (n : ℕ) (hn : 2 ≤ n) (p q : ℤ) (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) : ↑(countingFunctionS n p q) = ∑ k : ZMod n, ∑ l : ZMod n, normalizedDFT n (intervalIndicator n (2 * p - 1).toNat) k * normalizedDFT n (intervalIndicator n (2 * q - 1).toNat) l * ramanujanSum n (↑k.val * p + ↑l.val * q)

theorem largestPrimeFactor_pos_helper_fb (n : ℕ) (hn : 2 ≤ n) : ∃ (a : ℕ), n.primeFactors.max = ↑a ∧ 0 < a

theorem largestPrimeFactor_ge_two (n : ℕ) (hn : 2 ≤ n) : 2 ≤ largestPrimeFactor n

theorem ceil_log_ge_one (n : ℕ) (hn : 2 ≤ n) : 1 ≤ ⌈Real.log ↑n⌉₊

theorem bound_first_term (P R A : ℝ) (hP : 2 ≤ P) (hR : 1 ≤ R) (hA : 0 ≤ A) : A / (P - 1) ≤ 2 * R * A / P

theorem combine_error_terms_real (P R A : ℝ) (hP : 2 ≤ P) (hR : 1 ≤ R) (hA : 0 ≤ A) : A / (P - 1) + 7 * R * A / P ≤ 9 * R * A / P

noncomputable def errorTermEP0 (n : ℕ) [NeZero n] (p q : ℤ) : ℂ

The error term E_{P₀}(p, q): the contribution of frequencies (k, l) with P ^ (α - 1) ∣ k * p + l * q but P ^ α ∤ k * p + l * q to the Fourier expansion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def errorTermEPalpha (n : ℕ) [NeZero n] (p q : ℤ) : ℂ

The error term E_{P^α}(p, q): the contribution of nonzero frequencies (k, l) with P ^ α ∣ k * p + l * q to the Fourier expansion of countingFunctionS.

Equations

• One or more equations did not get rendered due to their size.

theorem zmod_mul_as_cast (n : ℕ) [NeZero n] (k : ZMod n) (p : ℤ) : k * ↑p = ↑(↑k.val * p)

theorem ramanujanSum_zero (n : ℕ) [NeZero n] : ramanujanSum n 0 = ↑n.totient

theorem card_intervalSet_filter (n : ℕ) [NeZero n] (m : ℕ) (hm2 : m < n) : {j : ZMod n | 1 ≤ j.val ∧ j.val ≤ m}.card = m

theorem sum_intervalIndicator_eq (n : ℕ) [NeZero n] (m : ℕ) (_hm1 : 1 ≤ m) (hm2 : m < n) : ∑ x : ZMod n, intervalIndicator n m x = ↑m

theorem normalizedDFT_intervalIndicator_zero (n : ℕ) [NeZero n] (m : ℕ) (hm1 : 1 ≤ m) (hm2 : m < n) : normalizedDFT n (intervalIndicator n m) 0 = ↑m / ↑n

theorem mp_lower_bound (p : ℤ) (hp : 1 ≤ p) : 1 ≤ (2 * p - 1).toNat

theorem mp_upper_bound (n : ℕ) (_hn : 2 ≤ n) (p q : ℤ) (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) : (2 * p - 1).toNat < n

theorem mp_valid (n : ℕ) (hn : 2 ≤ n) (p q : ℤ) (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) : 1 ≤ (2 * p - 1).toNat ∧ (2 * p - 1).toNat < n

theorem mq_valid (n : ℕ) (_hn : 2 ≤ n) (p q : ℤ) (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) : 1 ≤ (2 * q - 1).toNat ∧ (2 * q - 1).toNat < n

theorem zero_zero_term_eq_main (n : ℕ) [NeZero n] (hn : 2 ≤ n) (p q : ℤ) (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) : normalizedDFT n (intervalIndicator n (2 * p - 1).toNat) 0 * normalizedDFT n (intervalIndicator n (2 * q - 1).toNat) 0 * ramanujanSum n (↑(ZMod.val 0) * p + ↑(ZMod.val 0) * q) = ↑(2 * p - 1).toNat * ↑(2 * q - 1).toNat * ↑n.totient / ↑n ^ 2

theorem full_sum_split_zero_nonzero (n : ℕ) [NeZero n] (F : ZMod n → ZMod n → ℂ) : ∑ k : ZMod n, ∑ l : ZMod n, F k l = F 0 0 + ∑ k : ZMod n, ∑ l : ZMod n, if ¬(k = 0 ∧ l = 0) then F k l else 0

theorem sum_stdAddChar_mul_eq (n : ℕ) [NeZero n] (t : ℤ) : ∑ a : ZMod n, ZMod.stdAddChar (a * ↑t) = if ↑n ∣ t then ↑n else 0

theorem sum_filter_units_eq_sum_units (n : ℕ) [NeZero n] (f : ZMod n → ℂ) : ∑ a : ZMod n with IsUnit a, f a = ∑ u : (ZMod n)ˣ, f ↑u

theorem sum_eq_ramanujanSum_add_sum_nonunits (n : ℕ) [NeZero n] (t : ℤ) : ∑ a : ZMod n, ZMod.stdAddChar (a * ↑t) = ramanujanSum n t + ∑ a : ZMod n with ¬IsUnit a, ZMod.stdAddChar (a * ↑t)

theorem p_mul_pow_pred {p k : ℕ} (hk : 0 < k) : p * p ^ (k - 1) = p ^ k

noncomputable def nonunitFwd {p k : ℕ} (b : ZMod (p ^ (k - 1))) : ZMod (p ^ k)

Lift a residue mod p ^ (k - 1) to a (non-unit) residue mod p ^ k by multiplying by p.

Equations

• nonunitFwd b = ↑p * ↑b.val

noncomputable def nonunitBwd {p k : ℕ} (a : ZMod (p ^ k)) : ZMod (p ^ (k - 1))

Send a residue mod p ^ k to the residue mod p ^ (k - 1) got by dividing its value by p.

Equations

• nonunitBwd a = ↑(a.val / p)

theorem val_nonunitFwd {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : 0 < k) (b : ZMod (p ^ (k - 1))) : (nonunitFwd b).val = p * b.val

theorem nonunitFwd_not_isUnit {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : 0 < k) (b : ZMod (p ^ (k - 1))) : ¬IsUnit (nonunitFwd b)

theorem nonunitBwd_nonunitFwd {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : 0 < k) (b : ZMod (p ^ (k - 1))) : nonunitBwd (nonunitFwd b) = b

theorem p_dvd_val_of_not_isUnit {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (a : ZMod (p ^ k)) (ha : ¬IsUnit a) : p ∣ a.val

theorem val_div_p_lt {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : 0 < k) (a : ZMod (p ^ k)) : a.val / p < p ^ (k - 1)

theorem nonunitFwd_nonunitBwd {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : 0 < k) (a : ZMod (p ^ k)) (ha : a ∈ {a : ZMod (p ^ k) | ¬IsUnit a}) : nonunitFwd (nonunitBwd a) = a

theorem lhs_cast_eq {p : ℕ} [_hp : Fact (Nat.Prime p)] {k : ℕ} (_hk : 0 < k) (b : ZMod (p ^ (k - 1))) (t : ℤ) : nonunitFwd b * ↑t = ↑(↑p * ↑b.val * t)

theorem rhs_cast_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (_hk : 0 < k) (b : ZMod (p ^ (k - 1))) (t : ℤ) : b * ↑t = ↑(↑b.val * t)

theorem exponent_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : 0 < k) (b : ZMod (p ^ (k - 1))) (t : ℤ) : 2 * ↑Real.pi * Complex.I * ↑(↑p * ↑b.val * t) / ↑(p ^ k) = 2 * ↑Real.pi * Complex.I * ↑(↑b.val * t) / ↑(p ^ (k - 1))

theorem stdAddChar_nonunitFwd_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : 0 < k) (b : ZMod (p ^ (k - 1))) (t : ℤ) : ZMod.stdAddChar (nonunitFwd b * ↑t) = ZMod.stdAddChar (b * ↑t)

theorem sum_nonunits_eq_sum_lower {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : 0 < k) (t : ℤ) : ∑ a : ZMod (p ^ k) with ¬IsUnit a, ZMod.stdAddChar (a * ↑t) = ∑ b : ZMod (p ^ (k - 1)), ZMod.stdAddChar (b * ↑t)

theorem ramanujanSum_prime_pow_decomp {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : 0 < k) (t : ℤ) : ramanujanSum (p ^ k) t = ∑ a : ZMod (p ^ k), ZMod.stdAddChar (a * ↑t) - ∑ b : ZMod (p ^ (k - 1)), ZMod.stdAddChar (b * ↑t)

theorem ramanujanSum_prime_pow_eq_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : 0 < k) {t : ℤ} (ht : ¬↑p ^ (k - 1) ∣ t) : ramanujanSum (p ^ k) t = 0

theorem ramanujanSum_unit_shift (n : ℕ) [NeZero n] (u : (ZMod n)ˣ) (s : ZMod n) : ∑ a : (ZMod n)ˣ, ZMod.stdAddChar (↑a * (↑u * s)) = ∑ a : (ZMod n)ˣ, ZMod.stdAddChar (↑a * s)

theorem dvd_sub_mul_crt_val {n₁ n₂ : ℕ} [NeZero n₁] (h : n₁.Coprime n₂) (j : ℤ) : ↑n₁ ∣ j - ↑n₂ * ↑(↑j * (↑n₂)⁻¹).val

theorem crt_exponent_eq {n₁ n₂ : ℕ} [hn₁ : NeZero n₁] [hn₂ : NeZero n₂] (h : n₁.Coprime n₂) (j : ℤ) : ∃ (m : ℤ), 2 * ↑Real.pi * Complex.I * ↑j / ↑(n₁ * n₂) = 2 * ↑Real.pi * Complex.I * ↑(↑j * (↑n₂)⁻¹).val / ↑n₁ + 2 * ↑Real.pi * Complex.I * ↑(↑j * (↑n₁)⁻¹).val / ↑n₂ + ↑m * (2 * ↑Real.pi * Complex.I)

theorem stdAddChar_crt_split {n₁ n₂ : ℕ} [hn₁ : NeZero n₁] [hn₂ : NeZero n₂] (h : n₁.Coprime n₂) (x : ZMod (n₁ * n₂)) : ZMod.stdAddChar x = ZMod.stdAddChar (((ZMod.chineseRemainder h) x).1 * (↑n₂)⁻¹) * ZMod.stdAddChar (((ZMod.chineseRemainder h) x).2 * (↑n₁)⁻¹)

theorem crt_proj_fst {n₁ n₂ : ℕ} [_hn₁ : NeZero n₁] [_hn₂ : NeZero n₂] (h : n₁.Coprime n₂) (a₁ : (ZMod n₁)ˣ) (a₂ : (ZMod n₂)ˣ) (t : ℤ) : have e := (Units.mapEquiv (ZMod.chineseRemainder h).toMulEquiv).trans MulEquiv.prodUnits.toEquiv; ((ZMod.chineseRemainder h) (↑(e.symm (a₁, a₂)) * ↑t)).1 = ↑a₁ * ↑t

theorem crt_proj_snd {n₁ n₂ : ℕ} [_hn₁ : NeZero n₁] [_hn₂ : NeZero n₂] (h : n₁.Coprime n₂) (a₁ : (ZMod n₁)ˣ) (a₂ : (ZMod n₂)ˣ) (t : ℤ) : have e := (Units.mapEquiv (ZMod.chineseRemainder h).toMulEquiv).trans MulEquiv.prodUnits.toEquiv; ((ZMod.chineseRemainder h) (↑(e.symm (a₁, a₂)) * ↑t)).2 = ↑a₂ * ↑t

theorem ramanujanSum_crt_decomp {n₁ n₂ : ℕ} [hn₁ : NeZero n₁] [hn₂ : NeZero n₂] (h : n₁.Coprime n₂) (t : ℤ) : ∑ a : (ZMod (n₁ * n₂))ˣ, ZMod.stdAddChar (↑a * ↑t) = ∑ ab : (ZMod n₁)ˣ × (ZMod n₂)ˣ, ZMod.stdAddChar (↑ab.1 * ((↑n₂)⁻¹ * ↑t)) * ZMod.stdAddChar (↑ab.2 * ((↑n₁)⁻¹ * ↑t))

theorem ramanujanSum_absorb_inv {n m : ℕ} [NeZero n] (hc : m.Coprime n) (s : ZMod n) : ∑ a : (ZMod n)ˣ, ZMod.stdAddChar (↑a * ((↑m)⁻¹ * s)) = ∑ a : (ZMod n)ˣ, ZMod.stdAddChar (↑a * s)

theorem sum_prod_factor {n₁ n₂ : ℕ} [NeZero n₁] [NeZero n₂] (s₁ : ZMod n₁) (s₂ : ZMod n₂) : ∑ ab : (ZMod n₁)ˣ × (ZMod n₂)ˣ, ZMod.stdAddChar (↑ab.1 * s₁) * ZMod.stdAddChar (↑ab.2 * s₂) = (∑ a : (ZMod n₁)ˣ, ZMod.stdAddChar (↑a * s₁)) * ∑ a : (ZMod n₂)ˣ, ZMod.stdAddChar (↑a * s₂)

theorem ramanujanSum_multiplicative {n₁ n₂ : ℕ} [hn₁ : NeZero n₁] [hn₂ : NeZero n₂] (h : n₁.Coprime n₂) (t : ℤ) : ramanujanSum (n₁ * n₂) t = ramanujanSum n₁ t * ramanujanSum n₂ t

theorem largestPrimeFactor_mem_primeFactors (n : ℕ) (hn : 2 ≤ n) : largestPrimeFactor n ∈ n.primeFactors

theorem largest_prime_factor_multiplicity_pos (n : ℕ) (hn : 2 ≤ n) : n.factorization (largestPrimeFactor n) ≥ 1

theorem largest_prime_factor_prime (n : ℕ) (hn : 2 ≤ n) : Nat.Prime (largestPrimeFactor n)

theorem decompose_largest_prime (n : ℕ) (hn : 2 ≤ n) : have P := largestPrimeFactor n; have α := n.factorization P; have m := n / P ^ α; P ^ α * m = n ∧ (P ^ α).Coprime m ∧ 0 < m

theorem ramanujan_vanish_low_valuation (n : ℕ) [NeZero n] (hn : 2 ≤ n) (t : ℤ) (ht : ¬↑(largestPrimeFactor n) ^ (n.factorization (largestPrimeFactor n) - 1) ∣ t) : ramanujanSum n t = 0

theorem summand_eq_EP0_plus_EPalpha (n : ℕ) [NeZero n] (hn : 2 ≤ n) (p q : ℤ) (_hp : 1 ≤ p) (_hq : 1 ≤ q) (_hpq : ↑p + ↑q < ↑n / 2) (k l : ZMod n) : (if ¬(k = 0 ∧ l = 0) then normalizedDFT n (intervalIndicator n (2 * p - 1).toNat) k * normalizedDFT n (intervalIndicator n (2 * q - 1).toNat) l * ramanujanSum n (↑k.val * p + ↑l.val * q) else 0) = have P := largestPrimeFactor n; have alpha := n.factorization P; have P0 := P ^ (alpha - 1); have d := P ^ alpha; have fp := intervalIndicator n (2 * p - 1).toNat; have fq := intervalIndicator n (2 * q - 1).toNat; (if (k, l) ≠ (0, 0) ∧ ↑P0 ∣ ↑k.val * p + ↑l.val * q ∧ ¬↑d ∣ ↑k.val * p + ↑l.val * q then normalizedDFT n fp k * normalizedDFT n fq l * ramanujanSum n (↑k.val * p + ↑l.val * q) else 0) + if (k, l) ≠ (0, 0) ∧ ↑d ∣ ↑k.val * p + ↑l.val * q then normalizedDFT n fp k * normalizedDFT n fq l * ramanujanSum n (↑k.val * p + ↑l.val * q) else 0

theorem nonzero_sum_eq_EP0_plus_EPalpha (n : ℕ) [NeZero n] (hn : 2 ≤ n) (p q : ℤ) (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) : (∑ k : ZMod n, ∑ l : ZMod n, if ¬(k = 0 ∧ l = 0) then normalizedDFT n (intervalIndicator n (2 * p - 1).toNat) k * normalizedDFT n (intervalIndicator n (2 * q - 1).toNat) l * ramanujanSum n (↑k.val * p + ↑l.val * q) else 0) = errorTermEP0 n p q + errorTermEPalpha n p q

theorem fourier_sum_split_into_main_and_errors (n : ℕ) (hn : 2 ≤ n) (p q : ℤ) (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) : ∑ k : ZMod n, ∑ l : ZMod n, normalizedDFT n (intervalIndicator n (2 * p - 1).toNat) k * normalizedDFT n (intervalIndicator n (2 * q - 1).toNat) l * ramanujanSum n (↑k.val * p + ↑l.val * q) - ↑(2 * p - 1).toNat * ↑(2 * q - 1).toNat * ↑n.totient / ↑n ^ 2 = errorTermEP0 n p q + errorTermEPalpha n p q

theorem re_complex_lhs_eq_real_lhs (n : ℕ) (_hn : 2 ≤ n) (p q : ℤ) (_hp : 1 ≤ p) (_hq : 1 ≤ q) (_hpq : ↑p + ↑q < ↑n / 2) : (↑(countingFunctionS n p q) - ↑(2 * p - 1).toNat * ↑(2 * q - 1).toNat * ↑n.totient / ↑n ^ 2).re = ↑(countingFunctionS n p q) - ↑(2 * p - 1).toNat * ↑(2 * q - 1).toNat * ↑n.totient / ↑n ^ 2

theorem error_decomposition_from_complex (n : ℕ) (hn : 2 ≤ n) (p q : ℤ) (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) (h_complex : ↑(countingFunctionS n p q) - ↑(2 * p - 1).toNat * ↑(2 * q - 1).toNat * ↑n.totient / ↑n ^ 2 = errorTermEP0 n p q + errorTermEPalpha n p q) : ↑(countingFunctionS n p q) - ↑(2 * p - 1).toNat * ↑(2 * q - 1).toNat * ↑n.totient / ↑n ^ 2 = (errorTermEP0 n p q).re + (errorTermEPalpha n p q).re

theorem error_decomposition (n : ℕ) (hn : 2 ≤ n) (p q : ℤ) (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) : ↑(countingFunctionS n p q) - ↑(2 * p - 1).toNat * ↑(2 * q - 1).toNat * ↑n.totient / ↑n ^ 2 = (errorTermEP0 n p q).re + (errorTermEPalpha n p q).re

theorem double_sum_norms_eq_product (n : ℕ) [NeZero n] (f g : ZMod n → ℂ) : ∑ k : ZMod n, ∑ l : ZMod n, ‖f k‖ * ‖g l‖ = (∑ k : ZMod n, ‖f k‖) * ∑ l : ZMod n, ‖g l‖

theorem ramanujanSum_norm_le_totient (n : ℕ) [NeZero n] (t : ℤ) : ‖ramanujanSum n t‖ ≤ ↑n.totient

theorem ramanujanSum_prime_pow_eq_neg {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : 0 < k) {t : ℤ} (ht1 : ↑p ^ (k - 1) ∣ t) (ht2 : ¬↑p ^ k ∣ t) : ramanujanSum (p ^ k) t = -↑p ^ (k - 1)

theorem norm_ramanujanSum_prime_pow_eq_neg {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : 0 < k) {t : ℤ} (ht1 : ↑p ^ (k - 1) ∣ t) (ht2 : ¬↑p ^ k ∣ t) : ‖ramanujanSum (p ^ k) t‖ = ↑p ^ (k - 1)

theorem totient_div_prime_minus_one (n P α m : ℕ) (hP : Nat.Prime P) (hα : 0 < α) (hcop : (P ^ α).Coprime m) (hn : P ^ α * m = n) : ↑P ^ (α - 1) * ↑m.totient = ↑n.totient / (↑P - 1)

theorem ramanujanSum_EP0_norm_bound (n : ℕ) [NeZero n] (hn : 2 ≤ n) (t : ℤ) (hP0 : ↑(largestPrimeFactor n ^ (n.factorization (largestPrimeFactor n) - 1)) ∣ t) (hd : ¬↑(largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) ∣ t) : ‖ramanujanSum n t‖ ≤ ↑n.totient / (↑(largestPrimeFactor n) - 1)

theorem sum_split_zero (n : ℕ) [NeZero n] (f : ZMod n → ℝ) : ∑ k : ZMod n, f k = f 0 + ∑ k : ZMod n with k ≠ 0, f k

theorem indicator_formula (n : ℕ) [NeZero n] (m : ℕ) (j k : ZMod n) : ZMod.stdAddChar (-(j * k)) • intervalIndicator n m j = if j ∈ intervalSet n m then ZMod.stdAddChar (-(j * k)) else 0

theorem summand_reindex (n : ℕ) [NeZero n] (m : ℕ) (hm2 : m < n) (k : ZMod n) : (∑ j : ZMod n, if j ∈ intervalSet n m then ZMod.stdAddChar (-(j * k)) else 0) = ∑ t ∈ Finset.range m, ZMod.stdAddChar (-((↑t + 1) * k))

theorem character_multiplication_simplify (n : ℕ) [NeZero n] (t : ℕ) (k : ZMod n) : ZMod.stdAddChar (-((↑t + 1) * k)) = ZMod.stdAddChar (-k) ^ (t + 1)

theorem dft_intervalIndicator_eq_geom_sum (n : ℕ) [NeZero n] (m : ℕ) (hm2 : m < n) (k : ZMod n) : ZMod.dft (intervalIndicator n m) k = ∑ t ∈ Finset.range m, ZMod.stdAddChar (-k) ^ (t + 1)

theorem exponent_algebra (n : ℕ) (k : ZMod n) : 2 * ↑Real.pi * Complex.I * ↑(-↑k.val) / ↑n = Complex.I * ↑(-2 * Real.pi * ↑k.val / ↑n)

theorem stdAddChar_neg_eq_exp (n : ℕ) [NeZero n] (k : ZMod n) : ZMod.stdAddChar (-k) = Complex.exp (Complex.I * ↑(-2 * Real.pi * ↑k.val / ↑n))

theorem norm_one_sub_stdAddChar_eq (n : ℕ) [NeZero n] (k : ZMod n) : ‖1 - ZMod.stdAddChar (-k)‖ = 2 * |Real.sin (Real.pi * ↑k.val / ↑n)|

theorem abs_bound_helper (n : ℕ) (v : ℝ) (hn : 0 < ↑n) (hvn : v ≤ ↑n / 2) : Real.pi * v / ↑n ≤ Real.pi / 2

theorem two_v_div_n_le_abs_sin (n : ℕ) (v : ℝ) (hn : 0 < ↑n) (hv : 0 < v) (hvn : v ≤ ↑n / 2) : 2 * v / ↑n ≤ |Real.sin (Real.pi * v / ↑n)|

theorem abs_sin_val_eq_abs_sin_complement (n : ℕ) [NeZero n] (k : ZMod n) : |Real.sin (Real.pi * ↑k.val / ↑n)| = |Real.sin (Real.pi * (↑n - ↑k.val) / ↑n)|

theorem abs_sin_ge_two_min_div (n : ℕ) [NeZero n] (k : ZMod n) (hk : k ≠ 0) : 2 * min (↑k.val) (↑n - ↑k.val) / ↑n ≤ |Real.sin (Real.pi * ↑k.val / ↑n)|

theorem geom_sum_shift_eq (r : ℂ) (hr_ne : r ≠ 1) (m : ℕ) : ∑ t ∈ Finset.range m, r ^ (t + 1) = r * (r ^ m - 1) / (r - 1)

theorem norm_pow_sub_one_le_two (r : ℂ) (hr_norm : ‖r‖ = 1) (m : ℕ) : ‖r ^ m - 1‖ ≤ 2

theorem norm_geom_sum_le (r : ℂ) (hr_ne : r ≠ 1) (hr_norm : ‖r‖ = 1) (m : ℕ) : ‖∑ t ∈ Finset.range m, r ^ (t + 1)‖ ≤ 2 / ‖1 - r‖

theorem norm_one_sub_stdAddChar_lower_bound (n : ℕ) [NeZero n] (k : ZMod n) (hk : k ≠ 0) : 4 * min (↑k.val) (↑n - ↑k.val) / ↑n ≤ ‖1 - ZMod.stdAddChar (-k)‖

theorem stdAddChar_ne_one (n : ℕ) [NeZero n] (k : ZMod n) (hk : k ≠ 0) : ZMod.stdAddChar (-k) ≠ 1

theorem norm_stdAddChar_eq_one (n : ℕ) [NeZero n] (k : ZMod n) : ‖ZMod.stdAddChar (-k)‖ = 1

theorem normalizedDFT_intervalIndicator_nonzero_bound (n : ℕ) [NeZero n] (m : ℕ) (_hm1 : 1 ≤ m) (hm2 : m < n) (k : ZMod n) (hk : k ≠ 0) : ‖normalizedDFT n (intervalIndicator n m) k‖ ≤ 1 / (2 * min (↑k.val) (↑n - ↑k.val))

theorem sum_nonzero_reindex (n : ℕ) [NeZero n] (hn : 2 ≤ n) : ∑ k : ZMod n with k ≠ 0, 1 / (2 * min (↑k.val) (↑n - ↑k.val)) = ∑ t ∈ Finset.Icc 1 (n - 1), 1 / (2 * min (↑t) (↑n - ↑t))

theorem first_half_eq (N : ℕ) (_hN : 1 ≤ N) : ∑ t ∈ Finset.Icc 1 N, 1 / (2 * min (↑t) (2 * ↑N + 1 - ↑t)) = ∑ t ∈ Finset.Icc 1 N, 1 / (2 * ↑t)

theorem summand_min_eq (N : ℕ) (_hN : 1 ≤ N) (t : ℕ) (ht : t ∈ Finset.Icc (N + 1) (2 * N)) : 1 / (2 * min (↑t) (2 * ↑N + 1 - ↑t)) = 1 / (2 * (2 * ↑N + 1 - ↑t))

theorem second_half_min_simplify (N : ℕ) (hN : 1 ≤ N) : ∑ t ∈ Finset.Icc (N + 1) (2 * N), 1 / (2 * min (↑t) (2 * ↑N + 1 - ↑t)) = ∑ t ∈ Finset.Icc (N + 1) (2 * N), 1 / (2 * (2 * ↑N + 1 - ↑t))

theorem second_half_reindex (N : ℕ) (_hN : 1 ≤ N) : ∑ t ∈ Finset.Icc (N + 1) (2 * N), 1 / (2 * (2 * ↑N + 1 - ↑t)) = ∑ u ∈ Finset.Icc 1 N, 1 / (2 * ↑u)

theorem second_half_eq (N : ℕ) (hN : 1 ≤ N) : ∑ t ∈ Finset.Icc (N + 1) (2 * N), 1 / (2 * min (↑t) (2 * ↑N + 1 - ↑t)) = ∑ u ∈ Finset.Icc 1 N, 1 / (2 * ↑u)

theorem combine_halves (N : ℕ) : ∑ u ∈ Finset.Icc 1 N, 1 / (2 * ↑u) + ∑ u ∈ Finset.Icc 1 N, 1 / (2 * ↑u) = ∑ u ∈ Finset.Icc 1 N, (↑u)⁻¹

theorem symmetric_sum_odd (N : ℕ) (hN : 1 ≤ N) : ∑ t ∈ Finset.Icc 1 (2 * N), 1 / (2 * min (↑t) (2 * ↑N + 1 - ↑t)) = ∑ u ∈ Finset.Icc 1 N, (↑u)⁻¹

theorem Icc_split_three (N : ℕ) (hN : 2 ≤ N) : Finset.Icc 1 (2 * N - 1) = Finset.Icc 1 (N - 1) ∪ {N} ∪ Finset.Icc (N + 1) (2 * N - 1)

theorem Icc_disjoint_high (N : ℕ) (hN : 2 ≤ N) : Disjoint (Finset.Icc 1 (N - 1) ∪ {N}) (Finset.Icc (N + 1) (2 * N - 1))

theorem Icc_disjoint_mid (N : ℕ) (hN : 2 ≤ N) : Disjoint (Finset.Icc 1 (N - 1)) {N}

theorem sum_region_A (N : ℕ) (hN : 2 ≤ N) : ∑ t ∈ Finset.Icc 1 (N - 1), 1 / (2 * min (↑t) (2 * ↑N - ↑t)) = ∑ t ∈ Finset.Icc 1 (N - 1), 1 / (2 * ↑t)

theorem min_midpoint (N : ℕ) : min (↑N) (2 * ↑N - ↑N) = ↑N

theorem min_eq_complement_in_region_C (N t : ℕ) (ht : t ∈ Finset.Icc (N + 1) (2 * N - 1)) : min (↑t) (2 * ↑N - ↑t) = 2 * ↑N - ↑t

theorem sum_region_C (N : ℕ) (hN : 2 ≤ N) : ∑ t ∈ Finset.Icc (N + 1) (2 * N - 1), 1 / (2 * min (↑t) (2 * ↑N - ↑t)) = ∑ u ∈ Finset.Icc 1 (N - 1), 1 / (2 * ↑u)

theorem symmetric_sum_even (N : ℕ) (hN : 1 ≤ N) : ∑ t ∈ Finset.Icc 1 (2 * N - 1), 1 / (2 * min (↑t) (2 * ↑N - ↑t)) = ∑ u ∈ Finset.Icc 1 (N - 1), (↑u)⁻¹ + 1 / (2 * ↑N)

theorem ratio_rewrite (u : ℕ) (hu : 1 ≤ u) : (2 * ↑u + 1) / (2 * ↑u - 1) = 1 + 2 / (2 * ↑u - 1)

theorem pade_algebraic_identity (u : ℕ) (hu : 1 ≤ u) : 2 * (2 / (2 * ↑u - 1)) / (2 / (2 * ↑u - 1) + 2) = (↑u)⁻¹

theorem inv_le_log_ratio (u : ℕ) (hu : 1 ≤ u) : (↑u)⁻¹ ≤ Real.log ((2 * ↑u + 1) / (2 * ↑u - 1))

theorem telescoping_log_sum (N : ℕ) (hN : 1 ≤ N) : ∑ u ∈ Finset.Icc 1 N, Real.log ((2 * ↑u + 1) / (2 * ↑u - 1)) = Real.log (2 * ↑N + 1)

theorem harmonic_Icc_le_log_odd (N : ℕ) (hN : 1 ≤ N) : ∑ u ∈ Finset.Icc 1 N, (↑u)⁻¹ ≤ Real.log (2 * ↑N + 1)

theorem one_sub_inv_ratio_eq (N : ℕ) (hN : 1 ≤ N) : 1 - (2 * ↑N / (2 * ↑N - 1))⁻¹ = 1 / (2 * ↑N)

theorem inv_two_N_le_log_ratio (N : ℕ) (hN : 1 ≤ N) : 1 / (2 * ↑N) ≤ Real.log (2 * ↑N / (2 * ↑N - 1))

theorem half_le_log_two : 1 / 2 ≤ Real.log 2

theorem harmonic_Icc_plus_remainder_le_log_even (N : ℕ) (hN : 1 ≤ N) : ∑ u ∈ Finset.Icc 1 (N - 1), (↑u)⁻¹ + 1 / (2 * ↑N) ≤ Real.log (2 * ↑N)

theorem symmetric_harmonic_sum_le_log (n : ℕ) (hn : 2 ≤ n) : ∑ t ∈ Finset.Icc 1 (n - 1), 1 / (2 * min (↑t) (↑n - ↑t)) ≤ Real.log ↑n

theorem fourier_intervalIndicator_l1_bound (n : ℕ) [NeZero n] (hn : 2 ≤ n) (m : ℕ) (hm1 : 1 ≤ m) (hm2 : m < n) : ∑ k : ZMod n, ‖normalizedDFT n (intervalIndicator n m) k‖ ≤ 1 + Real.log ↑n

theorem summand_norm_bound (n : ℕ) [NeZero n] (hn : 2 ≤ n) (p q : ℤ) (k l : ZMod n) : ‖if (k, l) ≠ (0, 0) ∧ ↑(largestPrimeFactor n ^ (n.factorization (largestPrimeFactor n) - 1)) ∣ ↑k.val * p + ↑l.val * q ∧ ¬↑(largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) ∣ ↑k.val * p + ↑l.val * q then normalizedDFT n (intervalIndicator n (2 * p - 1).toNat) k * normalizedDFT n (intervalIndicator n (2 * q - 1).toNat) l * ramanujanSum n (↑k.val * p + ↑l.val * q) else 0‖ ≤ ↑n.totient / (↑(largestPrimeFactor n) - 1) * (‖normalizedDFT n (intervalIndicator n (2 * p - 1).toNat) k‖ * ‖normalizedDFT n (intervalIndicator n (2 * q - 1).toNat) l‖)

theorem norm_errorTermEP0_le_double_sum (n : ℕ) [NeZero n] (hn : 2 ≤ n) (p q : ℤ) (_hp : 1 ≤ p) (_hq : 1 ≤ q) (_hpq : ↑p + ↑q < ↑n / 2) : ‖errorTermEP0 n p q‖ ≤ ↑n.totient / (↑(largestPrimeFactor n) - 1) * ∑ k : ZMod n, ∑ l : ZMod n, ‖normalizedDFT n (intervalIndicator n (2 * p - 1).toNat) k‖ * ‖normalizedDFT n (intervalIndicator n (2 * q - 1).toNat) l‖

theorem norm_errorTermEP0_le_product (n : ℕ) [NeZero n] (hn : 2 ≤ n) (p q : ℤ) (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) : ‖errorTermEP0 n p q‖ ≤ (↑n.totient / (↑(largestPrimeFactor n) - 1) * ∑ k : ZMod n, ‖normalizedDFT n (intervalIndicator n (2 * p - 1).toNat) k‖) * ∑ l : ZMod n, ‖normalizedDFT n (intervalIndicator n (2 * q - 1).toNat) l‖

theorem norm_errorTermEP0_le (n : ℕ) [NeZero n] (hn : 2 ≤ n) (p q : ℤ) (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) : ‖errorTermEP0 n p q‖ ≤ ↑n.totient * (1 + Real.log ↑n) ^ 2 / (↑(largestPrimeFactor n) - 1)

theorem error_EP0_universal_bound (n : ℕ) (hn : 2 ≤ n) (p q : ℤ) (hp : 1 ≤ p) (hq : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) : |(errorTermEP0 n p q).re| ≤ ↑n.totient * (1 + Real.log ↑n) ^ 2 / (↑(largestPrimeFactor n) - 1)

theorem summand_norm_le_aux (n : ℕ) [NeZero n] (_p _q : ℤ) (k l : ZMod n) (fp fq : ZMod n → ℂ) (t : ℤ) (cond : Prop) [Decidable cond] : ‖if cond then normalizedDFT n fp k * normalizedDFT n fq l * ramanujanSum n t else 0‖ ≤ ↑n.totient * if cond then ‖normalizedDFT n fp k‖ * ‖normalizedDFT n fq l‖ else 0

theorem summand_norm_le (n : ℕ) [NeZero n] (p q : ℤ) (k l : ZMod n) : have P := largestPrimeFactor n; have alpha := n.factorization P; have d := P ^ alpha; have fp := intervalIndicator n (2 * p - 1).toNat; have fq := intervalIndicator n (2 * q - 1).toNat; ‖if (k, l) ≠ (0, 0) ∧ ↑d ∣ ↑k.val * p + ↑l.val * q then normalizedDFT n fp k * normalizedDFT n fq l * ramanujanSum n (↑k.val * p + ↑l.val * q) else 0‖ ≤ ↑n.totient * if (k, l) ≠ (0, 0) ∧ ↑(largestPrimeFactor n) ^ n.factorization (largestPrimeFactor n) ∣ ↑k.val * p + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n (2 * p - 1).toNat) k‖ * ‖normalizedDFT n (intervalIndicator n (2 * q - 1).toNat) l‖ else 0

theorem errorTermEPalpha_norm_le_totient_mul (n : ℕ) [NeZero n] (p q : ℤ) : ‖errorTermEPalpha n p q‖ ≤ ↑n.totient * ∑ k : ZMod n, ∑ l : ZMod n, if (k, l) ≠ (0, 0) ∧ ↑(largestPrimeFactor n) ^ n.factorization (largestPrimeFactor n) ∣ ↑k.val * p + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n (2 * p - 1).toNat) k‖ * ‖normalizedDFT n (intervalIndicator n (2 * q - 1).toNat) l‖ else 0

theorem d_pos (n : ℕ) (hn : 2 ≤ n) : 0 < largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)

theorem val_unitOfCoprime_eq_mod (d a : ℕ) (hcoprime : a.Coprime d) : (↑(ZMod.unitOfCoprime a hcoprime)).val = a % d

theorem combine_cases_arithmetic (C L d : ℝ) : C * (5 * L / d) + C * (L / d) = C * (6 * L / d)

theorem min_val_pos (n : ℕ) [NeZero n] (k : ZMod n) (hk : k ≠ 0) : 0 < min (↑k.val) (↑n - ↑k.val)

theorem sum_exchange_weighted (n d : ℕ) [NeZero n] [NeZero d] (mq : ℕ) (q : ℤ) : (∑ u : (ZMod d)ˣ, ∑ k : ZMod n, ∑ l : ZMod n, if k ≠ 0 ∧ ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0) = ∑ k : ZMod n, ∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if k ≠ 0 ∧ ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0

theorem outer_sum_split (n : ℕ) [NeZero n] (G : ZMod n → ℝ) : ∑ k : ZMod n, G k = G 0 + ∑ k : ZMod n with k ≠ 0, G k

theorem zero_term_vanishes (n d : ℕ) [NeZero n] [NeZero d] (mq : ℕ) (q : ℤ) : (∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if 0 ≠ 0 ∧ ↑d ∣ ↑(ZMod.val 0) * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑(ZMod.val 0)) (↑n - ↑(ZMod.val 0))) else 0) = 0

theorem summand_congr_on_filter (n d : ℕ) [NeZero n] [NeZero d] (mq : ℕ) (q : ℤ) (k : ZMod n) (hk : k ≠ 0) : (∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if k ≠ 0 ∧ ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0) = ∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0

theorem sum_restrict_to_nonzero (n d : ℕ) [NeZero n] [NeZero d] (mq : ℕ) (q : ℤ) : (∑ k : ZMod n, ∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if k ≠ 0 ∧ ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0) = ∑ k : ZMod n with k ≠ 0, ∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0

theorem split_nonzero_by_divisibility (n d : ℕ) [NeZero n] [NeZero d] (mq : ℕ) (q : ℤ) : (∑ k : ZMod n with k ≠ 0, ∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0) = (∑ k : ZMod n with k ≠ 0 ∧ ¬d ∣ k.val, ∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0) + ∑ k : ZMod n with k ≠ 0 ∧ d ∣ k.val, ∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0

theorem k_sum_split_by_d_divisibility (n d : ℕ) [NeZero n] [NeZero d] (mq : ℕ) (q : ℤ) : (∑ k : ZMod n, ∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if k ≠ 0 ∧ ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0) = (∑ k : ZMod n with k ≠ 0 ∧ ¬d ∣ k.val, ∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0) + ∑ k : ZMod n with k ≠ 0 ∧ d ∣ k.val, ∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0

theorem factor_weight_from_double_sum (n d : ℕ) [NeZero n] [NeZero d] (mq : ℕ) (q : ℤ) (k : ZMod n) (hk : k ≠ 0) : (∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0) = (∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) / (2 * min (↑k.val) (↑n - ↑k.val))

theorem dvd_simplify_multiple_case (n d : ℕ) [NeZero n] [NeZero d] (k l : ZMod n) (u : (ZMod d)ˣ) (q : ℤ) (hdk : d ∣ k.val) (hq_coprime_d : q.gcd ↑d = 1) : ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q ↔ ↑d ∣ ↑l.val

theorem mq_bounds (n : ℕ) (_hn : 2 ≤ n) (q : ℤ) (hq_pos : 1 ≤ q) (hq_bound : ↑q < ↑n / 2) : 1 ≤ (2 * q - 1).toNat ∧ (2 * q - 1).toNat < n

theorem symmetric_sum_le_one_plus_log (n d : ℕ) (hn : 2 ≤ n) (_hd_dvd : d ∣ n) (_hd_pos : 0 < d) : ∑ j ∈ Finset.Icc 1 (n / d - 1), 1 / (2 * min (↑j) (↑(n / d) - ↑j)) ≤ 1 + Real.log ↑n

theorem mul_lt_of_mem_Icc (n d : ℕ) (_hd_dvd : d ∣ n) (hd_pos : 0 < d) (j : ℕ) (hj : j ∈ Finset.Icc 1 (n / d - 1)) : j * d < n

theorem fwd_mem (n d : ℕ) [NeZero n] (hd_dvd : d ∣ n) (hd_pos : 0 < d) (j : ℕ) (hj : j ∈ Finset.Icc 1 (n / d - 1)) : ↑(j * d) ∈ {k : ZMod n | k ≠ 0 ∧ d ∣ k.val}

theorem bwd_mem (n d : ℕ) [NeZero n] (hd_dvd : d ∣ n) (hd_pos : 0 < d) (k : ZMod n) (hk : k ∈ {k : ZMod n | k ≠ 0 ∧ d ∣ k.val}) : k.val / d ∈ Finset.Icc 1 (n / d - 1)

theorem left_inv (n d : ℕ) (hd_dvd : d ∣ n) (hd_pos : 0 < d) (j : ℕ) (hj : j ∈ Finset.Icc 1 (n / d - 1)) : (↑(j * d)).val / d = j

theorem right_inv (n d : ℕ) [NeZero n] (_hd_dvd : d ∣ n) (_hd_pos : 0 < d) (k : ZMod n) (hk : k ∈ {k : ZMod n | k ≠ 0 ∧ d ∣ k.val}) : ↑(k.val / d * d) = k

theorem div_lt_div_of_dvd (n d : ℕ) [NeZero n] (hd_dvd : d ∣ n) (k : ZMod n) (_hd_dvd_val : d ∣ k.val) : k.val / d < n / d

theorem min_factor_d_nat (n d : ℕ) [NeZero n] (hd_dvd : d ∣ n) (k : ZMod n) (_hk_ne : k ≠ 0) (hd_dvd_val : d ∣ k.val) : min (↑k.val) (↑n - ↑k.val) = ↑d * min (↑(k.val / d)) (↑(n / d) - ↑(k.val / d))

theorem div_factor_d (d M : ℝ) (hd : d ≠ 0) : 1 / (2 * (d * M)) = 1 / d * (1 / (2 * M))

theorem summand_eq_via_bwd (n d : ℕ) [NeZero n] [NeZero d] (hd_dvd : d ∣ n) (_hd_pos : 0 < d) (k : ZMod n) (hk : k ∈ {k : ZMod n | k ≠ 0 ∧ d ∣ k.val}) : have N := n / d; have j := k.val / d; 1 / (2 * min (↑k.val) (↑n - ↑k.val)) = 1 / ↑d * (1 / (2 * min (↑j) (↑N - ↑j)))

theorem reindex_multiples_of_d (n d : ℕ) [NeZero n] [NeZero d] (hd_dvd : d ∣ n) (hd_pos : 0 < d) : have N := n / d; ∑ k : ZMod n with k ≠ 0 ∧ d ∣ k.val, 1 / (2 * min (↑k.val) (↑n - ↑k.val)) = 1 / ↑d * ∑ j ∈ Finset.Icc 1 (N - 1), 1 / (2 * min (↑j) (↑N - ↑j))

theorem weight_sum_multiples_of_d_bound (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd_dvd : d ∣ n) (hd_pos : 0 < d) : ∑ k : ZMod n with k ≠ 0 ∧ d ∣ k.val, 1 / (2 * min (↑k.val) (↑n - ↑k.val)) ≤ (1 + Real.log ↑n) / ↑d

theorem d_dvd_n (n : ℕ) (_hn : 2 ≤ n) : largestPrimeFactor n ^ n.factorization (largestPrimeFactor n) ∣ n

theorem coprimality_q_d (n : ℕ) (_hn : 2 ≤ n) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) (d : ℕ) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) : q.gcd ↑d = 1

theorem simplify_u_sum_when_d_dvd_k (n d : ℕ) [NeZero n] [NeZero d] (mq : ℕ) (q : ℤ) (k : ZMod n) (hdk : d ∣ k.val) (hq_coprime_d : q.gcd ↑d = 1) : (∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) = ↑(Fintype.card (ZMod d)ˣ) * ∑ l : ZMod n, if ↑d ∣ ↑l.val then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0

theorem restricted_fourier_mass_le (n d : ℕ) [NeZero n] (hn : 2 ≤ n) (mq : ℕ) (hmq1 : 1 ≤ mq) (hmq2 : mq < n) : (∑ l : ZMod n, if ↑d ∣ ↑l.val then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) ≤ 1 + Real.log ↑n

theorem triple_sum_eq_card_times_product (n d : ℕ) [NeZero n] [NeZero d] (_hn : 2 ≤ n) (mq : ℕ) (q : ℤ) (hq_coprime_d : q.gcd ↑d = 1) (_hd_dvd : d ∣ n) : (∑ k : ZMod n with k ≠ 0 ∧ d ∣ k.val, ∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0) ≤ (↑(Fintype.card (ZMod d)ˣ) * ∑ l : ZMod n, if ↑d ∣ ↑l.val then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) * ∑ k : ZMod n with k ≠ 0 ∧ d ∣ k.val, 1 / (2 * min (↑k.val) (↑n - ↑k.val))

theorem triple_sum_bound_via_factoring (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) (_hq_pos : 1 ≤ q) (_hq_bound : ↑q < ↑n / 2) (mq : ℕ) (_hmq : mq = (2 * q - 1).toNat) (hmq1 : 1 ≤ mq) (hmq2 : mq < n) : (∑ k : ZMod n with k ≠ 0 ∧ d ∣ k.val, ∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0) ≤ ↑(Fintype.card (ZMod d)ˣ) * ((1 + Real.log ↑n) ^ 2 / ↑d)

theorem multiple_d_weighted_bound (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) (hq_pos : 1 ≤ q) (hq_bound : ↑q < ↑n / 2) (mq : ℕ) (hmq : mq = (2 * q - 1).toNat) : (∑ k : ZMod n with k ≠ 0 ∧ d ∣ k.val, ∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0) ≤ ↑(Fintype.card (ZMod d)ˣ) * ((1 + Real.log ↑n) ^ 2 / ↑d)

theorem weight_nonneg (n : ℕ) [NeZero n] (k : ZMod n) (hk : k ≠ 0) : 0 ≤ 2 * min (↑k.val) (↑n - ↑k.val)

theorem weight_sum_le_log (n d : ℕ) [NeZero n] (hn : 2 ≤ n) : ∑ k : ZMod n with k ≠ 0 ∧ ¬d ∣ k.val, 1 / (2 * min (↑k.val) (↑n - ↑k.val)) ≤ 1 + Real.log ↑n

theorem const_bound_nonneg (n d : ℕ) [NeZero d] (_hn : 2 ≤ n) : 0 ≤ ↑(Fintype.card (ZMod d)ˣ) * (5 * (1 + Real.log ↑n) / ↑d)

theorem sum_eq_two_mul_half_sum (M : ℕ) : ∑ t ∈ Finset.Icc 1 (M - 1), 1 / min (↑t) (↑M - ↑t) = 2 * ∑ t ∈ Finset.Icc 1 (M - 1), 1 / (2 * min (↑t) (↑M - ↑t))

theorem harmonic_min_sum_le_two_log (M n : ℕ) (hM : 2 ≤ M) (hMn : M ≤ n) : ∑ t ∈ Finset.Icc 1 (M - 1), 1 / min (↑t) (↑M - ↑t) ≤ 2 * (1 + Real.log ↑n)

theorem d_ge_P (n : ℕ) (hn : 2 ≤ n) : largestPrimeFactor n ≤ largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)

theorem one_plus_log_nonneg (n : ℕ) (hn : 2 ≤ n) : 0 ≤ 1 + Real.log ↑n

theorem key_val_eq (d k_val : ℕ) (hcop : k_val.Coprime d) (u : (ZMod d)ˣ) : have k_unit := ZMod.unitOfCoprime k_val hcop; (↑(k_unit * u)).val = k_val * (↑u).val % d

theorem coprime_case_sum_eq (d : ℕ) [NeZero d] (k_val : ℕ) (hcop : k_val.Coprime d) : ∑ u : (ZMod d)ˣ, 1 / min (↑(k_val * (↑u).val % d)) (↑d - ↑(k_val * (↑u).val % d)) = ∑ u : (ZMod d)ˣ, 1 / min (↑(↑u).val) (↑d - ↑(↑u).val)

theorem units_val_injective (d : ℕ) [NeZero d] : Function.Injective fun (u : (ZMod d)ˣ) => (↑u).val

theorem unit_val_mem_Icc (d : ℕ) [NeZero d] (hd : 2 ≤ d) (u : (ZMod d)ˣ) : (↑u).val ∈ Finset.Icc 1 (d - 1)

theorem units_sum_summand_nonneg (d t : ℕ) (ht : t ∈ Finset.Icc 1 (d - 1)) : 0 ≤ 1 / min (↑t) (↑d - ↑t)

theorem units_sum_le_Icc_sum (d : ℕ) [NeZero d] (hd : 2 ≤ d) : ∑ u : (ZMod d)ˣ, 1 / min (↑(↑u).val) (↑d - ↑(↑u).val) ≤ ∑ t ∈ Finset.Icc 1 (d - 1), 1 / min (↑t) (↑d - ↑t)

theorem nat_mul_mod_right (a b n : ℕ) : a * b % n = a * (b % n) % n

theorem kval_mul_unit_mod_eq_pv_mul (d p : ℕ) (_hp : Nat.Prime p) (α : ℕ) (_hα : 1 ≤ α) (hd_eq : d = p ^ α) (k_val : ℕ) (_hk_nd : ¬d ∣ k_val) (_hk_dvd_p : p ∣ k_val) (v : ℕ) (_hv_pos : 1 ≤ v) (hv_lt : v < α) (hv_val : p ^ v ∣ k_val) (_hv_max : ¬p ^ (v + 1) ∣ k_val) (u : (ZMod d)ˣ) : k_val * (↑u).val % d = p ^ v * (k_val / p ^ v * ((↑u).val % p ^ (α - v)) % p ^ (α - v))

theorem not_p_dvd_div_pow_1 (p : ℕ) (_hp : Nat.Prime p) (k_val v : ℕ) (hv_val : p ^ v ∣ k_val) (hv_max : ¬p ^ (v + 1) ∣ k_val) : ¬p ∣ k_val / p ^ v

theorem dvd_of_dvd_mod_of_dvd (p a m : ℕ) (hpm : p ∣ m) (hpr : p ∣ a % m) : p ∣ a

theorem not_p_dvd_unit_val_mod (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (hα : 1 ≤ α) (v : ℕ) (hv_lt : v < α) (u : (ZMod (p ^ α))ˣ) : ¬p ∣ (↑u).val % p ^ (α - v)

theorem mul_not_dvd_of_not_dvd (p a b : ℕ) (hp : Nat.Prime p) (ha : ¬p ∣ a) (hb : ¬p ∣ b) : ¬p ∣ a * b

theorem mod_ne_zero_of_not_dvd_prime (p : ℕ) (_hp : Nat.Prime p) (k : ℕ) (hk : 1 ≤ k) (n : ℕ) (hn : ¬p ∣ n) : n % p ^ k ≠ 0

theorem reduced_product_mod_ne_zero (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (hα : 1 ≤ α) (k_val v : ℕ) (hv_pos : 1 ≤ v) (hv_lt : v < α) (hv_val : p ^ v ∣ k_val) (hv_max : ¬p ^ (v + 1) ∣ k_val) (u : (ZMod (p ^ α))ˣ) : k_val / p ^ v * ((↑u).val % p ^ (α - v)) % p ^ (α - v) ≠ 0

theorem min_pv_factor (p v M x : ℕ) (_hx_pos : 0 < x) (_hx_lt : x < M) : min (↑(p ^ v * x)) (↑(p ^ v * M) - ↑(p ^ v * x)) = ↑(p ^ v) * min (↑x) (↑M - ↑x)

theorem fiber_element_lt (p : ℕ) (hp : Nat.Prime p) (α v : ℕ) (hv_lt : v < α) (s : ℕ) (hs_lt : s < p ^ (α - v)) (j : ℕ) (hj : j < p ^ v) : s + j * p ^ (α - v) < p ^ α

theorem not_p_dvd_fiber_element (p : ℕ) (hp : Nat.Prime p) (α v : ℕ) (hv_lt : v < α) (s : ℕ) (hs_cop : s.Coprime p) (j : ℕ) : ¬p ∣ s + j * p ^ (α - v)

theorem fiber_element_coprime (p : ℕ) (hp : Nat.Prime p) (α v : ℕ) (hv_lt : v < α) (s : ℕ) (hs_cop : s.Coprime p) (j : ℕ) : (s + j * p ^ (α - v)).Coprime (p ^ α)

theorem fiber_element_mod_eq (p α v s : ℕ) (hs_lt : s < p ^ (α - v)) (j : ℕ) : (s + j * p ^ (α - v)) % p ^ (α - v) = s

theorem fiber_index_lt (p : ℕ) (_hp : Nat.Prime p) (α v : ℕ) (hv_lt : v < α) [NeZero (p ^ α)] (s : ℕ) (_hs_lt : s < p ^ (α - v)) (u : (ZMod (p ^ α))ˣ) (hu : (↑u).val % p ^ (α - v) = s) : ((↑u).val - s) / p ^ (α - v) < p ^ v

theorem fiber_reconstruct (M s n : ℕ) (hn : n % M = s) (hs_le : s ≤ n) : s + (n - s) / M * M = n

theorem fiber_fwd_bwd (p : ℕ) (hp : Nat.Prime p) (α v : ℕ) (hv_lt : v < α) (s : ℕ) (hs_lt : s < p ^ (α - v)) (hs_cop : s.Coprime p) (j : ℕ) (hj : j < p ^ v) : let a := s + j * p ^ (α - v); have hcop := ⋯; ((↑(ZMod.unitOfCoprime a hcop)).val - s) / p ^ (α - v) = j

theorem fiber_bwd_fwd (p : ℕ) (hp : Nat.Prime p) (α v : ℕ) (hv_lt : v < α) [NeZero (p ^ α)] (s : ℕ) (_hs_lt : s < p ^ (α - v)) (hs_cop : s.Coprime p) (u : (ZMod (p ^ α))ˣ) (hu : (↑u).val % p ^ (α - v) = s) : have idx := ((↑u).val - s) / p ^ (α - v); let a := s + idx * p ^ (α - v); have hcop := ⋯; ZMod.unitOfCoprime a hcop = u

theorem fiber_fwd_mem (p : ℕ) (hp : Nat.Prime p) (α v : ℕ) (hv_lt : v < α) (s : ℕ) (hs_lt : s < p ^ (α - v)) (hs_cop : s.Coprime p) (j : ℕ) (hj : j < p ^ v) : let a := s + j * p ^ (α - v); have hcop := ⋯; have u := ZMod.unitOfCoprime a hcop; (↑u).val % p ^ (α - v) = s

theorem projection_fiber_card (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (_hα : 1 ≤ α) (v : ℕ) (_hv_pos : 1 ≤ v) (hv_lt : v < α) [NeZero (p ^ α)] (s : ℕ) (hs_lt : s < p ^ (α - v)) (hs_cop : s.Coprime p) : {u : (ZMod (p ^ α))ˣ | (↑u).val % p ^ (α - v) = s}.card = p ^ v

theorem reduced_product_mod_lt (p : ℕ) (_hp : Nat.Prime p) (α v : ℕ) (_hv_lt : v < α) [NeZero (p ^ (α - v))] (k_val : ℕ) (u : (ZMod (p ^ α))ˣ) : k_val / p ^ v * ((↑u).val % p ^ (α - v)) % p ^ (α - v) < p ^ (α - v)

theorem summand_rewrite (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (hα : 1 ≤ α) (k_val : ℕ) (hk_nd : ¬p ^ α ∣ k_val) (hk_dvd_p : p ∣ k_val) (v : ℕ) (hv_pos : 1 ≤ v) (hv_lt : v < α) (hv_val : p ^ v ∣ k_val) (hv_max : ¬p ^ (v + 1) ∣ k_val) [NeZero (p ^ α)] [NeZero (p ^ (α - v))] : ∑ u : (ZMod (p ^ α))ˣ, 1 / min (↑(k_val * (↑u).val % p ^ α)) (↑(p ^ α) - ↑(k_val * (↑u).val % p ^ α)) = ∑ u : (ZMod (p ^ α))ˣ, 1 / (↑(p ^ v) * min (↑(k_val / p ^ v * ((↑u).val % p ^ (α - v)) % p ^ (α - v))) (↑(p ^ (α - v)) - ↑(k_val / p ^ v * ((↑u).val % p ^ (α - v)) % p ^ (α - v))))

theorem pv_cancel (pv x : ℝ) (hpv : 0 < pv) (hx : x ≠ 0) : pv * (1 / (pv * x)) = 1 / x

theorem unit_mod_coprime_p (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (hα : 1 ≤ α) (v : ℕ) (hv_lt : v < α) (u : (ZMod (p ^ α))ˣ) : ((↑u).val % p ^ (α - v)).Coprime p

theorem summand_fiber_constant (k' M s u_val : ℕ) (hs : u_val % M = s) : k' * (u_val % M) % M = k' * s % M

theorem reduced_product_mod_ne_zero_of_coprime (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (_hα : 1 ≤ α) (k_val v : ℕ) (_hv_pos : 1 ≤ v) (hv_lt : v < α) (hv_val : p ^ v ∣ k_val) (hv_max : ¬p ^ (v + 1) ∣ k_val) (s : ℕ) (hs_cop : s.Coprime p) : k_val / p ^ v * s % p ^ (α - v) ≠ 0

theorem min_pos_of_ne_zero_lt (r M : ℕ) (hr_ne : r ≠ 0) (hr_lt : r < M) : 0 < min (↑r) (↑M - ↑r)

theorem fiber_sum_cancel (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (hα : 1 ≤ α) (k_val : ℕ) (_hk_nd : ¬p ^ α ∣ k_val) (v : ℕ) (hv_pos : 1 ≤ v) (hv_lt : v < α) (hv_val : p ^ v ∣ k_val) (hv_max : ¬p ^ (v + 1) ∣ k_val) [NeZero (p ^ α)] [NeZero (p ^ (α - v))] (s : ℕ) (hs_lt : s < p ^ (α - v)) (hs_cop : s.Coprime p) : ∑ u : (ZMod (p ^ α))ˣ with (↑u).val % p ^ (α - v) = s, 1 / (↑(p ^ v) * min (↑(k_val / p ^ v * ((↑u).val % p ^ (α - v)) % p ^ (α - v))) (↑(p ^ (α - v)) - ↑(k_val / p ^ v * ((↑u).val % p ^ (α - v)) % p ^ (α - v)))) = 1 / min (↑(k_val / p ^ v * s % p ^ (α - v))) (↑(p ^ (α - v)) - ↑(k_val / p ^ v * s % p ^ (α - v)))

theorem unit_mod_coprime_pow (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (hα : 1 ≤ α) (v : ℕ) (hv_lt : v < α) (u : (ZMod (p ^ α))ˣ) : ((↑u).val % p ^ (α - v)).Coprime (p ^ (α - v))

theorem unitProjection_filter_iff (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (hα : 1 ≤ α) (v : ℕ) (hv_lt : v < α) [NeZero (p ^ (α - v))] (u : (ZMod (p ^ α))ˣ) (t : (ZMod (p ^ (α - v)))ˣ) : ZMod.unitOfCoprime ((↑u).val % p ^ (α - v)) ⋯ = t ↔ (↑u).val % p ^ (α - v) = (↑t).val

theorem fiberwise_sum_eq_double_sum (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (hα : 1 ≤ α) (k_val : ℕ) (_hk_nd : ¬p ^ α ∣ k_val) (v : ℕ) (_hv_pos : 1 ≤ v) (hv_lt : v < α) (_hv_val : p ^ v ∣ k_val) (_hv_max : ¬p ^ (v + 1) ∣ k_val) [NeZero (p ^ α)] [NeZero (p ^ (α - v))] : ∑ u : (ZMod (p ^ α))ˣ, 1 / (↑(p ^ v) * min (↑(k_val / p ^ v * ((↑u).val % p ^ (α - v)) % p ^ (α - v))) (↑(p ^ (α - v)) - ↑(k_val / p ^ v * ((↑u).val % p ^ (α - v)) % p ^ (α - v)))) = ∑ t : (ZMod (p ^ (α - v)))ˣ, ∑ u : (ZMod (p ^ α))ˣ with (↑u).val % p ^ (α - v) = (↑t).val, 1 / (↑(p ^ v) * min (↑(k_val / p ^ v * ((↑u).val % p ^ (α - v)) % p ^ (α - v))) (↑(p ^ (α - v)) - ↑(k_val / p ^ v * ((↑u).val % p ^ (α - v)) % p ^ (α - v))))

theorem fiber_grouping_step (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (hα : 1 ≤ α) (k_val : ℕ) (hk_nd : ¬p ^ α ∣ k_val) (v : ℕ) (hv_pos : 1 ≤ v) (hv_lt : v < α) (hv_val : p ^ v ∣ k_val) (hv_max : ¬p ^ (v + 1) ∣ k_val) [NeZero (p ^ α)] [NeZero (p ^ (α - v))] : ∑ u : (ZMod (p ^ α))ˣ, 1 / (↑(p ^ v) * min (↑(k_val / p ^ v * ((↑u).val % p ^ (α - v)) % p ^ (α - v))) (↑(p ^ (α - v)) - ↑(k_val / p ^ v * ((↑u).val % p ^ (α - v)) % p ^ (α - v)))) = ∑ t : (ZMod (p ^ (α - v)))ˣ, 1 / min (↑(k_val / p ^ v * (↑t).val % p ^ (α - v))) (↑(p ^ (α - v)) - ↑(k_val / p ^ v * (↑t).val % p ^ (α - v)))

theorem coprime_of_prime_power_not_dvd (d p : ℕ) (hp : Nat.Prime p) (α : ℕ) (_hα : 1 ≤ α) (hd_eq : d = p ^ α) (k_val : ℕ) (hp_ndvd : ¬p ∣ k_val) : k_val.Coprime d

theorem permutation_step (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (_hα : 1 ≤ α) (k_val v : ℕ) (_hv_pos : 1 ≤ v) (hv_lt : v < α) (hv_val : p ^ v ∣ k_val) (hv_max : ¬p ^ (v + 1) ∣ k_val) [NeZero (p ^ (α - v))] : ∑ t : (ZMod (p ^ (α - v)))ˣ, 1 / min (↑(k_val / p ^ v * (↑t).val % p ^ (α - v))) (↑(p ^ (α - v)) - ↑(k_val / p ^ v * (↑t).val % p ^ (α - v))) = ∑ t : (ZMod (p ^ (α - v)))ˣ, 1 / min (↑(↑t).val) (↑(p ^ (α - v)) - ↑(↑t).val)

theorem orbit_fiber_sum_eq (d : ℕ) [NeZero d] (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (hα : 1 ≤ α) (hd_eq : d = p ^ α) (k_val : ℕ) (hk_nd : ¬d ∣ k_val) (hk_dvd_p : p ∣ k_val) (v : ℕ) (hv_pos : 1 ≤ v) (hv_lt : v < α) (hv_val : p ^ v ∣ k_val) (hv_max : ¬p ^ (v + 1) ∣ k_val) [NeZero (p ^ (α - v))] : ∑ u : (ZMod d)ˣ, 1 / min (↑(k_val * (↑u).val % d)) (↑d - ↑(k_val * (↑u).val % d)) = ∑ t : (ZMod (p ^ (α - v)))ˣ, 1 / min (↑(↑t).val) (↑(p ^ (α - v)) - ↑(↑t).val)

theorem distribute_two_over_sum (k : ℕ) (hk : 1 ≤ k) : 2 * (∑ u ∈ Finset.Icc 1 (k - 1), (↑u)⁻¹ + 1 / (2 * ↑k)) = 2 * ∑ u ∈ Finset.Icc 1 (k - 1), (↑u)⁻¹ + 1 / ↑k

theorem even_step_lhs_eq (k : ℕ) (hk : 1 ≤ k) : ∑ t ∈ Finset.Icc 1 (2 * k - 1), 1 / min (↑t) (2 * ↑k - ↑t) = 2 * ∑ u ∈ Finset.Icc 1 (k - 1), (↑u)⁻¹ + 1 / ↑k

theorem lhs_eq_1 (k : ℕ) (hk : 1 ≤ k) : ∑ t ∈ Finset.Icc 1 (2 * k), 1 / min (↑t) (2 * ↑k + 1 - ↑t) = 2 * ∑ u ∈ Finset.Icc 1 k, (↑u)⁻¹

theorem harmonic_split (k : ℕ) (hk : 1 ≤ k) : ∑ u ∈ Finset.Icc 1 k, (↑u)⁻¹ = ∑ u ∈ Finset.Icc 1 (k - 1), (↑u)⁻¹ + (↑k)⁻¹

theorem even_step (k : ℕ) (hk : 1 ≤ k) : ∑ t ∈ Finset.Icc 1 (2 * k - 1), 1 / min (↑t) (2 * ↑k - ↑t) ≤ ∑ t ∈ Finset.Icc 1 (2 * k), 1 / min (↑t) (2 * ↑k + 1 - ↑t)

theorem rhs_eq (k : ℕ) (hk : 1 ≤ k) : ∑ t ∈ Finset.Icc 1 (2 * k + 1), 1 / min (↑t) (2 * ↑k + 1 + 1 - ↑t) = 2 * (∑ u ∈ Finset.Icc 1 k, (↑u)⁻¹ + 1 / (2 * (↑k + 1)))

theorem odd_step (k : ℕ) (hk : 1 ≤ k) : ∑ t ∈ Finset.Icc 1 (2 * k), 1 / min (↑t) (2 * ↑k + 1 - ↑t) ≤ ∑ t ∈ Finset.Icc 1 (2 * k + 1), 1 / min (↑t) (2 * ↑k + 1 + 1 - ↑t)

theorem harmonic_min_sum_step (N : ℕ) (hN : 2 ≤ N) : ∑ t ∈ Finset.Icc 1 (N - 1), 1 / min (↑t) (↑N - ↑t) ≤ ∑ t ∈ Finset.Icc 1 (N + 1 - 1), 1 / min (↑t) (↑(N + 1) - ↑t)

theorem harmonic_min_sum_mono (M d : ℕ) (hM : 2 ≤ M) (hMd : M ≤ d) : ∑ t ∈ Finset.Icc 1 (M - 1), 1 / min (↑t) (↑M - ↑t) ≤ ∑ t ∈ Finset.Icc 1 (d - 1), 1 / min (↑t) (↑d - ↑t)

theorem exists_padic_valuation (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (_hα : 1 ≤ α) (k_val : ℕ) (hk_dvd_p : p ∣ k_val) (hk_nd : ¬p ^ α ∣ k_val) : ∃ (v : ℕ), 1 ≤ v ∧ v < α ∧ p ^ v ∣ k_val ∧ ¬p ^ (v + 1) ∣ k_val

theorem general_case_bound (d : ℕ) [NeZero d] (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (hα : 1 ≤ α) (hd_eq : d = p ^ α) (k_val : ℕ) (hk_nd : ¬d ∣ k_val) (hk_dvd_p : p ∣ k_val) : ∑ u : (ZMod d)ˣ, 1 / min (↑(k_val * (↑u).val % d)) (↑d - ↑(k_val * (↑u).val % d)) ≤ ∑ t ∈ Finset.Icc 1 (d - 1), 1 / min (↑t) (↑d - ↑t)

theorem orbit_fiber_sum_bound (d : ℕ) [NeZero d] (p : ℕ) (hp : Nat.Prime p) (α : ℕ) (hα : 1 ≤ α) (hd_eq : d = p ^ α) (k_val : ℕ) (hk_nd : ¬d ∣ k_val) : ∑ u : (ZMod d)ˣ, 1 / min (↑(k_val * (↑u).val % d)) (↑d - ↑(k_val * (↑u).val % d)) ≤ ∑ t ∈ Finset.Icc 1 (d - 1), 1 / min (↑t) (↑d - ↑t)

theorem d_ge_two (n d : ℕ) (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) : 2 ≤ d

theorem d_le_n (n d : ℕ) (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) : d ≤ n

theorem orbit_sum_le_two_log (n d : ℕ) [NeZero d] (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (k : ZMod n) (_hk : k ≠ 0) (hk_nd : ¬d ∣ k.val) : ∑ u : (ZMod d)ˣ, 1 / min (↑(k.val * (↑u).val % d)) (↑d - ↑(k.val * (↑u).val % d)) ≤ 2 * (1 + Real.log ↑n)

theorem pow_pred_mul_eq (P α : ℕ) (hα : 0 < α) : P ^ (α - 1) * P = P ^ α

theorem cast_nat_sub_one (P : ℕ) (hP2 : 2 ≤ P) : ↑(P - 1) = ↑P - 1

theorem totient_prime_pow_simplify (P α : ℕ) (hP2 : 2 ≤ P) (hα : 0 < α) : ↑(P ^ (α - 1) * (P - 1)) * (4 / ↑(P ^ α)) = 4 * (↑P - 1) / ↑P

theorem four_times_sub_one_div_ge_two (P : ℕ) (hP2 : 2 ≤ P) : 2 ≤ 4 * (↑P - 1) / ↑P

theorem totient_prime_pow_times_four_div_ge_two (P α : ℕ) (hP : Nat.Prime P) (hα : 0 < α) (hP2 : 2 ≤ P) : 2 ≤ ↑(P ^ α).totient * (4 / ↑(P ^ α))

theorem totient_times_four_div_d_ge_two (n d : ℕ) (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) : 2 ≤ ↑d.totient * (4 / ↑d)

theorem two_log_le_card_times_bound (n d : ℕ) [NeZero d] (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) : 2 * (1 + Real.log ↑n) ≤ ↑(Fintype.card (ZMod d)ˣ) * (4 * (1 + Real.log ↑n) / ↑d)

theorem orbit_reciprocal_sum_bound (n d : ℕ) [NeZero d] (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (k : ZMod n) (hk : k ≠ 0) (hk_nd : ¬d ∣ k.val) : ∑ u : (ZMod d)ˣ, 1 / min (↑(k.val * (↑u).val % d)) (↑d - ↑(k.val * (↑u).val % d)) ≤ ↑(Fintype.card (ZMod d)ˣ) * (4 * (1 + Real.log ↑n) / ↑d)

theorem PerUnitMerge.neg_inv_isUnit (d : ℕ) (q : ℤ) (hq : q.gcd ↑d = 1) : IsUnit (-(↑q)⁻¹)

theorem PerUnitMerge.dvd_of_dvd_mul_unit_val (d k_val : ℕ) (u : (ZMod d)ˣ) (h : d ∣ k_val * (↑u).val) : d ∣ k_val

theorem PerUnitMerge.b_ne_zero (d : ℕ) (q : ℤ) (hq_coprime_d : q.gcd ↑d = 1) (k_val : ℕ) (hk_nd : ¬d ∣ k_val) (u : (ZMod d)ˣ) : -(↑q)⁻¹ * ↑(k_val * (↑u).val) ≠ 0

theorem PerUnitMerge.b_bounds (d : ℕ) [NeZero d] (q : ℤ) (hq_coprime_d : q.gcd ↑d = 1) (k_val : ℕ) (hk_nd : ¬d ∣ k_val) (u : (ZMod d)ˣ) : have b := (-(↑q)⁻¹ * ↑(k_val * (↑u).val)).val; 1 ≤ b ∧ b < d

theorem PerUnitMerge.q_isUnit_of_gcd (d : ℕ) (q : ℤ) (hq : q.gcd ↑d = 1) : IsUnit ↑q

theorem PerUnitMerge.neg_inv_eq_inv_neg (d : ℕ) (q : ℤ) (hq : q.gcd ↑d = 1) : -(↑q)⁻¹ = (-↑q)⁻¹

theorem PerUnitMerge.dvd_iff_zmod_eq_zero (d k_val u_val l_val : ℕ) (q : ℤ) : ↑d ∣ ↑k_val * ↑u_val + ↑l_val * q ↔ ↑k_val * ↑u_val + ↑l_val * ↑q = 0

theorem PerUnitMerge.zmod_eq_zero_forward (d k_val u_val l_val : ℕ) (q : ℤ) (hq : IsUnit ↑q) (h : ↑k_val * ↑u_val + ↑l_val * ↑q = 0) : ↑l_val = -(↑q)⁻¹ * ↑(k_val * u_val)

theorem PerUnitMerge.zmod_eq_zero_backward (d k_val u_val l_val : ℕ) (q : ℤ) (hq : IsUnit ↑q) (h : ↑l_val = -(↑q)⁻¹ * ↑(k_val * u_val)) : ↑k_val * ↑u_val + ↑l_val * ↑q = 0

theorem PerUnitMerge.zmod_eq_zero_iff_eq_neg_inv_mul (d k_val u_val l_val : ℕ) (q : ℤ) (hq : IsUnit ↑q) : ↑k_val * ↑u_val + ↑l_val * ↑q = 0 ↔ ↑l_val = -(↑q)⁻¹ * ↑(k_val * u_val)

theorem PerUnitMerge.residue_iff_zmod_eq (d : ℕ) [NeZero d] (k_val u_val l_val : ℕ) (q : ℤ) : l_val % d = (-(↑q)⁻¹ * ↑(k_val * u_val)).val ↔ ↑l_val = -(↑q)⁻¹ * ↑(k_val * u_val)

theorem PerUnitMerge.divisibility_iff_residue_class (n d : ℕ) [NeZero d] (_hd_dvd : d ∣ n) (q : ℤ) (hq_coprime_d : q.gcd ↑d = 1) (k : ZMod n) (_hk : k ≠ 0) (u : (ZMod d)ˣ) (l : ZMod n) : have b := (-(↑q)⁻¹ * ↑(k.val * (↑u).val)).val; ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q ↔ l.val % d = b

theorem PerUnitMerge.cond_sum_eq_residue_class_sum (n d : ℕ) [NeZero n] [NeZero d] (hd_dvd : d ∣ n) (q : ℤ) (hq_coprime_d : q.gcd ↑d = 1) (mq : ℕ) (k : ZMod n) (hk : k ≠ 0) (u : (ZMod d)ˣ) : have b := (-(↑q)⁻¹ * ↑(k.val * (↑u).val)).val; (∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) = ∑ l : ZMod n, if l.val % d = b then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0

theorem PerUnitMerge.nonzero_of_val_mod_eq_pos (n d : ℕ) (l : ZMod n) (b : ℕ) (hb_pos : 1 ≤ b) (_hb_lt : b < d) (hmod : l.val % d = b) : l ≠ 0

theorem PerUnitMerge.min_eq_val_of_two_mul_le (n : ℕ) (l : ZMod n) (h2 : 2 * l.val ≤ n) : min (↑l.val) (↑n - ↑l.val) = ↑l.val

theorem PerUnitMerge.pointwise_bound_in_low_range (n d : ℕ) [NeZero n] (mq : ℕ) (hmq_lo : 1 ≤ mq) (hmq_hi : mq < n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) (l : ZMod n) (hmod : l.val % d = b) (hlow : 2 * l.val ≤ n) : ‖normalizedDFT n (intervalIndicator n mq) l‖ ≤ 1 / (2 * ↑l.val)

theorem PerUnitMerge.val_eq_of_mod_eq_and_quot_eq (n d b : ℕ) (_hb_lt : b < d) (l₁ l₂ : ZMod n) (h1 : l₁.val % d = b) (h2 : l₂.val % d = b) (heq : (l₁.val - b) / d = (l₂.val - b) / d) : l₁.val = l₂.val

theorem PerUnitMerge.quotient_injOn (n d : ℕ) [NeZero n] (_hd_dvd : d ∣ n) (b : ℕ) (hb_lt : b < d) : Set.InjOn (fun (l : ZMod n) => (l.val - b) / d) ↑{l : ZMod n | l.val % d = b ∧ 2 * l.val ≤ n}

theorem PerUnitMerge.quotient_mem_range (n d : ℕ) (_hd_dvd : d ∣ n) (b : ℕ) (_hb_pos : 1 ≤ b) (_hb_lt : b < d) (l : ZMod n) (hl : l.val % d = b ∧ 2 * l.val ≤ n) : (l.val - b) / d ∈ Finset.range (n / (2 * d) + 1)

theorem PerUnitMerge.summand_eq (n d b : ℕ) (_hb_pos : 1 ≤ b) (_hb_lt : b < d) (l : ZMod n) (hl : l.val % d = b ∧ 2 * l.val ≤ n) : 1 / (2 * ↑l.val) = 1 / (2 * (↑b + ↑((l.val - b) / d) * ↑d))

theorem PerUnitMerge.rhs_term_nonneg (b d : ℕ) (hb_pos : 1 ≤ b) (j : ℕ) : 0 ≤ 1 / (2 * (↑b + ↑j * ↑d))

theorem PerUnitMerge.sum_val_reciprocal_le_sum_range (n d : ℕ) [NeZero n] (_hn : 2 ≤ n) (hd_dvd : d ∣ n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) : (∑ l : ZMod n, if l.val % d = b ∧ 2 * l.val ≤ n then 1 / (2 * ↑l.val) else 0) ≤ ∑ j ∈ Finset.range (n / (2 * d) + 1), 1 / (2 * (↑b + ↑j * ↑d))

theorem PerUnitMerge.low_range_le_sum_over_j (n d : ℕ) [NeZero n] (hn : 2 ≤ n) (hd_dvd : d ∣ n) (mq : ℕ) (hmq_lo : 1 ≤ mq) (hmq_hi : mq < n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) : (∑ l : ZMod n, if l.val % d = b ∧ 2 * l.val ≤ n then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) ≤ ∑ j ∈ Finset.range (n / (2 * d) + 1), 1 / (2 * (↑b + ↑j * ↑d))

theorem PerUnitMerge.sum_range_split (J : ℕ) (f : ℕ → ℝ) : ∑ j ∈ Finset.range (J + 1), f j = f 0 + ∑ j ∈ Finset.Icc 1 J, f j

theorem PerUnitMerge.two_mul_add_one_le_real (M n : ℕ) (hM : M ≤ n) : 2 * ↑M + 1 ≤ 2 * ↑n + 1

theorem PerUnitMerge.two_mul_add_one_pos (M : ℕ) : 0 < 2 * ↑M + 1

theorem PerUnitMerge.log_two_n_plus_one_le_one_plus_log (n : ℕ) (hn : 2 ≤ n) : Real.log (2 * ↑n + 1) ≤ 1 + Real.log ↑n

theorem PerUnitMerge.sum_range_eq_sum_Icc (M : ℕ) : ∑ j ∈ Finset.range M, 1 / (↑j + 1) = ∑ u ∈ Finset.Icc 1 M, (↑u)⁻¹

theorem PerUnitMerge.harmonic_range_le_one_plus_log (M n : ℕ) (hn : 2 ≤ n) (hM : M ≤ n) : ∑ j ∈ Finset.range M, 1 / (↑j + 1) ≤ 1 + Real.log ↑n

theorem PerUnitMerge.summand_bound (d : ℕ) (hd_pos : 0 < d) (b : ℕ) (hb_pos : 1 ≤ b) (j : ℕ) (hj : 1 ≤ j) : 1 / (2 * (↑b + ↑j * ↑d)) ≤ 1 / (2 * (↑j * ↑d))

theorem PerUnitMerge.sum_factor_Icc (n d : ℕ) (hd_pos : 0 < d) : ∑ j ∈ Finset.Icc 1 (n / (2 * d)), 1 / (2 * (↑j * ↑d)) = (∑ j ∈ Finset.Icc 1 (n / (2 * d)), 1 / ↑j) / (2 * ↑d)

theorem PerUnitMerge.sum_Icc_eq_sum_range (J : ℕ) : ∑ j ∈ Finset.Icc 1 J, 1 / ↑j = ∑ j ∈ Finset.range J, 1 / (↑j + 1)

theorem PerUnitMerge.harmonic_sum_over_Icc_le_log_div (n d : ℕ) (hn : 2 ≤ n) (hd_pos : 0 < d) (_hd_le : d ≤ n) : ∑ j ∈ Finset.Icc 1 (n / (2 * d)), 1 / (2 * (↑j * ↑d)) ≤ (1 + Real.log ↑n) / (2 * ↑d)

theorem PerUnitMerge.tail_sum_le_log_div (n d : ℕ) (hn : 2 ≤ n) (hd_pos : 0 < d) (hd_le : d ≤ n) (b : ℕ) (hb_pos : 1 ≤ b) : ∑ j ∈ Finset.Icc 1 (n / (2 * d)), 1 / (2 * (↑b + ↑j * ↑d)) ≤ (1 + Real.log ↑n) / (2 * ↑d)

theorem PerUnitMerge.arith_prog_sum_le_low (n d : ℕ) (hn : 2 ≤ n) (hd_pos : 0 < d) (hd_le : d ≤ n) (b : ℕ) (hb_pos : 1 ≤ b) (_hb_lt : b < d) : ∑ j ∈ Finset.range (n / (2 * d) + 1), 1 / (2 * (↑b + ↑j * ↑d)) ≤ 1 / (2 * ↑b) + (1 + Real.log ↑n) / (2 * ↑d)

theorem PerUnitMerge.low_range_bound (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd_dvd : d ∣ n) (mq : ℕ) (hmq_lo : 1 ≤ mq) (hmq_hi : mq < n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) : (∑ l : ZMod n, if l.val % d = b ∧ 2 * l.val ≤ n then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) ≤ 1 / (2 * ↑b) + (1 + Real.log ↑n) / (2 * ↑d)

theorem PerUnitMerge.high_range_pointwise_bound (n : ℕ) [NeZero n] (mq : ℕ) (hmq_lo : 1 ≤ mq) (hmq_hi : mq < n) (d b : ℕ) (hb_pos : 1 ≤ b) (l : ZMod n) (hl_mod : l.val % d = b) (hl_high : ¬2 * l.val ≤ n) : ‖normalizedDFT n (intervalIndicator n mq) l‖ ≤ 1 / (2 * (↑n - ↑l.val))

theorem PerUnitMerge.quot_lt (n d : ℕ) (hd_dvd : d ∣ n) (b : ℕ) (hb_pos : 1 ≤ b) (_hb_lt : b < d) (v : ℕ) (hv_lt : v < n) (hv_mod : v % d = b) : v / d < n / d

theorem PerUnitMerge.nat_sub_mul_add (A B d b : ℕ) (hBA : B < A) (hbd : b < d) : d * A - (d * B + b) = d * (A - B - 1) + (d - b)

theorem PerUnitMerge.n_sub_v_eq (n d : ℕ) (hd_dvd : d ∣ n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) (v : ℕ) (hv_lt : v < n) (hv_mod : v % d = b) (hquot : v / d < n / d) : n - v = d * (n / d - v / d - 1) + (d - b)

theorem PerUnitMerge.n_sub_v_mod_eq_d_sub_b (n d : ℕ) (hd_dvd : d ∣ n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) (v : ℕ) (hv_lt : v < n) (hv_mod : v % d = b) : (n - v) % d = d - b

theorem PerUnitMerge.d_sub_b_le_n_sub_v (n d : ℕ) (hd_dvd : d ∣ n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) (v : ℕ) (hv_lt : v < n) (hv_mod : v % d = b) (_hv_big : n < 2 * v) : d - b ≤ n - v

theorem PerUnitMerge.n_modEq_d_of_dvd (n d : ℕ) (hd_dvd : d ∣ n) : n ≡ d [MOD d]

theorem PerUnitMerge.v_modEq_b_of_mod (d b : ℕ) (hb_lt : b < d) (v : ℕ) (hv_mod : v % d = b) : v ≡ b [MOD d]

theorem PerUnitMerge.complement_div_d_dvd (n d : ℕ) (hd_dvd : d ∣ n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) (v : ℕ) (hv_lt : v < n) (hv_mod : v % d = b) (hv_big : n < 2 * v) : d ∣ n - v - (d - b)

theorem PerUnitMerge.sub_d_sub_b_le_sub_v (n d : ℕ) (_hd_pos : 0 < d) (_hd_dvd : d ∣ n) (b : ℕ) (_hb_pos : 1 ≤ b) (_hb_lt : b < d) (v : ℕ) (_hv_lt : v < n) (_hv_mod : v % d = b) (_hv_big : n < 2 * v) : n - v - (d - b) ≤ n - v

theorem PerUnitMerge.n_sub_v_le_half_n (n v : ℕ) (hv_lt : v < n) (hv_big : n < 2 * v) : n - v ≤ n / 2

theorem PerUnitMerge.complement_j_in_range (n d : ℕ) (hd_pos : 0 < d) (hd_dvd : d ∣ n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) (v : ℕ) (hv_lt : v < n) (hv_mod : v % d = b) (hv_big : n < 2 * v) : (n - v - (d - b)) / d < n / (2 * d) + 1

theorem PerUnitMerge.complement_eq_arith_prog (n d : ℕ) (hd_dvd : d ∣ n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) (v : ℕ) (hv_lt : v < n) (hv_mod : v % d = b) (hv_big : n < 2 * v) : n - v = d - b + (n - v - (d - b)) / d * d

theorem PerUnitMerge.complement_eq_arith_prog_real (n d : ℕ) (hd_dvd : d ∣ n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) (v : ℕ) (hv_lt : v < n) (hv_mod : v % d = b) (hv_big : n < 2 * v) : ↑n - ↑v = ↑d - ↑b + ↑((n - v - (d - b)) / d) * ↑d

theorem PerUnitMerge.eq_of_dvd_div_eq (a b d : ℕ) (_hd : 0 < d) (ha : d ∣ a) (hb : d ∣ b) (h : a / d = b / d) : a = b

theorem PerUnitMerge.complement_map_injective (n d : ℕ) (hd_dvd : d ∣ n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) (v₁ v₂ : ℕ) : v₁ < n → v₁ % d = b → n < 2 * v₁ → v₂ < n → v₂ % d = b → n < 2 * v₂ → (n - v₁ - (d - b)) / d = (n - v₂ - (d - b)) / d → v₁ = v₂

theorem PerUnitMerge.arith_prog_summand_nonneg (d b : ℕ) (_hb_pos : 1 ≤ b) (hb_lt : b < d) (j : ℕ) : 0 ≤ 1 / (2 * (↑d - ↑b + ↑j * ↑d))

theorem PerUnitMerge.reindex_map_injOn (n d : ℕ) [NeZero n] (_hn : 2 ≤ n) (hd_dvd : d ∣ n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) : Set.InjOn (fun (l : ZMod n) => (n - l.val - (d - b)) / d) ↑{l : ZMod n | l.val % d = b ∧ ¬2 * l.val ≤ n}

theorem PerUnitMerge.reindex_filtered_sum (n d : ℕ) [NeZero n] (hn : 2 ≤ n) (hd_dvd : d ∣ n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) : ∑ l : ZMod n with l.val % d = b ∧ ¬2 * l.val ≤ n, 1 / (2 * (↑n - ↑l.val)) = ∑ j ∈ Finset.image (fun (l : ZMod n) => (n - l.val - (d - b)) / d) {l : ZMod n | l.val % d = b ∧ ¬2 * l.val ≤ n}, 1 / (2 * (↑d - ↑b + ↑j * ↑d))

theorem PerUnitMerge.image_subset_range (n d : ℕ) [NeZero n] [NeZero d] (_hn : 2 ≤ n) (hd_dvd : d ∣ n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) : Finset.image (fun (l : ZMod n) => (n - l.val - (d - b)) / d) {l : ZMod n | l.val % d = b ∧ ¬2 * l.val ≤ n} ⊆ Finset.range (n / (2 * d) + 1)

theorem PerUnitMerge.high_range_reindex_bound (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd_dvd : d ∣ n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) : (∑ l : ZMod n, if l.val % d = b ∧ ¬2 * l.val ≤ n then 1 / (2 * (↑n - ↑l.val)) else 0) ≤ ∑ j ∈ Finset.range (n / (2 * d) + 1), 1 / (2 * (↑d - ↑b + ↑j * ↑d))

theorem PerUnitMerge.sum_range_le_sum_Icc (n d : ℕ) (hd_pos : 0 < d) (b : ℕ) (_hb_pos : 1 ≤ b) (hb_lt : b < d) : ∑ j ∈ Finset.range (n / (2 * d)), 1 / (2 * (↑d - ↑b + (↑j + 1) * ↑d)) ≤ ∑ j ∈ Finset.Icc 1 (n / (2 * d)), 1 / (2 * (↑j * ↑d))

theorem PerUnitMerge.tail_sum_le (n d : ℕ) (hn : 2 ≤ n) (hd_pos : 0 < d) (hd_le : d ≤ n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) : ∑ j ∈ Finset.range (n / (2 * d)), 1 / (2 * (↑d - ↑b + (↑j + 1) * ↑d)) ≤ (1 + Real.log ↑n) / (2 * ↑d)

theorem PerUnitMerge.arith_prog_sum_le (n d : ℕ) (hn : 2 ≤ n) (hd_pos : 0 < d) (hd_le : d ≤ n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) : ∑ j ∈ Finset.range (n / (2 * d) + 1), 1 / (2 * (↑d - ↑b + ↑j * ↑d)) ≤ 1 / (2 * (↑d - ↑b)) + (1 + Real.log ↑n) / (2 * ↑d)

theorem PerUnitMerge.high_range_bound (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd_dvd : d ∣ n) (mq : ℕ) (hmq_lo : 1 ≤ mq) (hmq_hi : mq < n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) : (∑ l : ZMod n, if l.val % d = b ∧ ¬2 * l.val ≤ n then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) ≤ 1 / (2 * (↑d - ↑b)) + (1 + Real.log ↑n) / (2 * ↑d)

theorem PerUnitMerge.split_sum_low_high (n d : ℕ) [NeZero n] (mq b : ℕ) : (∑ l : ZMod n, if l.val % d = b then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) = (∑ l : ZMod n, if l.val % d = b ∧ 2 * l.val ≤ n then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) + ∑ l : ZMod n, if l.val % d = b ∧ ¬2 * l.val ≤ n then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0

theorem PerUnitMerge.half_reciprocal_sum_le_min_reciprocal (b d : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) : 1 / (2 * ↑b) + 1 / (2 * (↑d - ↑b)) ≤ 1 / min (↑b) (↑d - ↑b)

theorem PerUnitMerge.fourier_mass_residue_class_bound (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd_dvd : d ∣ n) (mq : ℕ) (hmq_lo : 1 ≤ mq) (hmq_hi : mq < n) (b : ℕ) (hb_pos : 1 ≤ b) (hb_lt : b < d) : (∑ l : ZMod n, if l.val % d = b then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) ≤ 1 / min (↑b) (↑d - ↑b) + (1 + Real.log ↑n) / ↑d

theorem PerUnitMerge.inner_sum_bound_at_residue (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd_dvd : d ∣ n) (q : ℤ) (hq_coprime_d : q.gcd ↑d = 1) (_hq_pos : 1 ≤ q) (_hq_bound : ↑q < ↑n / 2) (mq : ℕ) (hmq_lo : 1 ≤ mq) (hmq_hi : mq < n) (k : ZMod n) (hk : k ≠ 0) (hk_nd : ¬d ∣ k.val) (u : (ZMod d)ˣ) : have b := (-(↑q)⁻¹ * ↑(k.val * (↑u).val)).val; (∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) ≤ 1 / min (↑b) (↑d - ↑b) + (1 + Real.log ↑n) / ↑d

theorem PerUnitMerge.zmod_expr_simplify (d : ℕ) [NeZero d] (q : ℤ) (hq_coprime_d : q.gcd ↑d = 1) (k_val : ℕ) (w : (ZMod d)ˣ) (hw : ↑w = -↑q) (v : (ZMod d)ˣ) : -(↑q)⁻¹ * ↑(k_val * (↑(w * v)).val) = ↑(k_val * (↑v).val)

theorem PerUnitMerge.summand_val_eq_after_bijection (d : ℕ) [NeZero d] (q : ℤ) (hq_coprime_d : q.gcd ↑d = 1) (k_val : ℕ) (_hk_nd : ¬d ∣ k_val) (w : (ZMod d)ˣ) (hw : ↑w = -↑q) (v : (ZMod d)ˣ) : (-(↑q)⁻¹ * ↑(k_val * (↑(w * v)).val)).val = k_val * (↑v).val % d

theorem PerUnitMerge.neg_q_unit_exists (d : ℕ) (q : ℤ) (hq_coprime_d : q.gcd ↑d = 1) : ∃ (w : (ZMod d)ˣ), ↑w = -↑q

theorem PerUnitMerge.bijection_sum_eq (d : ℕ) [NeZero d] (q : ℤ) (hq_coprime_d : q.gcd ↑d = 1) (k_val : ℕ) (hk_nd : ¬d ∣ k_val) : (∑ u : (ZMod d)ˣ, have b := (-(↑q)⁻¹ * ↑(k_val * (↑u).val)).val; 1 / min (↑b) (↑d - ↑b)) = ∑ u : (ZMod d)ˣ, 1 / min (↑(k_val * (↑u).val % d)) (↑d - ↑(k_val * (↑u).val % d))

theorem per_unit_inner_sum_bound (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) (hq_pos : 1 ≤ q) (hq_bound : ↑q < ↑n / 2) (mq : ℕ) (hmq : mq = (2 * q - 1).toNat) (k : ZMod n) (hk : k ≠ 0) (hk_nd : ¬d ∣ k.val) : (∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) ≤ ∑ u : (ZMod d)ˣ, 1 / min (↑(k.val * (↑u).val % d)) (↑d - ↑(k.val * (↑u).val % d)) + ↑(Fintype.card (ZMod d)ˣ) * ((1 + Real.log ↑n) / ↑d)

theorem combine_orbit_and_tail_bounds (C L d_real : ℝ) (_hC : 0 ≤ C) (_hL : 0 ≤ L) (hd : 0 < d_real) : C * (4 * L / d_real) + C * (L / d_real) ≤ C * (5 * L / d_real)

theorem orbit_average_bound (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) (hq_pos : 1 ≤ q) (hq_bound : ↑q < ↑n / 2) (mq : ℕ) (hmq : mq = (2 * q - 1).toNat) (k : ZMod n) (hk : k ≠ 0) (hk_nd : ¬d ∣ k.val) : (∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) ≤ ↑(Fintype.card (ZMod d)ˣ) * (5 * (1 + Real.log ↑n) / ↑d)

theorem nonmultiple_d_weighted_bound (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) (hq_pos : 1 ≤ q) (hq_bound : ↑q < ↑n / 2) (mq : ℕ) (hmq : mq = (2 * q - 1).toNat) : (∑ k : ZMod n with k ≠ 0 ∧ ¬d ∣ k.val, ∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0) ≤ ↑(Fintype.card (ZMod d)ˣ) * (5 * (1 + Real.log ↑n) ^ 2 / ↑d)

theorem weighted_orbit_total (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) (hq_pos : 1 ≤ q) (hq_bound : ↑q < ↑n / 2) (mq : ℕ) (hmq : mq = (2 * q - 1).toNat) : (∑ k : ZMod n, ∑ u : (ZMod d)ˣ, ∑ l : ZMod n, if k ≠ 0 ∧ ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0) ≤ ↑(Fintype.card (ZMod d)ˣ) * (6 * (1 + Real.log ↑n) ^ 2 / ↑d)

theorem average_S_bound (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) (hq_pos : 1 ≤ q) (hq_bound : ↑q < ↑n / 2) (mq : ℕ) (hmq : mq = (2 * q - 1).toNat) : (∑ u : (ZMod d)ˣ, ∑ k : ZMod n, ∑ l : ZMod n, if k ≠ 0 ∧ ↑d ∣ ↑k.val * ↑(↑u).val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0) ≤ ↑(Fintype.card (ZMod d)ˣ) * (6 * (1 + Real.log ↑n) ^ 2 / ↑d)

theorem sum_filter_lower_bound (d : ℕ) (f : (ZMod d)ˣ → ℝ) (_hf : ∀ (u : (ZMod d)ˣ), 0 ≤ f u) (avg : ℝ) (R : ℕ) (S : Finset (ZMod d)ˣ) (hS : ∀ u ∈ S, ↑R * avg < f u) : S.card • (↑R * avg) ≤ ∑ u ∈ S, f u

theorem sum_filter_le_sum_univ (d : ℕ) [NeZero d] (f : (ZMod d)ˣ → ℝ) (hf : ∀ (u : (ZMod d)ˣ), 0 ≤ f u) (avg : ℝ) (R : ℕ) : ∑ u : (ZMod d)ˣ with ↑R * avg < f u, f u ≤ ∑ u : (ZMod d)ˣ, f u

theorem card_mul_R_le_of_nsmul_le (s C R : ℕ) (avg : ℝ) (havg : 0 < avg) (h : s • (↑R * avg) ≤ ↑C * avg) : s * R ≤ C

theorem filter_empty_of_avg_zero (d : ℕ) [NeZero d] (f : (ZMod d)ˣ → ℝ) (hf : ∀ (u : (ZMod d)ˣ), 0 ≤ f u) (hsum : ∑ u : (ZMod d)ˣ, f u ≤ 0) (_R : ℕ) : {u : (ZMod d)ˣ | 0 < f u} = ∅

theorem markov_card_mul_le (d : ℕ) [NeZero d] (f : (ZMod d)ˣ → ℝ) (hf : ∀ (u : (ZMod d)ˣ), 0 ≤ f u) (avg : ℝ) (havg : 0 ≤ avg) (hsum : ∑ u : (ZMod d)ˣ, f u ≤ ↑(Fintype.card (ZMod d)ˣ) * avg) (R : ℕ) (hR : 1 ≤ R) : {u : (ZMod d)ˣ | ↑R * avg < f u}.card * R ≤ Fintype.card (ZMod d)ˣ

theorem markov_card_filter_le (d : ℕ) [NeZero d] (f : (ZMod d)ˣ → ℝ) (hf : ∀ (u : (ZMod d)ˣ), 0 ≤ f u) (avg : ℝ) (havg : 0 ≤ avg) (hsum : ∑ u : (ZMod d)ˣ, f u ≤ ↑(Fintype.card (ZMod d)ˣ) * avg) (R : ℕ) (hR : 1 ≤ R) : {u : (ZMod d)ˣ | ↑R * avg < f u}.card ≤ Fintype.card (ZMod d)ˣ / R

theorem image_val_card_le (d : ℕ) [NeZero d] (S : Finset (ZMod d)ˣ) (R : ℕ) (_hR : 1 ≤ R) (hcard : S.card ≤ Fintype.card (ZMod d)ˣ / R) : (Finset.image (fun (u : (ZMod d)ˣ) => (↑u).val) S).card ≤ d / R

theorem bad_set_from_average (d : ℕ) [NeZero d] (f : (ZMod d)ˣ → ℝ) (hf : ∀ (u : (ZMod d)ˣ), 0 ≤ f u) (avg : ℝ) (havg : 0 ≤ avg) (hsum : ∑ u : (ZMod d)ˣ, f u ≤ ↑(Fintype.card (ZMod d)ˣ) * avg) (R : ℕ) (hR : 1 ≤ R) : ∃ (B : Finset ℕ), B.card ≤ d / R ∧ ∀ (u : (ZMod d)ˣ), (↑u).val ∉ B → f u ≤ ↑R * avg

theorem k_zero_term_eq (n d : ℕ) [NeZero n] (mp mq : ℕ) (p q : ℤ) : (∑ l : ZMod n, if (0, l) ≠ (0, 0) ∧ ↑d ∣ ↑(ZMod.val 0) * p + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mp) 0‖ * ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) = ∑ l : ZMod n, if l ≠ 0 ∧ ↑d ∣ ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mp) 0‖ * ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0

theorem inner_sum_eq_of_k_ne_zero (n d : ℕ) [NeZero n] (mp mq : ℕ) (p q : ℤ) (k : ZMod n) (hk : k ≠ 0) : (∑ l : ZMod n, if (k, l) ≠ (0, 0) ∧ ↑d ∣ ↑k.val * p + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mp) k‖ * ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) = ∑ l : ZMod n, if k ≠ 0 ∧ ↑d ∣ ↑k.val * p + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mp) k‖ * ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0

theorem filtered_sum_to_full_sum (n d : ℕ) [NeZero n] (mp mq : ℕ) (p q : ℤ) : (∑ k : ZMod n with k ≠ 0, ∑ l : ZMod n, if (k, l) ≠ (0, 0) ∧ ↑d ∣ ↑k.val * p + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mp) k‖ * ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) = ∑ k : ZMod n, ∑ l : ZMod n, if k ≠ 0 ∧ ↑d ∣ ↑k.val * p + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mp) k‖ * ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0

theorem double_sum_split_k0_kneq0 (n d : ℕ) [NeZero n] (mp mq : ℕ) (p q : ℤ) : (∑ k : ZMod n, ∑ l : ZMod n, if (k, l) ≠ (0, 0) ∧ ↑d ∣ ↑k.val * p + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mp) k‖ * ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) = (∑ l : ZMod n, if l ≠ 0 ∧ ↑d ∣ ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mp) 0‖ * ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) + ∑ k : ZMod n, ∑ l : ZMod n, if k ≠ 0 ∧ ↑d ∣ ↑k.val * p + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mp) k‖ * ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0

theorem int_coprime_dvd_mul_imp_dvd (d v : ℕ) (q : ℤ) (hgcd : q.gcd ↑d = 1) (hdvd : ↑d ∣ ↑v * q) : d ∣ v

theorem dvd_val_of_dvd_val_mul_q (n d : ℕ) (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) (l : ZMod n) (_hl : l ≠ 0) (hdvd : ↑d ∣ ↑l.val * q) : d ∣ l.val

theorem norm_normalizedDFT_zero_le_one (n : ℕ) [NeZero n] (m : ℕ) (hm1 : 1 ≤ m) (hm2 : m < n) : ‖normalizedDFT n (intervalIndicator n m) 0‖ ≤ 1

theorem sum_nonzero_multiples_dft_bound (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd_dvd : d ∣ n) (hd_pos : 0 < d) (mq : ℕ) (hmq1 : 1 ≤ mq) (hmq2 : mq < n) : ∑ l : ZMod n with l ≠ 0 ∧ d ∣ l.val, ‖normalizedDFT n (intervalIndicator n mq) l‖ ≤ (1 + Real.log ↑n) / ↑d

theorem filter_int_dvd_subset_filter_nat_dvd (n d : ℕ) [NeZero n] (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) : {l : ZMod n | l ≠ 0 ∧ ↑d ∣ ↑l.val * q} ⊆ {l : ZMod n | l ≠ 0 ∧ d ∣ l.val}

theorem sum_int_dvd_le_sum_nat_dvd (n d : ℕ) [NeZero n] (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) (f g : ZMod n → ℝ) (hf_nonneg : ∀ (l : ZMod n), 0 ≤ f l) (hg_nonneg : ∀ (l : ZMod n), 0 ≤ g l) : (∑ l : ZMod n, if l ≠ 0 ∧ ↑d ∣ ↑l.val * q then f l * g l else 0) ≤ ∑ l : ZMod n with l ≠ 0 ∧ d ∣ l.val, f l * g l

theorem sum_mul_le_sum_of_le_one (n : ℕ) (c : ℝ) (hc : c ≤ 1) (_hc_nonneg : 0 ≤ c) (g : ZMod n → ℝ) (hg_nonneg : ∀ (l : ZMod n), 0 ≤ g l) (S : Finset (ZMod n)) : ∑ l ∈ S, c * g l ≤ ∑ l ∈ S, g l

theorem k_zero_contribution_bound (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (p q : ℤ) (hp_pos : 1 ≤ p) (hq_pos : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) : have mp := (2 * p - 1).toNat; have mq := (2 * q - 1).toNat; (∑ l : ZMod n, if l ≠ 0 ∧ ↑d ∣ ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mp) 0‖ * ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) ≤ (1 + Real.log ↑n) / ↑d

theorem dvd_diff_from_zmod_eq (d : ℕ) (p : ℤ) (u_val : ℕ) (hu : ↑p = ↑u_val) (k_val l_val : ℕ) (q : ℤ) : ↑d ∣ ↑k_val * p + ↑l_val * q - (↑k_val * ↑u_val + ↑l_val * q)

theorem congr_dvd_equiv (d : ℕ) (p : ℤ) (u_val : ℕ) (hu : ↑p = ↑u_val) (k_val l_val : ℕ) (q : ℤ) : ↑d ∣ ↑k_val * p + ↑l_val * q ↔ ↑d ∣ ↑k_val * ↑u_val + ↑l_val * q

theorem summand_le (n d : ℕ) [NeZero n] (hn : 2 ≤ n) (p q : ℤ) (hp_pos : 1 ≤ p) (hq_pos : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) (u_val : ℕ) (hu_congr : ↑p = ↑u_val) (k l : ZMod n) : have mp := (2 * p - 1).toNat; have mq := (2 * q - 1).toNat; (if k ≠ 0 ∧ ↑d ∣ ↑k.val * p + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mp) k‖ * ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) ≤ if k ≠ 0 ∧ ↑d ∣ ↑k.val * ↑u_val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0

theorem k_nonzero_contribution_bound (n d : ℕ) [NeZero n] (hn : 2 ≤ n) (_hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (p q : ℤ) (hp_pos : 1 ≤ p) (hq_pos : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) (u_val : ℕ) (hu_congr : ↑p = ↑u_val) : have mp := (2 * p - 1).toNat; have mq := (2 * q - 1).toNat; (∑ k : ZMod n, ∑ l : ZMod n, if k ≠ 0 ∧ ↑d ∣ ↑k.val * p + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mp) k‖ * ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) ≤ ∑ k : ZMod n, ∑ l : ZMod n, if k ≠ 0 ∧ ↑d ∣ ↑k.val * ↑u_val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0

theorem combine_bounds_arithmetic (R P d : ℕ) (hR : 1 ≤ R) (hP : 0 < P) (hd : 0 < d) (hdP : P ≤ d) (n_real : ℝ) (hn_log : 0 ≤ Real.log n_real) (S0 Sneq0 : ℝ) (hS0 : S0 ≤ (1 + Real.log n_real) / ↑d) (hSneq0 : Sneq0 ≤ 6 * ↑R * (1 + Real.log n_real) ^ 2 / ↑d) : S0 + Sneq0 ≤ 7 * ↑R * (1 + Real.log n_real) ^ 2 / ↑P

theorem combine_k0_kneq0_bounds (n : ℕ) (hn : 2 ≤ n) (d : ℕ) [NeZero d] (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) : have P := largestPrimeFactor n; have R := ⌈Real.log ↑n⌉₊; ∀ (S0 Sneq0 : ℝ), S0 ≤ (1 + Real.log ↑n) / ↑d → Sneq0 ≤ 6 * ↑R * (1 + Real.log ↑n) ^ 2 / ↑d → S0 + Sneq0 ≤ 7 * ↑R * (1 + Real.log ↑n) ^ 2 / ↑P

theorem good_p_double_sum_bound (n d : ℕ) [NeZero n] [NeZero d] (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (p q : ℤ) (hp_pos : 1 ≤ p) (hq_pos : 1 ≤ q) (hpq : ↑p + ↑q < ↑n / 2) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) (hp_coprime : ¬↑(largestPrimeFactor n) ∣ p) (u_val : ℕ) (hu_congr : ↑p = ↑u_val) : have P := largestPrimeFactor n; have R := ⌈Real.log ↑n⌉₊; have mp := (2 * p - 1).toNat; have mq := (2 * q - 1).toNat; (∑ k : ZMod n, ∑ l : ZMod n, if k ≠ 0 ∧ ↑d ∣ ↑k.val * ↑u_val + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mq) l‖ / (2 * min (↑k.val) (↑n - ↑k.val)) else 0) ≤ 6 * ↑R * (1 + Real.log ↑n) ^ 2 / ↑d → (∑ k : ZMod n, ∑ l : ZMod n, if (k, l) ≠ (0, 0) ∧ ↑d ∣ ↑k.val * p + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n mp) k‖ * ‖normalizedDFT n (intervalIndicator n mq) l‖ else 0) ≤ 7 * ↑R * (1 + Real.log ↑n) ^ 2 / ↑P

theorem int_not_dvd_imp_nat_not_dvd (P : ℕ) (p : ℤ) (_hp_pos : 1 ≤ p) (hp_not_dvd : ¬↑P ∣ p) : ¬P ∣ p.natAbs

theorem natAbs_mod_eq_emod_toNat (d : ℕ) (d_pos : 0 < d) (p : ℤ) (hp_pos : 1 ≤ p) : p.natAbs % d = (p % ↑d).toNat

theorem intCast_eq_natCast_of_pos (d : ℕ) (p : ℤ) (hp_pos : 1 ≤ p) : ↑p = ↑p.natAbs

theorem p_mod_d_unit (n d : ℕ) [NeZero d] (hn : 2 ≤ n) (hd : d = largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) (p : ℤ) (hp_pos : 1 ≤ p) (hp_coprime : ¬↑(largestPrimeFactor n) ∣ p) : ∃ (u : (ZMod d)ˣ), (↑u).val = (p % ↑d).toNat ∧ ↑p = ↑u

theorem double_sum_bad_set_construction (n : ℕ) [NeZero n] (hn : 2 ≤ n) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) (hq_pos : 1 ≤ q) (hq_bound : ↑q < ↑n / 2) : have P := largestPrimeFactor n; have d := P ^ n.factorization P; have R := ⌈Real.log ↑n⌉₊; ∃ (B : Finset ℕ), B.card ≤ d / R ∧ ∀ (p : ℤ), ¬↑P ∣ p → 1 ≤ p → ↑p + ↑q < ↑n / 2 → (p % ↑d).toNat ∉ B → (∑ k : ZMod n, ∑ l : ZMod n, if (k, l) ≠ (0, 0) ∧ ↑(largestPrimeFactor n) ^ n.factorization (largestPrimeFactor n) ∣ ↑k.val * p + ↑l.val * q then ‖normalizedDFT n (intervalIndicator n (2 * p - 1).toNat) k‖ * ‖normalizedDFT n (intervalIndicator n (2 * q - 1).toNat) l‖ else 0) ≤ 7 * ↑R * (1 + Real.log ↑n) ^ 2 / ↑P

theorem error_EPalpha_markov (n : ℕ) (hn : 2 ≤ n) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) (hq_pos : 1 ≤ q) (hq_bound : ↑q < ↑n / 2) : have P := largestPrimeFactor n; have d := P ^ n.factorization P; have R := ⌈Real.log ↑n⌉₊; ∃ (B : Finset ℕ), B.card ≤ d / R ∧ ∀ (p : ℤ), ¬↑P ∣ p → 1 ≤ p → ↑p + ↑q < ↑n / 2 → (p % ↑d).toNat ∉ B → |(errorTermEPalpha n p q).re| ≤ 7 * ↑R * ↑n.totient * (1 + Real.log ↑n) ^ 2 / ↑P

theorem error_split_bound (n : ℕ) (hn : 2 ≤ n) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) (hq_pos : 1 ≤ q) (hq_bound : ↑q < ↑n / 2) : ∃ (B : Finset ℕ), B.card ≤ largestPrimeFactor n ^ n.factorization (largestPrimeFactor n) / ⌈Real.log ↑n⌉₊ ∧ ∀ (p : ℤ), ¬↑(largestPrimeFactor n) ∣ p → 1 ≤ p → ↑p + ↑q < ↑n / 2 → (p % ↑(largestPrimeFactor n ^ n.factorization (largestPrimeFactor n))).toNat ∉ B → |↑(countingFunctionS n p q) - ↑(2 * p - 1).toNat * ↑(2 * q - 1).toNat * ↑n.totient / ↑n ^ 2| ≤ ↑n.totient * (1 + Real.log ↑n) ^ 2 / (↑(largestPrimeFactor n) - 1) + 7 * ↑⌈Real.log ↑n⌉₊ * ↑n.totient * (1 + Real.log ↑n) ^ 2 / ↑(largestPrimeFactor n)

theorem combine_error_P0_Palpha (n : ℕ) (hn : 2 ≤ n) : ↑n.totient * (1 + Real.log ↑n) ^ 2 / (↑(largestPrimeFactor n) - 1) + 7 * ↑⌈Real.log ↑n⌉₊ * ↑n.totient * (1 + Real.log ↑n) ^ 2 / ↑(largestPrimeFactor n) ≤ 9 * ↑⌈Real.log ↑n⌉₊ * ↑n.totient * (1 + Real.log ↑n) ^ 2 / ↑(largestPrimeFactor n)

theorem fourier_markov_bad_set (n : ℕ) (hn : 2 ≤ n) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) (hq_pos : 1 ≤ q) (hq_bound : ↑q < ↑n / 2) : ∃ (B : Finset ℕ), B.card ≤ largestPrimeFactor n ^ n.factorization (largestPrimeFactor n) / ⌈Real.log ↑n⌉₊ ∧ ∀ (p : ℤ), ¬↑(largestPrimeFactor n) ∣ p → 1 ≤ p → ↑p + ↑q < ↑n / 2 → (p % ↑(largestPrimeFactor n ^ n.factorization (largestPrimeFactor n))).toNat ∉ B → |↑(countingFunctionS n p q) - (2 * ↑p - 1) * (2 * ↑q - 1) * ↑n.totient / ↑n ^ 2| ≤ 9 * ↑⌈Real.log ↑n⌉₊ * ↑n.totient * (1 + Real.log ↑n) ^ 2 / ↑(largestPrimeFactor n)

theorem ceil_log_mul_sq_le_cube' (n : ℕ) (hn : 2 ≤ n) : 9 * ↑⌈Real.log ↑n⌉₊ * (1 + Real.log ↑n) ^ 2 ≤ 9 * (1 + Real.log ↑n) ^ 3

theorem log_cube_div_P_le_div_rpow' (θ : ℝ) (_hθ_pos : 0 < θ) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) : 9 * (1 + Real.log ↑n) ^ 3 / ↑(largestPrimeFactor n) ≤ 9 * (1 + Real.log ↑n) ^ 3 / ↑n ^ θ

theorem nine_hundredths_lt_tenth' (η : ℝ) (hη_pos : 0 < η) : 9 * (η ^ 2 / 100) < η ^ 2 / 10

theorem fourier_without_totient' (η θ : ℝ) (hη_pos : 0 < η) (hθ_pos : 0 < θ) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) : 9 * ↑⌈Real.log ↑n⌉₊ * (1 + Real.log ↑n) ^ 2 / ↑(largestPrimeFactor n) < η ^ 2 / 10

theorem fourier_bound_lt_target (η θ : ℝ) (hη_pos : 0 < η) (hθ_pos : 0 < θ) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) : 9 * ↑⌈Real.log ↑n⌉₊ * ↑n.totient * (1 + Real.log ↑n) ^ 2 / ↑(largestPrimeFactor n) < η ^ 2 / 10 * ↑n.totient

theorem region_implies_bounds (n : ℕ) (η : ℝ) (hη_pos : 0 < η) (hn : 2 ≤ n) (p q : ℤ) (hpq : (p, q) ∈ truncatedObtuseRegion n η) : 1 ≤ p ∧ 1 ≤ q ∧ ↑p + ↑q < ↑n / 2 ∧ ↑q < ↑n / 2

theorem error_bound_with_bad_set (η θ : ℝ) (hη_pos : 0 < η) (_hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (_hθ_lt : θ < 1) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) : ∃ (B : Finset ℕ), B.card ≤ largestPrimeFactor n ^ n.factorization (largestPrimeFactor n) / ⌈Real.log ↑n⌉₊ ∧ ∀ (p : ℤ), ¬↑(largestPrimeFactor n) ∣ p → (p, q) ∈ truncatedObtuseRegion n η → (p % ↑(largestPrimeFactor n ^ n.factorization (largestPrimeFactor n))).toNat ∉ B → |↑(countingFunctionS n p q) - (2 * ↑p - 1) * (2 * ↑q - 1) * ↑n.totient / ↑n ^ 2| < η ^ 2 / 10 * ↑n.totient

theorem combine_main_and_error (η : ℝ) (hη_pos : 0 < η) (n : ℕ) (S_val M_val : ℝ) (hM : η ^ 2 * ↑n.totient ≤ M_val) (hE : |S_val - M_val| < η ^ 2 / 10 * ↑n.totient) : η ^ 2 / 2 * ↑n.totient ≤ S_val

theorem fourier_markov_residue_bound (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) : ∃ (B : Finset ℕ), B.card ≤ largestPrimeFactor n ^ n.factorization (largestPrimeFactor n) / ⌈Real.log ↑n⌉₊ ∧ ∀ (p : ℤ), ¬↑(largestPrimeFactor n) ∣ p → (p, q) ∈ truncatedObtuseRegion n η → (p % ↑(largestPrimeFactor n ^ n.factorization (largestPrimeFactor n))).toNat ∉ B → η ^ 2 / 2 * ↑n.totient ≤ ↑(countingFunctionS n p q)

theorem bad_residues_bound (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) : ∃ (B : Finset ℕ), B.card ≤ largestPrimeFactor n ^ n.factorization (largestPrimeFactor n) / ⌈Real.log ↑n⌉₊ ∧ ∀ (p : ℤ), (p, q) ∈ residueBadPairs n η → (p % ↑(largestPrimeFactor n ^ n.factorization (largestPrimeFactor n))).toNat ∈ B

theorem residue_class_fiber_ncard_le (n d : ℕ) (hd_pos : 0 < d) (b : ℕ) (S : Set ℤ) (hS_sub : S ⊆ Set.Ico 0 (↑n / 2)) (_hS_fin : S.Finite) : {x : ℤ | x ∈ S ∧ (x % ↑d).toNat = b}.ncard ≤ n / (2 * d) + 1

theorem subset_biUnion_residue_fibers (d : ℕ) (B : Finset ℕ) (S : Set ℤ) (hS_res : ∀ x ∈ S, (x % ↑d).toNat ∈ B) : S ⊆ ⋃ b ∈ B, {x : ℤ | x ∈ S ∧ (x % ↑d).toNat = b}

theorem ncard_union_residue_classes_bound (n d K : ℕ) (hd_pos : 0 < d) (B : Finset ℕ) (hB_card : B.card ≤ K) (S : Set ℤ) (hS_sub : S ⊆ Set.Ico 0 (↑n / 2)) (hS_fin : S.Finite) (hS_res : ∀ x ∈ S, (x % ↑d).toNat ∈ B) : S.ncard ≤ K * (n / (2 * d) + 1)

theorem fiber_ncard_bound_coprime (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) (q : ℤ) (hq_coprime : q.gcd ↑(largestPrimeFactor n) = 1) : {p : ℤ | (p, q) ∈ residueBadPairs n η}.ncard ≤ largestPrimeFactor n ^ n.factorization (largestPrimeFactor n) / ⌈Real.log ↑n⌉₊ * (n / (2 * largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) + 1)

theorem fiber_ncard_bound (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) (q : ℤ) : {p : ℤ | (p, q) ∈ residueBadPairs n η}.ncard ≤ largestPrimeFactor n ^ n.factorization (largestPrimeFactor n) / ⌈Real.log ↑n⌉₊ * (n / (2 * largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) + 1)

theorem pos_of_mem_truncatedObtuseRegion_snd (n : ℕ) (η : ℝ) (hη_pos : 0 < η) (pq : ℤ × ℤ) (h : pq ∈ truncatedObtuseRegion n η) : 0 < pq.2

theorem pos_of_mem_truncatedObtuseRegion_fst (n : ℕ) (η : ℝ) (hη_pos : 0 < η) (pq : ℤ × ℤ) (h : pq ∈ truncatedObtuseRegion n η) : 0 < pq.1

theorem snd_lt_half_of_mem_truncatedObtuseRegion' (n : ℕ) (η : ℝ) (pq : ℤ × ℤ) (h : pq ∈ truncatedObtuseRegion n η) (hp_pos : 0 < pq.1) : ↑pq.2 < ↑n / 2

theorem intLe_half_of_real_lt_half (n : ℕ) (q : ℤ) (hq : ↑q < ↑n / 2) : q ≤ ↑n / 2

theorem snd_mem_Icc_of_mem_residueBadPairs (n : ℕ) (η : ℝ) (hη : 0 < η) (_hn : 2 ≤ n) (pq : ℤ × ℤ) (hpq : pq ∈ residueBadPairs n η) : pq.2 ∈ Finset.Icc 1 (↑n / 2)

theorem fiber_pair_ncard_le (S : Set (ℤ × ℤ)) (q : ℤ) : {pq : ℤ × ℤ | pq ∈ S ∧ pq.2 = q}.ncard ≤ {p : ℤ | (p, q) ∈ S}.ncard

theorem card_Icc_one_half_le (n : ℕ) (_hn : 2 ≤ n) : (Finset.Icc 1 (↑n / 2)).card ≤ n / 2

theorem residueBadPairs_ncard_from_fibers (η θ : ℝ) (hη_pos : 0 < η) (_hη_lt : η < 1 / 6) (_hθ_pos : 0 < θ) (_hθ_lt : θ < 1) (n : ℕ) (hn : 2 ≤ n) (_hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (_h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) (hfiber : ∀ (q : ℤ), {p : ℤ | (p, q) ∈ residueBadPairs n η}.ncard ≤ largestPrimeFactor n ^ n.factorization (largestPrimeFactor n) / ⌈Real.log ↑n⌉₊ * (n / (2 * largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) + 1)) : (residueBadPairs n η).ncard ≤ n / 2 * (largestPrimeFactor n ^ n.factorization (largestPrimeFactor n) / ⌈Real.log ↑n⌉₊ * (n / (2 * largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) + 1))

theorem residueBadPairs_ncard_le_counting (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) : (residueBadPairs n η).ncard ≤ n / 2 * (largestPrimeFactor n ^ n.factorization (largestPrimeFactor n) / ⌈Real.log ↑n⌉₊) * (n / (2 * largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) + 1)

theorem nat_div_prod_le (a b c d : ℕ) (hc : 0 < c) (hd : 0 < d) : a / c * (b / d) ≤ a * b / (c * d)

theorem dR_mul_n2d_le_n2R (n d R : ℕ) (hd_pos : 0 < d) (hR_pos : 0 < R) (hd_dvd : d ∣ n) : d / R * (n / (2 * d)) ≤ n / (2 * R)

theorem n2_mul_n2R_le_nsq_4R (n R : ℕ) (hR_pos : 0 < R) : n / 2 * (n / (2 * R)) ≤ n ^ 2 / (4 * R)

theorem product_bound_first_term (n d R : ℕ) (hd_pos : 0 < d) (hR_pos : 0 < R) (hd_dvd : d ∣ n) : n / 2 * (d / R) * (n / (2 * d)) ≤ n ^ 2 / (4 * R)

theorem product_bound_second_term (n d R : ℕ) (hR_pos : 0 < R) (hd_le : d ≤ n) : n / 2 * (d / R) ≤ n ^ 2 / (2 * R)

theorem combine_frac_bounds (n R : ℕ) (hR_pos : 0 < R) : n ^ 2 / (4 * R) + n ^ 2 / (2 * R) ≤ 3 * n ^ 2 / (4 * R)

theorem counting_bound_simplify (n : ℕ) (hn : 2 ≤ n) (hP_pos : 0 < largestPrimeFactor n) : n / 2 * (largestPrimeFactor n ^ n.factorization (largestPrimeFactor n) / ⌈Real.log ↑n⌉₊) * (n / (2 * largestPrimeFactor n ^ n.factorization (largestPrimeFactor n)) + 1) ≤ 3 * n ^ 2 / (4 * ⌈Real.log ↑n⌉₊)

theorem residueBadPairs_ncard_le_nat (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) : (residueBadPairs n η).ncard ≤ 3 * n ^ 2 / (4 * ⌈Real.log ↑n⌉₊)

theorem ncard_nat_to_real_bound (ncard_val n : ℕ) (_hn : 2 ≤ n) (h : ncard_val ≤ 3 * n ^ 2 / (4 * ⌈Real.log ↑n⌉₊)) : ↑ncard_val ≤ 3 / 4 * ↑n ^ 2 / ↑⌈Real.log ↑n⌉₊

theorem residueBadPairs_ncard_le (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) : ↑(residueBadPairs n η).ncard ≤ 3 / 4 * ↑n ^ 2 / ↑⌈Real.log ↑n⌉₊

theorem three_fourths_ceil_le_inv_log (n : ℕ) (hn : 2 ≤ n) : 3 / 4 * ↑n ^ 2 / ↑⌈Real.log ↑n⌉₊ ≤ ↑n ^ 2 / Real.log ↑n

theorem residueBadPairs_ncard_bound (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) : ↑(residueBadPairs n η).ncard ≤ ↑n ^ 2 / Real.log ↑n

theorem pos_of_mem_truncatedObtuseRegion_fst_pd (n : ℕ) (η : ℝ) (hη_pos : 0 < η) (pq : ℤ × ℤ) (h : pq ∈ truncatedObtuseRegion n η) : 0 < pq.1

theorem pos_of_mem_truncatedObtuseRegion_snd_pd (n : ℕ) (η : ℝ) (hη_pos : 0 < η) (pq : ℤ × ℤ) (h : pq ∈ truncatedObtuseRegion n η) : 0 < pq.2

theorem fst_lt_half_of_mem_truncatedObtuseRegion (n : ℕ) (η : ℝ) (pq : ℤ × ℤ) (h : pq ∈ truncatedObtuseRegion n η) (hq_pos : 0 < pq.2) : ↑pq.1 < ↑n / 2

theorem largestPrimeFactor_le_of_dvd_pos (P : ℕ) (p : ℤ) (hp_pos : 0 < p) (hdvd : ↑P ∣ p) : ↑P ≤ p

theorem pdivPairs_empty_of_large_P (n : ℕ) (η : ℝ) (hη_pos : 0 < η) (hP_large : n < 2 * largestPrimeFactor n) : pdivPairs n η = ∅

theorem pdivPairs_subset_prod_half (n : ℕ) (η : ℝ) (hη_pos : 0 < η) : pdivPairs n η ⊆ {x : ℤ | 0 ≤ x ∧ x ≤ ↑n / 2 ∧ ↑(largestPrimeFactor n) ∣ x} ×ˢ Set.Icc 0 (↑n / 2)

theorem ncard_nonneg_multiples_eq (B : ℤ) (P : ℕ) (hP : 0 < P) (hB : 0 ≤ B) : {x : ℤ | 0 ≤ x ∧ x ≤ B ∧ ↑P ∣ x}.ncard = B.toNat / P + 1

theorem div_two_add_one_le_1 (a : ℕ) (ha : 2 ≤ a) : a / 2 + 1 ≤ a

theorem ncard_multiples_half_le (n P : ℕ) (hP_pos : 0 < P) (h2P : 2 * P ≤ n) : {x : ℤ | 0 ≤ x ∧ x ≤ ↑n / 2 ∧ ↑P ∣ x}.ncard ≤ n / P

theorem ncard_Icc_zero_half_le (n : ℕ) (hn : 2 ≤ n) : (Set.Icc 0 (↑n / 2)).ncard ≤ n

theorem multiples_in_half_finite (n P : ℕ) : {x : ℤ | 0 ≤ x ∧ x ≤ ↑n / 2 ∧ ↑P ∣ x}.Finite

theorem Icc_zero_half_finite (n : ℕ) : (Set.Icc 0 (↑n / 2)).Finite

theorem prod_half_finite (n P : ℕ) : ({x : ℤ | 0 ≤ x ∧ x ≤ ↑n / 2 ∧ ↑P ∣ x} ×ˢ Set.Icc 0 (↑n / 2)).Finite

theorem nat_div_mul_le_mul_div (n P : ℕ) (hP_pos : 0 < P) : n / P * n ≤ n * n / P

theorem pdivPairs_ncard_le_when_small_P (n : ℕ) (η : ℝ) (hη_pos : 0 < η) (hn : 2 ≤ n) (hP_pos : 0 < largestPrimeFactor n) (h2P : 2 * largestPrimeFactor n ≤ n) : (pdivPairs n η).ncard ≤ n * n / largestPrimeFactor n

theorem nat_sq_div_le_real (n P : ℕ) (θ : ℝ) (hn : 2 ≤ n) (hP_pos : 0 < P) (hP : ↑P ≥ ↑n ^ θ) : ↑(n * n / P) ≤ ↑n ^ 2 / ↑n ^ θ

theorem pdivPairs_ncard_bound (η θ : ℝ) (hη_pos : 0 < η) (_hη_lt : η < 1 / 6) (_hθ_pos : 0 < θ) (_hθ_lt : θ < 1) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) : ↑(pdivPairs n η).ncard ≤ ↑n ^ 2 / ↑n ^ θ

theorem badPairsE_subset_union (n : ℕ) (η : ℝ) : badPairsE n η ⊆ pdivPairs n η ∪ residueBadPairs n η

theorem badPairsE_ncard_le (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) : ↑(badPairsE n η).ncard ≤ ↑n ^ 2 * (1 / ↑n ^ θ + 1 / Real.log ↑n)

theorem exists_fourier_exceptional_superset (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) : ∃ (E' : Set (ℤ × ℤ)), E'.Finite ∧ badPairsE n η ⊆ E' ∧ ↑E'.ncard ≤ ↑n ^ 2 * (1 / ↑n ^ θ + 1 / Real.log ↑n)

theorem badPairsE_ncard_bound (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) : ↑(badPairsE n η).ncard ≤ ↑n ^ 2 * (1 / ↑n ^ θ + 1 / Real.log ↑n)

theorem exceptional_set_construction_single_n (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) (n : ℕ) (hn : 2 ≤ n) (hP : ↑(largestPrimeFactor n) ≥ ↑n ^ θ) (h_small : (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < η ^ 2 / 100) : ∃ E ⊆ truncatedObtuseRegion n η, E.Finite ∧ ↑E.ncard ≤ ↑n ^ 2 * (1 / ↑n ^ θ + 1 / Real.log ↑n) ∧ ∀ pq ∈ truncatedObtuseRegion n η, pq.2.gcd ↑(largestPrimeFactor n) = 1 → pq ∉ E → η ^ 2 / 2 * ↑n.totient ≤ ↑(countingFunctionS n pq.1 pq.2)

theorem log_ge_one_of_ge_three (n : ℕ) (hn : 3 ≤ n) : 1 ≤ Real.log ↑n

theorem one_plus_log_pow_le (n : ℕ) (hn : 3 ≤ n) : (1 + Real.log ↑n) ^ 3 ≤ 8 * Real.log ↑n ^ 3

theorem norm_log_pow_le_mul_norm_rpow (θ : ℝ) (hθ : 0 < θ) (c : ℝ) (hc : 0 < c) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖Real.log ↑n ^ 3‖ ≤ c * ‖↑n ^ θ‖

theorem norm_bound_implies_div_lt (θ ε : ℝ) (hε : 0 < ε) (n : ℕ) (hn : 1 ≤ n) (hbound : ‖Real.log ↑n ^ 3‖ ≤ ε / 2 * ‖↑n ^ θ‖) : Real.log ↑n ^ 3 / ↑n ^ θ < ε

theorem norm_bound_to_div_lt (θ : ℝ) (_hθ : 0 < θ) (ε : ℝ) (hε : 0 < ε) (N : ℕ) (hN : ∀ (n : ℕ), N ≤ n → ‖Real.log ↑n ^ 3‖ ≤ ε / 2 * ‖↑n ^ θ‖) : ∃ (N' : ℕ), ∀ (n : ℕ), N' ≤ n → Real.log ↑n ^ 3 / ↑n ^ θ < ε

theorem log_pow_three_div_rpow_eventually_lt (θ : ℝ) (hθ : 0 < θ) (ε : ℝ) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → Real.log ↑n ^ 3 / ↑n ^ θ < ε

theorem log_pow_over_rpow_eventually_lt (θ : ℝ) (hθ_pos : 0 < θ) (ε : ℝ) (hε : 0 < ε) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → (1 + Real.log ↑n) ^ 3 / ↑n ^ θ < ε

theorem exceptional_set_with_counting_bound (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) : ∃ (N₁ : ℕ), ∀ (n : ℕ), N₁ ≤ n → ↑(largestPrimeFactor n) ≥ ↑n ^ θ → ∃ E ⊆ truncatedObtuseRegion n η, E.Finite ∧ ↑E.ncard ≤ ↑n ^ 2 * (1 / ↑n ^ θ + 1 / Real.log ↑n) ∧ ∀ pq ∈ truncatedObtuseRegion n η, pq.2.gcd ↑(largestPrimeFactor n) = 1 → pq ∉ E → η ^ 2 / 2 * ↑n.totient ≤ ↑(countingFunctionS n pq.1 pq.2)

theorem pred_sq_ge (p : ℕ) (hp : 3 ≤ p) : p ≤ (p - 1) ^ 2

theorem odd_prime_pow_le_totient_sq (p k : ℕ) (hp : Nat.Prime p) (hodd : p ≠ 2) (hk : 1 ≤ k) : p ^ k ≤ (p ^ k).totient ^ 2

theorem ordCompl_lt_of_dvd (n p : ℕ) (hn : 0 < n) (hp : Nat.Prime p) (hdvd : p ∣ n) : n / p ^ n.factorization p < n

theorem not_two_dvd_of_dvd_odd (n d : ℕ) (hodd : ¬2 ∣ n) (hdvd : d ∣ n) : ¬2 ∣ d

theorem totient_sq_mul_of_coprime (a b : ℕ) (hcop : a.Coprime b) (ha : a ≤ a.totient ^ 2) (hb : b ≤ b.totient ^ 2) : a * b ≤ (a * b).totient ^ 2

theorem odd_le_totient_sq (n : ℕ) (hn : 1 ≤ n) (hodd : ¬2 ∣ n) : n ≤ n.totient ^ 2

theorem pow_two_le_two_mul_totient_sq (k : ℕ) (hk : 1 ≤ k) : 2 ^ k ≤ 2 * (2 ^ k).totient ^ 2

theorem totient_sq_lower_bound (n : ℕ) (hn : 1 ≤ n) : n ≤ 2 * n.totient ^ 2

theorem totient_tendsto_atTop (K : ℕ) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → K ≤ n.totient

theorem totient_large_enough (η : ℝ) (hη_pos : 0 < η) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → 5 ≤ η ^ 2 / 2 * ↑n.totient

theorem countingFunctionS_ge_five_outside_exceptional (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) : ∃ (N₀ : ℕ), ∀ (n : ℕ), N₀ ≤ n → ↑(largestPrimeFactor n) ≥ ↑n ^ θ → ∃ (exceptionalPairs : Set (ℤ × ℤ)), exceptionalPairs.Finite ∧ ↑exceptionalPairs.ncard ≤ ↑n ^ 2 * (1 / ↑n ^ θ + 1 / Real.log ↑n) ∧ ∀ pq ∈ truncatedObtuseRegion n η, pq.2.gcd ↑(largestPrimeFactor n) = 1 → pq ∉ exceptionalPairs → 5 ≤ countingFunctionS n pq.1 pq.2

theorem badPairsSet_ncard_upper_bound (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) : ∃ (C : ℝ) (N₂ : ℕ), 0 < C ∧ ∀ (n : ℕ), N₂ ≤ n → ↑(largestPrimeFactor n) ≥ ↑n ^ θ → ↑(badPairsSet n η).ncard ≤ C * ↑n ^ 2 * (1 / ↑n ^ θ + 1 / Real.log ↑n)

theorem inv_rpow_tendsto_zero (θ : ℝ) (hθ_pos : 0 < θ) : Filter.Tendsto (fun (n : ℕ) => 1 / ↑n ^ θ) Filter.atTop (nhds 0)

theorem dist_to_ineq (θ : ℝ) (_hθ_pos : 0 < θ) (ε : ℝ) (_hε : 0 < ε) : (∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → dist (1 / ↑n ^ θ) 0 < ε) → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → 1 / ↑n ^ θ < ε

theorem inv_rpow_eventually_lt (θ : ℝ) (hθ_pos : 0 < θ) (ε : ℝ) : 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → 1 / ↑n ^ θ < ε

theorem inv_log_eventually_lt (ε : ℝ) : 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → 1 / Real.log ↑n < ε

theorem asymptotic_decay (θ : ℝ) (hθ_pos : 0 < θ) (ε : ℝ) : 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → 1 / ↑n ^ θ + 1 / Real.log ↑n < ε

theorem ratio_bound_core (bad Hn c C n2 decay ε : ℝ) (hc_pos : 0 < c) (hC_pos : 0 < C) (hε_pos : 0 < ε) (hn2_pos : 0 < n2) (_h_bad_nonneg : 0 ≤ bad) (h_upper : bad ≤ C * n2 * decay) (h_lower : c * n2 ≤ Hn) (h_decay : decay < c * ε / C) : bad / Hn < ε

theorem ratio_bound_from_three_lemmas (c C : ℝ) (N₁ N₂ : ℕ) (η θ : ℝ) (hc_pos : 0 < c) (hC_pos : 0 < C) (h_lower : ∀ (n : ℕ), N₁ ≤ n → c * ↑n ^ 2 ≤ ↑(truncatedObtuseRegion n η).ncard) (h_upper : ∀ (n : ℕ), N₂ ≤ n → ↑(largestPrimeFactor n) ≥ ↑n ^ θ → ↑(badPairsSet n η).ncard ≤ C * ↑n ^ 2 * (1 / ↑n ^ θ + 1 / Real.log ↑n)) (_hη_pos : 0 < η) (_hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (ε : ℝ) : 0 < ε → ∃ (N₀ : ℕ), ∀ (n : ℕ), N₀ ≤ n → ↑(largestPrimeFactor n) ≥ ↑n ^ θ → ↑(badPairsSet n η).ncard / ↑(truncatedObtuseRegion n η).ncard < ε

theorem analyticEngine_lower_bound (η θ : ℝ) (hη_pos : 0 < η) (hη_lt : η < 1 / 6) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) (ε : ℝ) : 0 < ε → ∃ (N₀ : ℕ), ∀ (n : ℕ), N₀ ≤ n → ↑(largestPrimeFactor n) ≥ ↑n ^ θ → ↑(badPairsSet n η).ncard / ↑(truncatedObtuseRegion n η).ncard < ε