Weighted Rectangle Argument Principle #
Supporting definitions and lemmas for the Odlyzko-bound formalization.
theorem
NumberField.Odlyzko.rectangleIntegral_fill_weightedLogDerivFiniteRemainder_eq_zero
{f h : ℂ → ℂ}
{S : Finset ℂ}
{order : ℂ → ℤ}
{a b u v : ℝ}
(hab : a ≤ b)
(huv : u ≤ v)
(hf : ∀ z ∈ Set.Icc a b ×ℂ Set.Icc u v, AnalyticAt ℂ f z)
(hh : ∀ z ∈ Set.Icc a b ×ℂ Set.Icc u v, AnalyticAt ℂ h z)
(hzero : ∀ z ∈ Set.Icc a b ×ℂ Set.Icc u v, f z = 0 → z ∈ S)
(horder : ∀ p ∈ S, meromorphicOrderAt f p = ↑(order p))
:
rectangleIntegral (fillFinitePunctures (weightedLogDerivFiniteRemainder f h S order) S) (↑a + ↑u * Complex.I)
(↑b + ↑v * Complex.I) = 0
theorem
NumberField.Odlyzko.rectangleIntegral_weightedLogDerivFiniteRemainder_eq_zero
{f h : ℂ → ℂ}
{S : Finset ℂ}
{order : ℂ → ℤ}
{a b u v : ℝ}
(hab : a ≤ b)
(huv : u ≤ v)
(hS : ∀ p ∈ S, a < p.re ∧ p.re < b ∧ u < p.im ∧ p.im < v)
(hf : ∀ z ∈ Set.Icc a b ×ℂ Set.Icc u v, AnalyticAt ℂ f z)
(hh : ∀ z ∈ Set.Icc a b ×ℂ Set.Icc u v, AnalyticAt ℂ h z)
(hzero : ∀ z ∈ Set.Icc a b ×ℂ Set.Icc u v, f z = 0 → z ∈ S)
(horder : ∀ p ∈ S, meromorphicOrderAt f p = ↑(order p))
:
rectangleIntegral (weightedLogDerivFiniteRemainder f h S order) (↑a + ↑u * Complex.I) (↑b + ↑v * Complex.I) = 0
theorem
NumberField.Odlyzko.rectangleIntegral_mul_logDeriv_eq_two_pi_I_mul_sum
{f h : ℂ → ℂ}
{S : Finset ℂ}
{order : ℂ → ℤ}
{a b u v : ℝ}
(hab : a ≤ b)
(huv : u ≤ v)
(hS : ∀ p ∈ S, a < p.re ∧ p.re < b ∧ u < p.im ∧ p.im < v)
(hf : ∀ z ∈ Set.Icc a b ×ℂ Set.Icc u v, AnalyticAt ℂ f z)
(hh : ∀ z ∈ Set.Icc a b ×ℂ Set.Icc u v, AnalyticAt ℂ h z)
(hzero : ∀ z ∈ Set.Icc a b ×ℂ Set.Icc u v, f z = 0 → z ∈ S)
(horder : ∀ p ∈ S, meromorphicOrderAt f p = ↑(order p))
: