Theorem: Perron.horizontal_integral_isBigO (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
⊢ (fun y => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑y * I) ∂μ) =O[atBot ⊔ atTop] fun y => 1 / y ^ 2
Tactic:
let g := fun ((σ, y) : ℝ × ℝ) ↦ f x (σ + y * I)
State after:
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

State before:
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
Tactic:
calc
  _ =Θ[atBot ⊔ atTop] fun (y : ℝ) ↦ ∫ (σ : ℝ) in uIoc σ' σ'', g (σ, y) ∂μ :=
      isTheta_of_norm_eventuallyEq <| univ_mem'
        fun _ ↦ intervalIntegral.norm_intervalIntegral_eq _ _ _ _
  _ =O[atBot ⊔ atTop] _ :=
    (isTheta_uniformlyOn_uIoc xpos σ' σ'').isBigO.set_integral_isBigO
      measurableSet_uIoc measure_Ioc_lt_top
State after:
no goals