theorem CohnElkies.mellinShellPhase_neg (ε : ℝ)
  (z : ℂ) :
  CohnElkies.h_ε ε (-z) =
    CohnElkies.h_ε ε z

theorem CohnElkies.mellinShellPhase_ofReal
  (ε t : ℝ) :
  CohnElkies.h_ε ε ↑t =
    ↑(CohnElkies.realOscillatoryShellPhase
        ε t)

theorem CohnElkies.mellinShellPhase_imaginary
  (ε u : ℝ) :
  CohnElkies.h_ε ε (Complex.I * ↑u) =
    ↑(CohnElkies.h_εI ε u)

theorem CohnElkies.upperFirstBranch_shortMeasure_pointwise
  {ε ℓ u a : ℝ} (hε : 0 < ε)
  (hεsmall : ε ≤ 1 / 4) (hℓ : 0 < ℓ)
  (ha : 0 < a) (hulower : -1 ≤ u)
  (huupper : u ≤ 1 + ε / 2)
  (hmargin : 0 ≤ CohnElkies.bε ε a) :
  ℓ * -CohnElkies.w_s ε a *
      Real.cosh (u * a) ≤
    (1 - 2 * ε) *
      CohnElkies.μ_ℓ ℓ (1 + u) a

theorem CohnElkies.upperFirstBranch_shortRatio_le
  {ε u a : ℝ} (hε : 0 < ε) (ha : 0 ≤ a)
  (hulower : -1 ≤ u)
  (huupper : u ≤ 1 + ε / 2)
  (hmargin : 0 ≤ CohnElkies.bε ε a) :
  CohnElkies.bε ε a *
        Real.exp ((u - 1) * a) *
      (Real.cosh (u * a) / Real.cosh a) ≤
    1 - 2 * ε

theorem CohnElkies.tendsto_shortShellRadiusContribution :
  Filter.Tendsto
    CohnElkies.shortShellRadiusContribution
    (nhdsWithin 0 (Set.Ioi 0))
    (nhds
      (∫ (a : ℝ) in Set.Ioi 0,
        CohnElkies.wallisRadiusIntegrand
          a))

theorem CohnElkies.positiveShellRadiusContribution_bounds
  {ε : ℝ} (hε : 0 < ε) :
  0 ≤
      CohnElkies.positiveShellRadiusContribution
        ε ∧
    CohnElkies.positiveShellRadiusContribution
        ε ≤
      (CohnElkies.Bε ε + 1) *
          CohnElkies.Qε ε *
        Real.exp
          (ε / 4 * (CohnElkies.Bε ε + 1))

theorem CohnElkies.tendsto_positiveShellRadiusContribution :
  Filter.Tendsto
    CohnElkies.positiveShellRadiusContribution
    (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

theorem CohnElkies.eventually_upper_shell_parameter_margin :
  ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0),
    CohnElkies.upperShellShortCoefficient
          ε *
        Real.exp
          (ε / 2 * CohnElkies.Aε ε) ≤
      1 / 5000 * CohnElkies.Qε ε *
        Real.exp (ε / 2 * CohnElkies.Bε ε)

theorem CohnElkies.minusPolynomial_neg (ε : ℝ)
  (z : ℂ) :
  CohnElkies.PMinus ε (-z) =
    CohnElkies.PPlus ε z

theorem CohnElkies.PZero_neg (z : ℂ) :
  CohnElkies.PZero (-z) =
    CohnElkies.PZero z

theorem CohnElkies.plusPolynomial_conj (ε : ℝ)
  (z : ℂ) :
  (starRingEnd ℂ) (CohnElkies.PPlus ε z) =
    CohnElkies.PMinus ε
      ((starRingEnd ℂ) z)

theorem CohnElkies.minusPolynomial_conj (ε : ℝ)
  (z : ℂ) :
  (starRingEnd ℂ)
      (CohnElkies.PMinus ε z) =
    CohnElkies.PPlus ε ((starRingEnd ℂ) z)

theorem CohnElkies.PZero_conj (z : ℂ) :
  (starRingEnd ℂ) (CohnElkies.PZero z) =
    CohnElkies.PZero (-(starRingEnd ℂ) z)

theorem CohnElkies.plusPolynomial_neg_I (ε : ℝ) :
  CohnElkies.PPlus ε (-Complex.I) =
    ↑(CohnElkies.β ε)

theorem CohnElkies.minusPolynomial_neg_I (ε : ℝ) :
  CohnElkies.PMinus ε (-Complex.I) =
    ↑(CohnElkies.β ε)

theorem CohnElkies.PZero_neg_I :
  CohnElkies.PZero (-Complex.I) = 0

theorem CohnElkies.plusPolynomial_imaginary
  (ε u : ℝ) :
  CohnElkies.PPlus ε (Complex.I * ↑u) =
    ↑(CohnElkies.β ε) +
      (1 - ↑u) ^ 2 * (1 + ↑u)

theorem CohnElkies.minusPolynomial_imaginary
  (ε u : ℝ) :
  CohnElkies.PMinus ε (Complex.I * ↑u) =
    ↑(CohnElkies.β ε) +
      (1 - ↑u) * (1 + ↑u) ^ 2

theorem CohnElkies.PZero_imaginary (u : ℝ) :
  CohnElkies.PZero (Complex.I * ↑u) =
    ↑u ^ 2 - 1

theorem CohnElkies.plusPolynomial_imaginary_re_pos
  {ε u : ℝ} (hε : 0 < ε) (hu : -1 < u) :
  0 <
    (CohnElkies.PPlus ε
        (Complex.I * ↑u)).re

theorem CohnElkies.minusPolynomial_imaginary_re_neg
  {ε u : ℝ} (hε : 0 < ε)
  (hu : 1 + ε / 4 ≤ u) :
  (CohnElkies.PMinus ε
        (Complex.I * ↑u)).re <
    0

theorem CohnElkies.PZero_imaginary_re_pos
  {ε u : ℝ} (hε : 0 < ε)
  (hu : 1 + ε / 4 ≤ u) :
  0 <
    (CohnElkies.PZero (Complex.I * ↑u)).re

theorem CohnElkies.saddleSource_fourier_minus_eq_plus
  {ε : ℝ} (hε : 0 < ε) {d : ℕ}
  (hd : 0 < d)
  (horder :
    CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε)
  (fminus fplus :
    CohnElkies.TestFunction d)
  (hminus :
    ∀ (x : CohnElkies.Euclidean d),
      fminus x =
        CohnElkies.fMinusFun ε d x)
  (hplus :
    ∀ (x : CohnElkies.Euclidean d),
      fplus x =
        CohnElkies.fPlusFun ε d x) :
  FourierTransform.fourier fminus = fplus

theorem CohnElkies.fourier_zeroSaddleSchwartz
  {ε : ℝ} (hε : 0 < ε) {d : ℕ}
  (hd : 0 < d)
  (horder :
    CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) :
  FourierTransform.fourier
      (CohnElkies.zeroSaddleSchwartz hε hd
        horder) =
    CohnElkies.zeroSaddleSchwartz hε hd
      horder

theorem CohnElkies.saddleSource_zero_pos {ε : ℝ}
  (hε : 0 < ε) {d : ℕ}
  (fminus fplus :
    CohnElkies.TestFunction d)
  (hminus :
    ∀ (x : CohnElkies.Euclidean d),
      fminus x =
        CohnElkies.fMinusFun ε d x)
  (hplus :
    ∀ (x : CohnElkies.Euclidean d),
      fplus x =
        CohnElkies.fPlusFun ε d x) :
  0 < (fminus 0).re ∧ 0 < (fplus 0).re

theorem CohnElkies.saddleSource_zero_eq {ε : ℝ}
  {d : ℕ}
  (fminus fplus :
    CohnElkies.TestFunction d)
  (hminus :
    ∀ (x : CohnElkies.Euclidean d),
      fminus x =
        CohnElkies.fMinusFun ε d x)
  (hplus :
    ∀ (x : CohnElkies.Euclidean d),
      fplus x =
        CohnElkies.fPlusFun ε d x) :
  fminus 0 = fplus 0

theorem CohnElkies.fZero_zero (ε ℓ : ℝ) :
  CohnElkies.fZero ε ℓ 0 = 0