Theorem: Zeta_diff_Bnd (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C),
          ∀ (σ₁ σ₂ t : ℝ),
            3 < |t| →
              1 - A / |t|.log ≤ σ₁ →
                σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Tactic:
obtain ⟨A, hA, C, Cpos, hC⟩ := ZetaDerivUpperBnd
State after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C),
          ∀ (σ₁ σ₂ t : ℝ),
            3 < |t| →
              1 - A / |t|.log ≤ σ₁ →
                σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)

State before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C),
          ∀ (σ₁ σ₂ t : ℝ),
            3 < |t| →
              1 - A / |t|.log ≤ σ₁ →
                σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Tactic:
refine ⟨A, hA, C, Cpos, ?_⟩
State after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
⊢ ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)

State before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
⊢ ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Tactic:
intro σ₁ σ₂ t t_gt σ₁_ge σ₂_le σ₁_lt_σ₂
State after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
⊢ ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)

State before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
⊢ ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Tactic:
have t_ne_zero : t ≠ 0 := by contrapose! t_gt; simp only [t_gt, abs_zero, Nat.ofNat_nonneg]
State after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)

State before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Tactic:
rw [← Zeta_eq_int_derivZeta t_ne_zero]
State after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ‖∫ (σ : ℝ) in σ₁..σ₂, deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)

State before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ‖∫ (σ : ℝ) in σ₁..σ₂, deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Tactic:
convert intervalIntegral.norm_integral_le_of_norm_le_const ?_ using 1
State after:
case h.e'_4
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ C * |t|.log ^ 2 * (σ₂ - σ₁) = ?intro.intro.intro.intro.convert_6 * |σ₂ - σ₁|

case intro.intro.intro.intro.convert_6
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ℝ

case intro.intro.intro.intro.convert_8
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ∀ x ∈ Ι σ₁ σ₂, ‖deriv ζ (↑x + ↑t * I)‖ ≤ ?intro.intro.intro.intro.convert_6

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
⊢ t ≠ 0
Tactic:
contrapose! t_gt
State after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_gt : t = 0
⊢ |t| ≤ 3

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_gt : t = 0
⊢ |t| ≤ 3
Tactic:
simp only [t_gt, abs_zero, Nat.ofNat_nonneg]
State after:
no goals

State before:
case h.e'_4
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ C * |t|.log ^ 2 * (σ₂ - σ₁) = ?intro.intro.intro.intro.convert_6 * |σ₂ - σ₁|
Tactic:
congr
State after:
case h.e'_4.e_a
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ σ₂ - σ₁ = |σ₂ - σ₁|

State before:
case h.e'_4.e_a
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ σ₂ - σ₁ = |σ₂ - σ₁|
Tactic:
rw [_root_.abs_of_nonneg (by linarith)]
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ 0 ≤ σ₂ - σ₁
Tactic:
linarith
State after:
no goals

State before:
case intro.intro.intro.intro.convert_8
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ∀ x ∈ Ι σ₁ σ₂, ‖deriv ζ (↑x + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
intro σ hσ
State after:
case intro.intro.intro.intro.convert_8
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
σ : ℝ
hσ : σ ∈ Ι σ₁ σ₂
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2

State before:
case intro.intro.intro.intro.convert_8
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
σ : ℝ
hσ : σ ∈ Ι σ₁ σ₂
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
rw [uIoc_of_le σ₁_lt_σ₂.le, mem_Ioc] at hσ
State after:
case intro.intro.intro.intro.convert_8
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
σ : ℝ
hσ : σ₁ < σ ∧ σ ≤ σ₂
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2

State before:
case intro.intro.intro.intro.convert_8
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
σ : ℝ
hσ : σ₁ < σ ∧ σ ≤ σ₂
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
exact hC σ t t_gt ⟨le_trans σ₁_ge hσ.1.le, le_trans hσ.2 σ₂_le⟩
State after:
no goals