Theorem: BoundedAtFilter.comp_add (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
⊢ (atTop.BoundedAtFilter fun n => u (n + N)) ↔ atTop.BoundedAtFilter u
Tactic:
simp [BoundedAtFilter, isBigO_iff]
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
⊢ (∃ c a, ∀ (b : ℕ), a ≤ b → |u (b + N)| ≤ c) ↔ ∃ c a, ∀ (b : ℕ), a ≤ b → |u b| ≤ c

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
⊢ (∃ c a, ∀ (b : ℕ), a ≤ b → |u (b + N)| ≤ c) ↔ ∃ c a, ∀ (b : ℕ), a ≤ b → |u b| ≤ c
Tactic:
constructor <;> intro ⟨C, n₀, h⟩ <;> use C
State after:
case h
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → |u b| ≤ C

case h
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u b| ≤ C
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → |u (b + N)| ≤ C

State before:
case h
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → |u b| ≤ C
Tactic:
refine ⟨n₀ + N, fun n hn => ?_⟩
State after:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
n : ℕ
hn : n₀ + N ≤ n
⊢ |u n| ≤ C

State before:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
n : ℕ
hn : n₀ + N ≤ n
⊢ |u n| ≤ C
Tactic:
obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_le' (m := N) (by linarith)
State after:
case h.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
n : ℕ
hn : n₀ + N ≤ n
k : ℕ
hk : n = k + N
⊢ |u n| ≤ C

State before:
case h.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
n : ℕ
hn : n₀ + N ≤ n
k : ℕ
hk : n = k + N
⊢ |u n| ≤ C
Tactic:
subst n
State after:
case h.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
k : ℕ
hn : n₀ + N ≤ k + N
⊢ |u (k + N)| ≤ C

State before:
case h.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
k : ℕ
hn : n₀ + N ≤ k + N
⊢ |u (k + N)| ≤ C
Tactic:
exact h _ <| Nat.add_le_add_iff_right.mp hn
State after:
no goals

State before:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
n : ℕ
hn : n₀ + N ≤ n
⊢ N ≤ ?m.960186
Tactic:
linarith
State after:
no goals

State before:
case h
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u b| ≤ C
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → |u (b + N)| ≤ C
Tactic:
exact ⟨n₀, fun n hn => h _ (by linarith)⟩
State after:
no goals

State before:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u b| ≤ C
n : ℕ
hn : n₀ ≤ n
⊢ n₀ ≤ n + N
Tactic:
linarith
State after:
no goals