internlm/Lean-Github huggingface dataset:
Theorem: NormDerivZeta0Le
Proof state before:
N : ℕ
Npos : 0 < N
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ t : ℝ
σ_ge : 1 - A / |t|.log ≤ σ
σpos : 0 < σ
t_gt : 3 < |t|
s : ℂ := ↑σ + ↑t * I
⊢ let s := s;
  ‖deriv (ζ₀ N) s‖ ≤
    4 * (↑N).log *
      (‖∑ 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)‖)
Tactic:
sorry
Proof state after:
no goals
Theorem: ZetaDerivUpperBnd
Proof state before:
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
obtain ⟨A, hA, _, _, _⟩ := ZetaUpperBnd
Proof state after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Theorem: ZetaDerivUpperBnd
Proof state before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
let C := 4 * Real.exp A * (5 + 8 * 2)
Proof state after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Theorem: ZetaDerivUpperBnd
Proof state before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
refine ⟨A, hA, C, by positivity, ?_⟩
Proof state after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
⊢ ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Theorem: ZetaDerivUpperBnd
Proof state before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
⊢ ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
intro σ t t_gt ⟨σ_ge, σ_le⟩
Proof state after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Theorem: ZetaDerivUpperBnd
Proof state before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
obtain ⟨Npos, N_le_t, _, _, σPos, neOne⟩ := UpperBnd_aux hA t_gt σ_ge
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Theorem: ZetaDerivUpperBnd
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
rw [← DerivZeta0EqDerivZeta Npos (by simp [σPos]) neOne]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖deriv (ζ₀ ⌊|t|⌋₊) (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Theorem: ZetaDerivUpperBnd
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖deriv (ζ₀ ⌊|t|⌋₊) (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
apply le_trans (NormDerivZeta0Le Npos hA σ_ge σPos t_gt) ?_
Proof state after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 4 * (↑⌊|t|⌋₊).log *
      (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
            ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
          ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
        ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) ≤
    C * |t|.log ^ 2
Theorem: ZetaDerivUpperBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 4 * (↑⌊|t|⌋₊).log *
      (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
            ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
          ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
        ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) ≤
    C * |t|.log ^ 2
Tactic:
conv => rw [mul_comm 4, mul_assoc _ 4 _]; rhs; rw [sq, ← mul_assoc, mul_comm C, mul_assoc]
Proof state after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ (↑⌊|t|⌋₊).log *
      (4 *
        (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
              ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
            ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
          ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖)) ≤
    |t|.log * (C * |t|.log)
Theorem: ZetaDerivUpperBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ (↑⌊|t|⌋₊).log *
      (4 *
        (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
              ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
            ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
          ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖)) ≤
    |t|.log * (C * |t|.log)
Tactic:
refine mul_le_mul (Real.log_le_log (by positivity) N_le_t) ?_ (by positivity) (by positivity)
Proof state after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 4 *
      (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
            ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
          ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
        ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) ≤
    C * |t|.log
Theorem: ZetaDerivUpperBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 4 *
      (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
            ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
          ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
        ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) ≤
    C * |t|.log
Tactic:
simp only [C, mul_assoc, Zeta0EqZeta Npos (by simp [σPos]) neOne]
Proof state after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 4 *
      (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
            ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
          ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
        ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) ≤
    4 * (A.exp * ((5 + 8 * 2) * |t|.log))
Theorem: ZetaDerivUpperBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 4 *
      (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
            ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
          ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
        ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) ≤
    4 * (A.exp * ((5 + 8 * 2) * |t|.log))
Tactic:
refine mul_le_mul_left (by norm_num) |>.mpr ?_
Proof state after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ + ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
        ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
      ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤
    A.exp * ((5 + 8 * 2) * |t|.log)
Theorem: ZetaDerivUpperBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ + ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
        ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
      ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤
    A.exp * ((5 + 8 * 2) * |t|.log)
Tactic:
convert ZetaUpperBnd' hA t_gt ⟨σ_ge, σ_le⟩ using 1
Proof state after:
case h.e'_4
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ A.exp * ((5 + 8 * 2) * |t|.log) = A.exp * (5 + 8 * 2) * |t|.log
Theorem: ZetaDerivUpperBnd
Proof state before:
case h.e'_4
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ A.exp * ((5 + 8 * 2) * |t|.log) = A.exp * (5 + 8 * 2) * |t|.log
Tactic:
ring
Proof state after:
no goals
Theorem: ZetaDerivUpperBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
⊢ 0 < C
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaDerivUpperBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 0 < (↑σ + ↑t * I).re
Tactic:
simp [σPos]
Proof state after:
no goals
Theorem: ZetaDerivUpperBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 0 < ↑⌊|t|⌋₊
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaDerivUpperBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 0 ≤
    4 *
      (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
            ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
          ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
        ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖)
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaDerivUpperBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 0 ≤ |t|.log
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaDerivUpperBnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 0 < 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
⊢ Tendsto (fun y => f y + a) (𝓝[>] x) (𝓝[>] (f x + a))
Tactic:
refine tendsto_iff_forall_eventually_mem.mpr ?_
Proof state after:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
⊢ ∀ s ∈ 𝓝[>] (f x + a), ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ s
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
⊢ ∀ s ∈ 𝓝[>] (f x + a), ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ s
Tactic:
intro v hv
Proof state after:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v : Set ℝ
hv : v ∈ 𝓝[>] (f x + a)
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v : Set ℝ
hv : v ∈ 𝓝[>] (f x + a)
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
Tactic:
simp only [mem_nhdsWithin] at hv
Proof state after:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v : Set ℝ
hv : ∃ u, IsOpen u ∧ f x + a ∈ u ∧ u ∩ Ioi (f x + a) ⊆ v
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v : Set ℝ
hv : ∃ u, IsOpen u ∧ f x + a ∈ u ∧ u ∩ Ioi (f x + a) ⊆ v
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
Tactic:
obtain ⟨u, hu, hu2, hu3⟩ := hv
Proof state after:
case intro.intro.intro
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case intro.intro.intro
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
Tactic:
let t := {x | f x + a ∈ u}
Proof state after:
case intro.intro.intro
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case intro.intro.intro
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
Tactic:
have : t ∩ Ioi x ∈ 𝓝[>] x := by
  simp only [mem_nhdsWithin]
  use t
  simp only [subset_inter_iff, inter_subset_left, inter_subset_right, and_self,
    and_true, t]
  simp
  refine ⟨?_, by simp [hu2]⟩
  simp [Metric.isOpen_iff] at hu ⊢
  intro x hx
  obtain ⟨ε, εpos, hε⟩ := hu (f x + a) hx
  simp only [Metric.ball, dist_sub_eq_dist_add_right, setOf_subset_setOf] at hε ⊢
  exact ⟨ε, εpos, fun _ hy ↦ hε (by simp [isometry_iff_dist_eq.mp f_iso, hy])⟩
Proof state after:
case intro.intro.intro
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case intro.intro.intro
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
Tactic:
filter_upwards [this]
Proof state after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
⊢ ∀ a_1 ∈ t ∩ Ioi x, f a_1 + a ∈ v
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
⊢ ∀ a_1 ∈ t ∩ Ioi x, f a_1 + a ∈ v
Tactic:
intro b hb
Proof state after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : b ∈ t ∩ Ioi x
⊢ f b + a ∈ v
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : b ∈ t ∩ Ioi x
⊢ f b + a ∈ v
Tactic:
simp only [mem_inter_iff, mem_setOf_eq, mem_Ioi, t] at hb
Proof state after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : f b + a ∈ u ∧ x < b
⊢ f b + a ∈ v
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : f b + a ∈ u ∧ x < b
⊢ f b + a ∈ v
Tactic:
refine hu3 ?_
Proof state after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : f b + a ∈ u ∧ x < b
⊢ f b + a ∈ u ∩ Ioi (f x + a)
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : f b + a ∈ u ∧ x < b
⊢ f b + a ∈ u ∩ Ioi (f x + a)
Tactic:
simp only [mem_inter_iff, mem_Ioi, add_lt_add_iff_right]
Proof state after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : f b + a ∈ u ∧ x < b
⊢ f b + a ∈ u ∧ f x < f b
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : f b + a ∈ u ∧ x < b
⊢ f b + a ∈ u ∧ f x < f b
Tactic:
exact ⟨hb.1, f_mono hb.2⟩
Proof state after:
no goals
Theorem: Tendsto_nhdsWithin_punctured_map_add
Proof state before:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ t ∩ Ioi x ∈ 𝓝[>] x
Tactic:
simp only [mem_nhdsWithin]
Proof state after:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ Ioi x ⊆ t ∩ Ioi x