Source indexedtheorem · leanprover/lean4:v4.32.0

Perron.horizontal_integral_isBigO

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:664 to 676

Mathematical statement

Exact Lean statement

theorem horizontal_integral_isBigO {x : ℝ} (xpos : 0 < x) (σ' σ'' : ℝ) (μ : Measure ℝ)
    [IsLocallyFiniteMeasure μ] :
    (fun (y : ℝ) ↦ ∫ (σ : ℝ) in σ'..σ'', f x (σ + y * I) ∂μ) =O[atBot ⊔ atTop]
      fun y ↦ 1 / y^2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem horizontal_integral_isBigO {x : ℝ} (xpos : 0 < x) (σ' σ'' : ℝ) (μ : Measure ℝ)    [IsLocallyFiniteMeasure μ] :    (fun (y : ℝ) ↦ ∫ (σ : ℝ) in σ'..σ'', f x (σ + y * I) ∂μ) =O[atBot ⊔ atTop]      fun y ↦ 1 / y^2 := by  let g := fun ((σ, y) : ℝ × ℝ) ↦ f x (σ + y * I)  calc    _ =Θ[atBot ⊔ atTop] fun (y : ℝ) ↦ ∫ (σ : ℝ) in uIoc σ' σ'', g (σ, y) ∂μ :=        IsTheta.of_norm_eventuallyEq_norm <| univ_mem'          fun _ ↦ intervalIntegral.norm_intervalIntegral_eq _ _ _ _    _ =O[atBot ⊔ atTop] fun y ↦ 1 / y^2 :=      (isTheta_uniformlyOn_uIoc xpos σ' σ'').isBigO.set_integral_isBigO        (g := fun x => 1 / (x ^ 2))        measure_Ioc_lt_top