internlm/Lean-Github huggingface dataset:
Theorem: ZetaInvBnd
Proof state before:
case intro.intro
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
obtain ⟨A', hA', C₂, C₂pos, hC₂⟩ := Zeta_diff_Bnd
Proof state after:
case intro.intro.intro.intro.intro.intro
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 * (σ₂ - σ₁)
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Theorem: ZetaInvBnd
Proof state before:
case intro.intro.intro.intro.intro.intro
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 * (σ₂ - σ₁)
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
set C₁ := 1 / C'
Proof state after:
case intro.intro.intro.intro.intro.intro
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,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Theorem: ZetaInvBnd
Proof state before:
case intro.intro.intro.intro.intro.intro
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,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
let A := min A' <| (1 / 2 : ℝ) * (C₁ / (C₂ * 2)) ^ (4 : ℝ)
Proof state after:
case intro.intro.intro.intro.intro.intro
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)
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Theorem: ZetaInvBnd
Proof state before:
case intro.intro.intro.intro.intro.intro
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)
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
have Apos : 0 < A := by have := hA'.1; positivity
Proof state after:
case intro.intro.intro.intro.intro.intro
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
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Theorem: ZetaInvBnd
Proof state before:
case intro.intro.intro.intro.intro.intro
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
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
have Ale : A ≤ 1 / 2 := by dsimp only [A]; apply min_le_iff.mpr; left; exact hA'.2
Proof state after:
case intro.intro.intro.intro.intro.intro
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
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Theorem: ZetaInvBnd
Proof state before:
case intro.intro.intro.intro.intro.intro
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
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
set C := (C₁ * A ^ (3 / 4 : ℝ) - C₂ * 2 * A)⁻¹
Proof state after:
case intro.intro.intro.intro.intro.intro
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)⁻¹
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Theorem: ZetaInvBnd
Proof state before:
case intro.intro.intro.intro.intro.intro
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)⁻¹
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
have Cpos : 0 < C := by
  refine ZetaInvBnd_aux2 (by positivity) (by positivity) (by positivity) ?_
  apply min_le_iff.mpr; right; exact le_rfl
Proof state after:
case intro.intro.intro.intro.intro.intro
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
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Theorem: ZetaInvBnd
Proof state before:
case intro.intro.intro.intro.intro.intro
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
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
refine ⟨A, ⟨Apos, by linarith [hA'.2]⟩ , C, Cpos, ?_⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
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 : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Theorem: ZetaInvBnd
Proof state before:
case intro.intro.intro.intro.intro.intro
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 : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
intro σ t t_gt hσ
Proof state after:
case intro.intro.intro.intro.intro.intro
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
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Theorem: ZetaInvBnd
Proof state before:
case intro.intro.intro.intro.intro.intro
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
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
have logt_gt_one := logt_gt_one t_gt
Proof state after:
case intro.intro.intro.intro.intro.intro
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
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Theorem: ZetaInvBnd
Proof state before:
case intro.intro.intro.intro.intro.intro
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
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
have σ_ge : 1 - A / Real.log |t| ≤ σ := by
  apply le_trans ?_ hσ.1
  suffices A / Real.log |t| ^ 9 ≤ A / Real.log |t| by linarith
  exact div_le_div Apos.le (by rfl) (by positivity) <| ZetaInvBnd_aux logt_gt_one
Proof state after:
case intro.intro.intro.intro.intro.intro
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 ≤ σ
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Theorem: ZetaInvBnd
Proof state before:
case intro.intro.intro.intro.intro.intro
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 ≤ σ
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
obtain ⟨_, _, neOne⟩ := UpperBnd_aux ⟨Apos, Ale⟩ t_gt σ_ge
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
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|
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Theorem: ZetaInvBnd
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
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|
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
set σ' := 1 + A / Real.log |t| ^ 9
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
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|
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
σ' : ℝ := 1 + A / |t|.log ^ 9
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Theorem: ZetaInvBnd
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
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|
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
σ' : ℝ := 1 + A / |t|.log ^ 9
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
have σ'_gt : 1 < σ' := by simp only [σ', lt_add_iff_pos_right]; positivity
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
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|
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Theorem: ZetaInvBnd
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
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|
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
have σ'_le : σ' ≤ 2 := by
  simp only [σ']
  suffices A / Real.log |t| ^ 9 < 1 by linarith
  apply div_lt_one (by positivity) |>.mpr
  exact lt_trans₄ (by linarith) logt_gt_one <| ZetaInvBnd_aux' logt_gt_one
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
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|
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Theorem: ZetaInvBnd
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
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|
neOne : 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
σ' : ℝ := 1 + A / |t|.log ^ 9
σ'_gt : 1 < σ'
σ'_le : σ' ≤ 2
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
set s := σ + t * I
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
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
⊢ 1 / ‖ζ s‖ ≤ C * |t|.log ^ 7