internlm/Lean-Github huggingface dataset:
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ Ioi x ⊆ t ∩ Ioi x
Tactic:
use t
Proof state after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen t ∧ x ∈ t ∧ t ∩ Ioi x ⊆ t ∩ Ioi x
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen t ∧ x ∈ t ∧ t ∩ Ioi x ⊆ t ∩ Ioi x
Tactic:
simp only [subset_inter_iff, inter_subset_left, inter_subset_right, and_self,
  and_true, t]
Proof state after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen {x | f x + a ∈ u} ∧ x ∈ {x | f x + a ∈ u}
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen {x | f x + a ∈ u} ∧ x ∈ {x | f x + a ∈ u}
Tactic:
simp
Proof state after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen {x | f x + a ∈ u} ∧ f x + a ∈ u
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen {x | f x + a ∈ u} ∧ f x + a ∈ u
Tactic:
refine ⟨?_, by simp [hu2]⟩
Proof state after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen {x | f x + a ∈ u}
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen {x | f x + a ∈ u}
Tactic:
simp [Metric.isOpen_iff] at hu ⊢
Proof state after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
⊢ ∀ (x : ℝ), f x + a ∈ u → ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ {x | f x + a ∈ u}
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
⊢ ∀ (x : ℝ), f x + a ∈ u → ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ {x | f x + a ∈ u}
Tactic:
intro x hx
Proof state after:
case h
f : ℝ → ℝ
a x✝ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝ + a ∈ u
hu3 : u ∩ Ioi (f x✝ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
⊢ ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ {x | f x + a ∈ u}
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case h
f : ℝ → ℝ
a x✝ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝ + a ∈ u
hu3 : u ∩ Ioi (f x✝ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
⊢ ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ {x | f x + a ∈ u}
Tactic:
obtain ⟨ε, εpos, hε⟩ := hu (f x + a) hx
Proof state after:
case h.intro.intro
f : ℝ → ℝ
a x✝ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝ + a ∈ u
hu3 : u ∩ Ioi (f x✝ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
ε : ℝ
εpos : 0 < ε
hε : Metric.ball (f x + a) ε ⊆ u
⊢ ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ {x | f x + a ∈ u}
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case h.intro.intro
f : ℝ → ℝ
a x✝ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝ + a ∈ u
hu3 : u ∩ Ioi (f x✝ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
ε : ℝ
εpos : 0 < ε
hε : Metric.ball (f x + a) ε ⊆ u
⊢ ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ {x | f x + a ∈ u}
Tactic:
simp only [Metric.ball, dist_sub_eq_dist_add_right, setOf_subset_setOf] at hε ⊢
Proof state after:
case h.intro.intro
f : ℝ → ℝ
a x✝ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝ + a ∈ u
hu3 : u ∩ Ioi (f x✝ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
ε : ℝ
εpos : 0 < ε
hε : {y | dist y (f x + a) < ε} ⊆ u
⊢ ∃ ε, 0 < ε ∧ ∀ (a_1 : ℝ), dist a_1 x < ε → f a_1 + a ∈ u
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case h.intro.intro
f : ℝ → ℝ
a x✝ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝ + a ∈ u
hu3 : u ∩ Ioi (f x✝ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
ε : ℝ
εpos : 0 < ε
hε : {y | dist y (f x + a) < ε} ⊆ u
⊢ ∃ ε, 0 < ε ∧ ∀ (a_1 : ℝ), dist a_1 x < ε → f a_1 + a ∈ u
Tactic:
exact ⟨ε, εpos, fun _ hy ↦ hε (by simp [isometry_iff_dist_eq.mp f_iso, hy])⟩
Proof state after:
no goals
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ f x + a ∈ u
Tactic:
simp [hu2]
Proof state after:
no goals
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
f : ℝ → ℝ
a x✝¹ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝¹ + a ∈ u
hu3 : u ∩ Ioi (f x✝¹ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
ε : ℝ
εpos : 0 < ε
hε : {y | dist y (f x + a) < ε} ⊆ u
x✝ : ℝ
hy : dist x✝ x < ε
⊢ f x✝ + a ∈ {y | dist y (f x + a) < ε}
Tactic:
simp [isometry_iff_dist_eq.mp f_iso, hy]
Proof state after:
no goals
Theorem: ZetaNear1BndFilter
Proof state before:
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
Tactic:
have := Tendsto_nhdsWithin_punctured_add (a := -1) (x := 1)
Proof state after:
this : Tendsto (fun y => y + -1) (𝓝[>] 1) (𝓝[>] (1 + -1))
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
Theorem: ZetaNear1BndFilter
Proof state before:
this : Tendsto (fun y => y + -1) (𝓝[>] 1) (𝓝[>] (1 + -1))
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
Tactic:
simp only [add_right_neg, ← sub_eq_add_neg] at this
Proof state after:
this : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
Theorem: ZetaNear1BndFilter
Proof state before:
this : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
Tactic:
have := riemannZeta_isBigO_near_one_horizontal.comp_tendsto this
Proof state after:
this✝ : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
this : ((fun x => ζ (1 + ↑x)) ∘ fun y => y - 1) =O[𝓝[>] 1] ((fun x => 1 / ↑x) ∘ fun y => y - 1)
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
Theorem: ZetaNear1BndFilter
Proof state before:
this✝ : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
this : ((fun x => ζ (1 + ↑x)) ∘ fun y => y - 1) =O[𝓝[>] 1] ((fun x => 1 / ↑x) ∘ fun y => y - 1)
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
Tactic:
convert this using 1 <;> {ext; simp}
Proof state after:
no goals
Theorem: ZetaNear1BndFilter
Proof state before:
case h.e'_8
this✝ : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
this : ((fun x => ζ (1 + ↑x)) ∘ fun y => y - 1) =O[𝓝[>] 1] ((fun x => 1 / ↑x) ∘ fun y => y - 1)
⊢ (fun σ => 1 / (↑σ - 1)) = (fun x => 1 / ↑x) ∘ fun y => y - 1
Tactic:
ext
Proof state after:
case h.e'_8.h
this✝ : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
this : ((fun x => ζ (1 + ↑x)) ∘ fun y => y - 1) =O[𝓝[>] 1] ((fun x => 1 / ↑x) ∘ fun y => y - 1)
x✝ : ℝ
⊢ 1 / (↑x✝ - 1) = ((fun x => 1 / ↑x) ∘ fun y => y - 1) x✝
Theorem: ZetaNear1BndFilter
Proof state before:
case h.e'_8.h
this✝ : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
this : ((fun x => ζ (1 + ↑x)) ∘ fun y => y - 1) =O[𝓝[>] 1] ((fun x => 1 / ↑x) ∘ fun y => y - 1)
x✝ : ℝ
⊢ 1 / (↑x✝ - 1) = ((fun x => 1 / ↑x) ∘ fun y => y - 1) x✝
Tactic:
simp
Proof state after:
no goals
Theorem: ZetaNear1BndExact
Proof state before:
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
have := ZetaNear1BndFilter
Proof state after:
this : (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
this : (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
rw [Asymptotics.isBigO_iff] at this
Proof state after:
this : ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 1, ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
this : ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 1, ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
obtain ⟨c, U, hU, V, hV, h⟩ := this
Proof state after:
case intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
case intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
obtain ⟨T, hT, T_open, h1T⟩ := mem_nhds_iff.mp hU
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
obtain ⟨ε, εpos, hε⟩ := Metric.isOpen_iff.mp T_open 1 h1T
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Metric.ball 1 ε ⊆ T
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Metric.ball 1 ε ⊆ T
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
simp only [Metric.ball] at hε
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : {y | dist y 1 < ε} ⊆ T
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : {y | dist y 1 < ε} ⊆ T
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
replace hε : Ico 1 (1 + ε) ⊆ U := by
  refine subset_trans (subset_trans ?_ hε) hT
  intro x hx
  simp only [mem_Ico] at hx
  simp only [dist, abs_lt]
  exact ⟨by linarith, by linarith⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
let W := Icc (1 + ε) 2
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
have W_compact : IsCompact {ofReal' z | z ∈ W} :=
  IsCompact.image isCompact_Icc continuous_ofReal
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
have cont : ContinuousOn ζ {ofReal' z | z ∈ W} := by
  apply HasDerivAt.continuousOn (f' := deriv ζ)
  intro σ hσ
  exact (differentiableAt_riemannZeta (by contrapose! hσ; simp [W, hσ, εpos])).hasDerivAt
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
obtain ⟨C, hC⟩ := IsCompact.exists_bound_of_continuousOn W_compact cont
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
let C' := max (C + 1) 1
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
C' : ℝ := max (C + 1) 1
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
hC : ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, ‖ζ x‖ ≤ C
C' : ℝ := max (C + 1) 1
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
replace hC : ∀ (σ : ℝ), σ ∈ W → ‖ζ σ‖ < C' := by
  intro σ hσ
  simp only [lt_max_iff, C']
  have := hC σ
  simp only [mem_setOf_eq, ofReal_inj, exists_eq_right] at this
  exact Or.inl <| lt_of_le_of_lt (this hσ) (by norm_num)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
have Cpos : 0 < C' := by simp [C']
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
Tactic:
use max (2 * C') c, (by simp [Cpos])
Proof state after:
case h
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
⊢ ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
case h
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
⊢ ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
intro σ ⟨σ_ge, σ_le⟩
Proof state after:
case h
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
case h
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
by_cases hσ : σ ∈ U ∩ V
Proof state after:
case pos
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∈ U ∩ V
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)

case neg
c : ℝ
U : Set ℝ
hU : U ∈ 𝓝 1
V : Set ℝ
hV : V ∈ 𝓟 (Ioi 1)
h : {x | (fun x => ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖) x} = U ∩ V
T : Set ℝ
hT : T ⊆ U
T_open : IsOpen T
h1T : 1 ∈ T
ε : ℝ
εpos : ε > 0
hε : Ico 1 (1 + ε) ⊆ U
W : Set ℝ := Icc (1 + ε) 2
W_compact : IsCompact {x | ∃ z ∈ W, ↑z = x}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∉ U ∩ V
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)