ZetaAppendix.lemma_abadimpseri

@[blueprint  "lem:abadimpseri"  (title := "Estimate for an inverse cubic series")  (statement := /--For $\vartheta\in \mathbb{R}$ with $0\leq |\vartheta|< 1$,\[\sum_n\left(\frac{1}{(n-\vartheta)^3} + \frac{1}{(n+\vartheta)^3}\right)\leq \frac{1}{(1-|\vartheta|)^3} + 2\zeta(3)-1.\]-/)  (proof := /--Since $\frac{1}{(n-\vartheta)^3} + \frac{1}{(n+\vartheta)^3}$ is even,we may replace $\vartheta$ by $|\vartheta|$. Then we rearrange the sum:\[\sum_{n=1}^\infty \left(\frac{1}{(n-|\vartheta|)^3} + \frac{1}{(n+|\vartheta|)^3}\right)  = \frac{1}{(1-|\vartheta|)^3}  + \sum_{n=1}^\infty \left(\frac{1}{\left(n+1-|\vartheta|\right)^3}  + \frac{1}{\left(n+|\vartheta|\right)^3}\right).\]We may write $(n+1-|\vartheta|)^3$, $(n+|\vartheta|)^3$as $(n+\frac{1}{2}-t)^3$, $(n+\frac{1}{2} + t)^3$ for $t = |\vartheta|-1/2$.Since $1/u^3$ is convex, $\frac{1}{(n+1/2-t)^3} + \frac{1}{(n+1/2+t)^3}$ reaches itsmaximum on $[-1/2,1/2]$ at the endpoints. Hence\[\sum_{n=1}^\infty \left(\frac{1}{\left(n+1-|\vartheta|\right)^3}  + \frac{1}{\left(n+|\vartheta|\right)^3}\right)  \leq \sum_{n=1}^\infty \left(\frac{1}{n^3} + \frac{1}{(n+1)^3}\right) = 2 \zeta(3)-1.\]-/)  (latexEnv := "lemma")  (discussion := 571)]lemma lemma_abadimpseri (ϑ : ℝ) (hϑ : |ϑ| < 1) :    ∑' n : ℕ, (1 / ((n + 1 : ℝ) - ϑ) ^ 3 + 1 / ((n + 1 : ℝ) + ϑ) ^ 3) ≤      1 / (1 - |ϑ|) ^ 3 + 2 * (riemannZeta 3).re - 1 := by  have h_sum_bound : ∀ n : ℕ, (1 / (n + 1 - ϑ) ^ 3 + 1 / (n + 1 + ϑ) ^ 3) ≤      (1 / (n + 1 - |ϑ|) ^ 3 + 1 / (n + 1 + |ϑ|) ^ 3) := by intro n; cases abs_cases ϑ <;> grind  have h_sum_bound_endpoints : (∑' n : ℕ, (1 / (n + 1 - |ϑ|) ^ 3 + 1 / (n + 1 + |ϑ|) ^ 3)) ≤      (1 / (1 - |ϑ|) ^ 3) + 2 * (riemannZeta 3).re - 1 := by    have h_sum_endpoints_bound : (∑' n : ℕ, (1 / (n + 2 - |ϑ|) ^ 3 + 1 / (n + 1 + |ϑ|) ^ 3)) ≤        2 * (riemannZeta 3).re - 1 := by      have h_term_bound : ∀ n : ℕ, (1 / (n + 2 - |ϑ|) ^ 3 + 1 / (n + 1 + |ϑ|) ^ 3) ≤          (1 / (n + 1) ^ 3 + 1 / (n + 2) ^ 3) := by        intro n        rw [div_add_div, div_add_div, div_le_div_iff₀] <;> try positivity        · have h_simp : (n + 1 + |ϑ|) ^ 3 + (n + 2 - |ϑ|) ^ 3 ≤ (n + 1) ^ 3 + (n + 2) ^ 3 := by            nlinarith [abs_nonneg ϑ, pow_two_nonneg (|ϑ| : ℝ), pow_two_nonneg (n : ℝ),              mul_lt_mul_of_pos_left hϑ <| Nat.cast_add_one_pos n]          field_simp          refine le_trans (mul_le_mul_of_nonneg_left h_simp <| by positivity) ?_          have h_simp : (n + 1 : ℝ) ^ 3 * (n + 2) ^ 3 ≤ (n + 1 + |ϑ|) ^ 3 * (n + 2 - |ϑ|) ^ 3 := by            rw [← mul_pow, ← mul_pow]; exact pow_le_pow_left₀ (by positivity) (by nlinarith [abs_nonneg ϑ]) _          exact mul_le_mul h_simp (by linarith) (by positivity)            (by exact mul_nonneg (pow_nonneg (by positivity) _) (pow_nonneg (by linarith [abs_nonneg ϑ]) _))        · exact mul_pos (pow_pos (by linarith [abs_nonneg ϑ]) _) (pow_pos (by linarith [abs_nonneg ϑ]) _)        · exact pow_ne_zero _ (by linarith [abs_nonneg ϑ])      refine le_trans (Summable.tsum_le_tsum h_term_bound ?_ ?_) ?_      · exact of_nonneg_of_le (fun n ↦ add_nonneg (one_div_nonneg.mpr (pow_nonneg (by linarith [abs_nonneg ϑ]) _))          (one_div_nonneg.mpr (pow_nonneg (by linarith [abs_nonneg ϑ]) _)))            h_term_bound (add (by exact_mod_cast summable_nat_add_iff 1 |>.2 <| summable_one_div_nat_pow.2 <| by omega)              (by exact_mod_cast summable_nat_add_iff 2 |>.2 <| summable_one_div_nat_pow.2 <| by omega))      · exact add (by simpa using summable_nat_add_iff 1 |>.2 <| summable_one_div_nat_pow.2 <| by omega)          (by simpa using summable_nat_add_iff 2 |>.2 <| summable_one_div_nat_pow.2 <| by omega)      · have h_sum_zeta : ∑' n : ℕ, (1 / (n + 1 : ℝ) ^ 3 + 1 / (n + 2 : ℝ) ^ 3) =            2 * (∑' n : ℕ, (1 / (n + 1 : ℝ) ^ 3)) - 1 := by          rw [Summable.tsum_add, Summable.tsum_eq_zero_add] <;> norm_num          · norm_num [add_assoc]; ring          · exact_mod_cast summable_nat_add_iff 1 |>.2 <| summable_nat_pow_inv.2 <| by omega          · exact_mod_cast summable_nat_add_iff 1 |>.2 <| summable_nat_pow_inv.2 <| by omega          · exact_mod_cast summable_nat_add_iff 2 |>.2 <| summable_nat_pow_inv.2 <| by omega        convert h_sum_zeta.le using 2        erw [zeta_eq_tsum_one_div_nat_add_one_cpow] <;> norm_num        · convert ofReal_re _; simp [Complex.ofReal_tsum]    rw [Summable.tsum_eq_zero_add]    · norm_num [add_assoc, add_left_comm, add_comm, div_eq_mul_inv, mul_add, mul_comm,        mul_left_comm, tsum_mul_left] at *      have hs₁ : Summable fun n : ℕ ↦ ((|ϑ| + (n + 1)) ^ 3)⁻¹ :=        of_nonneg_of_le (fun n ↦ inv_nonneg.2 (pow_nonneg (by positivity) _))          (fun n ↦ by simpa using inv_anti₀ (by positivity) (pow_le_pow_left₀ (by positivity)            (show (|ϑ| + (n + 1) : ℝ) ≥ n + 1 by linarith [abs_nonneg ϑ]) 3))          (summable_nat_add_iff 1 |>.2 <| Real.summable_one_div_nat_pow.2 <| by omega)      have hs₂ : Summable fun n : ℕ ↦ (((n : ℝ) + 2 - |ϑ|) ^ 3)⁻¹ :=        of_nonneg_of_le (fun n ↦ inv_nonneg.2 (pow_nonneg (by linarith [abs_nonneg ϑ]) _))          (fun n ↦ by rw [inv_le_comm₀] <;> norm_num <;> ring_nf <;>            nlinarith [abs_nonneg ϑ, pow_two_nonneg ((n : ℝ) + 1 - |ϑ|)])          (summable_nat_add_iff 1 |>.2 <| Real.summable_one_div_nat_pow.2 one_lt_two)      rw [Summable.tsum_add hs₁ hs₂] at h_sum_endpoints_bound      rw [Summable.tsum_add]      · rw [show (∑' b : ℕ, ((|ϑ| + (b + 2)) ^ 3)⁻¹) = (∑' b : ℕ, ((|ϑ| + (b + 1)) ^ 3)⁻¹) - ((|ϑ| + 1) ^ 3)⁻¹ from ?_]        · nlinarith [show 0 < (|ϑ| + 1) ^ 3 by positivity, inv_mul_cancel₀ (show (|ϑ| + 1) ^ 3 ≠ 0 by positivity)]        · rw [eq_comm, Summable.tsum_eq_zero_add]          · norm_num [add_assoc]          · exact hs₁      · exact_mod_cast of_nonneg_of_le (fun n ↦ by positivity)          (fun n ↦ by rw [inv_le_comm₀] <;> norm_num <;> ring_nf <;> nlinarith only [abs_nonneg ϑ, hϑ])            (summable_nat_add_iff 1 |>.2 <| Real.summable_one_div_nat_pow.2 one_lt_two)      · exact hs₂    · refine Summable.add ?_ ?_      · have : Summable (fun n : ℕ ↦ (1 : ℝ) / (n : ℝ) ^ 3) := summable_one_div_nat_pow.2 (by omega)        rw [← summable_nat_add_iff 1] at this ⊢        exact of_nonneg_of_le (fun n ↦ one_div_nonneg.mpr (pow_nonneg (by cases abs_cases ϑ <;> linarith) _))          (fun n ↦ one_div_le_one_div_of_le (by positivity)            (pow_le_pow_left₀ (by positivity) (by cases abs_cases ϑ <;> linarith) _)) this      · exact_mod_cast of_nonneg_of_le (fun n ↦ by positivity)          (fun n ↦ by simpa using inv_anti₀ (by positivity) (pow_le_pow_left₀ (by positivity)            (show (n : ℝ) + 1 + |ϑ| ≥ n + 1 by linarith [abs_nonneg ϑ]) 3))          (summable_nat_add_iff 1 |>.2 <| Real.summable_one_div_nat_pow.2 <| by omega)  refine le_trans (Summable.tsum_le_tsum h_sum_bound ?_ ?_) h_sum_bound_endpoints  · have h_bound : ∀ n : ℕ,        (1 / (n + 1 - ϑ) ^ 3 + 1 / (n + 1 + ϑ) ^ 3) ≤ 2 / (n + 1 - |ϑ|) ^ 3 := fun n ↦ by      have : (1 / (n + 1 - ϑ) ^ 3 + 1 / (n + 1 + ϑ) ^ 3) ≤          (1 / (n + 1 - |ϑ|) ^ 3 + 1 / (n + 1 - |ϑ|) ^ 3) := by        cases abs_cases ϑ <;> simp only [add_le_add_iff_left, one_div, sub_neg_eq_add, add_le_add_iff_right, *]        · exact inv_anti₀ (pow_pos (by linarith) _) (by gcongr <;> linarith)        · exact inv_anti₀ (pow_pos (by linarith) _)            (pow_le_pow_left₀ (by linarith) (by linarith) _)      exact this.trans_eq (by ring)    refine of_nonneg_of_le (fun n ↦ ?_) (fun n ↦ h_bound n) ?_    · exact add_nonneg (one_div_nonneg.mpr (pow_nonneg (by linarith [abs_lt.mp hϑ]) _))        (one_div_nonneg.mpr (pow_nonneg (by linarith [abs_lt.mp hϑ]) _))    · have : Summable (fun n : ℕ ↦ 2 / (n : ℝ) ^ 3) :=        mul_left 2 <| Real.summable_nat_pow_inv.2 (by norm_num : (1 : ℕ) < 3)      rw [← summable_nat_add_iff 1] at this ⊢      exact of_nonneg_of_le (fun n ↦ div_nonneg zero_le_two (pow_nonneg (by linarith [abs_nonneg ϑ]) _))        (fun n ↦ div_le_div_of_nonneg_left (by positivity) (by positivity)          (pow_le_pow_left₀ (by linarith [abs_nonneg ϑ]) (by linarith [abs_nonneg ϑ]) _)) this  · refine add ?_ ?_    · rw [← summable_nat_add_iff 1]      simp only [one_div, Nat.cast_add, Nat.cast_one] at *      exact of_nonneg_of_le (fun n ↦ inv_nonneg.2 (pow_nonneg (by linarith [abs_nonneg ϑ]) _))        (fun n ↦ by rw [inv_le_comm₀] <;> norm_num <;> ring_nf <;>          nlinarith [abs_nonneg ϑ, pow_two_nonneg ((n : ℝ) ^ 2), pow_two_nonneg ((n : ℝ) + 1),            pow_two_nonneg ((n : ℝ) + 1 - |ϑ|)]) (summable_nat_add_iff 1 |>.2 <| summable_one_div_nat_pow.2 one_lt_two)    · exact of_nonneg_of_le (fun n ↦ by positivity)        (fun n ↦ by simpa using inv_anti₀ (by positivity) (pow_le_pow_left₀ (by positivity)          (show (n : ℝ) + 1 + |ϑ| ≥ n + 1 by linarith [abs_nonneg ϑ]) 3))            (summable_nat_add_iff 1 |>.2 <| summable_one_div_nat_pow.2 <| by omega)