let g := fun ((σ, y) : ℝ × ℝ) ↦ f x (σ + y * I)
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
⊢ (fun y => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑y * I) ∂μ) =O[atBot ⊔ atTop] fun y => 1 / y ^ 2
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
g : ℝ × ℝ → ℂ :=
  fun x_1 =>
    match x_1 with
    | (σ, y) => f x (↑σ + ↑y * I)
⊢ (fun y => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑y * I) ∂μ) =O[atBot ⊔ atTop] fun y => 1 / y ^ 2