internlm/Lean-Github huggingface dataset:
Theorem: ZetaNear1BndExact
Proof state before:
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
⊢ Ico 1 (1 + ε) ⊆ U
Tactic:
refine subset_trans (subset_trans ?_ hε) hT
Proof state after:
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
⊢ Ico 1 (1 + ε) ⊆ {y | dist y 1 < ε}
Theorem: ZetaNear1BndExact
Proof state before:
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
⊢ Ico 1 (1 + ε) ⊆ {y | dist y 1 < ε}
Tactic:
intro x hx
Proof state after:
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
x : ℝ
hx : x ∈ Ico 1 (1 + ε)
⊢ x ∈ {y | dist y 1 < ε}
Theorem: ZetaNear1BndExact
Proof state before:
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
x : ℝ
hx : x ∈ Ico 1 (1 + ε)
⊢ x ∈ {y | dist y 1 < ε}
Tactic:
simp only [mem_Ico] at hx
Proof state after:
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
x : ℝ
hx : 1 ≤ x ∧ x < 1 + ε
⊢ x ∈ {y | dist y 1 < ε}
Theorem: ZetaNear1BndExact
Proof state before:
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
x : ℝ
hx : 1 ≤ x ∧ x < 1 + ε
⊢ x ∈ {y | dist y 1 < ε}
Tactic:
simp only [dist, abs_lt]
Proof state after:
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
x : ℝ
hx : 1 ≤ x ∧ x < 1 + ε
⊢ x ∈ {y | -ε < y - 1 ∧ y - 1 < ε}
Theorem: ZetaNear1BndExact
Proof state before:
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
x : ℝ
hx : 1 ≤ x ∧ x < 1 + ε
⊢ x ∈ {y | -ε < y - 1 ∧ y - 1 < ε}
Tactic:
exact ⟨by linarith, by linarith⟩
Proof state after:
no goals
Theorem: ZetaNear1BndExact
Proof state before:
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
x : ℝ
hx : 1 ≤ x ∧ x < 1 + ε
⊢ -ε < x - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaNear1BndExact
Proof state before:
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
x : ℝ
hx : 1 ≤ x ∧ x < 1 + ε
⊢ x - 1 < ε
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaNear1BndExact
Proof state before:
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}
⊢ ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
Tactic:
apply HasDerivAt.continuousOn (f' := deriv ζ)
Proof state after:
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}
⊢ ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, HasDerivAt ζ (deriv ζ x) x
Theorem: ZetaNear1BndExact
Proof state before:
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}
⊢ ∀ x ∈ {x | ∃ z ∈ W, ↑z = x}, HasDerivAt ζ (deriv ζ x) x
Tactic:
intro σ hσ
Proof state after:
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}
σ : ℂ
hσ : σ ∈ {x | ∃ z ∈ W, ↑z = x}
⊢ HasDerivAt ζ (deriv ζ σ) σ
Theorem: ZetaNear1BndExact
Proof state before:
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}
σ : ℂ
hσ : σ ∈ {x | ∃ z ∈ W, ↑z = x}
⊢ HasDerivAt ζ (deriv ζ σ) σ
Tactic:
exact (differentiableAt_riemannZeta (by contrapose! hσ; simp [W, hσ, εpos])).hasDerivAt
Proof state after:
no goals
Theorem: ZetaNear1BndExact
Proof state before:
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}
σ : ℂ
hσ : σ ∈ {x | ∃ z ∈ W, ↑z = x}
⊢ σ ≠ 1
Tactic:
contrapose! hσ
Proof state after:
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}
σ : ℂ
hσ : σ = 1
⊢ σ ∉ {x | ∃ z ∈ W, ↑z = x}
Theorem: ZetaNear1BndExact
Proof state before:
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}
σ : ℂ
hσ : σ = 1
⊢ σ ∉ {x | ∃ z ∈ W, ↑z = x}
Tactic:
simp [W, hσ, εpos]
Proof state after:
no goals
Theorem: ZetaNear1BndExact
Proof state before:
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
⊢ ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Tactic:
intro σ hσ
Proof state after:
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
σ : ℝ
hσ : σ ∈ W
⊢ ‖ζ ↑σ‖ < C'
Theorem: ZetaNear1BndExact
Proof state before:
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
σ : ℝ
hσ : σ ∈ W
⊢ ‖ζ ↑σ‖ < C'
Tactic:
simp only [lt_max_iff, C']
Proof state after:
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
σ : ℝ
hσ : σ ∈ W
⊢ ‖ζ ↑σ‖ < C + 1 ∨ ‖ζ ↑σ‖ < 1
Theorem: ZetaNear1BndExact
Proof state before:
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
σ : ℝ
hσ : σ ∈ W
⊢ ‖ζ ↑σ‖ < C + 1 ∨ ‖ζ ↑σ‖ < 1
Tactic:
have := hC σ
Proof state after:
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
σ : ℝ
hσ : σ ∈ W
this : ↑σ ∈ {x | ∃ z ∈ W, ↑z = x} → ‖ζ ↑σ‖ ≤ C
⊢ ‖ζ ↑σ‖ < C + 1 ∨ ‖ζ ↑σ‖ < 1
Theorem: ZetaNear1BndExact
Proof state before:
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
σ : ℝ
hσ : σ ∈ W
this : ↑σ ∈ {x | ∃ z ∈ W, ↑z = x} → ‖ζ ↑σ‖ ≤ C
⊢ ‖ζ ↑σ‖ < C + 1 ∨ ‖ζ ↑σ‖ < 1
Tactic:
simp only [mem_setOf_eq, ofReal_inj, exists_eq_right] at this
Proof state after:
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
σ : ℝ
hσ : σ ∈ W
this : σ ∈ W → ‖ζ ↑σ‖ ≤ C
⊢ ‖ζ ↑σ‖ < C + 1 ∨ ‖ζ ↑σ‖ < 1
Theorem: ZetaNear1BndExact
Proof state before:
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
σ : ℝ
hσ : σ ∈ W
this : σ ∈ W → ‖ζ ↑σ‖ ≤ C
⊢ ‖ζ ↑σ‖ < C + 1 ∨ ‖ζ ↑σ‖ < 1
Tactic:
exact Or.inl <| lt_of_le_of_lt (this hσ) (by norm_num)
Proof state after:
no goals
Theorem: ZetaNear1BndExact
Proof state before:
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
σ : ℝ
hσ : σ ∈ W
this : σ ∈ W → ‖ζ ↑σ‖ ≤ C
⊢ C < C + 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaNear1BndExact
Proof state before:
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'
⊢ 0 < C'
Tactic:
simp [C']
Proof state after:
no goals
Theorem: ZetaNear1BndExact
Proof state before:
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'
⊢ 0 < max (2 * C') c
Tactic:
simp [Cpos]
Proof state after:
no goals
Theorem: ZetaNear1BndExact
Proof state before:
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)
Tactic:
simp only [← h, mem_setOf_eq] at hσ
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
apply le_trans hσ ?_
Proof state after:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ c * ‖1 / (↑σ - 1)‖ ≤ max (2 * C') c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ c * ‖1 / (↑σ - 1)‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
norm_cast
Proof state after:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ c * ‖↑(1 / (σ - 1))‖ ≤ max (2 * C') c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ c * ‖↑(1 / (σ - 1))‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
have : 0 ≤ 1 / (σ - 1) := by apply one_div_nonneg.mpr; linarith
Proof state after:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ c * ‖↑(1 / (σ - 1))‖ ≤ max (2 * C') c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ c * ‖↑(1 / (σ - 1))‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
simp only [norm_eq_abs, Complex.abs_ofReal, abs_eq_self.mpr this, mul_div, mul_one]
Proof state after:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ c / (σ - 1) ≤ max (2 * C') c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ c / (σ - 1) ≤ max (2 * C') c / (σ - 1)
Tactic:
exact div_le_div (by simp [Cpos.le]) (by simp) (by linarith) (by rfl)
Proof state after:
no goals
Theorem: ZetaNear1BndExact
Proof state before:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ 0 ≤ 1 / (σ - 1)
Tactic:
apply one_div_nonneg.mpr
Proof state after:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ 0 ≤ σ - 1
Theorem: ZetaNear1BndExact
Proof state before:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
⊢ 0 ≤ σ - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaNear1BndExact
Proof state before:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ 0 ≤ max (2 * C') c
Tactic:
simp [Cpos.le]
Proof state after:
no goals
Theorem: ZetaNear1BndExact
Proof state before:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ c ≤ max (2 * C') c
Tactic:
simp
Proof state after:
no goals
Theorem: ZetaNear1BndExact
Proof state before:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ 0 < σ - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaNear1BndExact
Proof state before:
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σ : ‖ζ ↑σ‖ ≤ c * ‖1 / (↑σ - 1)‖
this : 0 ≤ 1 / (σ - 1)
⊢ σ - 1 ≤ σ - 1
Tactic:
rfl
Proof state after:
no goals