internlm/Lean-Github huggingface dataset:
Theorem: ZetaInvBnd
Proof state before:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
this : 1 / (C' * (σ' - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)) ≤ ‖ζ (↑σ' + ↑t * I)‖
⊢ 0 ≤ σ' - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaInvBnd
Proof state before:
case calc_2.hab.refine_1
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ 0 < ‖ζ (↑σ' + ↑t * I)‖
Tactic:
apply norm_pos_iff.mpr <| riemannZeta_ne_zero_of_one_lt_re (by simp [σ'_gt])
Proof state after:
no goals
Theorem: ZetaInvBnd
Proof state before:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ 1 < (↑σ' + ↑t * I).re
Tactic:
simp [σ'_gt]
Proof state after:
no goals
Theorem: ZetaInvBnd
Proof state before:
case calc_2.hcd
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ ‖ζ s - ζ s'‖ ≤ C₂ * |t|.log ^ 2 * (σ' - σ)
Tactic:
rw [(by simp : ζ s - ζ s' = -(ζ s' - ζ s)), norm_neg]
Proof state after:
case calc_2.hcd
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ ‖ζ s' - ζ s‖ ≤ C₂ * |t|.log ^ 2 * (σ' - σ)
Theorem: ZetaInvBnd
Proof state before:
case calc_2.hcd
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ ‖ζ s' - ζ s‖ ≤ C₂ * |t|.log ^ 2 * (σ' - σ)
Tactic:
refine hC₂ σ σ' t t_gt ?_ σ'_le <| lt_trans hσ.2 σ'_gt
Proof state after:
case calc_2.hcd
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ 1 - A' / |t|.log ≤ σ
Theorem: ZetaInvBnd
Proof state before:
case calc_2.hcd
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ 1 - A' / |t|.log ≤ σ
Tactic:
apply le_trans ?_ hσ.1
Proof state after:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ 1 - A' / |t|.log ≤ 1 - A / |t|.log ^ 9
Theorem: ZetaInvBnd
Proof state before:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ 1 - A' / |t|.log ≤ 1 - A / |t|.log ^ 9
Tactic:
rw [tsub_le_iff_right, ← add_sub_right_comm, le_sub_iff_add_le, add_le_add_iff_left]
Proof state after:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ A / |t|.log ^ 9 ≤ A' / |t|.log
Theorem: ZetaInvBnd
Proof state before:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ A / |t|.log ^ 9 ≤ A' / |t|.log
Tactic:
exact div_le_div hA'.1.le (by simp [A]) (by positivity) <| ZetaInvBnd_aux logt_gt_one
Proof state after:
no goals
Theorem: ZetaInvBnd
Proof state before:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ ζ s - ζ s' = -(ζ s' - ζ s)
Tactic:
simp
Proof state after:
no goals
Theorem: ZetaInvBnd
Proof state before:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ A ≤ A'
Tactic:
simp [A]
Proof state after:
no goals
Theorem: ZetaInvBnd
Proof state before:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ 0 < |t|.log
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaInvBnd
Proof state before:
case calc_3
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ C₁ * (σ' - 1) ^ (3 / 4) * |t|.log ^ (-1 / 4) - C₂ * |t|.log ^ 2 * (σ' - σ) ≥
    C₁ * (A / |t|.log ^ 9) ^ (3 / 4) * |t|.log ^ (-1 / 4) - C₂ * |t|.log ^ 2 * 2 * A / |t|.log ^ 9
Tactic:
apply sub_le_sub (by simp only [add_sub_cancel_left, σ']; exact_mod_cast le_rfl) ?_
Proof state after:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ C₂ * |t|.log ^ 2 * (σ' - σ) ≤ C₂ * |t|.log ^ 2 * 2 * A / |t|.log ^ 9
Theorem: ZetaInvBnd
Proof state before:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ C₂ * |t|.log ^ 2 * (σ' - σ) ≤ C₂ * |t|.log ^ 2 * 2 * A / |t|.log ^ 9
Tactic:
rw [mul_div_assoc, mul_assoc _ 2 _]
Proof state after:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ C₂ * |t|.log ^ 2 * (σ' - σ) ≤ C₂ * |t|.log ^ 2 * (2 * (A / |t|.log ^ 9))
Theorem: ZetaInvBnd
Proof state before:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ C₂ * |t|.log ^ 2 * (σ' - σ) ≤ C₂ * |t|.log ^ 2 * (2 * (A / |t|.log ^ 9))
Tactic:
apply mul_le_mul (by exact_mod_cast le_rfl) ?_ (by linarith [hσ.2]) (by positivity)
Proof state after:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ σ' - σ ≤ 2 * (A / |t|.log ^ 9)
Theorem: ZetaInvBnd
Proof state before:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ σ' - σ ≤ 2 * (A / |t|.log ^ 9)
Tactic:
suffices h : σ' + (1 - A / Real.log |t| ^ 9) ≤ (1 + A / Real.log |t| ^ 9) + σ by
  simp only [tsub_le_iff_right]
  convert le_sub_right_of_add_le h using 1; ring_nf; norm_cast; simp
Proof state after:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ σ' + (1 - A / |t|.log ^ 9) ≤ 1 + A / |t|.log ^ 9 + σ
Theorem: ZetaInvBnd
Proof state before:
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C₂ : ℝ
C₂pos : 0 < C₂
hC₂ :
  ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A' / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C₂ * |t|.log ^ 2 * (σ₂ - σ₁)
C₁ : ℝ := 1 / C'
A : ℝ := min A' (1 / 2 * (C₁ / (C₂ * 2)) ^ 4)
Apos : 0 < A
Ale : A ≤ 1 / 2
C : ℝ := (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Cpos : 0 < C
σ t : ℝ
t_gt : 3 < |t|
hσ : σ ∈ Ico (1 - A / |t|.log ^ 9) 1
logt_gt_one : 1 < |t|.log
σ_ge : 1 - A / |t|.log ≤ σ
left✝¹ : 0 < ⌊|t|⌋₊
left✝ : ↑⌊|t|⌋₊ ≤ |t|
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
s : ℂ := ↑σ + ↑t * I
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ s ≠ 1
s' : ℂ := ↑σ' + ↑t * I
h0 : ‖ζ s‖ ≠ 0
pos_aux : 0 < σ' - 1
⊢ σ' + (1 - A / |t|.log ^ 9) ≤ 1 + A / |t|.log ^ 9 + σ
Tactic:
exact add_le_add (by linarith) (by linarith [hσ.1])
Proof state after:
no goals