internlm/Lean-Github huggingface dataset:
Theorem: ZetaNear1BndExact
Proof state before:
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)
Tactic:
replace hσ : σ ∈ W := by
  simp only [mem_inter_iff, hV σ_ge, and_true] at hσ
  simp only [mem_Icc, σ_le, and_true, W]
  contrapose! hσ; exact hε ⟨σ_ge.le, hσ⟩
Proof state after:
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σ : σ ∈ W
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)
Theorem: ZetaNear1BndExact
Proof state before:
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σ : σ ∈ W
⊢ ‖ζ ↑σ‖ ≤ max (2 * C') c / (σ - 1)
Tactic:
apply le_trans (hC σ hσ).le ((le_div_iff (by linarith)).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σ : σ ∈ W
⊢ C' * (σ - 1) ≤ max (2 * C') 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 : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∈ W
⊢ C' * (σ - 1) ≤ max (2 * C') c
Tactic:
rw [le_max_iff, mul_comm 2]
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σ : σ ∈ W
⊢ C' * (σ - 1) ≤ C' * 2 ∨ C' * (σ - 1) ≤ 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 : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ ∈ W
⊢ C' * (σ - 1) ≤ C' * 2 ∨ C' * (σ - 1) ≤ c
Tactic:
exact Or.inl <| mul_le_mul_of_nonneg_left (by linarith) 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σ : σ ∉ U ∩ V
⊢ σ ∈ W
Tactic:
simp only [mem_inter_iff, hV σ_ge, and_true] at 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σ : σ ∉ U
⊢ σ ∈ W
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σ : σ ∉ U
⊢ σ ∈ W
Tactic:
simp only [mem_Icc, σ_le, and_true, W]
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σ : σ ∉ U
⊢ 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σ : σ ∉ U
⊢ 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}
cont : ContinuousOn ζ {x | ∃ z ∈ W, ↑z = x}
C : ℝ
C' : ℝ := max (C + 1) 1
hC : ∀ σ ∈ W, ‖ζ ↑σ‖ < C'
Cpos : 0 < C'
σ : ℝ
σ_ge : 1 < σ
σ_le : σ ≤ 2
hσ : σ < 1 + ε
⊢ σ ∈ U
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σ : σ < 1 + ε
⊢ σ ∈ U
Tactic:
exact hε ⟨σ_ge.le, hσ⟩
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σ : σ ∈ W
⊢ 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σ : σ ∈ W
⊢ σ - 1 ≤ 2
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)
Tactic:
apply (div_le_iff ?_).mpr
Proof state after:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖

σ t : ℝ
σ_gt : 1 < σ
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖

σ t : ℝ
σ_gt : 1 < σ
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖
Tactic:
apply (Real.rpow_le_rpow_iff (z := 4) (by norm_num) ?_ (by norm_num)).mp
Proof state after:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ^ 4 ≤ (‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖) ^ 4

σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖

σ t : ℝ
σ_gt : 1 < σ
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 < 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ^ 4 ≤ (‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖) ^ 4
Tactic:
simp only [Real.one_rpow]
Proof state after:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ (‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖) ^ 4
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ (‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖) ^ 4
Tactic:
rw [Real.mul_rpow, Real.mul_rpow, ← Real.rpow_mul, ← Real.rpow_mul]
Proof state after:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ (3 / 4 * 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4 * 4) * ‖ζ (↑σ + ↑t * I)‖ ^ 4

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ (3 / 4 * 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4 * 4) * ‖ζ (↑σ + ↑t * I)‖ ^ 4

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
simp only [isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
  IsUnit.div_mul_cancel, IsUnit.inv_mul_cancel, Real.rpow_one]
Proof state after:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + 2 * ↑t * I)‖ * ‖ζ (↑σ + ↑t * I)‖ ^ 4

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + 2 * ↑t * I)‖ * ‖ζ (↑σ + ↑t * I)‖ ^ 4

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
conv => rw [mul_assoc]; rhs; rhs; rw [mul_comm]
Proof state after:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * (‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * (‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
rw [← mul_assoc]
Proof state after:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
have := norm_zeta_product_ge_one (x := σ - 1) (by linarith) t
Proof state after:
σ t : ℝ
σ_gt : 1 < σ
this : ‖ζ (1 + ↑(σ - 1)) ^ 3 * ζ (1 + ↑(σ - 1) + I * ↑t) ^ 4 * ζ (1 + ↑(σ - 1) + 2 * I * ↑t)‖ ≥ 1
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
this : ‖ζ (1 + ↑(σ - 1)) ^ 3 * ζ (1 + ↑(σ - 1) + I * ↑t) ^ 4 * ζ (1 + ↑(σ - 1) + 2 * I * ↑t)‖ ≥ 1
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
simp_rw [ge_iff_le, norm_mul, norm_pow, ofReal_sub, ofReal_one, add_sub_cancel, ← Real.rpow_natCast] at this
Proof state after:
σ t : ℝ
σ_gt : 1 < σ
this : 1 ≤ ‖ζ ↑σ‖ ^ ↑3 * ‖ζ (↑σ + I * ↑t)‖ ^ ↑4 * ‖ζ (↑σ + 2 * I * ↑t)‖
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
this : 1 ≤ ‖ζ ↑σ‖ ^ ↑3 * ‖ζ (↑σ + I * ↑t)‖ ^ ↑4 * ‖ζ (↑σ + 2 * I * ↑t)‖
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
convert this using 3 <;> ring_nf
Proof state after:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Theorem: ZetaInvBound1
Proof state before:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
any_goals ring_nf
Proof state after:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Theorem: ZetaInvBound1
Proof state before:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
any_goals apply norm_nonneg
Proof state after:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)
Theorem: ZetaInvBound1
Proof state before:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)
Tactic:
any_goals apply Real.rpow_nonneg <| norm_nonneg _
Proof state after:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)
Theorem: ZetaInvBound1
Proof state before:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)
Tactic:
apply mul_nonneg <;> apply Real.rpow_nonneg <| norm_nonneg _
Proof state after:
no goals
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 < σ - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaInvBound1
Proof state before:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)
Tactic:
ring_nf
Proof state after:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)
Theorem: ZetaInvBound1
Proof state before:
case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
apply norm_nonneg
Proof state after:
no goals
Theorem: ZetaInvBound1
Proof state before:
case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)
Tactic:
apply Real.rpow_nonneg <| norm_nonneg _
Proof state after:
no goals
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖
Tactic:
refine mul_nonneg (mul_nonneg ?_ ?_) ?_ <;> simp [Real.rpow_nonneg]
Proof state after:
no goals
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖
Tactic:
have s_ne_one : σ + t * I ≠ 1 := by
  contrapose! σ_gt; apply le_of_eq; apply And.left; simpa [Complex.ext_iff] using σ_gt
Proof state after:
σ t : ℝ
σ_gt : 1 < σ
s_ne_one : ↑σ + ↑t * I ≠ 1
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
s_ne_one : ↑σ + ↑t * I ≠ 1
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖
Tactic:
simpa using riemannZeta_ne_zero_of_one_le_re s_ne_one (by simp [σ_gt.le])
Proof state after:
no goals
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
⊢ ↑σ + ↑t * I ≠ 1
Tactic:
contrapose! σ_gt
Proof state after:
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ σ ≤ 1
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ σ ≤ 1
Tactic:
apply le_of_eq
Proof state after:
case a
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ σ = 1
Theorem: ZetaInvBound1
Proof state before:
case a
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ σ = 1
Tactic:
apply And.left
Proof state after:
case a.self
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ σ = 1 ∧ ?a.b✝

case a.b
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ Prop
Theorem: ZetaInvBound1
Proof state before:
case a.self
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ σ = 1 ∧ ?a.b✝

case a.b
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ Prop
Tactic:
simpa [Complex.ext_iff] using σ_gt
Proof state after:
no goals
Theorem: ZetaInvBound1
Proof state before:
σ t : ℝ
σ_gt : 1 < σ
s_ne_one : ↑σ + ↑t * I ≠ 1
⊢ 1 ≤ (↑σ + ↑t * I).re
Tactic:
simp [σ_gt.le]
Proof state after:
no goals
Theorem: Ioi_union_Iio_mem_cocompact
Proof state before:
a : ℝ
ha : 0 ≤ a
⊢ Ioi a ∪ Iio (-a) ∈ cocompact ℝ
Tactic:
simp only [Filter.mem_cocompact]
Proof state after:
a : ℝ
ha : 0 ≤ a
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ Ioi a ∪ Iio (-a)
Theorem: Ioi_union_Iio_mem_cocompact
Proof state before:
a : ℝ
ha : 0 ≤ a
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ Ioi a ∪ Iio (-a)
Tactic:
use Icc (-a) a
Proof state after:
case h
a : ℝ
ha : 0 ≤ a
⊢ IsCompact (Icc (-a) a) ∧ (Icc (-a) a)ᶜ ⊆ Ioi a ∪ Iio (-a)
Theorem: Ioi_union_Iio_mem_cocompact
Proof state before:
case h
a : ℝ
ha : 0 ≤ a
⊢ IsCompact (Icc (-a) a) ∧ (Icc (-a) a)ᶜ ⊆ Ioi a ∪ Iio (-a)
Tactic:
constructor
Proof state after:
case h.left
a : ℝ
ha : 0 ≤ a
⊢ IsCompact (Icc (-a) a)

case h.right
a : ℝ
ha : 0 ≤ a
⊢ (Icc (-a) a)ᶜ ⊆ Ioi a ∪ Iio (-a)
Theorem: Ioi_union_Iio_mem_cocompact
Proof state before:
case h.left
a : ℝ
ha : 0 ≤ a
⊢ IsCompact (Icc (-a) a)
Tactic:
exact isCompact_Icc
Proof state after:
no goals
Theorem: Ioi_union_Iio_mem_cocompact
Proof state before:
case h.right
a : ℝ
ha : 0 ≤ a
⊢ (Icc (-a) a)ᶜ ⊆ Ioi a ∪ Iio (-a)
Tactic:
rw [@compl_subset_iff_union, ← union_assoc, Icc_union_Ioi_eq_Ici, union_comm, Iio_union_Ici]
Proof state after:
case h.right
a : ℝ
ha : 0 ≤ a
⊢ -a ≤ a
Theorem: Ioi_union_Iio_mem_cocompact
Proof state before:
case h.right
a : ℝ
ha : 0 ≤ a
⊢ -a ≤ a
Tactic:
linarith
Proof state after:
no goals
Theorem: lt_abs_mem_cocompact
Proof state before:
a : ℝ
ha : 0 ≤ a
⊢ {t | a < |t|} ∈ cocompact ℝ
Tactic:
convert Ioi_union_Iio_mem_cocompact ha using 1
Proof state after:
case h.e'_4
a : ℝ
ha : 0 ≤ a
⊢ {t | a < |t|} = Ioi a ∪ Iio (-a)
Theorem: lt_abs_mem_cocompact
Proof state before:
case h.e'_4
a : ℝ
ha : 0 ≤ a
⊢ {t | a < |t|} = Ioi a ∪ Iio (-a)
Tactic:
ext t
Proof state after:
case h.e'_4.h
a : ℝ
ha : 0 ≤ a
t : ℝ
⊢ t ∈ {t | a < |t|} ↔ t ∈ Ioi a ∪ Iio (-a)
Theorem: lt_abs_mem_cocompact
Proof state before:
case h.e'_4.h
a : ℝ
ha : 0 ≤ a
t : ℝ
⊢ t ∈ {t | a < |t|} ↔ t ∈ Ioi a ∪ Iio (-a)
Tactic:
simp only [mem_setOf_eq, mem_union, mem_Ioi, mem_Iio, lt_abs, lt_neg]
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
⊢ ∃ C > 0,
    ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Tactic:
obtain ⟨A, ha, C, hC, h⟩ := ZetaUpperBnd
Proof state after:
case intro.intro.intro.intro
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
⊢ ∃ C > 0,
    ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)