Theorem: Perron.isTheta_uniformlyOn_uIcc (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 y => 1 / y ^ 2) ∘ Prod.snd)
Tactic:
set l := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop : Filter ℝ) with hl
State after:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
⊢ (fun x_1 =>
      match x_1 with
      | (σ, y) => f x (↑σ + ↑y * I)) =Θ[l]
    ((fun y => 1 / y ^ 2) ∘ Prod.snd)

State before:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
⊢ (fun x_1 =>
      match x_1 with
      | (σ, y) => f x (↑σ + ↑y * I)) =Θ[l]
    ((fun y => 1 / y ^ 2) ∘ Prod.snd)
Tactic:
refine IsTheta.div (isTheta_norm_left.mp ?_) ?_
State after:
case refine_1
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
⊢ (fun x_1 => ‖↑x ^ (↑x_1.1 + ↑x_1.2 * I)‖) =Θ[l] fun x => 1

case refine_2
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
⊢ (fun x => (↑x.1 + ↑x.2 * I) * (↑x.1 + ↑x.2 * I + 1)) =Θ[l] fun x => x.2 ^ 2

State before:
case refine_1
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
⊢ (fun x_1 => ‖↑x ^ (↑x_1.1 + ↑x_1.2 * I)‖) =Θ[l] fun x => 1
Tactic:
suffices (fun (σ, _y) ↦ |x| ^ σ) =Θ[l] fun _ ↦ (1 : ℝ) by
  simpa [Complex.abs_cpow_of_ne_zero <| ofReal_ne_zero.mpr (ne_of_gt xpos),
    arg_ofReal_of_nonneg xpos.le] using this
State after:
case refine_1
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
⊢ (fun x_1 =>
      match x_1 with
      | (σ, _y) => |x| ^ σ) =Θ[l]
    fun x => 1

State before:
case refine_1
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
⊢ (fun x_1 =>
      match x_1 with
      | (σ, _y) => |x| ^ σ) =Θ[l]
    fun x => 1
Tactic:
exact (continuousOn_const.rpow continuousOn_id fun _ _ ↦ Or.inl <| ne_of_gt (abs_pos_of_pos xpos))
  |>.const_isThetaUniformlyOn_isCompact isCompact_uIcc (by norm_num)
  (fun i _ ↦ ne_of_gt <| rpow_pos_of_pos (abs_pos_of_pos xpos) _) _
State after:
no goals

State before:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
this :
  (fun x_1 =>
      match x_1 with
      | (σ, _y) => |x| ^ σ) =Θ[l]
    fun x => 1
⊢ (fun x_1 => ‖↑x ^ (↑x_1.1 + ↑x_1.2 * I)‖) =Θ[l] fun x => 1
Tactic:
simpa [Complex.abs_cpow_of_ne_zero <| ofReal_ne_zero.mpr (ne_of_gt xpos),
  arg_ofReal_of_nonneg xpos.le] using this
State after:
no goals

State before:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
⊢ ‖1‖ ≠ 0
Tactic:
norm_num
State after:
no goals

State before:
case refine_2
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
⊢ (fun x => (↑x.1 + ↑x.2 * I) * (↑x.1 + ↑x.2 * I + 1)) =Θ[l] fun x => x.2 ^ 2
Tactic:
have h_c {c : ℂ} : (fun (_ : ℝ × ℝ) ↦ c) =o[l] Prod.snd := by
  rewrite [hl, Filter.prod_sup, isLittleO_sup]
  exact ⟨isLittleO_const_snd_atBot c _, isLittleO_const_snd_atTop c _⟩
State after:
case refine_2
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
h_c : ∀ {c : ℂ}, (fun x => c) =o[l] Prod.snd
⊢ (fun x => (↑x.1 + ↑x.2 * I) * (↑x.1 + ↑x.2 * I + 1)) =Θ[l] fun x => x.2 ^ 2

State before:
case refine_2
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
h_c : ∀ {c : ℂ}, (fun x => c) =o[l] Prod.snd
⊢ (fun x => (↑x.1 + ↑x.2 * I) * (↑x.1 + ↑x.2 * I + 1)) =Θ[l] fun x => x.2 ^ 2
Tactic:
have h_yI : (fun ((_σ, y) : ℝ × ℝ) ↦ y * I) =Θ[l] Prod.snd :=
  isTheta_of_norm_eventuallyEq (by simp)
State after:
case refine_2
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
h_c : ∀ {c : ℂ}, (fun x => c) =o[l] Prod.snd
h_yI :
  (fun x =>
      match x with
      | (_σ, y) => ↑y * I) =Θ[l]
    Prod.snd
⊢ (fun x => (↑x.1 + ↑x.2 * I) * (↑x.1 + ↑x.2 * I + 1)) =Θ[l] fun x => x.2 ^ 2

State before:
case refine_2
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
h_c : ∀ {c : ℂ}, (fun x => c) =o[l] Prod.snd
h_yI :
  (fun x =>
      match x with
      | (_σ, y) => ↑y * I) =Θ[l]
    Prod.snd
⊢ (fun x => (↑x.1 + ↑x.2 * I) * (↑x.1 + ↑x.2 * I + 1)) =Θ[l] fun x => x.2 ^ 2
Tactic:
have h_σ_yI : (fun (σy : ℝ × ℝ) ↦ σy.1 + σy.2 * I) =Θ[l] Prod.snd := by
  refine IsLittleO.add_isTheta ?_ h_yI
  exact continuous_ofReal.continuousOn.const_isBigOUniformlyOn_isCompact isCompact_uIcc
    (by norm_num : ‖(1 : ℂ)‖ ≠ 0) _ |>.trans_isLittleO h_c
State after:
case refine_2
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
h_c : ∀ {c : ℂ}, (fun x => c) =o[l] Prod.snd
h_yI :
  (fun x =>
      match x with
      | (_σ, y) => ↑y * I) =Θ[l]
    Prod.snd
h_σ_yI : (fun σy => ↑σy.1 + ↑σy.2 * I) =Θ[l] Prod.snd
⊢ (fun x => (↑x.1 + ↑x.2 * I) * (↑x.1 + ↑x.2 * I + 1)) =Θ[l] fun x => x.2 ^ 2

State before:
case refine_2
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
h_c : ∀ {c : ℂ}, (fun x => c) =o[l] Prod.snd
h_yI :
  (fun x =>
      match x with
      | (_σ, y) => ↑y * I) =Θ[l]
    Prod.snd
h_σ_yI : (fun σy => ↑σy.1 + ↑σy.2 * I) =Θ[l] Prod.snd
⊢ (fun x => (↑x.1 + ↑x.2 * I) * (↑x.1 + ↑x.2 * I + 1)) =Θ[l] fun x => x.2 ^ 2
Tactic:
simp_rw [sq]
State after:
case refine_2
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
h_c : ∀ {c : ℂ}, (fun x => c) =o[l] Prod.snd
h_yI :
  (fun x =>
      match x with
      | (_σ, y) => ↑y * I) =Θ[l]
    Prod.snd
h_σ_yI : (fun σy => ↑σy.1 + ↑σy.2 * I) =Θ[l] Prod.snd
⊢ (fun x => (↑x.1 + ↑x.2 * I) * (↑x.1 + ↑x.2 * I + 1)) =Θ[l] fun x => x.2 * x.2

State before:
case refine_2
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
h_c : ∀ {c : ℂ}, (fun x => c) =o[l] Prod.snd
h_yI :
  (fun x =>
      match x with
      | (_σ, y) => ↑y * I) =Θ[l]
    Prod.snd
h_σ_yI : (fun σy => ↑σy.1 + ↑σy.2 * I) =Θ[l] Prod.snd
⊢ (fun x => (↑x.1 + ↑x.2 * I) * (↑x.1 + ↑x.2 * I + 1)) =Θ[l] fun x => x.2 * x.2
Tactic:
exact h_σ_yI.mul (h_σ_yI.add_isLittleO h_c)
State after:
no goals

State before:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
c : ℂ
⊢ (fun x => c) =o[l] Prod.snd
Tactic:
rewrite [hl, Filter.prod_sup, isLittleO_sup]
State after:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
c : ℂ
⊢ (fun x => c) =o[𝓟 [[σ', σ'']] ×ˢ atBot] Prod.snd ∧ (fun x => c) =o[𝓟 [[σ', σ'']] ×ˢ atTop] Prod.snd

State before:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
c : ℂ
⊢ (fun x => c) =o[𝓟 [[σ', σ'']] ×ˢ atBot] Prod.snd ∧ (fun x => c) =o[𝓟 [[σ', σ'']] ×ˢ atTop] Prod.snd
Tactic:
exact ⟨isLittleO_const_snd_atBot c _, isLittleO_const_snd_atTop c _⟩
State after:
no goals

State before:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
h_c : ∀ {c : ℂ}, (fun x => c) =o[l] Prod.snd
⊢ (fun x =>
      ‖match x with
        | (_σ, y) => ↑y * I‖) =ᶠ[l]
    fun x => ‖x.2‖
Tactic:
simp
State after:
no goals

State before:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
h_c : ∀ {c : ℂ}, (fun x => c) =o[l] Prod.snd
h_yI :
  (fun x =>
      match x with
      | (_σ, y) => ↑y * I) =Θ[l]
    Prod.snd
⊢ (fun σy => ↑σy.1 + ↑σy.2 * I) =Θ[l] Prod.snd
Tactic:
refine IsLittleO.add_isTheta ?_ h_yI
State after:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
h_c : ∀ {c : ℂ}, (fun x => c) =o[l] Prod.snd
h_yI :
  (fun x =>
      match x with
      | (_σ, y) => ↑y * I) =Θ[l]
    Prod.snd
⊢ (fun σy => ↑σy.1) =o[l] Prod.snd

State before:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
h_c : ∀ {c : ℂ}, (fun x => c) =o[l] Prod.snd
h_yI :
  (fun x =>
      match x with
      | (_σ, y) => ↑y * I) =Θ[l]
    Prod.snd
⊢ (fun σy => ↑σy.1) =o[l] Prod.snd
Tactic:
exact continuous_ofReal.continuousOn.const_isBigOUniformlyOn_isCompact isCompact_uIcc
  (by norm_num : ‖(1 : ℂ)‖ ≠ 0) _ |>.trans_isLittleO h_c
State after:
no goals

State before:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
h_c : ∀ {c : ℂ}, (fun x => c) =o[l] Prod.snd
h_yI :
  (fun x =>
      match x with
      | (_σ, y) => ↑y * I) =Θ[l]
    Prod.snd
⊢ ‖1‖ ≠ 0
Tactic:
norm_num
State after:
no goals