-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
/-- The odd kernel is continuous on `Ioi 0`. -/
lemma continuousOn_oddKernel (a : UnitAddCircle) : ContinuousOn (oddKernel a) (Ioi 0)

Proof state:
case H.refine_2.hg
a x : ℝ
hx : x ∈ Ioi 0
hf : Continuous fun u => (↑a * I * ↑u, I * ↑u)
⊢ ContinuousAt (fun x => ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)) x

Tactic:
exact continuousAt_const.mul <| (continuousAt_jacobiTheta₂ (a * I * x)
  (by rwa [I_mul_im, ofReal_re])).comp (f := fun u : ℝ ↦ (a * I * u, I * u)) hf.continuousAt

Result:
no goals

Proof state:
case H
a : ℝ
⊢ ContinuousOn (fun x => ↑(oddKernel (↑a) x)) (Ioi 0)

Tactic:
simp_rw [oddKernel_def' a]

Result:
case H
a : ℝ
⊢ ContinuousOn
    (fun x =>
      cexp (-↑π * ↑a ^ 2 * ↑x) *
        (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)))
    (Ioi 0)

Proof state:
a x : ℝ
hx : x ∈ Ioi 0
hf : Continuous fun u => (↑a * I * ↑u, I * ↑u)
⊢ 0 < (I * ↑x).im

Tactic:
rwa [I_mul_im, ofReal_re]

Result:
no goals

Proof state:
a x : ℝ
hx : x ∈ Ioi 0
⊢ Continuous fun u => (↑a * I * ↑u, I * ↑u)

Tactic:
fun_prop

Result:
no goals

Proof state:
case H
a : ℝ
⊢ ContinuousOn (oddKernel ↑a) (Ioi 0)

Tactic:
suffices ContinuousOn (fun x ↦ (oddKernel a x : ℂ)) (Ioi 0) from
  (continuous_re.comp_continuousOn this).congr fun a _ ↦ (ofReal_re _).symm

Result:
case H
a : ℝ
⊢ ContinuousOn (fun x => ↑(oddKernel (↑a) x)) (Ioi 0)

Proof state:
case H
a : ℝ
⊢ ContinuousOn
    (fun x =>
      cexp (-↑π * ↑a ^ 2 * ↑x) *
        (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)))
    (Ioi 0)

Tactic:
refine fun x hx ↦ ((Continuous.continuousAt ?_).mul ?_).continuousWithinAt

Result:
case H.refine_1
a x : ℝ
hx : x ∈ Ioi 0
⊢ Continuous fun x => cexp (-↑π * ↑a ^ 2 * ↑x)

case H.refine_2
a x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x => jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
    x

Proof state:
case H.refine_2.hf
a x : ℝ
hx : x ∈ Ioi 0
hf : Continuous fun u => (↑a * I * ↑u, I * ↑u)
⊢ ContinuousAt (fun x => jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I)) x

Tactic:
exact ((continuousAt_jacobiTheta₂' (a * I * x) (by rwa [I_mul_im, ofReal_re])).comp
  (f := fun u : ℝ ↦ (a * I * u, I * u)) hf.continuousAt).div_const _

Result:
no goals

Proof state:
case H.refine_2
a x : ℝ
hx : x ∈ Ioi 0
hf : Continuous fun u => (↑a * I * ↑u, I * ↑u)
⊢ ContinuousAt (fun x => jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
    x

Tactic:
apply ContinuousAt.add

Result:
case H.refine_2.hf
a x : ℝ
hx : x ∈ Ioi 0
hf : Continuous fun u => (↑a * I * ↑u, I * ↑u)
⊢ ContinuousAt (fun x => jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I)) x

case H.refine_2.hg
a x : ℝ
hx : x ∈ Ioi 0
hf : Continuous fun u => (↑a * I * ↑u, I * ↑u)
⊢ ContinuousAt (fun x => ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)) x

Proof state:
case H.refine_1
a x : ℝ
hx : x ∈ Ioi 0
⊢ Continuous fun x => cexp (-↑π * ↑a ^ 2 * ↑x)

Tactic:
fun_prop

Result:
no goals

Proof state:
case H.refine_2
a x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x => jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
    x

Tactic:
have hf : Continuous fun u : ℝ ↦ (a * I * u, I * u) := by fun_prop

Result:
case H.refine_2
a x : ℝ
hx : x ∈ Ioi 0
hf : Continuous fun u => (↑a * I * ↑u, I * ↑u)
⊢ ContinuousAt (fun x => jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
    x