11.17. HardyZeta.ThetaDecay🔗

theorem norm_psi_le_two_exp {z : ℂ} (hz : 1 ≤ z.re) : ‖psi z‖ ≤ 2 * Real.exp (-Real.pi * z.re) := byz:ℂhz:1 ≤ z.re⊢ ‖psi z‖ ≤ 2 * Real.exp (-Real.pi * z.re) have hz0 : 0 < z.re := by linarithz:ℂhz:1 ≤ z.rehz0:0 < z.re⊢ ‖psi z‖ ≤ 2 * Real.exp (-Real.pi * z.re) have hpi : 1 ≤ Real.pi * z.re := by nlinarith [Real.pi_gt_three]z:ℂhz:1 ≤ z.rehz0:0 < z.rehpi:1 ≤ Real.pi * z.re⊢ ‖psi z‖ ≤ 2 * Real.exp (-Real.pi * z.re) have hexp : 2 ≤ Real.exp (Real.pi * z.re) := by linarith [Real.add_one_le_exp (Real.pi * z.re)]z:ℂhz:1 ≤ z.rehz0:0 < z.rehpi:1 ≤ Real.pi * z.rehexp:2 ≤ Real.exp (Real.pi * z.re)⊢ ‖psi z‖ ≤ 2 * Real.exp (-Real.pi * z.re) have hsmall : Real.exp (-Real.pi * z.re) ≤ 1 / 2 := by rw [neg_mul,z:ℂhz:1 ≤ z.rehz0:0 < z.rehpi:1 ≤ Real.pi * z.rehexp:2 ≤ Real.exp (Real.pi * z.re)⊢ Real.exp (-(Real.pi * z.re)) ≤ 1 / 2 Real.exp_negz:ℂhz:1 ≤ z.rehz0:0 < z.rehpi:1 ≤ Real.pi * z.rehexp:2 ≤ Real.exp (Real.pi * z.re)⊢ (Real.exp (Real.pi * z.re))⁻¹ ≤ 1 / 2]z:ℂhz:1 ≤ z.rehz0:0 < z.rehpi:1 ≤ Real.pi * z.rehexp:2 ≤ Real.exp (Real.pi * z.re)⊢ (Real.exp (Real.pi * z.re))⁻¹ ≤ 1 / 2 simpa only [one_div] using (one_div_le_one_div_of_le (byz:ℂhz:1 ≤ z.rehz0:0 < z.rehpi:1 ≤ Real.pi * z.rehexp:2 ≤ Real.exp (Real.pi * z.re)⊢ 0 < 2 norm_numAll goals completed! 🐙 : (0 : ℝ) < 2) hexp)z:ℂhz:1 ≤ z.rehz0:0 < z.rehpi:1 ≤ Real.pi * z.rehexp:2 ≤ Real.exp (Real.pi * z.re)hsmall:Real.exp (-Real.pi * z.re) ≤ 1 / 2⊢ ‖psi z‖ ≤ 2 * Real.exp (-Real.pi * z.re) have hpos := Real.exp_pos (-Real.pi * z.re)z:ℂhz:1 ≤ z.rehz0:0 < z.rehpi:1 ≤ Real.pi * z.rehexp:2 ≤ Real.exp (Real.pi * z.re)hsmall:Real.exp (-Real.pi * z.re) ≤ 1 / 2hpos:0 < Real.exp (-Real.pi * z.re)⊢ ‖psi z‖ ≤ 2 * Real.exp (-Real.pi * z.re) apply (norm_psi_le hz0).transz:ℂhz:1 ≤ z.rehz0:0 < z.rehpi:1 ≤ Real.pi * z.rehexp:2 ≤ Real.exp (Real.pi * z.re)hsmall:Real.exp (-Real.pi * z.re) ≤ 1 / 2hpos:0 < Real.exp (-Real.pi * z.re)⊢ Real.exp (-Real.pi * z.re) / (1 - Real.exp (-Real.pi * z.re)) ≤ 2 * Real.exp (-Real.pi * z.re) apply (div_le_iff₀ (byz:ℂhz:1 ≤ z.rehz0:0 < z.rehpi:1 ≤ Real.pi * z.rehexp:2 ≤ Real.exp (Real.pi * z.re)hsmall:Real.exp (-Real.pi * z.re) ≤ 1 / 2hpos:0 < Real.exp (-Real.pi * z.re)⊢ 0 < 1 - Real.exp (-Real.pi * z.re) linarithAll goals completed! 🐙 : 0 < 1 - Real.exp (-Real.pi * z.re))).mpr nlinarithAll goals completed! 🐙 /-- A single exponential bounds both reciprocal terms in the cusp identity. -/theorem norm_psi_cusp_le_exp {z : ℂ} (hz : 0 < z.re) (hfar : 1 ≤ (1 / (4 * z)).re) : ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z ^ (1 / 2 : ℂ)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re) := byz:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).re⊢ ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re) have hz0 : z ≠ 0 := by intro hz:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).reh:z = 0⊢ False; simp [h] at hzz:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0⊢ ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re) have heq : (1 / z : ℂ) = 4 * (1 / (4 * z)) := by field_simpz:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))⊢ ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re) have hre : (1 / z).re = 4 * (1 / (4 * z)).re := by conv_lhs => rw [heq]z:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))| (4 * (1 / (4 * z))).re simpz:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).re⊢ ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re) have hfar' : 1 ≤ (1 / z).re := by rw [hrez:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).re⊢ 1 ≤ 4 * (1 / (4 * z)).re]z:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).re⊢ 1 ≤ 4 * (1 / (4 * z)).re; linarithz:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).rehfar':1 ≤ (1 / z).re⊢ ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re) have hexp : Real.exp (-Real.pi * (1 / z).re) ≤ Real.exp (-Real.pi * (1 / (4 * z)).re) := by apply Real.exp_le_exp.mprz:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).rehfar':1 ≤ (1 / z).re⊢ -Real.pi * (1 / z).re ≤ -Real.pi * (1 / (4 * z)).re rw [hrez:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).rehfar':1 ≤ (1 / z).re⊢ -Real.pi * (4 * (1 / (4 * z)).re) ≤ -Real.pi * (1 / (4 * z)).re]z:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).rehfar':1 ≤ (1 / z).re⊢ -Real.pi * (4 * (1 / (4 * z)).re) ≤ -Real.pi * (1 / (4 * z)).re nlinarith [Real.pi_pos]z:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).rehfar':1 ≤ (1 / z).rehexp:Real.exp (-Real.pi * (1 / z).re) ≤ Real.exp (-Real.pi * (1 / (4 * z)).re)⊢ ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re) rw [psi_cusp_identity hz,z:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).rehfar':1 ≤ (1 / z).rehexp:Real.exp (-Real.pi * (1 / z).re) ≤ Real.exp (-Real.pi * (1 / (4 * z)).re)⊢ ‖1 / z ^ (1 / 2) * (psi (1 / (4 * z)) - psi (1 / z))‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re) norm_mul,z:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).rehfar':1 ≤ (1 / z).rehexp:Real.exp (-Real.pi * (1 / z).re) ≤ Real.exp (-Real.pi * (1 / (4 * z)).re)⊢ ‖1 / z ^ (1 / 2)‖ * ‖psi (1 / (4 * z)) - psi (1 / z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re) norm_div,z:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).rehfar':1 ≤ (1 / z).rehexp:Real.exp (-Real.pi * (1 / z).re) ≤ Real.exp (-Real.pi * (1 / (4 * z)).re)⊢ ‖1‖ / ‖z ^ (1 / 2)‖ * ‖psi (1 / (4 * z)) - psi (1 / z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re) norm_one,z:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).rehfar':1 ≤ (1 / z).rehexp:Real.exp (-Real.pi * (1 / z).re) ≤ Real.exp (-Real.pi * (1 / (4 * z)).re)⊢ 1 / ‖z ^ (1 / 2)‖ * ‖psi (1 / (4 * z)) - psi (1 / z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re) one_divz:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).rehfar':1 ≤ (1 / z).rehexp:Real.exp (-Real.pi * (1 / z).re) ≤ Real.exp (-Real.pi * (1 / (4 * z)).re)⊢ ‖z ^ (1 / 2)‖⁻¹ * ‖psi (1 / (4 * z)) - psi (1 / z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re)]z:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).rehfar':1 ≤ (1 / z).rehexp:Real.exp (-Real.pi * (1 / z).re) ≤ Real.exp (-Real.pi * (1 / (4 * z)).re)⊢ ‖z ^ (1 / 2)‖⁻¹ * ‖psi (1 / (4 * z)) - psi (1 / z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re) calc ‖z ^ (1 / 2 : ℂ)‖⁻¹ * ‖psi (1 / (4 * z)) - psi (1 / z)‖ ≤ ‖z ^ (1 / 2 : ℂ)‖⁻¹ * (2 * Real.exp (-Real.pi * (1 / (4 * z)).re) + 2 * Real.exp (-Real.pi * (1 / z).re)) := byz:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).rehfar':1 ≤ (1 / z).rehexp:Real.exp (-Real.pi * (1 / z).re) ≤ Real.exp (-Real.pi * (1 / (4 * z)).re)⊢ ‖z ^ (1 / 2)‖⁻¹ * ‖psi (1 / (4 * z)) - psi (1 / z)‖ ≤ ‖z ^ (1 / 2)‖⁻¹ * (2 * Real.exp (-Real.pi * (1 / (4 * z)).re) + 2 * Real.exp (-Real.pi * (1 / z).re)) apply mul_le_mul_of_nonneg_left _ (inv_nonneg.mpr (norm_nonneg _))z:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).rehfar':1 ≤ (1 / z).rehexp:Real.exp (-Real.pi * (1 / z).re) ≤ Real.exp (-Real.pi * (1 / (4 * z)).re)⊢ ‖psi (1 / (4 * z)) - psi (1 / z)‖ ≤ 2 * Real.exp (-Real.pi * (1 / (4 * z)).re) + 2 * Real.exp (-Real.pi * (1 / z).re) exact (norm_sub_le _ _).trans (add_le_add (norm_psi_le_two_exp hfar) (norm_psi_le_two_exp hfar'))All goals completed! 🐙 _ ≤ _ := byz:ℂhz:0 < z.rehfar:1 ≤ (1 / (4 * z)).rehz0:z ≠ 0heq:1 / z = 4 * (1 / (4 * z))hre:(1 / z).re = 4 * (1 / (4 * z)).rehfar':1 ≤ (1 / z).rehexp:Real.exp (-Real.pi * (1 / z).re) ≤ Real.exp (-Real.pi * (1 / (4 * z)).re)⊢ ‖z ^ (1 / 2)‖⁻¹ * (2 * Real.exp (-Real.pi * (1 / (4 * z)).re) + 2 * Real.exp (-Real.pi * (1 / z).re)) ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re) nlinarith [inv_nonneg.mpr (norm_nonneg (z ^ (1 / 2 : ℂ))), mul_le_mul_of_nonneg_left hexp (inv_nonneg.mpr (norm_nonneg (z ^ (1 / 2 : ℂ))))]All goals completed! 🐙 /-- Real part of the reciprocal argument in terms of the original norm. -/theorem re_reciprocal_four_mul (z : ℂ) : (1 / (4 * z)).re = z.re / (4 * ‖z‖ ^ 2) := byz:ℂ⊢ (1 / (4 * z)).re = z.re / (4 * ‖z‖ ^ 2) simp only [one_div, mul_inv_rev, mul_re, inv_re, inv_im]z:ℂ⊢ z.re / normSq z * (re 4 / normSq 4) - -z.im / normSq z * (-im 4 / normSq 4) = z.re / (4 * ‖z‖ ^ 2) norm_numz:ℂ⊢ z.re / normSq z * (1 / 4) = z.re / (4 * ‖z‖ ^ 2) rw [normSq_eq_norm_sqz:ℂ⊢ z.re / ‖z‖ ^ 2 * (1 / 4) = z.re / (4 * ‖z‖ ^ 2)]z:ℂ⊢ z.re / ‖z‖ ^ 2 * (1 / 4) = z.re / (4 * ‖z‖ ^ 2) ringAll goals completed! 🐙 /-- A sector condition gives a lower bound on the reciprocal real part. -/theorem sector_reciprocal_lower {z : ℂ} {c : ℝ} (hz : z ≠ 0) (hsector : c * ‖z‖ ≤ z.re) : c / (4 * ‖z‖) ≤ (1 / (4 * z)).re := byz:ℂc:ℝhz:z ≠ 0hsector:c * ‖z‖ ≤ z.re⊢ c / (4 * ‖z‖) ≤ (1 / (4 * z)).re have hn : 0 < ‖z‖ := norm_pos_iff.mpr hzz:ℂc:ℝhz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehn:0 < ‖z‖⊢ c / (4 * ‖z‖) ≤ (1 / (4 * z)).re rw [re_reciprocal_four_mulz:ℂc:ℝhz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehn:0 < ‖z‖⊢ c / (4 * ‖z‖) ≤ z.re / (4 * ‖z‖ ^ 2)]z:ℂc:ℝhz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehn:0 < ‖z‖⊢ c / (4 * ‖z‖) ≤ z.re / (4 * ‖z‖ ^ 2) apply (div_le_div_iff₀ (byz:ℂc:ℝhz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehn:0 < ‖z‖⊢ 0 < 4 * ‖z‖ positivityAll goals completed! 🐙) (byz:ℂc:ℝhz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehn:0 < ‖z‖⊢ 0 < 4 * ‖z‖ ^ 2 positivityAll goals completed! 🐙)).mpr nlinarith [mul_le_mul_of_nonneg_right hsector hn.le]All goals completed! 🐙 /-- Uniform exponential control in any fixed closed sector of the right half-plane. -/theorem norm_psi_cusp_le_sector {z : ℂ} {c : ℝ} (hc : 0 < c) (hz : z ≠ 0) (hsector : c * ‖z‖ ≤ z.re) (hsmall : ‖z‖ ≤ c / 4) : ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z ^ (1 / 2 : ℂ)‖⁻¹ * Real.exp (-Real.pi * c / (4 * ‖z‖)) := byz:ℂc:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4⊢ ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * c / (4 * ‖z‖)) have hn : 0 < ‖z‖ := norm_pos_iff.mpr hzz:ℂc:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖⊢ ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * c / (4 * ‖z‖)) have hzre : 0 < z.re := (mul_pos hc hn).trans_le hsectorz:ℂc:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖hzre:0 < z.re⊢ ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * c / (4 * ‖z‖)) have hrec := sector_reciprocal_lower hz hsectorz:ℂc:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖hzre:0 < z.rehrec:c / (4 * ‖z‖) ≤ (1 / (4 * z)).re⊢ ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * c / (4 * ‖z‖)) have hone : 1 ≤ c / (4 * ‖z‖) := by apply (le_div_iff₀ (byz:ℂc:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖hzre:0 < z.rehrec:c / (4 * ‖z‖) ≤ (1 / (4 * z)).re⊢ 0 < 4 * ‖z‖ positivityAll goals completed! 🐙)).mpr linarithz:ℂc:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖hzre:0 < z.rehrec:c / (4 * ‖z‖) ≤ (1 / (4 * z)).rehone:1 ≤ c / (4 * ‖z‖)⊢ ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * c / (4 * ‖z‖)) apply (norm_psi_cusp_le_exp hzre (hone.trans hrec)).transz:ℂc:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖hzre:0 < z.rehrec:c / (4 * ‖z‖) ≤ (1 / (4 * z)).rehone:1 ≤ c / (4 * ‖z‖)⊢ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re) ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * c / (4 * ‖z‖)) apply mul_le_mul_of_nonneg_left _ (byz:ℂc:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖hzre:0 < z.rehrec:c / (4 * ‖z‖) ≤ (1 / (4 * z)).rehone:1 ≤ c / (4 * ‖z‖)⊢ 0 ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ positivityAll goals completed! 🐙) apply Real.exp_le_exp.mprz:ℂc:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖hzre:0 < z.rehrec:c / (4 * ‖z‖) ≤ (1 / (4 * z)).rehone:1 ≤ c / (4 * ‖z‖)⊢ -Real.pi * (1 / (4 * z)).re ≤ -Real.pi * c / (4 * ‖z‖) have h := mul_le_mul_of_nonpos_left hrec (neg_nonpos.mpr Real.pi_pos.le)z:ℂc:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖hzre:0 < z.rehrec:c / (4 * ‖z‖) ≤ (1 / (4 * z)).rehone:1 ≤ c / (4 * ‖z‖)h:-Real.pi * (1 / (4 * z)).re ≤ -Real.pi * (c / (4 * ‖z‖))⊢ -Real.pi * (1 / (4 * z)).re ≤ -Real.pi * c / (4 * ‖z‖) simpa only [mul_div_assoc] using hAll goals completed! 🐙 /-- The sector bound absorbs any real power of the inverse distance to the cusp. -/theorem weighted_norm_psi_cusp_le_sector {z : ℂ} {c : ℝ} (s : ℝ) (hc : 0 < c) (hz : z ≠ 0) (hsector : c * ‖z‖ ≤ z.re) (hsmall : ‖z‖ ≤ c / 4) : (‖z‖⁻¹) ^ s * ‖1 / 2 + psi (I + z)‖ ≤ 4 * (‖z‖⁻¹) ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹) := byz:ℂc:ℝs:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4⊢ ‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹) have hn : 0 < ‖z‖ := norm_pos_iff.mpr hzz:ℂc:ℝs:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖⊢ ‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹) have h := mul_le_mul_of_nonneg_left (norm_psi_cusp_le_sector hc hz hsector hsmall) (Real.rpow_nonneg (inv_nonneg.mpr hn.le) s)z:ℂc:ℝs:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖h:‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ ‖z‖⁻¹ ^ s * (4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * c / (4 * ‖z‖)))⊢ ‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹) have hp : ‖z ^ (1 / 2 : ℂ)‖⁻¹ = (‖z‖⁻¹) ^ (1 / 2 : ℝ) := by rw [show (1 / 2 : ℂ) = ((1 / 2 : ℝ) : ℂ) byz:ℂc:ℝs:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4⊢ ‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹) norm_numAll goals completed! 🐙, norm_cpow_real,z:ℂc:ℝs:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖h:‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ ‖z‖⁻¹ ^ s * (4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * c / (4 * ‖z‖)))⊢ (‖z‖ ^ (1 / 2))⁻¹ = ‖z‖⁻¹ ^ (1 / 2) Real.inv_rpow hn.lez:ℂc:ℝs:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖h:‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ ‖z‖⁻¹ ^ s * (4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * c / (4 * ‖z‖)))⊢ (‖z‖ ^ (1 / 2))⁻¹ = (‖z‖ ^ (1 / 2))⁻¹]z:ℂc:ℝs:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖h:‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ ‖z‖⁻¹ ^ s * (4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * c / (4 * ‖z‖)))hp:‖z ^ (1 / 2)‖⁻¹ = ‖z‖⁻¹ ^ (1 / 2)⊢ ‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹) rw [hpz:ℂc:ℝs:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖h:‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ ‖z‖⁻¹ ^ s * (4 * ‖z‖⁻¹ ^ (1 / 2) * Real.exp (-Real.pi * c / (4 * ‖z‖)))hp:‖z ^ (1 / 2)‖⁻¹ = ‖z‖⁻¹ ^ (1 / 2)⊢ ‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹)] at hz:ℂc:ℝs:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖h:‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ ‖z‖⁻¹ ^ s * (4 * ‖z‖⁻¹ ^ (1 / 2) * Real.exp (-Real.pi * c / (4 * ‖z‖)))hp:‖z ^ (1 / 2)‖⁻¹ = ‖z‖⁻¹ ^ (1 / 2)⊢ ‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹) rw [Real.rpow_add (inv_pos.mpr hn)z:ℂc:ℝs:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖h:‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ ‖z‖⁻¹ ^ s * (4 * ‖z‖⁻¹ ^ (1 / 2) * Real.exp (-Real.pi * c / (4 * ‖z‖)))hp:‖z ^ (1 / 2)‖⁻¹ = ‖z‖⁻¹ ^ (1 / 2)⊢ ‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ 4 * (‖z‖⁻¹ ^ s * ‖z‖⁻¹ ^ (1 / 2)) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹)]z:ℂc:ℝs:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖h:‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ ‖z‖⁻¹ ^ s * (4 * ‖z‖⁻¹ ^ (1 / 2) * Real.exp (-Real.pi * c / (4 * ‖z‖)))hp:‖z ^ (1 / 2)‖⁻¹ = ‖z‖⁻¹ ^ (1 / 2)⊢ ‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ 4 * (‖z‖⁻¹ ^ s * ‖z‖⁻¹ ^ (1 / 2)) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹) have he : -Real.pi * c / (4 * ‖z‖) = -(Real.pi * c / 4) * ‖z‖⁻¹ := byz:ℂc:ℝs:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4⊢ ‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ 4 * ‖z‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹) ringz:ℂc:ℝs:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖h:‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ ‖z‖⁻¹ ^ s * (4 * ‖z‖⁻¹ ^ (1 / 2) * Real.exp (-Real.pi * c / (4 * ‖z‖)))hp:‖z ^ (1 / 2)‖⁻¹ = ‖z‖⁻¹ ^ (1 / 2)he:-Real.pi * c / (4 * ‖z‖) = -(Real.pi * c / 4) * ‖z‖⁻¹⊢ ‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ 4 * (‖z‖⁻¹ ^ s * ‖z‖⁻¹ ^ (1 / 2)) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹) rw [hez:ℂc:ℝs:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖h:‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ ‖z‖⁻¹ ^ s * (4 * ‖z‖⁻¹ ^ (1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹))hp:‖z ^ (1 / 2)‖⁻¹ = ‖z‖⁻¹ ^ (1 / 2)he:-Real.pi * c / (4 * ‖z‖) = -(Real.pi * c / 4) * ‖z‖⁻¹⊢ ‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ 4 * (‖z‖⁻¹ ^ s * ‖z‖⁻¹ ^ (1 / 2)) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹)] at hz:ℂc:ℝs:ℝhc:0 < chz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehsmall:‖z‖ ≤ c / 4hn:0 < ‖z‖h:‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ ‖z‖⁻¹ ^ s * (4 * ‖z‖⁻¹ ^ (1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹))hp:‖z ^ (1 / 2)‖⁻¹ = ‖z‖⁻¹ ^ (1 / 2)he:-Real.pi * c / (4 * ‖z‖) = -(Real.pi * c / 4) * ‖z‖⁻¹⊢ ‖z‖⁻¹ ^ s * ‖1 / 2 + psi (I + z)‖ ≤ 4 * (‖z‖⁻¹ ^ s * ‖z‖⁻¹ ^ (1 / 2)) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹) simpa only [mul_assoc, mul_comm, mul_left_comm] using hAll goals completed! 🐙 /-- Along a nontangential approach, the cusp value decays faster than every power. -/theorem tendsto_weighted_psi_cusp {ι : Type*} {l : Filter ι} {z : ι → ℂ} {c : ℝ} (hc : 0 < c) (s : ℝ) (hz : Tendsto z l (𝓝 0)) (hne : ∀ᶠ t in l, z t ≠ 0) (hsector : ∀ᶠ t in l, c * ‖z t‖ ≤ (z t).re) : Tendsto (fun t ↦ (‖z t‖⁻¹) ^ s * ‖1 / 2 + psi (I + z t)‖) l (𝓝 0) := byι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).re⊢ Tendsto (fun t => ‖z t‖⁻¹ ^ s * ‖1 / 2 + psi (I + z t)‖) l (𝓝 0) have hnorm : Tendsto (fun t ↦ ‖z t‖) l (𝓝 (0 : ℝ)) := by simpa using hz.normι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)⊢ Tendsto (fun t => ‖z t‖⁻¹ ^ s * ‖1 / 2 + psi (I + z t)‖) l (𝓝 0) have hpos : ∀ᶠ t in l, 0 < ‖z t‖ := hne.mono fun _ h ↦ norm_pos_iff.mpr hι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖⊢ Tendsto (fun t => ‖z t‖⁻¹ ^ s * ‖1 / 2 + psi (I + z t)‖) l (𝓝 0) have hnorm' : Tendsto (fun t ↦ ‖z t‖) l (𝓝[>] (0 : ℝ)) := tendsto_nhdsWithin_iff.mpr ⟨hnorm, hpos⟩ι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖hnorm':Tendsto (fun t => ‖z t‖) l (𝓝[>] 0)⊢ Tendsto (fun t => ‖z t‖⁻¹ ^ s * ‖1 / 2 + psi (I + z t)‖) l (𝓝 0) have hinv : Tendsto (fun t ↦ ‖z t‖⁻¹) l atTop := tendsto_inv_nhdsGT_zero.comp hnorm'ι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖hnorm':Tendsto (fun t => ‖z t‖) l (𝓝[>] 0)hinv:Tendsto (fun t => ‖z t‖⁻¹) l atTop⊢ Tendsto (fun t => ‖z t‖⁻¹ ^ s * ‖1 / 2 + psi (I + z t)‖) l (𝓝 0) have hlim := (tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (s + 1 / 2) (Real.pi * c / 4) (byι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖hnorm':Tendsto (fun t => ‖z t‖) l (𝓝[>] 0)hinv:Tendsto (fun t => ‖z t‖⁻¹) l atTop⊢ 0 < Real.pi * c / 4 positivityAll goals completed! 🐙)).comp hinvι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖hnorm':Tendsto (fun t => ‖z t‖) l (𝓝[>] 0)hinv:Tendsto (fun t => ‖z t‖⁻¹) l atTophlim:Tendsto ((fun x => x ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * x)) ∘ fun t => ‖z t‖⁻¹) l (𝓝 0)⊢ Tendsto (fun t => ‖z t‖⁻¹ ^ s * ‖1 / 2 + psi (I + z t)‖) l (𝓝 0) have hbound : Tendsto (fun t ↦ 4 * (‖z t‖⁻¹) ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹)) l (𝓝 0) := by simpa only [Function.comp_apply, mul_zero, mul_assoc] using hlim.const_mul 4ι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖hnorm':Tendsto (fun t => ‖z t‖) l (𝓝[>] 0)hinv:Tendsto (fun t => ‖z t‖⁻¹) l atTophlim:Tendsto ((fun x => x ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * x)) ∘ fun t => ‖z t‖⁻¹) l (𝓝 0)hbound:Tendsto (fun t => 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹)) l (𝓝 0)⊢ Tendsto (fun t => ‖z t‖⁻¹ ^ s * ‖1 / 2 + psi (I + z t)‖) l (𝓝 0) have hsmall : ∀ᶠ t in l, ‖z t‖ ≤ c / 4 := by exact (hnorm.eventually (gt_mem_nhds (byι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖hnorm':Tendsto (fun t => ‖z t‖) l (𝓝[>] 0)hinv:Tendsto (fun t => ‖z t‖⁻¹) l atTophlim:Tendsto ((fun x => x ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * x)) ∘ fun t => ‖z t‖⁻¹) l (𝓝 0)hbound:Tendsto (fun t => 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹)) l (𝓝 0)⊢ 0 < c / 4 positivityAll goals completed! 🐙 : (0 : ℝ) < c / 4))).mono fun _ h ↦ h.leι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖hnorm':Tendsto (fun t => ‖z t‖) l (𝓝[>] 0)hinv:Tendsto (fun t => ‖z t‖⁻¹) l atTophlim:Tendsto ((fun x => x ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * x)) ∘ fun t => ‖z t‖⁻¹) l (𝓝 0)hbound:Tendsto (fun t => 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹)) l (𝓝 0)hsmall:∀ᶠ (t : ι) in l, ‖z t‖ ≤ c / 4⊢ Tendsto (fun t => ‖z t‖⁻¹ ^ s * ‖1 / 2 + psi (I + z t)‖) l (𝓝 0) apply squeeze_zero' _ _ hboundι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖hnorm':Tendsto (fun t => ‖z t‖) l (𝓝[>] 0)hinv:Tendsto (fun t => ‖z t‖⁻¹) l atTophlim:Tendsto ((fun x => x ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * x)) ∘ fun t => ‖z t‖⁻¹) l (𝓝 0)hbound:Tendsto (fun t => 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹)) l (𝓝 0)hsmall:∀ᶠ (t : ι) in l, ‖z t‖ ≤ c / 4⊢ ∀ᶠ (t : ι) in l, 0 ≤ ‖z t‖⁻¹ ^ s * ‖1 / 2 + psi (I + z t)‖ι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖hnorm':Tendsto (fun t => ‖z t‖) l (𝓝[>] 0)hinv:Tendsto (fun t => ‖z t‖⁻¹) l atTophlim:Tendsto ((fun x => x ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * x)) ∘ fun t => ‖z t‖⁻¹) l (𝓝 0)hbound:Tendsto (fun t => 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹)) l (𝓝 0)hsmall:∀ᶠ (t : ι) in l, ‖z t‖ ≤ c / 4⊢ ∀ᶠ (t : ι) in l, ‖z t‖⁻¹ ^ s * ‖1 / 2 + psi (I + z t)‖ ≤ 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹) ·ι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖hnorm':Tendsto (fun t => ‖z t‖) l (𝓝[>] 0)hinv:Tendsto (fun t => ‖z t‖⁻¹) l atTophlim:Tendsto ((fun x => x ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * x)) ∘ fun t => ‖z t‖⁻¹) l (𝓝 0)hbound:Tendsto (fun t => 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹)) l (𝓝 0)hsmall:∀ᶠ (t : ι) in l, ‖z t‖ ≤ c / 4⊢ ∀ᶠ (t : ι) in l, 0 ≤ ‖z t‖⁻¹ ^ s * ‖1 / 2 + psi (I + z t)‖ filter_upwards with t using mul_nonneg (Real.rpow_nonneg (byι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖hnorm':Tendsto (fun t => ‖z t‖) l (𝓝[>] 0)hinv:Tendsto (fun t => ‖z t‖⁻¹) l atTophlim:Tendsto ((fun x => x ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * x)) ∘ fun t => ‖z t‖⁻¹) l (𝓝 0)hbound:Tendsto (fun t => 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹)) l (𝓝 0)hsmall:∀ᶠ (t : ι) in l, ‖z t‖ ≤ c / 4t:ι⊢ 0 ≤ ‖z t‖⁻¹ positivityAll goals completed! 🐙) _) (norm_nonneg _) ·ι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖hnorm':Tendsto (fun t => ‖z t‖) l (𝓝[>] 0)hinv:Tendsto (fun t => ‖z t‖⁻¹) l atTophlim:Tendsto ((fun x => x ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * x)) ∘ fun t => ‖z t‖⁻¹) l (𝓝 0)hbound:Tendsto (fun t => 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹)) l (𝓝 0)hsmall:∀ᶠ (t : ι) in l, ‖z t‖ ≤ c / 4⊢ ∀ᶠ (t : ι) in l, ‖z t‖⁻¹ ^ s * ‖1 / 2 + psi (I + z t)‖ ≤ 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹) filter_upwards [hne, hsector, hsmall] with t htι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖hnorm':Tendsto (fun t => ‖z t‖) l (𝓝[>] 0)hinv:Tendsto (fun t => ‖z t‖⁻¹) l atTophlim:Tendsto ((fun x => x ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * x)) ∘ fun t => ‖z t‖⁻¹) l (𝓝 0)hbound:Tendsto (fun t => 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹)) l (𝓝 0)hsmall:∀ᶠ (t : ι) in l, ‖z t‖ ≤ c / 4t:ιht:z t ≠ 0⊢ c * ‖z t‖ ≤ (z t).re → ‖z t‖ ≤ c / 4 → ‖z t‖⁻¹ ^ s * ‖1 / 2 + psi (I + z t)‖ ≤ 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹) hsι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖hnorm':Tendsto (fun t => ‖z t‖) l (𝓝[>] 0)hinv:Tendsto (fun t => ‖z t‖⁻¹) l atTophlim:Tendsto ((fun x => x ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * x)) ∘ fun t => ‖z t‖⁻¹) l (𝓝 0)hbound:Tendsto (fun t => 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹)) l (𝓝 0)hsmall:∀ᶠ (t : ι) in l, ‖z t‖ ≤ c / 4t:ιht:z t ≠ 0hs:c * ‖z t‖ ≤ (z t).re⊢ ‖z t‖ ≤ c / 4 → ‖z t‖⁻¹ ^ s * ‖1 / 2 + psi (I + z t)‖ ≤ 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹) hsmι:Type u_1l:Filter ιz:ι → ℂc:ℝhc:0 < cs:ℝhz:Tendsto z l (𝓝 0)hne:∀ᶠ (t : ι) in l, z t ≠ 0hsector:∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).rehnorm:Tendsto (fun t => ‖z t‖) l (𝓝 0)hpos:∀ᶠ (t : ι) in l, 0 < ‖z t‖hnorm':Tendsto (fun t => ‖z t‖) l (𝓝[>] 0)hinv:Tendsto (fun t => ‖z t‖⁻¹) l atTophlim:Tendsto ((fun x => x ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * x)) ∘ fun t => ‖z t‖⁻¹) l (𝓝 0)hbound:Tendsto (fun t => 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹)) l (𝓝 0)hsmall:∀ᶠ (t : ι) in l, ‖z t‖ ≤ c / 4t:ιht:z t ≠ 0hs:c * ‖z t‖ ≤ (z t).rehsm:‖z t‖ ≤ c / 4⊢ ‖z t‖⁻¹ ^ s * ‖1 / 2 + psi (I + z t)‖ ≤ 4 * ‖z t‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z t‖⁻¹) exact weighted_norm_psi_cusp_le_sector s hc ht hs hsmAll goals completed! 🐙 end HardyZeta