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

State before:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
⊢ (fun x_1 =>
      match x_1 with
      | (σ, y) => f x (↑σ + ↑y * I)) =Θ[𝓟 (Ι σ' σ'') ×ˢ (atBot ⊔ atTop)]
    fun x =>
    match x with
    | (σ, y) => 1 / y ^ 2
Tactic:
refine (𝓟 (uIoc σ' σ'')).eq_or_neBot.casesOn (fun hbot ↦ by simp [hbot]) (fun _ ↦ ?_)
State after:
x✝¹ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
x✝ : (𝓟 (Ι σ' σ'')).NeBot
⊢ (fun x_1 =>
      match x_1 with
      | (σ, y) => f x (↑σ + ↑y * I)) =Θ[𝓟 (Ι σ' σ'') ×ˢ (atBot ⊔ atTop)]
    fun x =>
    match x with
    | (σ, y) => 1 / y ^ 2

State before:
x✝¹ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
x✝ : (𝓟 (Ι σ' σ'')).NeBot
⊢ (fun x_1 =>
      match x_1 with
      | (σ, y) => f x (↑σ + ↑y * I)) =Θ[𝓟 (Ι σ' σ'') ×ˢ (atBot ⊔ atTop)]
    fun x =>
    match x with
    | (σ, y) => 1 / y ^ 2
Tactic:
haveI : NeBot (atBot (α := ℝ) ⊔ atTop) := sup_neBot.mpr (Or.inl atBot_neBot)
State after:
x✝¹ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
x✝ : (𝓟 (Ι σ' σ'')).NeBot
this : (atBot ⊔ atTop).NeBot
⊢ (fun x_1 =>
      match x_1 with
      | (σ, y) => f x (↑σ + ↑y * I)) =Θ[𝓟 (Ι σ' σ'') ×ˢ (atBot ⊔ atTop)]
    fun x =>
    match x with
    | (σ, y) => 1 / y ^ 2

State before:
x✝¹ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
x✝ : (𝓟 (Ι σ' σ'')).NeBot
this : (atBot ⊔ atTop).NeBot
⊢ (fun x_1 =>
      match x_1 with
      | (σ, y) => f x (↑σ + ↑y * I)) =Θ[𝓟 (Ι σ' σ'') ×ˢ (atBot ⊔ atTop)]
    fun x =>
    match x with
    | (σ, y) => 1 / y ^ 2
Tactic:
exact (isTheta_uniformlyOn_uIcc xpos σ' σ'').mono (by simpa using Ioc_subset_Icc_self)
State after:
no goals

State before:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
hbot : 𝓟 (Ι σ' σ'') = ⊥
⊢ (fun x_1 =>
      match x_1 with
      | (σ, y) => f x (↑σ + ↑y * I)) =Θ[𝓟 (Ι σ' σ'') ×ˢ (atBot ⊔ atTop)]
    fun x =>
    match x with
    | (σ, y) => 1 / y ^ 2
Tactic:
simp [hbot]
State after:
no goals

State before:
x✝¹ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
x✝ : (𝓟 (Ι σ' σ'')).NeBot
this : (atBot ⊔ atTop).NeBot
⊢ 𝓟 (Ι σ' σ'') ×ˢ (atBot ⊔ atTop) ≤ 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
Tactic:
simpa using Ioc_subset_Icc_self
State after:
no goals