mem_nonzeroS_iff

the one or two numbers s where ψ (D ^ (-s) * x) is possibly nonzero -/ def nonzeroS (x : ℝ) : Finset ℤ := Finset.Icc ⌊(1 + logb D (2 * x))⌋ ⌈logb D (4 * x)⌉

---

section include_hD

/- The goal of the next several lemmas is to prove sum_ψ, which says that ∑ s ∈ nonzeroS D x, ψ D (D ^ (-s) * x) = 1.

The first four lemmas prove some properties of the endpoints of nonzeroS D x, and in particular show that nonzeroS D x has either 1 or 2 elements. The next two lemmas prove sum_ψ in the 1-element and 2-element cases, respectively, and then sum_ψ follows immediately. -/

include hD

private lemma le_div_ceil_mul (hx : 0 < x) : 1 / (4 * D) ≤ D ^ (-⌈logb D (4 * x)⌉) * x := by rw [← div_le_iff₀ hx, div_div, ← rpow_logb (D0 hD) (ne_of_gt hD) (cDx0 hD four_pos hx), ← inv_eq_one_div, (by norm_cast : (D : ℝ) ^ (-⌈logb D (4 * x)⌉) = D ^ (-⌈logb D (4 * x)⌉ : ℝ)), ← rpow_neg (D0 hD).le, rpow_le_rpow_left_iff hD, neg_le_neg_iff] apply le_of_le_of_eq <| calc (⌈logb D (4 * x)⌉ : ℝ) ≤ ⌊logb D (4 * x)⌋ + 1 := by exact_mod_cast Int.ceil_le_floor_add_one _ _ ≤ logb D (4 * x) + 1 := by gcongr; exact Int.floor_le (logb D (4 * x)) rw [← logb_self_eq_one hD, ← logb_mul (mul_pos four_pos hx).ne.symm (ne_of_gt (D0 hD)), mul_assoc, mul_assoc, mul_comm _ x]

private lemma one_add_logb (hx : x > 0) : 1 + logb D (2 * x) = logb D (2 * D * x) := by rw [← logb_self_eq_one hD, ← logb_mul (D0 hD).ne.symm (mul_pos two_pos hx).ne.symm, ← mul_assoc, mul_comm (D : ℝ) 2]

-- If D ^ (-⌈logb D (4 * x)⌉) ≥ 1 / (2 * D * x), then the endpoints of nonzeroS x are equal. private lemma eq_endpoints (hx : 0 < x) (h : D ^ (-⌈logb D (4 * x)⌉) ≥ 1 / (2 * D * x)) : ⌊(1 + logb D (2 * x))⌋ = ⌈logb D (4 * x)⌉ := by rw [Int.floor_eq_iff, one_add_logb hD hx] constructor · rw [← rpow_le_rpow_left_iff hD, ← inv_le_inv₀ (by positivity) (by positivity), rpow_logb (D0 hD) (ne_of_gt hD) (cDx0 hD two_pos hx), ← rpow_neg (D0 hD).le, inv_eq_one_div] exact_mod_cast h.le · have : logb D (2 * D * x) < logb D (4 * D * x) := by refine (strictMonoOn_logb hD) ?_ ?_ (by linarith [(cDx0 hD two_pos hx)]) <;> exact mem_Ioi.2 (cDx0 hD (by norm_num) hx) apply lt_of_lt_of_le this rw [mul_comm, ← mul_assoc, mul_comm x 4, logb_mul (mul_pos four_pos hx).ne.symm (D0 hD).ne.symm, logb_self_eq_one hD, add_le_add_iff_right, mul_comm] exact Int.le_ceil _

-- If D ^ (-⌈logb D (4 * x)⌉) < 1 / (2 * D * x), then the endpoints of nonzeroS x differ by 1. private lemma endpoint_sub_one (hx : 0 < x) (h : D ^ (-⌈logb D (4 * x)⌉) < 1 / (2 * D * x)) : ⌊1 + logb D (2 * x)⌋ = ⌈logb D (4 * x)⌉ - 1 := by rw [one_add_logb hD hx] apply le_antisymm · rw [← inv_eq_one_div, zpow_neg, inv_lt_inv₀ (by positivity) (cDx0 hD two_pos hx)] at h rw [Int.le_sub_one_iff, Int.floor_lt, ← rpow_lt_rpow_left_iff hD, rpow_logb (D0 hD) (ne_of_gt hD) (cDx0 hD two_pos hx)] exact_mod_cast h · apply sub_le_iff_le_add.2 ∘ Int.ceil_le.2 suffices logb D (4 * x) ≤ logb D (2 * D * x) by exact_mod_cast (lt_of_le_of_lt this (Int.lt_floor_add_one )).le have : 4 * x ≤ 2 * D * x := (mul_le_mul_iff_left₀ hx).2 (by linarith [D2 hD]) refine (strictMonoOn_logb hD).monotoneOn ? ?_ this <;> exact mem_Ioi.2 (by positivity)

-- Special case of sum_ψ, for the case where nonzeroS D x has one element. private lemma sum_ψ₁ (hx : 0 < x) (h : D ^ (-⌈logb D (4 * x)⌉) ≥ 1 / (2 * D * x)) : ∑ s ∈ nonzeroS D x, ψ D (D ^ (-s) * x) = 1 := by rw [nonzeroS, eq_endpoints hD hx h, Finset.Icc_self, Finset.sum_singleton] refine ψ_formula₂ hD ⟨le_of_eq_of_le (by field_simp) ((mul_le_mul_iff_left₀ hx).2 h), ?_⟩ calc D ^ (-⌈logb D (4 * x)⌉) * x = D ^ (-⌈logb D (4 * x)⌉ : ℝ) * x := by norm_cast _ ≤ D ^ (-logb D (4 * x)) * x := by gcongr; exacts [hD.le, Int.le_ceil _] _ = 1 / (4 * x) * x := by rw [rpow_neg (D0 hD).le, inv_eq_one_div, rpow_logb (D0 hD) hD.ne.symm (by linarith)] _ = 1 / 4 := by field_simp

-- Special case of sum_ψ, for the case where nonzeroS D x has two elements. private lemma sum_ψ₂ (hx : 0 < x) (h : D ^ (-⌈logb D (4 * x)⌉) < 1 / (2 * D * x)) : ∑ s ∈ nonzeroS D x, ψ D (D ^ (-s) * x) = 1 := by -- Replace nonzeroS D x with {s₀ - 1, s₀}, where s₀ := ⌈logb D (4 * x)⌉ have endpts := endpoint_sub_one hD hx h have ne : ⌈logb D (4 * x)⌉ - 1 ≠ ⌈logb D (4 * x)⌉ := pred_ne_self _ have : nonzeroS D x = {⌈logb D (4 * x)⌉ - 1, ⌈logb D (4 * x)⌉} := by rw [nonzeroS, ← endpts] have Icc_of_eq_add_one {a b : ℤ} (h : a + 1 = b) : Finset.Icc a b = {a, b} := by subst h; exact Int.Icc_eq_pair a exact Icc_of_eq_add_one (add_eq_of_eq_sub endpts) set s₀ := ⌈logb D (4 * x)⌉ rw [this, Finset.sum_insert ((Finset.notMem_singleton).2 ne), Finset.sum_singleton] -- Now calculate the sum have Ds₀x_lt := (mul_lt_mul_iff_left₀ hx).2 h rw [← div_div, div_mul_cancel₀ _ (ne_of_gt hx)] at Ds₀x_lt have hs₀ := And.intro (le_div_ceil_mul hD hx) Ds₀x_lt.le suffices 1 / 4 ≤ D ^ (-(s₀ - 1)) * x ∧ D ^ (-(s₀ - 1)) * x ≤ 1 / 2 by rw [ψ_formula₁ hD hs₀, ψ_formula₃ hD this] suffices (D : ℝ) ^ (1 - s₀) = D * D ^ (-s₀) by rw [neg_sub, this]; ring rw [zpow_sub₀ (ne_of_gt (D0 hD)), zpow_neg, zpow_one, div_eq_mul_inv] rw [neg_sub, sub_eq_add_neg, zpow_add₀ (ne_of_gt (D0 hD)), zpow_one, mul_assoc] constructor · rw [← div_le_iff₀' (D0 hD), div_div]; exact hs₀.1 · rw [← le_div_iff₀' (D0 hD), div_div]; exact hs₀.2

-- See finsum_ψ for the version that doesn't explicitly restrict to the support. lemma sum_ψ (hx : 0 < x) : ∑ s ∈ nonzeroS D x, ψ D (D ^ (-s) * x) = 1 := by by_cases h : D ^ (-⌈logb D (4 * x)⌉) ≥ 1 / (2 * D * x) · exact sum_ψ₁ hD hx h · exact sum_ψ₂ hD hx (lt_of_not_ge h)

---

/- Now we prove that nonzeroS D x is the support of s ↦ ψ D (D ^ (-s) * x). This converts sum_ψ into finsum_ψ, which states that ∑ᶠ s : ℤ, ψ D (D ^ (-s) * x) = 1.