[Merged by Bors] - feat: characterizations of IsBigO along atTop

[dupuisf]

This PR adds a way to characterize IsBigO along the atTop filter, for cases where we want the constant to depend on a "starting point" n₀.

It also adds the lemma tendsto_nhds_of_eventually_eq.

---

[ocfnash]

Thanks: these will be very useful lemmas but I think worth a few tweaks.

[ADedecker]

I have suggestions for this PR that I didn't yet have the time to write down, including some proof simplification. Could you wait for them before merging? I should be able to write them in a few hours.

[ADedecker]

Sorry for the delay!

[ADedecker]

Actually I have an even better suggestion: you should add

lemma exists_eventually_atTop {α : Type _} [SemilatticeSup α] [Nonempty α] {r : α → β → Prop} :
    (∃ b, ∀ᶠ a in atTop, r a b) ↔ ∀ᶠ a₀ in atTop, ∃ b, ∀ a ≥ a₀, r a b := by
  simp_rw [eventually_atTop, ← exists_swap (α := α)]
  refine exists_congr fun a ↦ .symm <| forall_ge_iff <| Monotone.exists fun _ _ _ hb H n hn ↦
    H n (hb.trans hn)

Then, your proofs become:

theorem isBigO_atTop_iff_dep_const {α : Type _} [SemilatticeSup α] [Nonempty α]
    {f : α → E} {g : α → F} : f =O[atTop] g ↔ ∀ᶠ n₀ in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖ := by
  rw [isBigO_iff, exists_eventually_atTop]

theorem isBigO_atTop_iff_dep_const' {α : Type _}
    [SemilatticeSup α] [Nonempty α] {f : α → G} {g : α → G'} :
    f =O[atTop] g ↔ ∀ᶠ n₀ in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖ := by
  simp_rw [isBigO_iff'', ← exists_prop, Subtype.exists', exists_eventually_atTop]

[dupuisf]

Thanks a lot for the suggestions, Anatole, this is indeed much nicer! I have now implemented your last version, and changed the lemma names to what Oliver suggested.

[ADedecker]

@ocfnash I don't want to pull the trigger since I made quite heavy suggestions, would you mind having a final look?

[ocfnash]

Thank you both, this is great!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style