Conversion lemmas

The main procedure of the compute_asymptotics tactic is able to compute limits of functions at atTop filter. This file contains lemmas we use to reduce other asymptotic goals to the case Tendsto f atTop l.

Main theorems

This file contains the following lemmas:

• tendsto_nhdsGT_of_tendsto_atTop for Tendsto f (𝓝[>] c) l
• tendsto_nhdsLT_of_tendsto_atTop for Tendsto f (𝓝[<] c) l
• tendsto_nhdsNE_of_tendsto_atTop for Tendsto f (𝓝[≠] c) l
• isBigO_of_div_tendsto_atTop and isBigO_of_div_tendsto_atBot for f =O[l] g

We also use lemmas from other files:

• tendsto_comp_neg_atTop_iff for Tendsto f atBot l
• IsLittleO.of_tendsto_div_atBot and IsLittleO.of_tendsto_div_atTop for f =o[l] g
• isEquivalent_of_tendsto_one for f ∼ g

theorem Tactic.ComputeAsymptotics.tendsto_nhdsGT_of_tendsto_atTop {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} (f : 𝕜 → α) (c : 𝕜) (h : Filter.Tendsto (fun (x : 𝕜) => f (c + x⁻¹)) Filter.atTop l) : Filter.Tendsto f (nhdsWithin c (Set.Ioi c)) l

theorem Tactic.ComputeAsymptotics.tendsto_nhdsLT_of_tendsto_atTop {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} (f : 𝕜 → α) (c : 𝕜) (h : Filter.Tendsto (fun (x : 𝕜) => f (c - x⁻¹)) Filter.atTop l) : Filter.Tendsto f (nhdsWithin c (Set.Iio c)) l

theorem Tactic.ComputeAsymptotics.tendsto_nhdsNE_of_tendsto_atTop {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} (f : 𝕜 → α) (c : 𝕜) (h_neg : Filter.Tendsto (fun (x : 𝕜) => f (c - x⁻¹)) Filter.atTop l) (h_pos : Filter.Tendsto (fun (x : 𝕜) => f (c + x⁻¹)) Filter.atTop l) : Filter.Tendsto f (nhdsWithin c {c}ᶜ) l

theorem Tactic.ComputeAsymptotics.tendsto_nhdsNE_of_tendsto_atTop_nhds_of_eq {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (f : 𝕜 → α) (c : 𝕜) [TopologicalSpace α] {a b : α} (h_neg : Filter.Tendsto (fun (x : 𝕜) => f (c - x⁻¹)) Filter.atTop (nhds a)) (h_pos : Filter.Tendsto (fun (x : 𝕜) => f (c + x⁻¹)) Filter.atTop (nhds b)) (h_eq : a = b) : Filter.Tendsto f (nhdsWithin c {c}ᶜ) (nhds a)

theorem Tactic.ComputeAsymptotics.isBigOWith_of_tendsto_top {C : ℝ} {f g : ℝ → ℝ} {l : Filter ℝ} (h : Filter.Tendsto (fun (x : ℝ) => g x / f x) l Filter.atTop) (hC : 0 < C) : Asymptotics.IsBigOWith C l f g

theorem Tactic.ComputeAsymptotics.isBigOWith_of_tendsto_bot {C : ℝ} {f g : ℝ → ℝ} {l : Filter ℝ} (h : Filter.Tendsto (fun (x : ℝ) => g x / f x) l Filter.atBot) (hC : 0 < C) : Asymptotics.IsBigOWith C l f g

theorem Tactic.ComputeAsymptotics.isBigO_of_div_tendsto_atTop {f g : ℝ → ℝ} {l : Filter ℝ} (h : Filter.Tendsto (fun (x : ℝ) => g x / f x) l Filter.atTop) : f =O[l] g

theorem Tactic.ComputeAsymptotics.isBigO_of_div_tendsto_atBot {f g : ℝ → ℝ} {l : Filter ℝ} (h : Filter.Tendsto (fun (x : ℝ) => g x / f x) l Filter.atBot) : f =O[l] g