internlm/Lean-Github huggingface dataset:
Theorem: UpperBnd_aux5
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
h₁ : 1 ≤ |t| / ↑⌊|t|⌋₊
h₂ : |t| / ↑⌊|t|⌋₊ ≤ 2
⊢ (|t| / ↑⌊|t|⌋₊) ^ 2 ≤ 2 ^ 2
Tactic:
gcongr
Proof state after:
no goals
Theorem: UpperBnd_aux5
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
h₁ : 1 ≤ |t| / ↑⌊|t|⌋₊
h₂ : |t| / ↑⌊|t|⌋₊ ≤ 2
⊢ 2 ^ 2 = 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2 ∧
    ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ) ∧ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
Tactic:
have bnd := UpperBnd_aux5 t_ge hσ.2
Proof state after:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2 ∧
    ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ) ∧ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2 ∧
    ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ) ∧ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
Tactic:
have bnd' : (|t| / ⌊|t|⌋₊) ^ σ ≤ 2 * |t| := by linarith
Proof state after:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2 ∧
    ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ) ∧ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2 ∧
    ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ) ∧ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
Tactic:
split_ands
Proof state after:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2

case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ)

case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
⊢ (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
Tactic:
linarith
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2
Tactic:
apply (div_le_iff <| norm_pos_iff.mpr <| sub_ne_zero_of_ne neOne.symm).mpr
Proof state after:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) ≤ |t| ^ (1 - σ) * 2 * ‖1 - (↑σ + ↑t * I)‖
Theorem: UpperBnd_aux6
Proof state before:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) ≤ |t| ^ (1 - σ) * 2 * ‖1 - (↑σ + ↑t * I)‖
Tactic:
conv => rw [mul_assoc]; rhs; rw [mul_comm]
Proof state after:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) ≤ 2 * ‖1 - (↑σ + ↑t * I)‖ * |t| ^ (1 - σ)
Theorem: UpperBnd_aux6
Proof state before:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) ≤ 2 * ‖1 - (↑σ + ↑t * I)‖ * |t| ^ (1 - σ)
Tactic:
apply (div_le_iff <| Real.rpow_pos_of_pos (by linarith) _).mp
Proof state after:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / |t| ^ (1 - σ) ≤ 2 * ‖1 - (↑σ + ↑t * I)‖
Theorem: UpperBnd_aux6
Proof state before:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / |t| ^ (1 - σ) ≤ 2 * ‖1 - (↑σ + ↑t * I)‖
Tactic:
rw [div_rpow_eq_rpow_div_neg (by positivity) (by positivity), neg_sub]
Proof state after:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ (|t| / ↑⌊|t|⌋₊) ^ (σ - 1) ≤ 2 * ‖1 - (↑σ + ↑t * I)‖
Theorem: UpperBnd_aux6
Proof state before:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ (|t| / ↑⌊|t|⌋₊) ^ (σ - 1) ≤ 2 * ‖1 - (↑σ + ↑t * I)‖
Tactic:
refine le_trans₄ ?_ bnd' ?_
Proof state after:
case refine_1.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ (|t| / ↑⌊|t|⌋₊) ^ (σ - 1) ≤ (|t| / ↑⌊|t|⌋₊) ^ σ

case refine_1.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 2 * |t| ≤ 2 * ‖1 - (↑σ + ↑t * I)‖
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 < |t|
Tactic:
linarith
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 ≤ ↑⌊|t|⌋₊
Tactic:
positivity
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 ≤ |t|
Tactic:
positivity
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
case refine_1.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ (|t| / ↑⌊|t|⌋₊) ^ (σ - 1) ≤ (|t| / ↑⌊|t|⌋₊) ^ σ
Tactic:
exact Real.rpow_le_rpow_of_exponent_le (one_le_div (by positivity) |>.mpr N_le_t) (by simp)
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 < ↑⌊|t|⌋₊
Tactic:
positivity
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ σ - 1 ≤ σ
Tactic:
simp
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
case refine_1.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 2 * |t| ≤ 2 * ‖1 - (↑σ + ↑t * I)‖
Tactic:
apply (mul_le_mul_left (by norm_num)).mpr
Proof state after:
case refine_1.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ |t| ≤ ‖1 - (↑σ + ↑t * I)‖
Theorem: UpperBnd_aux6
Proof state before:
case refine_1.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ |t| ≤ ‖1 - (↑σ + ↑t * I)‖
Tactic:
simpa using abs_im_le_abs (1 - (σ + t * I))
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ)
Tactic:
apply div_le_iff (by norm_num) |>.mpr
Proof state after:
case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ |t| ^ (1 - σ) * 2
Theorem: UpperBnd_aux6
Proof state before:
case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ |t| ^ (1 - σ) * 2
Tactic:
rw [Real.rpow_sub (by linarith), Real.rpow_one, div_mul_eq_mul_div, mul_comm]
Proof state after:
case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ 2 * |t| / |t| ^ σ
Theorem: UpperBnd_aux6
Proof state before:
case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ 2 * |t| / |t| ^ σ
Tactic:
apply div_le_iff (by positivity) |>.mp
Proof state after:
case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / (|t| ^ σ)⁻¹ ≤ 2 * |t|
Theorem: UpperBnd_aux6
Proof state before:
case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / (|t| ^ σ)⁻¹ ≤ 2 * |t|
Tactic:
convert bnd' using 1
Proof state after:
case h.e'_3
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / (|t| ^ σ)⁻¹ = (|t| / ↑⌊|t|⌋₊) ^ σ
Theorem: UpperBnd_aux6
Proof state before:
case h.e'_3
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / (|t| ^ σ)⁻¹ = (|t| / ↑⌊|t|⌋₊) ^ σ
Tactic:
rw [← Real.rpow_neg (by linarith), div_rpow_neg_eq_rpow_div (by positivity) (by positivity)]
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 < (|t| ^ σ)⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 ≤ |t|
Tactic:
linarith
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
Tactic:
apply div_le_iff (by linarith [hσ.1]) |>.mpr
Proof state after:
case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ 8 * |t| ^ (-σ) * σ
Theorem: UpperBnd_aux6
Proof state before:
case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ 8 * |t| ^ (-σ) * σ
Tactic:
rw [mul_assoc, mul_comm, mul_assoc]
Proof state after:
case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ |t| ^ (-σ) * (σ * 8)
Theorem: UpperBnd_aux6
Proof state before:
case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ |t| ^ (-σ) * (σ * 8)
Tactic:
apply div_le_iff' (by positivity) |>.mp
Proof state after:
case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / |t| ^ (-σ) ≤ σ * 8
Theorem: UpperBnd_aux6
Proof state before:
case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / |t| ^ (-σ) ≤ σ * 8
Tactic:
apply le_trans ?_ (by linarith [hσ.1] : 4 ≤ σ * 8)
Proof state after:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / |t| ^ (-σ) ≤ 4
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / |t| ^ (-σ) ≤ 4
Tactic:
convert bnd using 1
Proof state after:
case h.e'_3
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / |t| ^ (-σ) = (|t| / ↑⌊|t|⌋₊) ^ σ
Theorem: UpperBnd_aux6
Proof state before:
case h.e'_3
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / |t| ^ (-σ) = (|t| / ↑⌊|t|⌋₊) ^ σ
Tactic:
exact div_rpow_neg_eq_rpow_div (by positivity) (by positivity)
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 < σ
Tactic:
linarith [hσ.1]
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 < |t| ^ (-σ)
Tactic:
positivity
Proof state after:
no goals
Theorem: UpperBnd_aux6
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 4 ≤ σ * 8
Tactic:
linarith [hσ.1]
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
⊢ let C := A.exp * (5 + 8 * 2);
  let N := ⌊|t|⌋₊;
  let s := ↑σ + ↑t * I;
  ‖∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s‖ + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ +
      ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤
    C * |t|.log
Tactic:
intros C N s
Proof state after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
⊢ ‖∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s‖ + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ +
      ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤
    C * |t|.log
Theorem: ZetaUpperBnd'
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
⊢ ‖∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s‖ + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ +
      ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤
    C * |t|.log
Tactic:
obtain ⟨Npos, N_le_t, logt_gt, σ_gt, σPos, neOne⟩ := UpperBnd_aux hA t_gt hσ.1
Proof state after:
case intro.intro.intro.intro.intro
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s‖ + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ +
      ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤
    C * |t|.log
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s‖ + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ +
      ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤
    C * |t|.log
Tactic:
replace σ_gt : 1 / 2 < σ := by linarith [hA.2]
Proof state after:
case intro.intro.intro.intro.intro
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ ‖∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s‖ + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ +
      ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤
    C * |t|.log
Theorem: ZetaUpperBnd'
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 1 / 2 < σ
Tactic:
linarith [hA.2]
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + (3 + 8 * 2) * A.exp * |t|.log = C * |t|.log
Tactic:
ring
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_1
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ ‖∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s‖ + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ +
      ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤
    A.exp * 2 * |t|.log + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ +
      ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖
Tactic:
simp only [add_le_add_iff_right, one_div_cpow_eq_cpow_neg]
Proof state after:
case intro.intro.intro.intro.intro.calc_1
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ ‖∑ x ∈ Finset.range (N + 1), ↑x ^ (-s)‖ ≤ A.exp * 2 * |t|.log
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_1
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ ‖∑ x ∈ Finset.range (N + 1), ↑x ^ (-s)‖ ≤ A.exp * 2 * |t|.log
Tactic:
convert UpperBnd_aux3 (C := 2) hA hσ.1 t_gt le_rfl using 1
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_2
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ +
      ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤
    A.exp * 2 * |t|.log + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ + 2 * |t| * ↑N ^ (-σ) / σ
Tactic:
simp only [add_le_add_iff_left]
Proof state after:
case intro.intro.intro.intro.intro.calc_2
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤ 2 * |t| * ↑N ^ (-σ) / σ
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_2
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤ 2 * |t| * ↑N ^ (-σ) / σ
Tactic:
exact ZetaBnd_aux1 N (by linarith) ⟨σPos, hσ.2⟩ (by linarith)
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ 1 ≤ N
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ 2 ≤ |t|
Tactic:
linarith
Proof state after:
no goals