Theorem: bounded_of_shift (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
h : atTop.BoundedAtFilter (shift u)
⊢ atTop.BoundedAtFilter u
Tactic:
simp only [BoundedAtFilter, isBigO_iff, eventually_atTop] at h ⊢
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
h : ∃ c a, ∀ b ≥ a, ‖shift u b‖ ≤ c * ‖OfNat.ofNat 1 b‖
⊢ ∃ c a, ∀ b ≥ a, ‖u b‖ ≤ c * ‖OfNat.ofNat 1 b‖

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
h : ∃ c a, ∀ b ≥ a, ‖shift u b‖ ≤ c * ‖OfNat.ofNat 1 b‖
⊢ ∃ c a, ∀ b ≥ a, ‖u b‖ ≤ c * ‖OfNat.ofNat 1 b‖
Tactic:
obtain ⟨C, N, hC⟩ := h
State after:
case intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖shift u b‖ ≤ C * ‖OfNat.ofNat 1 b‖
⊢ ∃ c a, ∀ b ≥ a, ‖u b‖ ≤ c * ‖OfNat.ofNat 1 b‖

State before:
case intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖shift u b‖ ≤ C * ‖OfNat.ofNat 1 b‖
⊢ ∃ c a, ∀ b ≥ a, ‖u b‖ ≤ c * ‖OfNat.ofNat 1 b‖
Tactic:
refine ⟨C, N + 1, fun n hn => ?_⟩
State after:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖shift u b‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖

State before:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖shift u b‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖
Tactic:
simp only [shift] at hC
State after:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖u (b + 1)‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖

State before:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖u (b + 1)‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖
Tactic:
have r1 : n - 1 ≥ N := Nat.le_sub_one_of_lt hn
State after:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖u (b + 1)‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
r1 : n - 1 ≥ N
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖

State before:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖u (b + 1)‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
r1 : n - 1 ≥ N
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖
Tactic:
have r2 : n - 1 + 1 = n := Nat.sub_add_cancel <| NeZero.one_le.trans hn.le
State after:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖u (b + 1)‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
r1 : n - 1 ≥ N
r2 : n - 1 + 1 = n
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖

State before:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖u (b + 1)‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
r1 : n - 1 ≥ N
r2 : n - 1 + 1 = n
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖
Tactic:
simpa [r2] using hC (n - 1) r1
State after:
no goals