internlm/Lean-Github huggingface dataset:
Theorem: Perron.contourPull3
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) σ' = VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) σ''
Tactic:
unfold VerticalIntegral'
Proof state after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ (1 / (2 * ↑π * I)) • VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ' =
    (1 / (2 * ↑π * I)) • VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ''
Theorem: Perron.contourPull3
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ (1 / (2 * ↑π * I)) • VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ' =
    (1 / (2 * ↑π * I)) • VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ''
Tactic:
congr 1
Proof state after:
case e_a
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ' = VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ''
Theorem: Perron.contourPull3
Proof state before:
case e_a
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ' = VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ''
Tactic:
exact contourPull (by linarith) (not_mem_uIcc_of_gt (by linarith) (by linarith))
  (not_mem_uIcc_of_gt (by linarith) (by linarith))
Proof state after:
no goals
Theorem: Perron.contourPull3
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ 0 < x
Tactic:
linarith
Proof state after:
no goals
Theorem: Perron.contourPull3
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ σ' < 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Perron.contourPull3
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ σ'' < 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Perron.contourPull3
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ σ' < -1
Tactic:
linarith
Proof state after:
no goals
Theorem: Perron.contourPull3
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ σ'' < -1
Tactic:
linarith
Proof state after:
no goals
Theorem: Perron.formulaGtOne
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
⊢ VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) σ = 1 - 1 / ↑x
Tactic:
set f : ℂ → ℂ := (fun s ↦ x^s / (s * (s + 1)))
Proof state after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
⊢ VerticalIntegral' f σ = 1 - 1 / ↑x
Theorem: Perron.formulaGtOne
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
⊢ VerticalIntegral' f σ = 1 - 1 / ↑x
Tactic:
rw [residuePull1 x_gt_one σ_pos]
Proof state after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
⊢ 1 + VerticalIntegral' (Perron.f x) (-1 / 2) = 1 - 1 / ↑x
Theorem: Perron.formulaGtOne
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
⊢ 1 + VerticalIntegral' (Perron.f x) (-1 / 2) = 1 - 1 / ↑x
Tactic:
rw [residuePull2 x_gt_one]
Proof state after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
⊢ 1 + (-1 / ↑x + VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2)) = 1 - 1 / ↑x
Theorem: Perron.formulaGtOne
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
⊢ 1 + (-1 / ↑x + VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2)) = 1 - 1 / ↑x
Tactic:
have contourPull₃ (σ' σ'' : ℝ) (hσ' : σ' ≤ -3/2) (hσ'' : σ'' ≤ -3/2) :
    VerticalIntegral' f σ' = VerticalIntegral' f σ'' :=
  contourPull3 x_gt_one hσ' hσ''
Proof state after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
⊢ 1 + (-1 / ↑x + VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2)) = 1 - 1 / ↑x
Theorem: Perron.formulaGtOne
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
⊢ 1 + (-1 / ↑x + VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2)) = 1 - 1 / ↑x
Tactic:
have VertIntBound : ∃ C, ∀ σ' < -3/2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ' :=
  vertIntBoundLeft (by linarith : 0 < x)
Proof state after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
⊢ 1 + (-1 / ↑x + VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2)) = 1 - 1 / ↑x
Theorem: Perron.formulaGtOne
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
⊢ 1 + (-1 / ↑x + VerticalIntegral' (fun s => ↑x ^ s / (s * (s + 1))) (-3 / 2)) = 1 - 1 / ↑x
Tactic:
rw [limitOfConstantLeft (σ := -3/2) (Eq.le rfl) contourPull₃ ?_]
Proof state after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
⊢ 1 + (-1 / ↑x + 0) = 1 - 1 / ↑x

x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
⊢ Tendsto (fun σ' => VerticalIntegral' f σ') atBot (𝓝 0)
Theorem: Perron.formulaGtOne
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
⊢ 1 + (-1 / ↑x + 0) = 1 - 1 / ↑x

x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
⊢ Tendsto (fun σ' => VerticalIntegral' f σ') atBot (𝓝 0)
Tactic:
ring
Proof state after:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
⊢ Tendsto (fun σ' => VerticalIntegral' f σ') atBot (𝓝 0)
Theorem: Perron.formulaGtOne
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
AbsVertIntTendsto : Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
⊢ Tendsto (fun σ' => VerticalIntegral' f σ') atBot (𝓝 0)
Tactic:
exact tendsto_zero_iff_norm_tendsto_zero.mpr AbsVertIntTendsto
Proof state after:
no goals
Theorem: Perron.formulaGtOne
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
⊢ 0 < x
Tactic:
linarith
Proof state after:
no goals
Theorem: Perron.formulaGtOne
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
VertIntBound : ∃ C, ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
Tactic:
obtain ⟨C, hC⟩ := VertIntBound
Proof state after:
case intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
Theorem: Perron.formulaGtOne
Proof state before:
case intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
Tactic:
have := tendsto_rpow_atTop_nhds_zero_of_norm_gt_one x_gt_one C
Proof state after:
case intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
Theorem: Perron.formulaGtOne
Proof state before:
case intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ Tendsto (⇑Complex.abs ∘ VerticalIntegral' f) atBot (𝓝 0)
Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds this
Proof state after:
case intro.hgf
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ᶠ (b : ℝ) in atBot, 0 ≤ (⇑Complex.abs ∘ VerticalIntegral' f) b

case intro.hfh
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ᶠ (b : ℝ) in atBot, (⇑Complex.abs ∘ VerticalIntegral' f) b ≤ x ^ b * C
Theorem: Perron.formulaGtOne
Proof state before:
case intro.hgf
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ᶠ (b : ℝ) in atBot, 0 ≤ (⇑Complex.abs ∘ VerticalIntegral' f) b
Tactic:
filter_upwards using fun _ ↦ Complex.abs.nonneg' _
Proof state after:
no goals
Theorem: Perron.formulaGtOne
Proof state before:
case intro.hfh
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ᶠ (b : ℝ) in atBot, (⇑Complex.abs ∘ VerticalIntegral' f) b ≤ x ^ b * C
Tactic:
filter_upwards [eventually_lt_atBot (-3/2)]
Proof state after:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ a < -3 / 2, (⇑Complex.abs ∘ VerticalIntegral' f) a ≤ x ^ a * C
Theorem: Perron.formulaGtOne
Proof state before:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ a < -3 / 2, (⇑Complex.abs ∘ VerticalIntegral' f) a ≤ x ^ a * C
Tactic:
(conv at hC => intro σ hσ; rw [mul_comm])
Proof state after:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ < -3 / 2, ‖VerticalIntegral' f σ‖ ≤ x ^ σ * C
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ a < -3 / 2, (⇑Complex.abs ∘ VerticalIntegral' f) a ≤ x ^ a * C
Theorem: Perron.formulaGtOne
Proof state before:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ < -3 / 2, ‖VerticalIntegral' f σ‖ ≤ x ^ σ * C
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ a < -3 / 2, (⇑Complex.abs ∘ VerticalIntegral' f) a ≤ x ^ a * C
Tactic:
exact fun _ ↦ hC _
Proof state after:
no goals
Theorem: Perron.formulaGtOne
Proof state before:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ' < -3 / 2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ'
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ a < -3 / 2, (⇑Complex.abs ∘ VerticalIntegral' f) a ≤ x ^ a * C
Tactic:
conv at hC => intro σ hσ; rw [mul_comm]
Proof state after:
case h
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ_pos : 0 < σ
f : ℂ → ℂ := fun s => ↑x ^ s / (s * (s + 1))
contourPull₃ : ∀ (σ' σ'' : ℝ), σ' ≤ -3 / 2 → σ'' ≤ -3 / 2 → VerticalIntegral' f σ' = VerticalIntegral' f σ''
C : ℝ
hC : ∀ σ < -3 / 2, ‖VerticalIntegral' f σ‖ ≤ x ^ σ * C
this : Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
⊢ ∀ a < -3 / 2, (⇑Complex.abs ∘ VerticalIntegral' f) a ≤ x ^ a * C
Theorem: MeasureTheory.setIntegral_integral_swap
Proof state before:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SigmaFinite μ
f : α → β → E
s : Set α
t : Set β
hf : IntegrableOn (Function.uncurry f) (s ×ˢ t) (μ.prod ν)
⊢ ∫ (x : α) in s, ∫ (y : β) in t, f x y ∂ν ∂μ = ∫ (y : β) in t, ∫ (x : α) in s, f x y ∂μ ∂ν
Tactic:
apply integral_integral_swap
Proof state after:
case hf
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SigmaFinite μ
f : α → β → E
s : Set α
t : Set β
hf : IntegrableOn (Function.uncurry f) (s ×ˢ t) (μ.prod ν)
⊢ Integrable (Function.uncurry fun x y => f x y) ((μ.restrict s).prod (ν.restrict t))
Theorem: MeasureTheory.setIntegral_integral_swap
Proof state before:
case hf
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SigmaFinite μ
f : α → β → E
s : Set α
t : Set β
hf : IntegrableOn (Function.uncurry f) (s ×ˢ t) (μ.prod ν)
⊢ Integrable (Function.uncurry fun x y => f x y) ((μ.restrict s).prod (ν.restrict t))
Tactic:
convert hf.integrable
Proof state after:
case h.e'_6
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SigmaFinite μ
f : α → β → E
s : Set α
t : Set β
hf : IntegrableOn (Function.uncurry f) (s ×ˢ t) (μ.prod ν)
⊢ (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)
Theorem: MeasureTheory.setIntegral_integral_swap
Proof state before:
case h.e'_6
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SigmaFinite μ
f : α → β → E
s : Set α
t : Set β
hf : IntegrableOn (Function.uncurry f) (s ×ˢ t) (μ.prod ν)
⊢ (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)
Tactic:
exact Measure.prod_restrict s t
Proof state after:
no goals