internlm/Lean-Github huggingface dataset:
Theorem: Perron.vertIntBoundLeft
Proof state before:
case pos.h.h.h₂.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 4⁻¹ + t ^ 2 ≤ normSq (↑σ + ↑t * I + 1)
Tactic:
rw [(by push_cast; ring : σ + t * I + 1 = ofReal' (σ + 1) + t * I),
  normSq_add_mul_I, add_le_add_iff_right]
Proof state after:
case pos.h.h.h₂.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 4⁻¹ ≤ (σ + 1) ^ 2
Theorem: Perron.vertIntBoundLeft
Proof state before:
case pos.h.h.h₂.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 4⁻¹ ≤ (σ + 1) ^ 2
Tactic:
ring_nf
Proof state after:
case pos.h.h.h₂.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 1 / 4 ≤ 1 + σ * 2 + σ ^ 2
Theorem: Perron.vertIntBoundLeft
Proof state before:
case pos.h.h.h₂.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ 1 / 4 ≤ 1 + σ * 2 + σ ^ 2
Tactic:
nlinarith
Proof state after:
no goals
Theorem: Perron.vertIntBoundLeft
Proof state before:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ ↑σ + ↑t * I + 1 = ↑(σ + 1) + ↑t * I
Tactic:
push_cast
Proof state after:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ ↑σ + ↑t * I + 1 = ↑σ + 1 + ↑t * I
Theorem: Perron.vertIntBoundLeft
Proof state before:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
hint : Integrable (fun a => 1 / (‖↑σ + ↑a * I‖ * ‖↑σ + ↑a * I + 1‖)) volume
t : ℝ
⊢ ↑σ + ↑t * I + 1 = ↑σ + 1 + ↑t * I
Tactic:
ring
Proof state after:
no goals
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h.calc_5
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ x ^ σ * ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2)) ≤
    ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ
Tactic:
rw [mul_comm]
Proof state after:
case h.calc_5
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ (∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) * x ^ σ ≤
    ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h.calc_5
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ (∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) * x ^ σ ≤
    ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖ * x ^ σ
Tactic:
gcongr
Proof state after:
case h.calc_5.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2)) ≤ ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h.calc_5.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2)) ≤ ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖
Tactic:
have : 0 ≤ ∫ (t : ℝ), 1 / (sqrt (4⁻¹ + t ^ 2) * sqrt (4⁻¹ + t ^ 2)) := by positivity
Proof state after:
case h.calc_5.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2)) ≤ ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h.calc_5.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2)) ≤ ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖
Tactic:
rw [← _root_.abs_of_nonneg this, ← Complex.abs_ofReal]
Proof state after:
case h.calc_5.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ Complex.abs ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) ≤ ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h.calc_5.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ Complex.abs ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) ≤ ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖
Tactic:
apply le_of_eq
Proof state after:
case h.calc_5.h.a
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ Complex.abs ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) = ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h.calc_5.h.a
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ Complex.abs ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) = ‖∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))‖
Tactic:
congr
Proof state after:
case h.calc_5.h.a.h.e_6.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) = ∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h.calc_5.h.a.h.e_6.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) = ∫ (t : ℝ), 1 / (↑√(4⁻¹ + t ^ 2) * ↑√(4⁻¹ + t ^ 2))
Tactic:
norm_cast
Proof state after:
case h.calc_5.h.a.h.e_6.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) = ∫ (t : ℝ), ↑(1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2)))
Theorem: Perron.vertIntBoundLeft
Proof state before:
case h.calc_5.h.a.h.e_6.h
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
this : 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
⊢ ↑(∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))) = ∫ (t : ℝ), ↑(1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2)))
Tactic:
exact integral_ofReal.symm
Proof state after:
no goals
Theorem: Perron.vertIntBoundLeft
Proof state before:
x σ✝ σ' σ'' T : ℝ
xpos : 0 < x
σ : ℝ
hσ : σ < -3 / 2
⊢ 0 ≤ ∫ (t : ℝ), 1 / (√(4⁻¹ + t ^ 2) * √(4⁻¹ + t ^ 2))
Tactic:
positivity
Proof state after:
no goals
Theorem: Perron.map_conj
Proof state before:
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ f x ((starRingEnd ℂ) s) = (starRingEnd ℂ) (f x s)
Tactic:
simp only [f, map_div₀, map_mul, map_add, map_one]
Proof state after:
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ ↑x ^ (starRingEnd ℂ) s / ((starRingEnd ℂ) s * ((starRingEnd ℂ) s + 1)) =
    (starRingEnd ℂ) (↑x ^ s) / ((starRingEnd ℂ) s * ((starRingEnd ℂ) s + 1))
Theorem: Perron.map_conj
Proof state before:
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ ↑x ^ (starRingEnd ℂ) s / ((starRingEnd ℂ) s * ((starRingEnd ℂ) s + 1)) =
    (starRingEnd ℂ) (↑x ^ s) / ((starRingEnd ℂ) s * ((starRingEnd ℂ) s + 1))
Tactic:
congr
Proof state after:
case e_a
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ ↑x ^ (starRingEnd ℂ) s = (starRingEnd ℂ) (↑x ^ s)
Theorem: Perron.map_conj
Proof state before:
case e_a
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ ↑x ^ (starRingEnd ℂ) s = (starRingEnd ℂ) (↑x ^ s)
Tactic:
rw [cpow_conj, Complex.conj_ofReal]
Proof state after:
case e_a.hx
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ (↑x).arg ≠ π
Theorem: Perron.map_conj
Proof state before:
case e_a.hx
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ (↑x).arg ≠ π
Tactic:
rw [Complex.arg_ofReal_of_nonneg hx]
Proof state after:
case e_a.hx
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ 0 ≠ π
Theorem: Perron.map_conj
Proof state before:
case e_a.hx
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ 0 ≠ π
Tactic:
exact pi_ne_zero.symm
Proof state after:
no goals
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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
Proof 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)
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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 ?_) ?_
Proof 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
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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
Proof 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
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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) _) _
Proof state after:
no goals
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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
Proof state after:
no goals
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof state before:
x✝ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
l : Filter (ℝ × ℝ) := 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
hl : l = 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
⊢ ‖1‖ ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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 _⟩
Proof 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
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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)
Proof 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
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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
Proof 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
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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]
Proof 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
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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)
Proof state after:
no goals
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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]
Proof 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
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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 _⟩
Proof state after:
no goals
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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
Proof state after:
no goals
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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
Proof 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
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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
Proof state after:
no goals
Theorem: Perron.isTheta_uniformlyOn_uIcc
Proof 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
Proof state after:
no goals
Theorem: Perron.isTheta_uniformlyOn_uIoc
Proof 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 _ ↦ ?_)
Proof 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
Theorem: Perron.isTheta_uniformlyOn_uIoc
Proof 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)
Proof 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
Theorem: Perron.isTheta_uniformlyOn_uIoc
Proof 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)
Proof state after:
no goals
Theorem: Perron.isTheta_uniformlyOn_uIoc
Proof 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]
Proof state after:
no goals
Theorem: Perron.isTheta_uniformlyOn_uIoc
Proof 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
Proof state after:
no goals
Theorem: Perron.isIntegrable
Proof state before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
⊢ Integrable (fun t => f x (↑σ + ↑t * I)) volume
Tactic:
have : Continuous (fun (y : ℝ) ↦ f x (σ + y * I)) := by
  refine (isHolomorphicOn xpos).continuousOn.comp_continuous (by continuity) fun x ↦ not_or.mpr ?_
  simp [Complex.ext_iff, σ_ne_zero, σ_ne_neg_one]
Proof state after:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
⊢ Integrable (fun t => f x (↑σ + ↑t * I)) volume
Theorem: Perron.isIntegrable
Proof state before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
⊢ Integrable (fun t => f x (↑σ + ↑t * I)) volume
Tactic:
refine this.locallyIntegrable.integrable_of_isBigO_atTop_of_norm_eq_norm_neg
  (univ_mem' fun y ↦ ?_) (isTheta xpos).2.isBigO ⟨Ioi 1, Ioi_mem_atTop 1, ?_⟩
Proof state after:
case refine_1
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
y : ℝ
⊢ y ∈
    {x_1 |
      (fun x_2 =>
          (Norm.norm ∘ fun y => f x (↑σ + ↑y * I)) x_2 = (Norm.norm ∘ (fun y => f x (↑σ + ↑y * I)) ∘ Neg.neg) x_2)
        x_1}

case refine_2
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
⊢ IntegrableOn (fun y => 1 / y ^ 2) (Ioi 1) volume
Theorem: Perron.isIntegrable
Proof state before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
⊢ Continuous fun y => f x (↑σ + ↑y * I)
Tactic:
refine (isHolomorphicOn xpos).continuousOn.comp_continuous (by continuity) fun x ↦ not_or.mpr ?_
Proof state after:
x✝ σ σ' σ'' T : ℝ
xpos : 0 < x✝
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
x : ℝ
⊢ ¬↑σ + ↑x * I = 0 ∧ ↑σ + ↑x * I ∉ {-1}
Theorem: Perron.isIntegrable
Proof state before:
x✝ σ σ' σ'' T : ℝ
xpos : 0 < x✝
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
x : ℝ
⊢ ¬↑σ + ↑x * I = 0 ∧ ↑σ + ↑x * I ∉ {-1}
Tactic:
simp [Complex.ext_iff, σ_ne_zero, σ_ne_neg_one]
Proof state after:
no goals
Theorem: Perron.isIntegrable
Proof state before:
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
⊢ Continuous fun y => ↑σ + ↑y * I
Tactic:
continuity
Proof state after:
no goals
Theorem: Perron.isIntegrable
Proof state before:
case refine_1
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
y : ℝ
⊢ y ∈
    {x_1 |
      (fun x_2 =>
          (Norm.norm ∘ fun y => f x (↑σ + ↑y * I)) x_2 = (Norm.norm ∘ (fun y => f x (↑σ + ↑y * I)) ∘ Neg.neg) x_2)
        x_1}
Tactic:
show ‖f x (↑σ + ↑y * I)‖ = ‖f x (↑σ + ↑(-y) * I)‖
Proof state after:
case refine_1
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
y : ℝ
⊢ ‖f x (↑σ + ↑y * I)‖ = ‖f x (↑σ + ↑(-y) * I)‖