Hardy zeta

11.12. HardyZeta.SectorGeometry🔗

theorem sector_disk_bounds {z w : ℂ} {c : ℝ} (hc : 0 < c) (hc1 : c ≤ 1)
    (hz : z ≠ 0) (hsector : c * ‖z‖ ≤ z.re)
    (hclose : ‖w - z‖ ≤ c * ‖z‖ / 4) :
    ‖z‖ / 2 ≤ ‖w‖ ∧ ‖w‖ ≤ 2 * ‖z‖ ∧
      (c / 2) * ‖w‖ ≤ w.re ∧ 0 < w.re := byz:ℂw:ℂc:ℝhc:0 < chc1:c ≤ 1hz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehclose:‖w - z‖ ≤ c * ‖z‖ / 4⊢ ‖z‖ / 2 ≤ ‖w‖ ∧ ‖w‖ ≤ 2 * ‖z‖ ∧ c / 2 * ‖w‖ ≤ w.re ∧ 0 < w.re
  have hn : 0 < ‖z‖ := norm_pos_iff.mpr hzz:ℂw:ℂc:ℝhc:0 < chc1:c ≤ 1hz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehclose:‖w - z‖ ≤ c * ‖z‖ / 4hn:0 < ‖z‖⊢ ‖z‖ / 2 ≤ ‖w‖ ∧ ‖w‖ ≤ 2 * ‖z‖ ∧ c / 2 * ‖w‖ ≤ w.re ∧ 0 < w.re
  have hcN : c * ‖z‖ ≤ ‖z‖ := by nlinarithz:ℂw:ℂc:ℝhc:0 < chc1:c ≤ 1hz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehclose:‖w - z‖ ≤ c * ‖z‖ / 4hn:0 < ‖z‖hcN:c * ‖z‖ ≤ ‖z‖⊢ ‖z‖ / 2 ≤ ‖w‖ ∧ ‖w‖ ≤ 2 * ‖z‖ ∧ c / 2 * ‖w‖ ≤ w.re ∧ 0 < w.re
  have hupper : ‖w‖ ≤ ‖w - z‖ + ‖z‖ := by
    simpa only [sub_add_cancel] using norm_add_le (w - z) zz:ℂw:ℂc:ℝhc:0 < chc1:c ≤ 1hz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehclose:‖w - z‖ ≤ c * ‖z‖ / 4hn:0 < ‖z‖hcN:c * ‖z‖ ≤ ‖z‖hupper:‖w‖ ≤ ‖w - z‖ + ‖z‖⊢ ‖z‖ / 2 ≤ ‖w‖ ∧ ‖w‖ ≤ 2 * ‖z‖ ∧ c / 2 * ‖w‖ ≤ w.re ∧ 0 < w.re
  have hlower : ‖z‖ ≤ ‖w - z‖ + ‖w‖ := by
    simpa only [sub_add_cancel, norm_sub_rev] using norm_add_le (z - w) wz:ℂw:ℂc:ℝhc:0 < chc1:c ≤ 1hz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehclose:‖w - z‖ ≤ c * ‖z‖ / 4hn:0 < ‖z‖hcN:c * ‖z‖ ≤ ‖z‖hupper:‖w‖ ≤ ‖w - z‖ + ‖z‖hlower:‖z‖ ≤ ‖w - z‖ + ‖w‖⊢ ‖z‖ / 2 ≤ ‖w‖ ∧ ‖w‖ ≤ 2 * ‖z‖ ∧ c / 2 * ‖w‖ ≤ w.re ∧ 0 < w.re
  have hre : z.re - w.re ≤ ‖w - z‖ := by
    simpa only [Complex.sub_re, norm_sub_rev] using Complex.re_le_norm (z - w)z:ℂw:ℂc:ℝhc:0 < chc1:c ≤ 1hz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehclose:‖w - z‖ ≤ c * ‖z‖ / 4hn:0 < ‖z‖hcN:c * ‖z‖ ≤ ‖z‖hupper:‖w‖ ≤ ‖w - z‖ + ‖z‖hlower:‖z‖ ≤ ‖w - z‖ + ‖w‖hre:z.re - w.re ≤ ‖w - z‖⊢ ‖z‖ / 2 ≤ ‖w‖ ∧ ‖w‖ ≤ 2 * ‖z‖ ∧ c / 2 * ‖w‖ ≤ w.re ∧ 0 < w.re
  have hnormlower : ‖z‖ / 2 ≤ ‖w‖ := by linarithz:ℂw:ℂc:ℝhc:0 < chc1:c ≤ 1hz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehclose:‖w - z‖ ≤ c * ‖z‖ / 4hn:0 < ‖z‖hcN:c * ‖z‖ ≤ ‖z‖hupper:‖w‖ ≤ ‖w - z‖ + ‖z‖hlower:‖z‖ ≤ ‖w - z‖ + ‖w‖hre:z.re - w.re ≤ ‖w - z‖hnormlower:‖z‖ / 2 ≤ ‖w‖⊢ ‖z‖ / 2 ≤ ‖w‖ ∧ ‖w‖ ≤ 2 * ‖z‖ ∧ c / 2 * ‖w‖ ≤ w.re ∧ 0 < w.re
  have hnormupper : ‖w‖ ≤ 2 * ‖z‖ := by linarithz:ℂw:ℂc:ℝhc:0 < chc1:c ≤ 1hz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehclose:‖w - z‖ ≤ c * ‖z‖ / 4hn:0 < ‖z‖hcN:c * ‖z‖ ≤ ‖z‖hupper:‖w‖ ≤ ‖w - z‖ + ‖z‖hlower:‖z‖ ≤ ‖w - z‖ + ‖w‖hre:z.re - w.re ≤ ‖w - z‖hnormlower:‖z‖ / 2 ≤ ‖w‖hnormupper:‖w‖ ≤ 2 * ‖z‖⊢ ‖z‖ / 2 ≤ ‖w‖ ∧ ‖w‖ ≤ 2 * ‖z‖ ∧ c / 2 * ‖w‖ ≤ w.re ∧ 0 < w.re
  have hcn : 0 < c * ‖z‖ := mul_pos hc hnz:ℂw:ℂc:ℝhc:0 < chc1:c ≤ 1hz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehclose:‖w - z‖ ≤ c * ‖z‖ / 4hn:0 < ‖z‖hcN:c * ‖z‖ ≤ ‖z‖hupper:‖w‖ ≤ ‖w - z‖ + ‖z‖hlower:‖z‖ ≤ ‖w - z‖ + ‖w‖hre:z.re - w.re ≤ ‖w - z‖hnormlower:‖z‖ / 2 ≤ ‖w‖hnormupper:‖w‖ ≤ 2 * ‖z‖hcn:0 < c * ‖z‖⊢ ‖z‖ / 2 ≤ ‖w‖ ∧ ‖w‖ ≤ 2 * ‖z‖ ∧ c / 2 * ‖w‖ ≤ w.re ∧ 0 < w.re
  refine ⟨hnormlower, hnormupper, ?_, ?_⟩refine_1z:ℂw:ℂc:ℝhc:0 < chc1:c ≤ 1hz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehclose:‖w - z‖ ≤ c * ‖z‖ / 4hn:0 < ‖z‖hcN:c * ‖z‖ ≤ ‖z‖hupper:‖w‖ ≤ ‖w - z‖ + ‖z‖hlower:‖z‖ ≤ ‖w - z‖ + ‖w‖hre:z.re - w.re ≤ ‖w - z‖hnormlower:‖z‖ / 2 ≤ ‖w‖hnormupper:‖w‖ ≤ 2 * ‖z‖hcn:0 < c * ‖z‖⊢ c / 2 * ‖w‖ ≤ w.rerefine_2z:ℂw:ℂc:ℝhc:0 < chc1:c ≤ 1hz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehclose:‖w - z‖ ≤ c * ‖z‖ / 4hn:0 < ‖z‖hcN:c * ‖z‖ ≤ ‖z‖hupper:‖w‖ ≤ ‖w - z‖ + ‖z‖hlower:‖z‖ ≤ ‖w - z‖ + ‖w‖hre:z.re - w.re ≤ ‖w - z‖hnormlower:‖z‖ / 2 ≤ ‖w‖hnormupper:‖w‖ ≤ 2 * ‖z‖hcn:0 < c * ‖z‖⊢ 0 < w.re
  ·refine_1z:ℂw:ℂc:ℝhc:0 < chc1:c ≤ 1hz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehclose:‖w - z‖ ≤ c * ‖z‖ / 4hn:0 < ‖z‖hcN:c * ‖z‖ ≤ ‖z‖hupper:‖w‖ ≤ ‖w - z‖ + ‖z‖hlower:‖z‖ ≤ ‖w - z‖ + ‖w‖hre:z.re - w.re ≤ ‖w - z‖hnormlower:‖z‖ / 2 ≤ ‖w‖hnormupper:‖w‖ ≤ 2 * ‖z‖hcn:0 < c * ‖z‖⊢ c / 2 * ‖w‖ ≤ w.re have hscaled := mul_le_mul_of_nonneg_left hupper hc.lerefine_1z:ℂw:ℂc:ℝhc:0 < chc1:c ≤ 1hz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehclose:‖w - z‖ ≤ c * ‖z‖ / 4hn:0 < ‖z‖hcN:c * ‖z‖ ≤ ‖z‖hupper:‖w‖ ≤ ‖w - z‖ + ‖z‖hlower:‖z‖ ≤ ‖w - z‖ + ‖w‖hre:z.re - w.re ≤ ‖w - z‖hnormlower:‖z‖ / 2 ≤ ‖w‖hnormupper:‖w‖ ≤ 2 * ‖z‖hcn:0 < c * ‖z‖hscaled:c * ‖w‖ ≤ c * (‖w - z‖ + ‖z‖)⊢ c / 2 * ‖w‖ ≤ w.re
    have hscaledclose := mul_le_mul_of_nonneg_left hclose hc.lerefine_1z:ℂw:ℂc:ℝhc:0 < chc1:c ≤ 1hz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehclose:‖w - z‖ ≤ c * ‖z‖ / 4hn:0 < ‖z‖hcN:c * ‖z‖ ≤ ‖z‖hupper:‖w‖ ≤ ‖w - z‖ + ‖z‖hlower:‖z‖ ≤ ‖w - z‖ + ‖w‖hre:z.re - w.re ≤ ‖w - z‖hnormlower:‖z‖ / 2 ≤ ‖w‖hnormupper:‖w‖ ≤ 2 * ‖z‖hcn:0 < c * ‖z‖hscaled:c * ‖w‖ ≤ c * (‖w - z‖ + ‖z‖)hscaledclose:c * ‖w - z‖ ≤ c * (c * ‖z‖ / 4)⊢ c / 2 * ‖w‖ ≤ w.re
    nlinarith [mul_nonneg (sub_nonneg.mpr hc1) (norm_nonneg (w-z))]All goals completed! 🐙
  ·refine_2z:ℂw:ℂc:ℝhc:0 < chc1:c ≤ 1hz:z ≠ 0hsector:c * ‖z‖ ≤ z.rehclose:‖w - z‖ ≤ c * ‖z‖ / 4hn:0 < ‖z‖hcN:c * ‖z‖ ≤ ‖z‖hupper:‖w‖ ≤ ‖w - z‖ + ‖z‖hlower:‖z‖ ≤ ‖w - z‖ + ‖w‖hre:z.re - w.re ≤ ‖w - z‖hnormlower:‖z‖ / 2 ≤ ‖w‖hnormupper:‖w‖ ≤ 2 * ‖z‖hcn:0 < c * ‖z‖⊢ 0 < w.re linarithAll goals completed! 🐙

end HardyZeta