HardyZeta.ThetaContour

            
              11.15. HardyZeta.ThetaContour🔗
            def thetaFourierIntegrand (t : ℝ) (z : ℂ) : ℂ :=
  exp (-I * (t : ℂ) * z) * thetaLogKernel ztheorem norm_thetaFourierIntegrand (t : ℝ) (z : ℂ) :
    ‖thetaFourierIntegrand t z‖ = Real.exp (t * z.im) * ‖thetaLogKernel z‖ := byt:ℝz:ℂ⊢ ‖thetaFourierIntegrand t z‖ = Real.exp (t * z.im) * ‖thetaLogKernel z‖
  simp [thetaFourierIntegrand, norm_exp, mul_re, mul_im]All goals completed! 🐙theorem differentiableAt_thetaFourierIntegrand (t : ℝ) {z : ℂ}
    (hz : |z.im| < Real.pi / 2) : DifferentiableAt ℂ (thetaFourierIntegrand t) z := byt:ℝz:ℂhz:|z.im| < Real.pi / 2⊢ DifferentiableAt ℂ (thetaFourierIntegrand t) z
  have h := differentiableAt_thetaLogKernel hzt:ℝz:ℂhz:|z.im| < Real.pi / 2h:DifferentiableAt ℂ thetaLogKernel z⊢ DifferentiableAt ℂ (thetaFourierIntegrand t) z
  unfold thetaFourierIntegrandt:ℝz:ℂhz:|z.im| < Real.pi / 2h:DifferentiableAt ℂ thetaLogKernel z⊢ DifferentiableAt ℂ (fun z => cexp (-I * ↑t * z) * thetaLogKernel z) z
  fun_propAll goals completed! 🐙theorem integrable_thetaFourierIntegrand_horizontal (t : ℝ) {b : ℝ}
    (hb : |b| < Real.pi / 2) :
    Integrable (fun u : ℝ ↦ thetaFourierIntegrand t ((u : ℂ) + b * I)) := byt:ℝb:ℝhb:|b| < Real.pi / 2⊢ Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volume
  have h := (integrable_thetaLogKernel_horizontal hb).norm.const_mul (Real.exp (t * b))t:ℝb:ℝhb:|b| < Real.pi / 2h:Integrable (fun x => Real.exp (t * b) * ‖thetaLogKernel (↑x + ↑b * I)‖) volume⊢ Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volume
  apply h.mono'hft:ℝb:ℝhb:|b| < Real.pi / 2h:Integrable (fun x => Real.exp (t * b) * ‖thetaLogKernel (↑x + ↑b * I)‖) volume⊢ AEStronglyMeasurable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeht:ℝb:ℝhb:|b| < Real.pi / 2h:Integrable (fun x => Real.exp (t * b) * ‖thetaLogKernel (↑x + ↑b * I)‖) volume⊢ ∀ᵐ (a : ℝ), ‖thetaFourierIntegrand t (↑a + ↑b * I)‖ ≤ Real.exp (t * b) * ‖thetaLogKernel (↑a + ↑b * I)‖
  ·hft:ℝb:ℝhb:|b| < Real.pi / 2h:Integrable (fun x => Real.exp (t * b) * ‖thetaLogKernel (↑x + ↑b * I)‖) volume⊢ AEStronglyMeasurable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volume apply Continuous.aestronglyMeasurablehft:ℝb:ℝhb:|b| < Real.pi / 2h:Integrable (fun x => Real.exp (t * b) * ‖thetaLogKernel (↑x + ↑b * I)‖) volume⊢ Continuous fun u => thetaFourierIntegrand t (↑u + ↑b * I)
    apply continuous_iff_continuousAt.mprhft:ℝb:ℝhb:|b| < Real.pi / 2h:Integrable (fun x => Real.exp (t * b) * ‖thetaLogKernel (↑x + ↑b * I)‖) volume⊢ ∀ (x : ℝ), ContinuousAt (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) x
    intro uhft:ℝb:ℝhb:|b| < Real.pi / 2h:Integrable (fun x => Real.exp (t * b) * ‖thetaLogKernel (↑x + ↑b * I)‖) volumeu:ℝ⊢ ContinuousAt (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) u
    apply (differentiableAt_thetaFourierIntegrand t (byt:ℝb:ℝhb:|b| < Real.pi / 2h:Integrable (fun x => Real.exp (t * b) * ‖thetaLogKernel (↑x + ↑b * I)‖) volumeu:ℝ⊢ |(↑u + ↑b * I).im| < Real.pi / 2 simpa using hbAll goals completed! 🐙)).continuousAt.comp
    fun_propAll goals completed! 🐙
  ·ht:ℝb:ℝhb:|b| < Real.pi / 2h:Integrable (fun x => Real.exp (t * b) * ‖thetaLogKernel (↑x + ↑b * I)‖) volume⊢ ∀ᵐ (a : ℝ), ‖thetaFourierIntegrand t (↑a + ↑b * I)‖ ≤ Real.exp (t * b) * ‖thetaLogKernel (↑a + ↑b * I)‖ filter_upwards with uht:ℝb:ℝhb:|b| < Real.pi / 2h:Integrable (fun x => Real.exp (t * b) * ‖thetaLogKernel (↑x + ↑b * I)‖) volumeu:ℝ⊢ ‖thetaFourierIntegrand t (↑u + ↑b * I)‖ ≤ Real.exp (t * b) * ‖thetaLogKernel (↑u + ↑b * I)‖
    simp [norm_thetaFourierIntegrand]All goals completed! 🐙theorem norm_thetaFourierIntegrand_le (t : ℝ) {b T y : ℝ}
    (hb : b < Real.pi / 2) (hy : |y| ≤ b) :
    ‖thetaFourierIntegrand t ((T : ℂ) + y * I)‖ ≤
      Real.exp (|t| * b) * thetaStripConstant b * Real.exp (-|T| / 4) := byt:ℝb:ℝT:ℝy:ℝhb:b < Real.pi / 2hy:|y| ≤ b⊢ ‖thetaFourierIntegrand t (↑T + ↑y * I)‖ ≤ Real.exp (|t| * b) * thetaStripConstant b * Real.exp (-|T| / 4)
  have hk := norm_thetaLogKernel_le (z := (T : ℂ) + y * I) hb (byt:ℝb:ℝT:ℝy:ℝhb:b < Real.pi / 2hy:|y| ≤ b⊢ |(↑T + ↑y * I).im| ≤ b simpa using hyAll goals completed! 🐙)t:ℝb:ℝT:ℝy:ℝhb:b < Real.pi / 2hy:|y| ≤ bhk:‖thetaLogKernel (↑T + ↑y * I)‖ ≤ thetaStripConstant b * Real.exp (-|(↑T + ↑y * I).re| / 4)⊢ ‖thetaFourierIntegrand t (↑T + ↑y * I)‖ ≤ Real.exp (|t| * b) * thetaStripConstant b * Real.exp (-|T| / 4)
  have he : Real.exp (t * y) ≤ Real.exp (|t| * b) := by
    apply Real.exp_le_exp.mprt:ℝb:ℝT:ℝy:ℝhb:b < Real.pi / 2hy:|y| ≤ bhk:‖thetaLogKernel (↑T + ↑y * I)‖ ≤ thetaStripConstant b * Real.exp (-|(↑T + ↑y * I).re| / 4)⊢ t * y ≤ |t| * b
    calc
      t * y ≤ |t * y| := le_abs_self _
      _ = |t| * |y| := abs_mul _ _
      _ ≤ |t| * b := mul_le_mul_of_nonneg_left hy (abs_nonneg _)t:ℝb:ℝT:ℝy:ℝhb:b < Real.pi / 2hy:|y| ≤ bhk:‖thetaLogKernel (↑T + ↑y * I)‖ ≤ thetaStripConstant b * Real.exp (-|(↑T + ↑y * I).re| / 4)he:Real.exp (t * y) ≤ Real.exp (|t| * b)⊢ ‖thetaFourierIntegrand t (↑T + ↑y * I)‖ ≤ Real.exp (|t| * b) * thetaStripConstant b * Real.exp (-|T| / 4)
  rw [norm_thetaFourierIntegrandt:ℝb:ℝT:ℝy:ℝhb:b < Real.pi / 2hy:|y| ≤ bhk:‖thetaLogKernel (↑T + ↑y * I)‖ ≤ thetaStripConstant b * Real.exp (-|(↑T + ↑y * I).re| / 4)he:Real.exp (t * y) ≤ Real.exp (|t| * b)⊢ Real.exp (t * (↑T + ↑y * I).im) * ‖thetaLogKernel (↑T + ↑y * I)‖ ≤
  Real.exp (|t| * b) * thetaStripConstant b * Real.exp (-|T| / 4)]t:ℝb:ℝT:ℝy:ℝhb:b < Real.pi / 2hy:|y| ≤ bhk:‖thetaLogKernel (↑T + ↑y * I)‖ ≤ thetaStripConstant b * Real.exp (-|(↑T + ↑y * I).re| / 4)he:Real.exp (t * y) ≤ Real.exp (|t| * b)⊢ Real.exp (t * (↑T + ↑y * I).im) * ‖thetaLogKernel (↑T + ↑y * I)‖ ≤
  Real.exp (|t| * b) * thetaStripConstant b * Real.exp (-|T| / 4)
  simp only [add_im, ofReal_im, mul_im, ofReal_re, I_im, mul_one, I_re, mul_zero,
    zero_add, add_re, mul_re, sub_zero, add_zero] at hk ⊢t:ℝb:ℝT:ℝy:ℝhb:b < Real.pi / 2hy:|y| ≤ bhe:Real.exp (t * y) ≤ Real.exp (|t| * b)hk:‖thetaLogKernel (↑T + ↑y * I)‖ ≤ thetaStripConstant b * Real.exp (-|T| / 4)⊢ Real.exp (t * y) * ‖thetaLogKernel (↑T + ↑y * I)‖ ≤ Real.exp (|t| * b) * thetaStripConstant b * Real.exp (-|T| / 4)
  calc
    Real.exp (t * y) * ‖thetaLogKernel ((T : ℂ) + y * I)‖ ≤
        Real.exp (|t| * b) * ‖thetaLogKernel ((T : ℂ) + y * I)‖ :=
      mul_le_mul_of_nonneg_right he (norm_nonneg _)
    _ ≤ Real.exp (|t| * b) * (thetaStripConstant b * Real.exp (-|T| / 4)) :=
      mul_le_mul_of_nonneg_left hk (Real.exp_pos _).le
    _ = _ := byt:ℝb:ℝT:ℝy:ℝhb:b < Real.pi / 2hy:|y| ≤ bhe:Real.exp (t * y) ≤ Real.exp (|t| * b)hk:‖thetaLogKernel (↑T + ↑y * I)‖ ≤ thetaStripConstant b * Real.exp (-|T| / 4)⊢ Real.exp (|t| * b) * (thetaStripConstant b * Real.exp (-|T| / 4)) =
  Real.exp (|t| * b) * thetaStripConstant b * Real.exp (-|T| / 4) ringAll goals completed! 🐙theorem norm_theta_verticalIntegral_le (t : ℝ) {b : ℝ}
    (hb : |b| < Real.pi / 2) (T : ℝ) :
    ‖∫ y : ℝ in (0 : ℝ)..b, thetaFourierIntegrand t ((T : ℂ) + y * I)‖ ≤
      |b| * (Real.exp (|t| * |b|) * thetaStripConstant |b|) * Real.exp (-|T| / 4) := byt:ℝb:ℝhb:|b| < Real.pi / 2T:ℝ⊢ ‖∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑T + ↑y * I)‖ ≤
  |b| * (Real.exp (|t| * |b|) * thetaStripConstant |b|) * Real.exp (-|T| / 4)
  have h := intervalIntegral.norm_integral_le_of_norm_le_const
    (C := Real.exp (|t| * |b|) * thetaStripConstant |b| * Real.exp (-|T| / 4))
    (a := 0) (b := b) (f := fun y : ℝ ↦ thetaFourierIntegrand t ((T : ℂ) + y * I))
    (fun y hy ↦ norm_thetaFourierIntegrand_le t hb (byt:ℝb:ℝhb:|b| < Real.pi / 2T:ℝy:ℝhy:y ∈ uIoc 0 b⊢ |y| ≤ |b|
      simpa using abs_sub_left_of_mem_uIcc (uIoc_subset_uIcc hy)All goals completed! 🐙))t:ℝb:ℝhb:|b| < Real.pi / 2T:ℝh:‖∫ (x : ℝ) in 0..b, thetaFourierIntegrand t (↑T + ↑x * I)‖ ≤
  Real.exp (|t| * |b|) * thetaStripConstant |b| * Real.exp (-|T| / 4) * |b - 0|⊢ ‖∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑T + ↑y * I)‖ ≤
  |b| * (Real.exp (|t| * |b|) * thetaStripConstant |b|) * Real.exp (-|T| / 4)
  simpa only [sub_zero, mul_assoc, mul_comm, mul_left_comm] using hAll goals completed! 🐙theorem tendsto_theta_verticalIntegral (t : ℝ) {b : ℝ}
    (hb : |b| < Real.pi / 2) (ε : ℝ) (hε : |ε| = 1) :
    Tendsto (fun T : ℝ ↦ ∫ y : ℝ in (0 : ℝ)..b,
      thetaFourierIntegrand t (((ε * T : ℝ) : ℂ) + y * I)) atTop (𝓝 0) := byt:ℝb:ℝhb:|b| < Real.pi / 2ε:ℝhε:|ε| = 1⊢ Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(ε * T) + ↑y * I)) atTop (𝓝 0)
  have hl : Tendsto (fun T : ℝ ↦ Real.exp (-|T| / 4)) atTop (𝓝 0) := by
    have h := Real.tendsto_exp_neg_atTop_nhds_zero.comp
      (tendsto_id.atTop_div_const (byt:ℝb:ℝhb:|b| < Real.pi / 2ε:ℝhε:|ε| = 1⊢ 0 < 4 norm_numAll goals completed! 🐙 : (0 : ℝ) < 4))t:ℝb:ℝhb:|b| < Real.pi / 2ε:ℝhε:|ε| = 1h:Tendsto ((fun x => Real.exp (-x)) ∘ fun x => id x / 4) atTop (𝓝 0)⊢ Tendsto (fun T => Real.exp (-|T| / 4)) atTop (𝓝 0)
    apply h.congr't:ℝb:ℝhb:|b| < Real.pi / 2ε:ℝhε:|ε| = 1h:Tendsto ((fun x => Real.exp (-x)) ∘ fun x => id x / 4) atTop (𝓝 0)⊢ ((fun x => Real.exp (-x)) ∘ fun x => id x / 4) =ᶠ[atTop] fun T => Real.exp (-|T| / 4)
    filter_upwards [eventually_ge_atTop (0 : ℝ)] with T hTt:ℝb:ℝhb:|b| < Real.pi / 2ε:ℝhε:|ε| = 1h:Tendsto ((fun x => Real.exp (-x)) ∘ fun x => id x / 4) atTop (𝓝 0)T:ℝhT:0 ≤ T⊢ ((fun x => Real.exp (-x)) ∘ fun x => id x / 4) T = Real.exp (-|T| / 4)
    simp [abs_of_nonneg hT, neg_div]t:ℝb:ℝhb:|b| < Real.pi / 2ε:ℝhε:|ε| = 1hl:Tendsto (fun T => Real.exp (-|T| / 4)) atTop (𝓝 0)⊢ Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(ε * T) + ↑y * I)) atTop (𝓝 0)
  have hbnd := hl.const_mul (|b| * (Real.exp (|t| * |b|) * thetaStripConstant |b|))t:ℝb:ℝhb:|b| < Real.pi / 2ε:ℝhε:|ε| = 1hl:Tendsto (fun T => Real.exp (-|T| / 4)) atTop (𝓝 0)hbnd:Tendsto (fun x => |b| * (Real.exp (|t| * |b|) * thetaStripConstant |b|) * Real.exp (-|x| / 4)) atTop
  (𝓝 (|b| * (Real.exp (|t| * |b|) * thetaStripConstant |b|) * 0))⊢ Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(ε * T) + ↑y * I)) atTop (𝓝 0)
  apply squeeze_zero_norm' _ (byt:ℝb:ℝhb:|b| < Real.pi / 2ε:ℝhε:|ε| = 1hl:Tendsto (fun T => Real.exp (-|T| / 4)) atTop (𝓝 0)hbnd:Tendsto (fun x => |b| * (Real.exp (|t| * |b|) * thetaStripConstant |b|) * Real.exp (-|x| / 4)) atTop
  (𝓝 (|b| * (Real.exp (|t| * |b|) * thetaStripConstant |b|) * 0))⊢ Tendsto ?m.164 atTop (𝓝 0) simpa using hbndAll goals completed! 🐙)
  filter_upwards with Tt:ℝb:ℝhb:|b| < Real.pi / 2ε:ℝhε:|ε| = 1hl:Tendsto (fun T => Real.exp (-|T| / 4)) atTop (𝓝 0)hbnd:Tendsto (fun x => |b| * (Real.exp (|t| * |b|) * thetaStripConstant |b|) * Real.exp (-|x| / 4)) atTop
  (𝓝 (|b| * (Real.exp (|t| * |b|) * thetaStripConstant |b|) * 0))T:ℝ⊢ ‖∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(ε * T) + ↑y * I)‖ ≤
  |b| * (Real.exp (|t| * |b|) * thetaStripConstant |b|) * Real.exp (-|T| / 4)
  simpa only [abs_mul, hε, one_mul] using norm_theta_verticalIntegral_le t hb (ε * T)All goals completed! 🐙

/-- Moving the Fourier integral to an interior horizontal line is justified by
Cauchy's theorem and vanishing vertical edges. -/theorem thetaFourierIntegral_shift (t : ℝ) {b : ℝ} (hb : |b| < Real.pi / 2) :
    (∫ u : ℝ, thetaFourierIntegrand t (u : ℂ)) =
      ∫ u : ℝ, thetaFourierIntegrand t ((u : ℂ) + b * I) := byt:ℝb:ℝhb:|b| < Real.pi / 2⊢ ∫ (u : ℝ), thetaFourierIntegrand t ↑u = ∫ (u : ℝ), thetaFourierIntegrand t (↑u + ↑b * I)
  have hi0 : Integrable (fun u : ℝ ↦ thetaFourierIntegrand t (u : ℂ)) := by
    simpa using integrable_thetaFourierIntegrand_horizontal t
      (b := 0) (byt:ℝb:ℝhb:|b| < Real.pi / 2⊢ |0| < Real.pi / 2 simpa using half_pos Real.pi_posAll goals completed! 🐙)t:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volume⊢ ∫ (u : ℝ), thetaFourierIntegrand t ↑u = ∫ (u : ℝ), thetaFourierIntegrand t (↑u + ↑b * I)
  have hib := integrable_thetaFourierIntegrand_horizontal t hbt:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volume⊢ ∫ (u : ℝ), thetaFourierIntegrand t ↑u = ∫ (u : ℝ), thetaFourierIntegrand t (↑u + ↑b * I)
  have h0 := intervalIntegral_tendsto_integral hi0 tendsto_neg_atTop_atBot tendsto_idt:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))⊢ ∫ (u : ℝ), thetaFourierIntegrand t ↑u = ∫ (u : ℝ), thetaFourierIntegrand t (↑u + ↑b * I)
  have hb' := intervalIntegral_tendsto_integral hib tendsto_neg_atTop_atBot tendsto_idt:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))⊢ ∫ (u : ℝ), thetaFourierIntegrand t ↑u = ∫ (u : ℝ), thetaFourierIntegrand t (↑u + ↑b * I)
  have hp := tendsto_theta_verticalIntegral t hb 1 (byt:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))⊢ |1| = 1 norm_numAll goals completed! 🐙)t:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)⊢ ∫ (u : ℝ), thetaFourierIntegrand t ↑u = ∫ (u : ℝ), thetaFourierIntegrand t (↑u + ↑b * I)
  have hm := tendsto_theta_verticalIntegral t hb (-1) (byt:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)⊢ |(-1)| = 1 norm_numAll goals completed! 🐙)t:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)⊢ ∫ (u : ℝ), thetaFourierIntegrand t ↑u = ∫ (u : ℝ), thetaFourierIntegrand t (↑u + ↑b * I)
  have hrect (T : ℝ) :
      (∫ x : ℝ in -T..T, thetaFourierIntegrand t (x : ℂ)) -
      (∫ x : ℝ in -T..T, thetaFourierIntegrand t ((x : ℂ) + b * I)) +
      I * (∫ y : ℝ in (0 : ℝ)..b, thetaFourierIntegrand t ((T : ℂ) + y * I)) -
      I * (∫ y : ℝ in (0 : ℝ)..b, thetaFourierIntegrand t ((-T : ℂ) + y * I)) = 0 := by
    have h := integral_boundary_rect_eq_zero_of_differentiableOn
      (thetaFourierIntegrand t) (-T : ℂ) ((T : ℂ) + b * I) (byt:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)T:ℝ⊢ DifferentiableOn ℂ (thetaFourierIntegrand t) (uIcc (-↑T).re (↑T + ↑b * I).re ×ℂ uIcc (-↑T).im (↑T + ↑b * I).im)
        intro z hzt:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)T:ℝz:ℂhz:z ∈ uIcc (-↑T).re (↑T + ↑b * I).re ×ℂ uIcc (-↑T).im (↑T + ↑b * I).im⊢ DifferentiableWithinAt ℂ (thetaFourierIntegrand t) (uIcc (-↑T).re (↑T + ↑b * I).re ×ℂ uIcc (-↑T).im (↑T + ↑b * I).im) z
        apply (differentiableAt_thetaFourierIntegrand t _).differentiableWithinAtt:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)T:ℝz:ℂhz:z ∈ uIcc (-↑T).re (↑T + ↑b * I).re ×ℂ uIcc (-↑T).im (↑T + ↑b * I).im⊢ |z.im| < Real.pi / 2
        have hy : z.im ∈ uIcc 0 b := byt:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)T:ℝ⊢ DifferentiableOn ℂ (thetaFourierIntegrand t) (uIcc (-↑T).re (↑T + ↑b * I).re ×ℂ uIcc (-↑T).im (↑T + ↑b * I).im) simpa using hz.2t:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)T:ℝz:ℂhz:z ∈ uIcc (-↑T).re (↑T + ↑b * I).re ×ℂ uIcc (-↑T).im (↑T + ↑b * I).imhy:z.im ∈ uIcc 0 b⊢ |z.im| < Real.pi / 2
        have ha : |z.im| ≤ |b| := byt:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)T:ℝ⊢ DifferentiableOn ℂ (thetaFourierIntegrand t) (uIcc (-↑T).re (↑T + ↑b * I).re ×ℂ uIcc (-↑T).im (↑T + ↑b * I).im) simpa using abs_sub_left_of_mem_uIcc hyt:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)T:ℝz:ℂhz:z ∈ uIcc (-↑T).re (↑T + ↑b * I).re ×ℂ uIcc (-↑T).im (↑T + ↑b * I).imhy:z.im ∈ uIcc 0 bha:|z.im| ≤ |b|⊢ |z.im| < Real.pi / 2
        exact ha.trans_lt hbAll goals completed! 🐙)t:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)T:ℝh:(((∫ (x : ℝ) in (-↑T).re..(↑T + ↑b * I).re, thetaFourierIntegrand t (↑x + ↑(-↑T).im * I)) -
        ∫ (x : ℝ) in (-↑T).re..(↑T + ↑b * I).re, thetaFourierIntegrand t (↑x + ↑(↑T + ↑b * I).im * I)) +
      I • ∫ (y : ℝ) in (-↑T).im..(↑T + ↑b * I).im, thetaFourierIntegrand t (↑(↑T + ↑b * I).re + ↑y * I)) -
    I • ∫ (y : ℝ) in (-↑T).im..(↑T + ↑b * I).im, thetaFourierIntegrand t (↑(-↑T).re + ↑y * I) =
  0⊢ (((∫ (x : ℝ) in -T..T, thetaFourierIntegrand t ↑x) - ∫ (x : ℝ) in -T..T, thetaFourierIntegrand t (↑x + ↑b * I)) +
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑T + ↑y * I)) -
    I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑T + ↑y * I) =
  0
    simpa [smul_eq_mul] using ht:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)hrect:∀ (T : ℝ),
  (((∫ (x : ℝ) in -T..T, thetaFourierIntegrand t ↑x) - ∫ (x : ℝ) in -T..T, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑T + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑T + ↑y * I) =
    0⊢ ∫ (u : ℝ), thetaFourierIntegrand t ↑u = ∫ (u : ℝ), thetaFourierIntegrand t (↑u + ↑b * I)
  have hlim := ((h0.sub hb').add (hp.const_mul I)).sub (hm.const_mul I)t:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)hrect:∀ (T : ℝ),
  (((∫ (x : ℝ) in -T..T, thetaFourierIntegrand t ↑x) - ∫ (x : ℝ) in -T..T, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑T + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑T + ↑y * I) =
    0hlim:Tendsto
  (fun x =>
    (((∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t ↑x) -
          ∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * x) + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * x) + ↑y * I))
  atTop
  (𝓝
    (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume - ∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume + I * 0 -
      I * 0))⊢ ∫ (u : ℝ), thetaFourierIntegrand t ↑u = ∫ (u : ℝ), thetaFourierIntegrand t (↑u + ↑b * I)
  simp only [mul_zero, add_zero, sub_zero, one_mul, neg_one_mul, ofReal_neg] at hlimt:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)hrect:∀ (T : ℝ),
  (((∫ (x : ℝ) in -T..T, thetaFourierIntegrand t ↑x) - ∫ (x : ℝ) in -T..T, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑T + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑T + ↑y * I) =
    0hlim:Tendsto
  (fun x =>
    (((∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t ↑x) -
          ∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑x + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑x + ↑y * I))
  atTop (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume - ∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))⊢ ∫ (u : ℝ), thetaFourierIntegrand t ↑u = ∫ (u : ℝ), thetaFourierIntegrand t (↑u + ↑b * I)
  have heq : (∫ u : ℝ, thetaFourierIntegrand t (u : ℂ)) -
      (∫ u : ℝ, thetaFourierIntegrand t ((u : ℂ) + b * I)) = 0 := by
    apply tendsto_nhds_unique hlimt:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)hrect:∀ (T : ℝ),
  (((∫ (x : ℝ) in -T..T, thetaFourierIntegrand t ↑x) - ∫ (x : ℝ) in -T..T, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑T + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑T + ↑y * I) =
    0hlim:Tendsto
  (fun x =>
    (((∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t ↑x) -
          ∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑x + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑x + ↑y * I))
  atTop (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume - ∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))⊢ Tendsto
  (fun x =>
    (((∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t ↑x) -
          ∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑x + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑x + ↑y * I))
  atTop (𝓝 0)
    simp_rw [t:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)hrect:∀ (T : ℝ),
  (((∫ (x : ℝ) in -T..T, thetaFourierIntegrand t ↑x) - ∫ (x : ℝ) in -T..T, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑T + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑T + ↑y * I) =
    0hlim:Tendsto
  (fun x =>
    (((∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t ↑x) -
          ∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑x + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑x + ↑y * I))
  atTop (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume - ∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))⊢ Tendsto
  (fun x =>
    (((∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t ↑x) -
          ∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑x + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑x + ↑y * I))
  atTop (𝓝 0)id_eq,t:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)hrect:∀ (T : ℝ),
  (((∫ (x : ℝ) in -T..T, thetaFourierIntegrand t ↑x) - ∫ (x : ℝ) in -T..T, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑T + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑T + ↑y * I) =
    0hlim:Tendsto
  (fun x =>
    (((∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t ↑x) -
          ∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑x + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑x + ↑y * I))
  atTop (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume - ∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))⊢ Tendsto
  (fun x =>
    (((∫ (x : ℝ) in -x..x, thetaFourierIntegrand t ↑x) - ∫ (x : ℝ) in -x..x, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑x + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑x + ↑y * I))
  atTop (𝓝 0) hrectt:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)hrect:∀ (T : ℝ),
  (((∫ (x : ℝ) in -T..T, thetaFourierIntegrand t ↑x) - ∫ (x : ℝ) in -T..T, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑T + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑T + ↑y * I) =
    0hlim:Tendsto
  (fun x =>
    (((∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t ↑x) -
          ∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑x + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑x + ↑y * I))
  atTop (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume - ∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))⊢ Tendsto (fun x => 0) atTop (𝓝 0)]
    exact tendsto_const_nhdst:ℝb:ℝhb:|b| < Real.pi / 2hi0:Integrable (fun u => thetaFourierIntegrand t ↑u) volumehib:Integrable (fun u => thetaFourierIntegrand t (↑u + ↑b * I)) volumeh0:Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t ↑x) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume))hb':Tendsto (fun i => ∫ (x : ℝ) in -i..id i, thetaFourierIntegrand t (↑x + ↑b * I)) atTop
  (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))hp:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(1 * T) + ↑y * I)) atTop (𝓝 0)hm:Tendsto (fun T => ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑(-1 * T) + ↑y * I)) atTop (𝓝 0)hrect:∀ (T : ℝ),
  (((∫ (x : ℝ) in -T..T, thetaFourierIntegrand t ↑x) - ∫ (x : ℝ) in -T..T, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑T + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑T + ↑y * I) =
    0hlim:Tendsto
  (fun x =>
    (((∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t ↑x) -
          ∫ (x : ℝ) in -x..id x, thetaFourierIntegrand t (↑x + ↑b * I)) +
        I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (↑x + ↑y * I)) -
      I * ∫ (y : ℝ) in 0..b, thetaFourierIntegrand t (-↑x + ↑y * I))
  atTop (𝓝 (∫ (x : ℝ), thetaFourierIntegrand t ↑x ∂volume - ∫ (x : ℝ), thetaFourierIntegrand t (↑x + ↑b * I) ∂volume))heq:(∫ (u : ℝ), thetaFourierIntegrand t ↑u) - ∫ (u : ℝ), thetaFourierIntegrand t (↑u + ↑b * I) = 0⊢ ∫ (u : ℝ), thetaFourierIntegrand t ↑u = ∫ (u : ℝ), thetaFourierIntegrand t (↑u + ↑b * I)
  exact sub_eq_zero.mp heqAll goals completed! 🐙

/-- The L¹ mass on a horizontal line is a finite real constant. -/def thetaHorizontalMass (b : ℝ) : ℝ :=
  ∫ u : ℝ, ‖thetaLogKernel ((u : ℂ) + b * I)‖theorem thetaHorizontalMass_nonneg (b : ℝ) : 0 ≤ thetaHorizontalMass b :=
  integral_nonneg fun _ ↦ norm_nonneg _theorem norm_thetaFourierIntegral_le (t : ℝ) {b : ℝ} (hb : |b| < Real.pi / 2) :
    ‖∫ u : ℝ, thetaFourierIntegrand t (u : ℂ)‖ ≤
      Real.exp (t * b) * thetaHorizontalMass b := byt:ℝb:ℝhb:|b| < Real.pi / 2⊢ ‖∫ (u : ℝ), thetaFourierIntegrand t ↑u‖ ≤ Real.exp (t * b) * thetaHorizontalMass b
  rw [thetaFourierIntegral_shift t hbt:ℝb:ℝhb:|b| < Real.pi / 2⊢ ‖∫ (u : ℝ), thetaFourierIntegrand t (↑u + ↑b * I)‖ ≤ Real.exp (t * b) * thetaHorizontalMass b]t:ℝb:ℝhb:|b| < Real.pi / 2⊢ ‖∫ (u : ℝ), thetaFourierIntegrand t (↑u + ↑b * I)‖ ≤ Real.exp (t * b) * thetaHorizontalMass b
  apply (norm_integral_le_integral_norm _).trans_eqt:ℝb:ℝhb:|b| < Real.pi / 2⊢ ∫ (a : ℝ), ‖thetaFourierIntegrand t (↑a + ↑b * I)‖ = Real.exp (t * b) * thetaHorizontalMass b
  simp only [norm_thetaFourierIntegrand, add_im, ofReal_im, mul_im, ofReal_re, I_im,
    mul_one, I_re, mul_zero, zero_add, add_zero, integral_const_mul, thetaHorizontalMass]All goals completed! 🐙theorem completedZeta_eq_thetaFourierIntegral (t : ℝ) :
    completedRiemannZeta (criticalPoint t) =
      (∫ u : ℝ, thetaFourierIntegrand (t / 2) (u : ℂ)) / 2 := byt:ℝ⊢ completedRiemannZeta (criticalPoint t) = (∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u) / 2
  rw [completedZeta_eq_fourier_theta,t:ℝ⊢ FourierTransform.fourier (fun u => thetaLogKernel ↑u) (t / (4 * Real.pi)) / 2 =
  (∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u) / 2 Real.fourier_eq't:ℝ⊢ (∫ (v : ℝ), cexp (↑(-2 * Real.pi * inner ℝ v (t / (4 * Real.pi))) * I) • thetaLogKernel ↑v) / 2 =
  (∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u) / 2]t:ℝ⊢ (∫ (v : ℝ), cexp (↑(-2 * Real.pi * inner ℝ v (t / (4 * Real.pi))) * I) • thetaLogKernel ↑v) / 2 =
  (∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u) / 2
  congr 1e_at:ℝ⊢ ∫ (v : ℝ), cexp (↑(-2 * Real.pi * inner ℝ v (t / (4 * Real.pi))) * I) • thetaLogKernel ↑v =
  ∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u
  apply integral_congr_aee_at:ℝ⊢ (fun a => cexp (↑(-2 * Real.pi * inner ℝ a (t / (4 * Real.pi))) * I) • thetaLogKernel ↑a) =ᵐ[volume] fun a =>
  thetaFourierIntegrand (t / 2) ↑a
  filter_upwards with ue_at:ℝu:ℝ⊢ cexp (↑(-2 * Real.pi * inner ℝ u (t / (4 * Real.pi))) * I) • thetaLogKernel ↑u = thetaFourierIntegrand (t / 2) ↑u
  unfold thetaFourierIntegrande_at:ℝu:ℝ⊢ cexp (↑(-2 * Real.pi * inner ℝ u (t / (4 * Real.pi))) * I) • thetaLogKernel ↑u =
  cexp (-I * ↑(t / 2) * ↑u) * thetaLogKernel ↑u
  rw [smul_eq_mule_at:ℝu:ℝ⊢ cexp (↑(-2 * Real.pi * inner ℝ u (t / (4 * Real.pi))) * I) * thetaLogKernel ↑u =
  cexp (-I * ↑(t / 2) * ↑u) * thetaLogKernel ↑u]e_at:ℝu:ℝ⊢ cexp (↑(-2 * Real.pi * inner ℝ u (t / (4 * Real.pi))) * I) * thetaLogKernel ↑u =
  cexp (-I * ↑(t / 2) * ↑u) * thetaLogKernel ↑u
  congr 2e_a.e_at:ℝu:ℝ⊢ ↑(-2 * Real.pi * inner ℝ u (t / (4 * Real.pi))) * I = -I * ↑(t / 2) * ↑u
  simp only [RCLike.inner_apply, conj_trivial]e_a.e_at:ℝu:ℝ⊢ ↑(-2 * Real.pi * (t / (4 * Real.pi) * u)) * I = -I * ↑(t / 2) * ↑u
  push_caste_a.e_at:ℝu:ℝ⊢ -2 * ↑Real.pi * (↑t / (4 * ↑Real.pi) * ↑u) * I = -I * (↑t / 2) * ↑u
  field_simpe_a.e_at:ℝu:ℝ⊢ -(2 ^ 2 * ↑t * ↑u) = -(↑t * 4 * ↑u)
  ringAll goals completed! 🐙

/-- Exponential decay of the actual completed zeta on the positive critical line. -/theorem norm_completedZeta_critical_le {a : ℝ} (ha : 0 < a) (ha' : a < Real.pi / 4)
    (t : ℝ) :
    ‖completedRiemannZeta (criticalPoint t)‖ ≤
      (thetaHorizontalMass (-2 * a) / 2) * Real.exp (-a * t) := bya:ℝha:0 < aha':a < Real.pi / 4t:ℝ⊢ ‖completedRiemannZeta (criticalPoint t)‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)
  have hb : |(-2 * a)| < Real.pi / 2 := by rw [abs_of_neg (bya:ℝha:0 < aha':a < Real.pi / 4t:ℝ⊢ -2 * a < 0 linarithAll goals completed! 🐙)]a:ℝha:0 < aha':a < Real.pi / 4t:ℝ⊢ -(-2 * a) < Real.pi / 2; linaritha:ℝha:0 < aha':a < Real.pi / 4t:ℝhb:|-2 * a| < Real.pi / 2⊢ ‖completedRiemannZeta (criticalPoint t)‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)
  have h := norm_thetaFourierIntegral_le (t / 2) hba:ℝha:0 < aha':a < Real.pi / 4t:ℝhb:|-2 * a| < Real.pi / 2h:‖∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u‖ ≤ Real.exp (t / 2 * (-2 * a)) * thetaHorizontalMass (-2 * a)⊢ ‖completedRiemannZeta (criticalPoint t)‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)
  rw [completedZeta_eq_thetaFourierIntegral,a:ℝha:0 < aha':a < Real.pi / 4t:ℝhb:|-2 * a| < Real.pi / 2h:‖∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u‖ ≤ Real.exp (t / 2 * (-2 * a)) * thetaHorizontalMass (-2 * a)⊢ ‖(∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u) / 2‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t) norm_diva:ℝha:0 < aha':a < Real.pi / 4t:ℝhb:|-2 * a| < Real.pi / 2h:‖∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u‖ ≤ Real.exp (t / 2 * (-2 * a)) * thetaHorizontalMass (-2 * a)⊢ ‖∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u‖ / ‖2‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)]a:ℝha:0 < aha':a < Real.pi / 4t:ℝhb:|-2 * a| < Real.pi / 2h:‖∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u‖ ≤ Real.exp (t / 2 * (-2 * a)) * thetaHorizontalMass (-2 * a)⊢ ‖∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u‖ / ‖2‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)
  norm_num only [norm_ofNat]a:ℝha:0 < aha':a < Real.pi / 4t:ℝhb:|-2 * a| < Real.pi / 2h:‖∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u‖ ≤ Real.exp (t / 2 * (-2 * a)) * thetaHorizontalMass (-2 * a)⊢ ‖∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u‖ / 2 ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)
  have he : (t / 2) * (-2 * a) = -a * t := bya:ℝha:0 < aha':a < Real.pi / 4t:ℝ⊢ ‖completedRiemannZeta (criticalPoint t)‖ ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t) ringa:ℝha:0 < aha':a < Real.pi / 4t:ℝhb:|-2 * a| < Real.pi / 2h:‖∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u‖ ≤ Real.exp (t / 2 * (-2 * a)) * thetaHorizontalMass (-2 * a)he:t / 2 * (-2 * a) = -a * t⊢ ‖∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u‖ / 2 ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)
  rw [hea:ℝha:0 < aha':a < Real.pi / 4t:ℝhb:|-2 * a| < Real.pi / 2h:‖∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u‖ ≤ Real.exp (-a * t) * thetaHorizontalMass (-2 * a)he:t / 2 * (-2 * a) = -a * t⊢ ‖∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u‖ / 2 ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)] at ha:ℝha:0 < aha':a < Real.pi / 4t:ℝhb:|-2 * a| < Real.pi / 2h:‖∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u‖ ≤ Real.exp (-a * t) * thetaHorizontalMass (-2 * a)he:t / 2 * (-2 * a) = -a * t⊢ ‖∫ (u : ℝ), thetaFourierIntegrand (t / 2) ↑u‖ / 2 ≤ thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)
  nlinarithAll goals completed! 🐙