HardyZeta.ThetaKernelBounds

            
              11.19. HardyZeta.ThetaKernelBounds🔗
            theorem norm_psi_le_inv_re {z : ℂ} {c : ℝ} (hc : 0 < c) (hz : c ≤ z.re) :
    ‖psi z‖ ≤ 1 / (Real.pi * z.re * (1 - Real.exp (-Real.pi * c))) := byz:ℂc:ℝhc:0 < chz:c ≤ z.re⊢ ‖psi z‖ ≤ 1 / (Real.pi * z.re * (1 - Real.exp (-Real.pi * c)))
  have hz0 : 0 < z.re := hc.trans_le hzz:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.re⊢ ‖psi z‖ ≤ 1 / (Real.pi * z.re * (1 - Real.exp (-Real.pi * c)))
  have hpc : 0 < Real.pi * c := mul_pos Real.pi_pos hcz:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * c⊢ ‖psi z‖ ≤ 1 / (Real.pi * z.re * (1 - Real.exp (-Real.pi * c)))
  have hpz : 0 < Real.pi * z.re := mul_pos Real.pi_pos hz0z:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.re⊢ ‖psi z‖ ≤ 1 / (Real.pi * z.re * (1 - Real.exp (-Real.pi * c)))
  have hd : 0 < 1 - Real.exp (-Real.pi * c) := by
    have := Real.exp_lt_one_iff.mpr (byz:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.re⊢ -Real.pi * c < 0 nlinarithAll goals completed! 🐙 : -Real.pi * c < 0)z:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.rethis:Real.exp (-Real.pi * c) < 1⊢ 0 < 1 - Real.exp (-Real.pi * c)
    linarithz:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.rehd:0 < 1 - Real.exp (-Real.pi * c)⊢ ‖psi z‖ ≤ 1 / (Real.pi * z.re * (1 - Real.exp (-Real.pi * c)))
  have he : Real.exp (-Real.pi * z.re) ≤ 1 / (Real.pi * z.re) := by
    rw [neg_mul,z:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.rehd:0 < 1 - Real.exp (-Real.pi * c)⊢ Real.exp (-(Real.pi * z.re)) ≤ 1 / (Real.pi * z.re) Real.exp_negz:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.rehd:0 < 1 - Real.exp (-Real.pi * c)⊢ (Real.exp (Real.pi * z.re))⁻¹ ≤ 1 / (Real.pi * z.re)]z:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.rehd:0 < 1 - Real.exp (-Real.pi * c)⊢ (Real.exp (Real.pi * z.re))⁻¹ ≤ 1 / (Real.pi * z.re)
    have hle : Real.pi * z.re ≤ Real.exp (Real.pi * z.re) := byz:ℂc:ℝhc:0 < chz:c ≤ z.re⊢ ‖psi z‖ ≤ 1 / (Real.pi * z.re * (1 - Real.exp (-Real.pi * c)))
      linarith [Real.add_one_le_exp (Real.pi * z.re)]z:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.rehd:0 < 1 - Real.exp (-Real.pi * c)hle:Real.pi * z.re ≤ Real.exp (Real.pi * z.re)⊢ (Real.exp (Real.pi * z.re))⁻¹ ≤ 1 / (Real.pi * z.re)
    simpa only [one_div] using one_div_le_one_div_of_le hpz hlez:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.rehd:0 < 1 - Real.exp (-Real.pi * c)he:Real.exp (-Real.pi * z.re) ≤ 1 / (Real.pi * z.re)⊢ ‖psi z‖ ≤ 1 / (Real.pi * z.re * (1 - Real.exp (-Real.pi * c)))
  have hec : Real.exp (-Real.pi * z.re) ≤ Real.exp (-Real.pi * c) := by
    apply Real.exp_le_exp.mprz:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.rehd:0 < 1 - Real.exp (-Real.pi * c)he:Real.exp (-Real.pi * z.re) ≤ 1 / (Real.pi * z.re)⊢ -Real.pi * z.re ≤ -Real.pi * c
    nlinarith [Real.pi_pos]z:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.rehd:0 < 1 - Real.exp (-Real.pi * c)he:Real.exp (-Real.pi * z.re) ≤ 1 / (Real.pi * z.re)hec:Real.exp (-Real.pi * z.re) ≤ Real.exp (-Real.pi * c)⊢ ‖psi z‖ ≤ 1 / (Real.pi * z.re * (1 - Real.exp (-Real.pi * c)))
  apply (norm_psi_le hz0).transz:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.rehd:0 < 1 - Real.exp (-Real.pi * c)he:Real.exp (-Real.pi * z.re) ≤ 1 / (Real.pi * z.re)hec:Real.exp (-Real.pi * z.re) ≤ Real.exp (-Real.pi * c)⊢ Real.exp (-Real.pi * z.re) / (1 - Real.exp (-Real.pi * z.re)) ≤ 1 / (Real.pi * z.re * (1 - Real.exp (-Real.pi * c)))
  calc
    Real.exp (-Real.pi * z.re) / (1 - Real.exp (-Real.pi * z.re)) ≤
        (1 / (Real.pi * z.re)) / (1 - Real.exp (-Real.pi * c)) := byz:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.rehd:0 < 1 - Real.exp (-Real.pi * c)he:Real.exp (-Real.pi * z.re) ≤ 1 / (Real.pi * z.re)hec:Real.exp (-Real.pi * z.re) ≤ Real.exp (-Real.pi * c)⊢ Real.exp (-Real.pi * z.re) / (1 - Real.exp (-Real.pi * z.re)) ≤ 1 / (Real.pi * z.re) / (1 - Real.exp (-Real.pi * c))
      exact div_le_div₀ (byz:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.rehd:0 < 1 - Real.exp (-Real.pi * c)he:Real.exp (-Real.pi * z.re) ≤ 1 / (Real.pi * z.re)hec:Real.exp (-Real.pi * z.re) ≤ Real.exp (-Real.pi * c)⊢ 0 ≤ 1 / (Real.pi * z.re) positivityAll goals completed! 🐙) he hd (byz:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.rehd:0 < 1 - Real.exp (-Real.pi * c)he:Real.exp (-Real.pi * z.re) ≤ 1 / (Real.pi * z.re)hec:Real.exp (-Real.pi * z.re) ≤ Real.exp (-Real.pi * c)⊢ 1 - Real.exp (-Real.pi * c) ≤ 1 - Real.exp (-Real.pi * z.re) linarithAll goals completed! 🐙)
    _ = _ := byz:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.rehd:0 < 1 - Real.exp (-Real.pi * c)he:Real.exp (-Real.pi * z.re) ≤ 1 / (Real.pi * z.re)hec:Real.exp (-Real.pi * z.re) ≤ Real.exp (-Real.pi * c)⊢ 1 / (Real.pi * z.re) / (1 - Real.exp (-Real.pi * c)) = 1 / (Real.pi * z.re * (1 - Real.exp (-Real.pi * c))) rw [div_divz:ℂc:ℝhc:0 < chz:c ≤ z.rehz0:0 < z.rehpc:0 < Real.pi * chpz:0 < Real.pi * z.rehd:0 < 1 - Real.exp (-Real.pi * c)he:Real.exp (-Real.pi * z.re) ≤ 1 / (Real.pi * z.re)hec:Real.exp (-Real.pi * z.re) ≤ Real.exp (-Real.pi * c)⊢ 1 / (Real.pi * z.re * (1 - Real.exp (-Real.pi * c))) = 1 / (Real.pi * z.re * (1 - Real.exp (-Real.pi * c)))]All goals completed! 🐙

/-- A horizontal strip has a fixed positive lower bound for the cosine factor. -/theorem cos_im_lower {z : ℂ} {b : ℝ} (hb : b < Real.pi / 2) (hz : |z.im| ≤ b) :
    0 < Real.cos b ∧ Real.cos b ≤ Real.cos z.im := byz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ b⊢ 0 < Real.cos b ∧ Real.cos b ≤ Real.cos z.im
  have hb0 : 0 ≤ b := (abs_nonneg _).trans hzz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhb0:0 ≤ b⊢ 0 < Real.cos b ∧ Real.cos b ≤ Real.cos z.im
  constructorleftz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhb0:0 ≤ b⊢ 0 < Real.cos brightz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhb0:0 ≤ b⊢ Real.cos b ≤ Real.cos z.im
  ·leftz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhb0:0 ≤ b⊢ 0 < Real.cos b apply Real.cos_pos_of_mem_Iooleftz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhb0:0 ≤ b⊢ b ∈ Ioo (-(Real.pi / 2)) (Real.pi / 2)
    constructorleft.leftz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhb0:0 ≤ b⊢ -(Real.pi / 2) < bleft.rightz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhb0:0 ≤ b⊢ b < Real.pi / 2 <;>left.leftz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhb0:0 ≤ b⊢ -(Real.pi / 2) < bleft.rightz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhb0:0 ≤ b⊢ b < Real.pi / 2 linarith [Real.pi_pos]All goals completed! 🐙
  ·rightz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhb0:0 ≤ b⊢ Real.cos b ≤ Real.cos z.im simpa only [Real.cos_abs] using
      Real.cos_le_cos_of_nonneg_of_le_pi (abs_nonneg z.im) (byz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhb0:0 ≤ b⊢ b ≤ Real.pi linarith [Real.pi_pos]All goals completed! 🐙) hz

/-- A concrete horizontal-strip constant. -/def thetaStripConstant (b : ℝ) : ℝ :=
  2 / (Real.pi * Real.cos b * (1 - Real.exp (-Real.pi * Real.cos b))) + 1theorem norm_thetaLogKernel_le_of_re_nonneg {z : ℂ} {b : ℝ}
    (hb : b < Real.pi / 2) (hz : |z.im| ≤ b) (hx : 0 ≤ z.re) :
    ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-z.re / 4) := byz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.re⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-z.re / 4)
  obtain ⟨hc, hcos⟩ := cos_im_lower hb hzz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.im⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-z.re / 4)
  let c := Real.cos bz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos b⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-z.re / 4)
  let D := 1 - Real.exp (-Real.pi * c)z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-z.re / 4)
  have hc0 : 0 < c := hcz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < c⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-z.re / 4)
  have hD : 0 < D := by
    dsimp [D]z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < c⊢ 0 < 1 - Real.exp (-Real.pi * c)
    have := Real.exp_lt_one_iff.mpr (byz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < c⊢ -Real.pi * c < 0 nlinarith [Real.pi_pos]All goals completed! 🐙 : -Real.pi * c < 0)z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < cthis:Real.exp (-Real.pi * c) < 1⊢ 0 < 1 - Real.exp (-Real.pi * c)
    linarithz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < D⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-z.re / 4)
  have hex : 1 ≤ Real.exp z.re := Real.one_le_exp_iff.mpr hxz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.re⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-z.re / 4)
  have hre : c ≤ (exp z).re := by
    rw [exp_rez:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.re⊢ c ≤ Real.exp z.re * Real.cos z.im]z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.re⊢ c ≤ Real.exp z.re * Real.cos z.im
    dsimp [c]z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.re⊢ Real.cos b ≤ Real.exp z.re * Real.cos z.im
    nlinarithz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).re⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-z.re / 4)
  have hpsi : ‖psi (exp z)‖ ≤ (1 / (Real.pi * c * D)) * Real.exp (-z.re) := by
    apply (norm_psi_le_inv_re hc0 hre).transz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).re⊢ 1 / (Real.pi * (cexp z).re * (1 - Real.exp (-Real.pi * c))) ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)
    have hm : Real.pi * c * Real.exp z.re * D ≤ Real.pi * (exp z).re * D := byz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.re⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-z.re / 4)
      rw [exp_rez:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).re⊢ Real.pi * c * Real.exp z.re * D ≤ Real.pi * (Real.exp z.re * Real.cos z.im) * D]z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).re⊢ Real.pi * c * Real.exp z.re * D ≤ Real.pi * (Real.exp z.re * Real.cos z.im) * D
      have h := mul_le_mul_of_nonneg_right
        (mul_le_mul_of_nonneg_left hcos (mul_pos Real.pi_pos (Real.exp_pos z.re)).le) hD.lez:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).reh:Real.pi * Real.exp z.re * Real.cos b * D ≤ Real.pi * Real.exp z.re * Real.cos z.im * D⊢ Real.pi * c * Real.exp z.re * D ≤ Real.pi * (Real.exp z.re * Real.cos z.im) * D
      dsimp [c]z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).reh:Real.pi * Real.exp z.re * Real.cos b * D ≤ Real.pi * Real.exp z.re * Real.cos z.im * D⊢ Real.pi * Real.cos b * Real.exp z.re * D ≤ Real.pi * (Real.exp z.re * Real.cos z.im) * D
      nlinarith only [h]z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehm:Real.pi * c * Real.exp z.re * D ≤ Real.pi * (cexp z).re * D⊢ 1 / (Real.pi * (cexp z).re * (1 - Real.exp (-Real.pi * c))) ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)
    calc
      1 / (Real.pi * (exp z).re * D) ≤ 1 / (Real.pi * c * Real.exp z.re * D) :=
        one_div_le_one_div_of_le (byz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehm:Real.pi * c * Real.exp z.re * D ≤ Real.pi * (cexp z).re * D⊢ 0 < Real.pi * c * Real.exp z.re * D positivityAll goals completed! 🐙) hm
      _ = (1 / (Real.pi * c * D)) * Real.exp (-z.re) := byz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehm:Real.pi * c * Real.exp z.re * D ≤ Real.pi * (cexp z).re * D⊢ 1 / (Real.pi * c * Real.exp z.re * D) = 1 / (Real.pi * c * D) * Real.exp (-z.re)
        rw [Real.exp_negz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehm:Real.pi * c * Real.exp z.re * D ≤ Real.pi * (cexp z).re * D⊢ 1 / (Real.pi * c * Real.exp z.re * D) = 1 / (Real.pi * c * D) * (Real.exp z.re)⁻¹]z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehm:Real.pi * c * Real.exp z.re * D ≤ Real.pi * (cexp z).re * D⊢ 1 / (Real.pi * c * Real.exp z.re * D) = 1 / (Real.pi * c * D) * (Real.exp z.re)⁻¹
        field_simpz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-z.re / 4)
  have hstrip : |z.im| < Real.pi / 2 := hz.trans_lt hbz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-z.re / 4)
  have hbase : ‖thetaLogKernel z‖ ≤
      2 * Real.exp (z.re / 4) * ‖psi (exp z)‖ + Real.exp (-z.re / 4) := by
    rw [← thetaLogKernel_neg hstrip,z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2⊢ ‖thetaLogKernel (-z)‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4) thetaLogKernel,z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2⊢ ‖2 * cexp (- -z / 4) * psi (cexp (- -z)) - cexp (-z / 4)‖ ≤
  2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4) neg_negz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2⊢ ‖2 * cexp (z / 4) * psi (cexp z) - cexp (-z / 4)‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)]z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2⊢ ‖2 * cexp (z / 4) * psi (cexp z) - cexp (-z / 4)‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)
    apply (norm_sub_le _ _).transz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2⊢ ‖2 * cexp (z / 4) * psi (cexp z)‖ + ‖cexp (-z / 4)‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)
    simp [norm_exp]z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2hbase:‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-z.re / 4)
  have hprod : Real.exp (z.re / 4) * Real.exp (-z.re) = Real.exp (-3 * z.re / 4) := by
    rw [← Real.exp_addz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2hbase:‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)⊢ Real.exp (z.re / 4 + -z.re) = Real.exp (-3 * z.re / 4)]z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2hbase:‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)⊢ Real.exp (z.re / 4 + -z.re) = Real.exp (-3 * z.re / 4)
    congr 1z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2hbase:‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)⊢ z.re / 4 + -z.re = -3 * z.re / 4
    ringz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2hbase:‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)hprod:Real.exp (z.re / 4) * Real.exp (-z.re) = Real.exp (-3 * z.re / 4)⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-z.re / 4)
  have he : Real.exp (-3 * z.re / 4) ≤ Real.exp (-z.re / 4) := by
    apply Real.exp_le_exp.mprz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2hbase:‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)hprod:Real.exp (z.re / 4) * Real.exp (-z.re) = Real.exp (-3 * z.re / 4)⊢ -3 * z.re / 4 ≤ -z.re / 4
    linarithz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2hbase:‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)hprod:Real.exp (z.re / 4) * Real.exp (-z.re) = Real.exp (-3 * z.re / 4)he:Real.exp (-3 * z.re / 4) ≤ Real.exp (-z.re / 4)⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-z.re / 4)
  calc
    ‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) *
        ((1 / (Real.pi * c * D)) * Real.exp (-z.re)) + Real.exp (-z.re / 4) := byz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2hbase:‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)hprod:Real.exp (z.re / 4) * Real.exp (-z.re) = Real.exp (-3 * z.re / 4)he:Real.exp (-3 * z.re / 4) ≤ Real.exp (-z.re / 4)⊢ ‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * (1 / (Real.pi * c * D) * Real.exp (-z.re)) + Real.exp (-z.re / 4)
      have h := mul_le_mul_of_nonneg_left hpsi
        (show 0 ≤ 2 * Real.exp (z.re / 4) by positivityAll goals completed! 🐙)z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2hbase:‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)hprod:Real.exp (z.re / 4) * Real.exp (-z.re) = Real.exp (-3 * z.re / 4)he:Real.exp (-3 * z.re / 4) ≤ Real.exp (-z.re / 4)h:2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ ≤ 2 * Real.exp (z.re / 4) * (1 / (Real.pi * c * D) * Real.exp (-z.re))⊢ ‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * (1 / (Real.pi * c * D) * Real.exp (-z.re)) + Real.exp (-z.re / 4)
      linarithAll goals completed! 🐙
    _ = (2 / (Real.pi * c * D)) * Real.exp (-3 * z.re / 4) + Real.exp (-z.re / 4) := byz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2hbase:‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)hprod:Real.exp (z.re / 4) * Real.exp (-z.re) = Real.exp (-3 * z.re / 4)he:Real.exp (-3 * z.re / 4) ≤ Real.exp (-z.re / 4)⊢ 2 * Real.exp (z.re / 4) * (1 / (Real.pi * c * D) * Real.exp (-z.re)) + Real.exp (-z.re / 4) =
  2 / (Real.pi * c * D) * Real.exp (-3 * z.re / 4) + Real.exp (-z.re / 4)
      rw [show 2 * Real.exp (z.re / 4) * ((1 / (Real.pi * c * D)) * Real.exp (-z.re)) =
        (2 / (Real.pi * c * D)) * (Real.exp (z.re / 4) * Real.exp (-z.re)) byz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2hbase:‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)hprod:Real.exp (z.re / 4) * Real.exp (-z.re) = Real.exp (-3 * z.re / 4)he:Real.exp (-3 * z.re / 4) ≤ Real.exp (-z.re / 4)⊢ 2 * Real.exp (z.re / 4) * (1 / (Real.pi * c * D) * Real.exp (-z.re)) + Real.exp (-z.re / 4) =
  2 / (Real.pi * c * D) * Real.exp (-3 * z.re / 4) + Real.exp (-z.re / 4) ringAll goals completed! 🐙, hprodz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2hbase:‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)hprod:Real.exp (z.re / 4) * Real.exp (-z.re) = Real.exp (-3 * z.re / 4)he:Real.exp (-3 * z.re / 4) ≤ Real.exp (-z.re / 4)⊢ 2 / (Real.pi * c * D) * Real.exp (-3 * z.re / 4) + Real.exp (-z.re / 4) =
  2 / (Real.pi * c * D) * Real.exp (-3 * z.re / 4) + Real.exp (-z.re / 4)]All goals completed! 🐙
    _ ≤ (2 / (Real.pi * c * D)) * Real.exp (-z.re / 4) + Real.exp (-z.re / 4) := byz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2hbase:‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)hprod:Real.exp (z.re / 4) * Real.exp (-z.re) = Real.exp (-3 * z.re / 4)he:Real.exp (-3 * z.re / 4) ≤ Real.exp (-z.re / 4)⊢ 2 / (Real.pi * c * D) * Real.exp (-3 * z.re / 4) + Real.exp (-z.re / 4) ≤
  2 / (Real.pi * c * D) * Real.exp (-z.re / 4) + Real.exp (-z.re / 4) gcongrAll goals completed! 🐙
    _ = thetaStripConstant b * Real.exp (-z.re / 4) := byz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2hbase:‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)hprod:Real.exp (z.re / 4) * Real.exp (-z.re) = Real.exp (-3 * z.re / 4)he:Real.exp (-3 * z.re / 4) ≤ Real.exp (-z.re / 4)⊢ 2 / (Real.pi * c * D) * Real.exp (-z.re / 4) + Real.exp (-z.re / 4) = thetaStripConstant b * Real.exp (-z.re / 4)
      dsimp [thetaStripConstant, c, D]z:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.rehc:0 < Real.cos bhcos:Real.cos b ≤ Real.cos z.imc:ℝ := Real.cos bD:ℝ := 1 - Real.exp (-Real.pi * c)hc0:0 < chD:0 < Dhex:1 ≤ Real.exp z.rehre:c ≤ (cexp z).rehpsi:‖psi (cexp z)‖ ≤ 1 / (Real.pi * c * D) * Real.exp (-z.re)hstrip:|z.im| < Real.pi / 2hbase:‖thetaLogKernel z‖ ≤ 2 * Real.exp (z.re / 4) * ‖psi (cexp z)‖ + Real.exp (-z.re / 4)hprod:Real.exp (z.re / 4) * Real.exp (-z.re) = Real.exp (-3 * z.re / 4)he:Real.exp (-3 * z.re / 4) ≤ Real.exp (-z.re / 4)⊢ 2 / (Real.pi * Real.cos b * (1 - Real.exp (-Real.pi * Real.cos b))) * Real.exp (-z.re / 4) + Real.exp (-z.re / 4) =
  (2 / (Real.pi * Real.cos b * (1 - Real.exp (-Real.pi * Real.cos b))) + 1) * Real.exp (-z.re / 4)
      ringAll goals completed! 🐙

/-- Uniform exponential decay at both ends of every closed interior strip. -/theorem norm_thetaLogKernel_le {z : ℂ} {b : ℝ}
    (hb : b < Real.pi / 2) (hz : |z.im| ≤ b) :
    ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-|z.re| / 4) := byz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ b⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-|z.re| / 4)
  rcases le_total 0 z.re with hx | hxinlz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.re⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-|z.re| / 4)inrz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:z.re ≤ 0⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-|z.re| / 4)
  ·inlz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:0 ≤ z.re⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-|z.re| / 4) simpa only [abs_of_nonneg hx] using norm_thetaLogKernel_le_of_re_nonneg hb hz hxAll goals completed! 🐙
  ·inrz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:z.re ≤ 0⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-|z.re| / 4) have hz' : |(-z).im| ≤ b := by simpa using hzinrz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:z.re ≤ 0hz':|(-z).im| ≤ b⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-|z.re| / 4)
    have hx' : 0 ≤ (-z).re := by simpa using neg_nonneg.mpr hxinrz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:z.re ≤ 0hz':|(-z).im| ≤ bhx':0 ≤ (-z).re⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-|z.re| / 4)
    have h := norm_thetaLogKernel_le_of_re_nonneg hb hz' hx'inrz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:z.re ≤ 0hz':|(-z).im| ≤ bhx':0 ≤ (-z).reh:‖thetaLogKernel (-z)‖ ≤ thetaStripConstant b * Real.exp (-(-z).re / 4)⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-|z.re| / 4)
    rw [thetaLogKernel_neg (hz.trans_lt hb)inrz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:z.re ≤ 0hz':|(-z).im| ≤ bhx':0 ≤ (-z).reh:‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-(-z).re / 4)⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-|z.re| / 4)] at hinrz:ℂb:ℝhb:b < Real.pi / 2hz:|z.im| ≤ bhx:z.re ≤ 0hz':|(-z).im| ≤ bhx':0 ≤ (-z).reh:‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-(-z).re / 4)⊢ ‖thetaLogKernel z‖ ≤ thetaStripConstant b * Real.exp (-|z.re| / 4)
    simpa only [neg_re, neg_neg, abs_of_nonpos hx] using hAll goals completed! 🐙

/-- Absolute integrability on every horizontal line strictly inside the strip. -/theorem integrable_thetaLogKernel_horizontal {b : ℝ} (hb : |b| < Real.pi / 2) :
    Integrable (fun u : ℝ ↦ thetaLogKernel ((u : ℂ) + b * I)) := byb:ℝhb:|b| < Real.pi / 2⊢ Integrable (fun u => thetaLogKernel (↑u + ↑b * I)) volume
  have hbound : Integrable (fun u : ℝ ↦ thetaStripConstant |b| * Real.exp (-|u| / 4)) := by
    have h := (integrable_exp_neg_abs (byb:ℝhb:|b| < Real.pi / 2⊢ 0 < 1 / 4 norm_numAll goals completed! 🐙 : (0 : ℝ) < 1 / 4)).normb:ℝhb:|b| < Real.pi / 2h:Integrable (fun a => ‖↑(Real.exp (-(1 / 4) * |a|))‖) volume⊢ Integrable (fun u => thetaStripConstant |b| * Real.exp (-|u| / 4)) volume
    simp only [norm_real, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] at hb:ℝhb:|b| < Real.pi / 2h:Integrable (fun a => Real.exp (-(1 / 4) * |a|)) volume⊢ Integrable (fun u => thetaStripConstant |b| * Real.exp (-|u| / 4)) volume
    simpa only [show ∀ u : ℝ, -(1 / 4) * |u| = -|u| / 4 from fun u ↦ byb:ℝhb:|b| < Real.pi / 2h:Integrable (fun a => Real.exp (-(1 / 4) * |a|)) volumeu:ℝ⊢ -(1 / 4) * |u| = -|u| / 4 ringAll goals completed! 🐙] using
      h.const_mul (thetaStripConstant |b|)b:ℝhb:|b| < Real.pi / 2hbound:Integrable (fun u => thetaStripConstant |b| * Real.exp (-|u| / 4)) volume⊢ Integrable (fun u => thetaLogKernel (↑u + ↑b * I)) volume
  apply hbound.mono'hfb:ℝhb:|b| < Real.pi / 2hbound:Integrable (fun u => thetaStripConstant |b| * Real.exp (-|u| / 4)) volume⊢ AEStronglyMeasurable (fun u => thetaLogKernel (↑u + ↑b * I)) volumehb:ℝhb:|b| < Real.pi / 2hbound:Integrable (fun u => thetaStripConstant |b| * Real.exp (-|u| / 4)) volume⊢ ∀ᵐ (a : ℝ), ‖thetaLogKernel (↑a + ↑b * I)‖ ≤ thetaStripConstant |b| * Real.exp (-|a| / 4)
  ·hfb:ℝhb:|b| < Real.pi / 2hbound:Integrable (fun u => thetaStripConstant |b| * Real.exp (-|u| / 4)) volume⊢ AEStronglyMeasurable (fun u => thetaLogKernel (↑u + ↑b * I)) volume apply Continuous.aestronglyMeasurablehfb:ℝhb:|b| < Real.pi / 2hbound:Integrable (fun u => thetaStripConstant |b| * Real.exp (-|u| / 4)) volume⊢ Continuous fun u => thetaLogKernel (↑u + ↑b * I)
    apply continuous_iff_continuousAt.mprhfb:ℝhb:|b| < Real.pi / 2hbound:Integrable (fun u => thetaStripConstant |b| * Real.exp (-|u| / 4)) volume⊢ ∀ (x : ℝ), ContinuousAt (fun u => thetaLogKernel (↑u + ↑b * I)) x
    intro uhfb:ℝhb:|b| < Real.pi / 2hbound:Integrable (fun u => thetaStripConstant |b| * Real.exp (-|u| / 4)) volumeu:ℝ⊢ ContinuousAt (fun u => thetaLogKernel (↑u + ↑b * I)) u
    apply (differentiableAt_thetaLogKernel (byb:ℝhb:|b| < Real.pi / 2hbound:Integrable (fun u => thetaStripConstant |b| * Real.exp (-|u| / 4)) volumeu:ℝ⊢ |(↑u + ↑b * I).im| < Real.pi / 2 simpa using hbAll goals completed! 🐙)).continuousAt.comp
    fun_propAll goals completed! 🐙
  ·hb:ℝhb:|b| < Real.pi / 2hbound:Integrable (fun u => thetaStripConstant |b| * Real.exp (-|u| / 4)) volume⊢ ∀ᵐ (a : ℝ), ‖thetaLogKernel (↑a + ↑b * I)‖ ≤ thetaStripConstant |b| * Real.exp (-|a| / 4) filter_upwards with uhb:ℝhb:|b| < Real.pi / 2hbound:Integrable (fun u => thetaStripConstant |b| * Real.exp (-|u| / 4)) volumeu:ℝ⊢ ‖thetaLogKernel (↑u + ↑b * I)‖ ≤ thetaStripConstant |b| * Real.exp (-|u| / 4)
    simpa using norm_thetaLogKernel_le (z := (u : ℂ) + b * I) hb (byb:ℝhb:|b| < Real.pi / 2hbound:Integrable (fun u => thetaStripConstant |b| * Real.exp (-|u| / 4)) volumeu:ℝ⊢ |(↑u + ↑b * I).im| ≤ |b| simpAll goals completed! 🐙)