Source indexedlemma · leanprover/lean4:v4.32.0

BoundedAtFilter.comp_add

PrimeNumberTheoremAnd.Wiener · PrimeNumberTheoremAnd/Wiener.lean:640 to 648

Mathematical statement

Exact Lean statement

lemma BoundedAtFilter.comp_add {u : ℕ → ℝ} {N : ℕ} :
    BoundedAtFilter atTop (fun n => u (n + N)) ↔ BoundedAtFilter atTop u

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma BoundedAtFilter.comp_add {u : ℕ → ℝ} {N : ℕ} :    BoundedAtFilter atTop (fun n => u (n + N)) ↔ BoundedAtFilter atTop u := by  simp only [BoundedAtFilter, isBigO_iff, norm_eq_abs, Pi.one_apply,    eventually_atTop]  constructor <;> intro ⟨C, n₀, h⟩ <;> use C  · refine ⟨n₀ + N, fun n hn => ?_⟩    obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' (m := N) (n := n) (by grind)    exact h _ <| Nat.add_le_add_iff_right.mp hn  · exact ⟨n₀, fun n hn => h _ (by grind)⟩