Mathlib.Topology.Algebra.Order.Field

IsStrictOrderedRing.topologicalRing instance

: IsTopologicalRing 𝕜

Full source

instance (priority := 100) IsStrictOrderedRing.topologicalRing : IsTopologicalRing 𝕜 :=
  .of_norm abs abs_nonneg (fun _ _ ↦ (abs_mul _ _).le) <| by
    simpa using nhds_basis_abs_sub_lt (0 : 𝕜)

Strict Ordered Rings are Topological Rings

Informal description

Every strict ordered ring $\mathbb{K}$ with the order topology is a topological ring, meaning that the operations of addition, multiplication, and negation are continuous with respect to the order topology.

Filter.Tendsto.atTop_mul_pos theorem

{C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atTop) (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atTop

Full source

/-- In a linearly ordered field with the order topology, if `f` tends to `Filter.atTop` and `g`
tends to a positive constant `C` then `f * g` tends to `Filter.atTop`. -/
theorem Filter.Tendsto.atTop_mul_pos {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atTop)
    (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atTop := by
  refine tendsto_atTop_mono' _ ?_ (hf.atTop_mul_const (half_pos hC))
  filter_upwards [hg.eventually (lt_mem_nhds (half_lt_self hC)), hf.eventually_ge_atTop 0] with x hg
    hf using mul_le_mul_of_nonneg_left hg.le hf

Product of a Function Tending to Infinity and a Positive Function Tending to a Positive Constant Tends to Infinity

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology, and let $f, g : \alpha \to \mathbb{K}$ be functions. If $f$ tends to $+\infty$ along a filter $l$ and $g$ tends to a positive constant $C$ along $l$, then the product function $x \mapsto f(x) \cdot g(x)$ tends to $+\infty$ along $l$.

Filter.Tendsto.pos_mul_atTop theorem

{C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop

Full source

/-- In a linearly ordered field with the order topology, if `f` tends to a positive constant `C` and
`g` tends to `Filter.atTop` then `f * g` tends to `Filter.atTop`. -/
theorem Filter.Tendsto.pos_mul_atTop {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (𝓝 C))
    (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop := by
  simpa only [mul_comm] using hg.atTop_mul_pos hC hf

Product of a Positive Limit and an Unbounded Function Tends to Infinity ($C > 0 \implies C \cdot \infty = \infty$)

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology, and let $f, g : \alpha \to \mathbb{K}$ be functions. If $f$ tends to a positive constant $C$ along a filter $l$ and $g$ tends to $+\infty$ along $l$, then the product function $x \mapsto f(x) \cdot g(x)$ tends to $+\infty$ along $l$.

Filter.Tendsto.atTop_mul_neg theorem

{C : 𝕜} (hC : C < 0) (hf : Tendsto f l atTop) (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atBot

Full source

/-- In a linearly ordered field with the order topology, if `f` tends to `Filter.atTop` and `g`
tends to a negative constant `C` then `f * g` tends to `Filter.atBot`. -/
theorem Filter.Tendsto.atTop_mul_neg {C : 𝕜} (hC : C < 0) (hf : Tendsto f l atTop)
    (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atBot := by
  have := hf.atTop_mul_pos (neg_pos.2 hC) hg.neg
  simpa only [Function.comp_def, neg_mul_eq_mul_neg, neg_neg] using
    tendsto_neg_atTop_atBot.comp this

Product of a Function Tending to Infinity and a Negative Function Tending to a Negative Constant Tends to Negative Infinity

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology, and let $f, g : \alpha \to \mathbb{K}$ be functions. If $f$ tends to $+\infty$ along a filter $l$ and $g$ tends to a negative constant $C$ along $l$, then the product function $x \mapsto f(x) \cdot g(x)$ tends to $-\infty$ along $l$.

Filter.Tendsto.neg_mul_atTop theorem

{C : 𝕜} (hC : C < 0) (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atBot

Full source

/-- In a linearly ordered field with the order topology, if `f` tends to a negative constant `C` and
`g` tends to `Filter.atTop` then `f * g` tends to `Filter.atBot`. -/
theorem Filter.Tendsto.neg_mul_atTop {C : 𝕜} (hC : C < 0) (hf : Tendsto f l (𝓝 C))
    (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atBot := by
  simpa only [mul_comm] using hg.atTop_mul_neg hC hf

Product of a Negative Limit and an Unbounded Function Tends to Negative Infinity ($C < 0 \implies C \cdot \infty = -\infty$)

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology, and let $f, g : \alpha \to \mathbb{K}$ be functions. If $f$ tends to a negative constant $C$ along a filter $l$ and $g$ tends to $+\infty$ along $l$, then the product function $x \mapsto f(x) \cdot g(x)$ tends to $-\infty$ along $l$.

Filter.Tendsto.atBot_mul_pos theorem

{C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atBot) (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atBot

Full source

/-- In a linearly ordered field with the order topology, if `f` tends to `Filter.atBot` and `g`
tends to a positive constant `C` then `f * g` tends to `Filter.atBot`. -/
theorem Filter.Tendsto.atBot_mul_pos {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atBot)
    (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atBot := by
  have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul_pos hC hg
  simpa [Function.comp_def] using tendsto_neg_atTop_atBot.comp this

Product of a Function Tending to Negative Infinity and a Positive Function Tending to a Positive Constant Tends to Negative Infinity

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology, and let $f, g : \alpha \to \mathbb{K}$ be functions. If $f$ tends to $-\infty$ along a filter $l$ and $g$ tends to a positive constant $C$ along $l$, then the product function $x \mapsto f(x) \cdot g(x)$ tends to $-\infty$ along $l$.

Filter.Tendsto.atBot_mul_neg theorem

{C : 𝕜} (hC : C < 0) (hf : Tendsto f l atBot) (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atTop

Full source

/-- In a linearly ordered field with the order topology, if `f` tends to `Filter.atBot` and `g`
tends to a negative constant `C` then `f * g` tends to `Filter.atTop`. -/
theorem Filter.Tendsto.atBot_mul_neg {C : 𝕜} (hC : C < 0) (hf : Tendsto f l atBot)
    (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atTop := by
  have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul_neg hC hg
  simpa [Function.comp_def] using tendsto_neg_atBot_atTop.comp this

Product of a Function Tending to Negative Infinity and a Negative Function Tending to a Negative Constant Tends to Positive Infinity

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology, and let $f, g : \alpha \to \mathbb{K}$ be functions. If $f$ tends to $-\infty$ along a filter $l$ and $g$ tends to a negative constant $C$ along $l$, then the product function $x \mapsto f(x) \cdot g(x)$ tends to $+\infty$ along $l$.

Filter.Tendsto.pos_mul_atBot theorem

{C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atBot

Full source

/-- In a linearly ordered field with the order topology, if `f` tends to a positive constant `C` and
`g` tends to `Filter.atBot` then `f * g` tends to `Filter.atBot`. -/
theorem Filter.Tendsto.pos_mul_atBot {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (𝓝 C))
    (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atBot := by
  simpa only [mul_comm] using hg.atBot_mul_pos hC hf

Product of a Positive Limit and a Function Tending to Negative Infinity Tends to Negative Infinity

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology, and let $f, g : \alpha \to \mathbb{K}$ be functions. If $f$ tends to a positive constant $C$ along a filter $l$ and $g$ tends to $-\infty$ along $l$, then the product function $x \mapsto f(x) \cdot g(x)$ tends to $-\infty$ along $l$.

Filter.Tendsto.neg_mul_atBot theorem

{C : 𝕜} (hC : C < 0) (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atTop

Full source

/-- In a linearly ordered field with the order topology, if `f` tends to a negative constant `C` and
`g` tends to `Filter.atBot` then `f * g` tends to `Filter.atTop`. -/
theorem Filter.Tendsto.neg_mul_atBot {C : 𝕜} (hC : C < 0) (hf : Tendsto f l (𝓝 C))
    (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atTop := by
  simpa only [mul_comm] using hg.atBot_mul_neg hC hf

Product of a Negative Limit and a Function Tending to Negative Infinity Tends to Positive Infinity

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology, and let $f, g : \alpha \to \mathbb{K}$ be functions. If $f$ tends to a negative constant $C$ along a filter $l$ and $g$ tends to $-\infty$ along $l$, then the product function $x \mapsto f(x) \cdot g(x)$ tends to $+\infty$ along $l$.

inv_atTop₀ theorem

: (atTop : Filter 𝕜)⁻¹ = 𝓝[>] 0

Full source

@[simp]
lemma inv_atTop₀ : (atTop : Filter 𝕜)⁻¹ = 𝓝[>] 0 :=
  (((atTop_basis_Ioi' (0 : 𝕜)).map _).comp_surjective inv_surjective).eq_of_same_basis <|
    (nhdsGT_basis _).congr (by simp) fun a ha ↦ by simp [inv_Ioi₀ (inv_pos.2 ha)]

Inverse of Positive Infinity Filter Equals Right Neighborhood at Zero

Informal description

The inverse of the filter `atTop` (representing limits tending to positive infinity) on a linearly ordered field $\mathbb{K}$ is equal to the right neighborhood filter at zero, i.e., $(atTop)^{-1} = \mathcal{N}_{>}(0)$.

inv_atBot₀ theorem

: (atBot : Filter 𝕜)⁻¹ = 𝓝[<] 0

Full source

@[simp]
lemma inv_atBot₀ : (atBot : Filter 𝕜)⁻¹ = 𝓝[<] 0 :=
  (((atBot_basis_Iio' (0 : 𝕜)).map _).comp_surjective inv_surjective).eq_of_same_basis <|
    (nhdsLT_basis _).congr (by simp) fun a ha ↦ by simp [inv_Iio₀ (inv_neg''.2 ha)]

Inverse of Negative Infinity Filter Equals Left Neighborhood at Zero

Informal description

The inverse of the filter `atBot` (representing limits tending to negative infinity) on a linearly ordered field $\mathbb{K}$ is equal to the left neighborhood filter at zero, i.e., $(atBot)^{-1} = \mathcal{N}_{<}(0)$.

inv_nhdsGT_zero theorem

: (𝓝[>] (0 : 𝕜))⁻¹ = atTop

Full source

@[simp]
lemma inv_nhdsGT_zero : (𝓝[>] (0 : 𝕜))⁻¹ = atTop := by rw [← inv_atTop₀, inv_inv]

Inverse of Right Neighborhood at Zero Equals Filter at Positive Infinity

Informal description

The inverse of the right neighborhood filter at zero in a linearly ordered field $\mathbb{K}$ is equal to the filter at positive infinity, i.e., $(\mathcal{N}_{>}(0))^{-1} = \text{atTop}$.

inv_nhdsLT_zero theorem

: (𝓝[<] (0 : 𝕜))⁻¹ = atBot

Full source

@[simp]
lemma inv_nhdsLT_zero : (𝓝[<] (0 : 𝕜))⁻¹ = atBot := by
  rw [← inv_atBot₀, inv_inv]

Inverse of Left Neighborhood at Zero Equals Filter at Negative Infinity

Informal description

In a linearly ordered field $\mathbb{K}$ with the order topology, the inverse of the left neighborhood filter at zero is equal to the filter at negative infinity. That is, $(\mathcal{N}_{<}(0))^{-1} = \text{atBot}$.

tendsto_inv_nhdsGT_zero theorem

: Tendsto (fun x : 𝕜 => x⁻¹) (𝓝[>] (0 : 𝕜)) atTop

Full source

/-- The function `x ↦ x⁻¹` tends to `+∞` on the right of `0`. -/
theorem tendsto_inv_nhdsGT_zero : Tendsto (fun x : 𝕜 => x⁻¹) (𝓝[>] (0 : 𝕜)) atTop :=
  inv_nhdsGT_zero.le

Right Limit of Inverse at Zero: $\lim_{x \to 0^+} x^{-1} = +\infty$

Informal description

The function $x \mapsto x^{-1}$ tends to $+\infty$ as $x$ approaches $0$ from the right in a linearly ordered field $\mathbb{K}$ with the order topology. That is, for any neighborhood $V$ of $+\infty$ in $\mathbb{K}$, there exists a right neighborhood $U$ of $0$ such that for all $x \in U$ with $x > 0$, $x^{-1} \in V$.

tendsto_inv_atTop_nhdsGT_zero theorem

: Tendsto (fun r : 𝕜 => r⁻¹) atTop (𝓝[>] (0 : 𝕜))

Full source

/-- The function `r ↦ r⁻¹` tends to `0` on the right as `r → +∞`. -/
theorem tendsto_inv_atTop_nhdsGT_zero : Tendsto (fun r : 𝕜 => r⁻¹) atTop (𝓝[>] (0 : 𝕜)) :=
  inv_atTop₀.le

Right Limit of Inverse at Infinity: $\lim_{r \to +\infty} r^{-1} = 0^+$

Informal description

The function $r \mapsto r^{-1}$ tends to $0$ from the right as $r$ tends to positive infinity in a linearly ordered field $\mathbb{K}$ with the order topology. That is, for any neighborhood $U$ of $0$ in $\mathbb{K}$ restricted to positive elements, there exists $M > 0$ such that for all $r > M$, $r^{-1} \in U$.

tendsto_inv_atTop_zero theorem

: Tendsto (fun r : 𝕜 => r⁻¹) atTop (𝓝 0)

Full source

theorem tendsto_inv_atTop_zero : Tendsto (fun r : 𝕜 => r⁻¹) atTop (𝓝 0) :=
  tendsto_inv_atTop_nhdsGT_zero.mono_right inf_le_left

Limit of Inverse at Infinity: $\lim_{r \to +\infty} r^{-1} = 0$

Informal description

The function $r \mapsto r^{-1}$ tends to $0$ as $r$ tends to positive infinity in a linearly ordered field $\mathbb{K}$ with the order topology. That is, for any neighborhood $U$ of $0$ in $\mathbb{K}$, there exists $M > 0$ such that for all $r > M$, $r^{-1} \in U$.

tendsto_inv_zero_atBot theorem

: Tendsto (fun x : 𝕜 => x⁻¹) (𝓝[<] (0 : 𝕜)) atBot

Full source

/-- The function `x ↦ x⁻¹` tends to `-∞` on the left of `0`. -/
theorem tendsto_inv_zero_atBot : Tendsto (fun x : 𝕜 => x⁻¹) (𝓝[<] (0 : 𝕜)) atBot :=
  inv_nhdsLT_zero.le

Left Limit of Inverse at Zero: $\lim_{x \to 0^-} \frac{1}{x} = -\infty$

Informal description

In a linearly ordered field $\mathbb{K}$ with the order topology, the function $x \mapsto x^{-1}$ tends to $-\infty$ as $x$ approaches $0$ from the left. That is, $\lim_{x \to 0^-} \frac{1}{x} = -\infty$.

tendsto_inv_atBot_zero' theorem

: Tendsto (fun r : 𝕜 => r⁻¹) atBot (𝓝[<] (0 : 𝕜))

Full source

/-- The function `r ↦ r⁻¹` tends to `0` on the left as `r → -∞`. -/
theorem tendsto_inv_atBot_zero' : Tendsto (fun r : 𝕜 => r⁻¹) atBot (𝓝[<] (0 : 𝕜)) :=
  inv_atBot₀.le

Left Limit of Inverse at Negative Infinity: $\lim_{r \to -\infty} \frac{1}{r} = 0^-$

Informal description

The function $r \mapsto r^{-1}$ tends to $0$ from the left as $r$ tends to $-\infty$ in a linearly ordered field $\mathbb{K}$. That is, $\lim_{r \to -\infty} \frac{1}{r} = 0^-$.

tendsto_inv_atBot_zero theorem

: Tendsto (fun r : 𝕜 => r⁻¹) atBot (𝓝 0)

Full source

theorem tendsto_inv_atBot_zero : Tendsto (fun r : 𝕜 => r⁻¹) atBot (𝓝 0) :=
  tendsto_inv_atBot_zero'.mono_right inf_le_left

Limit of Inverse at Negative Infinity: $\lim_{r \to -\infty} \frac{1}{r} = 0$

Informal description

The function $r \mapsto r^{-1}$ tends to $0$ as $r$ tends to $-\infty$ in a linearly ordered field $\mathbb{K}$. That is, $\lim_{r \to -\infty} \frac{1}{r} = 0$.

Filter.Tendsto.div_atTop theorem

{a : 𝕜} (h : Tendsto f l (𝓝 a)) (hg : Tendsto g l atTop) : Tendsto (fun x => f x / g x) l (𝓝 0)

Full source

theorem Filter.Tendsto.div_atTop {a : 𝕜} (h : Tendsto f l (𝓝 a)) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x / g x) l (𝓝 0) := by
  simp only [div_eq_mul_inv]
  exact mul_zero a ▸ h.mul (tendsto_inv_atTop_zero.comp hg)

Limit of Quotient with Divergent Denominator: $\lim_{x \to l} \frac{f(x)}{g(x)} = 0$ when $f(x) \to a$ and $g(x) \to +\infty$

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology. Given functions $f, g : \alpha \to \mathbb{K}$ and a filter $l$ on $\alpha$, if $f$ tends to $a \in \mathbb{K}$ along $l$ and $g$ tends to $+\infty$ along $l$, then the function $x \mapsto f(x) / g(x)$ tends to $0$ along $l$. In symbols: \[ \left(f \underset{l}{\to} a \text{ and } g \underset{l}{\to} +\infty\right) \implies \left(\frac{f}{g} \underset{l}{\to} 0\right) \]

Filter.Tendsto.div_atBot theorem

{a : 𝕜} (h : Tendsto f l (𝓝 a)) (hg : Tendsto g l atBot) : Tendsto (fun x => f x / g x) l (𝓝 0)

Full source

theorem Filter.Tendsto.div_atBot {a : 𝕜} (h : Tendsto f l (𝓝 a)) (hg : Tendsto g l atBot) :
    Tendsto (fun x => f x / g x) l (𝓝 0) := by
  simp only [div_eq_mul_inv]
  exact mul_zero a ▸ h.mul (tendsto_inv_atBot_zero.comp hg)

Limit of Quotient with Divergent Denominator: $\lim_{x \to l} \frac{f(x)}{g(x)} = 0$ when $f(x) \to a$ and $g(x) \to -\infty$

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology. Given functions $f, g : \alpha \to \mathbb{K}$ and a filter $l$ on $\alpha$, if $f$ tends to $a \in \mathbb{K}$ along $l$ and $g$ tends to $-\infty$ along $l$, then the function $x \mapsto f(x) / g(x)$ tends to $0$ along $l$. In symbols: \[ \left(f \underset{l}{\to} a \text{ and } g \underset{l}{\to} -\infty\right) \implies \left(\frac{f}{g} \underset{l}{\to} 0\right) \]

Filter.Tendsto.const_div_atTop theorem

(hg : Tendsto g l atTop) (r : 𝕜) : Tendsto (fun n ↦ r / g n) l (𝓝 0)

Full source

lemma Filter.Tendsto.const_div_atTop (hg : Tendsto g l atTop) (r : 𝕜)  :
    Tendsto (fun n ↦ r / g n) l (𝓝 0) :=
  tendsto_const_nhds.div_atTop hg

Limit of Constant Divided by Divergent Function: $\frac{r}{g} \to 0$ as $g \to +\infty$

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology. Given a function $g : \alpha \to \mathbb{K}$ and a filter $l$ on $\alpha$, if $g$ tends to $+\infty$ along $l$, then for any constant $r \in \mathbb{K}$, the function $n \mapsto r / g(n)$ tends to $0$ along $l$. In symbols: \[ g \underset{l}{\to} +\infty \implies \left(\frac{r}{g} \underset{l}{\to} 0\right) \]

Filter.Tendsto.const_div_atBot theorem

(hg : Tendsto g l atBot) (r : 𝕜) : Tendsto (fun n ↦ r / g n) l (𝓝 0)

Full source

lemma Filter.Tendsto.const_div_atBot (hg : Tendsto g l atBot) (r : 𝕜)  :
    Tendsto (fun n ↦ r / g n) l (𝓝 0) :=
  tendsto_const_nhds.div_atBot hg

Limit of Constant Divided by Divergent Function: $\frac{r}{g} \to 0$ as $g \to -\infty$

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology. Given a function $g : \alpha \to \mathbb{K}$ and a filter $l$ on $\alpha$, if $g$ tends to $-\infty$ along $l$, then for any constant $r \in \mathbb{K}$, the function $n \mapsto r / g(n)$ tends to $0$ along $l$. In symbols: \[ g \underset{l}{\to} -\infty \implies \left(\frac{r}{g} \underset{l}{\to} 0\right) \]

Filter.Tendsto.inv_tendsto_atTop theorem

(h : Tendsto f l atTop) : Tendsto f⁻¹ l (𝓝 0)

Full source

theorem Filter.Tendsto.inv_tendsto_atTop (h : Tendsto f l atTop) : Tendsto f⁻¹ l (𝓝 0) :=
  tendsto_inv_atTop_zero.comp h

Limit of inverse function at infinity: $\lim_{x \to l} f(x) = +\infty \implies \lim_{x \to l} f(x)^{-1} = 0$

Informal description

Let $f$ be a function such that $f$ tends to positive infinity as its argument tends to some limit point (with respect to the filter $l$). Then the inverse function $f^{-1}$ tends to $0$ as the argument tends to the same limit point.

Filter.Tendsto.inv_tendsto_atBot theorem

(h : Tendsto f l atBot) : Tendsto f⁻¹ l (𝓝 0)

Full source

theorem Filter.Tendsto.inv_tendsto_atBot (h : Tendsto f l atBot) : Tendsto f⁻¹ l (𝓝 0) :=
  tendsto_inv_atBot_zero.comp h

Limit of reciprocal at negative infinity: $\lim_{x \to -\infty} f(x)^{-1} = 0$

Informal description

Let $f$ be a function from a type $\alpha$ to a linearly ordered field $\mathbb{K}$ with the order topology. If $f$ tends to $-\infty$ (i.e., $\lim_{x \to l} f(x) = -\infty$), then the reciprocal function $f^{-1}$ tends to $0$ (i.e., $\lim_{x \to l} f(x)^{-1} = 0$).

Filter.Tendsto.inv_tendsto_nhdsGT_zero theorem

(h : Tendsto f l (𝓝[>] 0)) : Tendsto f⁻¹ l atTop

Full source

theorem Filter.Tendsto.inv_tendsto_nhdsGT_zero (h : Tendsto f l (𝓝[>] 0)) : Tendsto f⁻¹ l atTop :=
  tendsto_inv_nhdsGT_zero.comp h

Right limit of reciprocal: $\lim_{x \to 0^+} f(x)^{-1} = +\infty$ when $\lim_{x \to l} f(x) = 0^+$

Informal description

Let $f$ be a function from a type $\alpha$ to a linearly ordered field $\mathbb{K}$ with the order topology. If $f$ tends to $0$ from the right (i.e., $\lim_{x \to l} f(x) = 0^+$), then the reciprocal function $f^{-1}$ tends to $+\infty$ (i.e., $\lim_{x \to l} f(x)^{-1} = +\infty$).

Filter.Tendsto.inv_tendsto_nhdsLT_zero theorem

(h : Tendsto f l (𝓝[<] 0)) : Tendsto f⁻¹ l atBot

Full source

theorem Filter.Tendsto.inv_tendsto_nhdsLT_zero (h : Tendsto f l (𝓝[<] 0)) : Tendsto f⁻¹ l atBot :=
  tendsto_inv_zero_atBot.comp h

Left limit of reciprocal: $\lim_{x \to 0^-} f(x)^{-1} = -\infty$ when $\lim_{x \to l} f(x) = 0^-$

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology, and let $f : \alpha \to \mathbb{K}$ be a function. If $f$ tends to $0$ from the left along a filter $l$ (i.e., $\lim_{x \to l} f(x) = 0^-$), then the reciprocal function $f^{-1}$ tends to $-\infty$ along $l$ (i.e., $\lim_{x \to l} f(x)^{-1} = -\infty$).

bdd_le_mul_tendsto_zero' theorem

 {f g : α → 𝕜} (C : 𝕜) (hf : ∀ᶠ x in l, |f x| ≤ C) (hg : Tendsto g l (𝓝 0)) : Tendsto (fun x ↦ f x * g x) l (𝓝 0)

Full source

/-- If `g` tends to zero and there exists a constant `C : 𝕜` such that eventually `|f x| ≤ C`,
  then the product `f * g` tends to zero. -/
theorem bdd_le_mul_tendsto_zero' {f g : α → 𝕜} (C : 𝕜) (hf : ∀ᶠ x in l, |f x| ≤ C)
    (hg : Tendsto g l (𝓝 0)) : Tendsto (fun x ↦ f x * g x) l (𝓝 0) := by
  rw [tendsto_zero_iff_abs_tendsto_zero]
  have hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0) := by
    convert (hg.const_mul C).abs
    simp_rw [mul_zero, abs_zero]
  apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hC
  · filter_upwards [hf] with x _ using abs_nonneg _
  · filter_upwards [hf] with x hx
    simp only [comp_apply, abs_mul]
    exact mul_le_mul_of_nonneg_right (hx.trans (le_abs_self C)) (abs_nonneg _)

Bounded function multiplied by zero-tending function tends to zero

Informal description

Let $\mathbb{K}$ be a linearly ordered field with order topology, and let $f, g : \alpha \to \mathbb{K}$ be functions. If there exists a constant $C \in \mathbb{K}$ such that eventually $|f(x)| \leq C$ for all $x$ in a filter $l$ on $\alpha$, and $g$ tends to $0$ along $l$, then the product function $f \cdot g$ tends to $0$ along $l$.

bdd_le_mul_tendsto_zero theorem

 {f g : α → 𝕜} {b B : 𝕜} (hb : ∀ᶠ x in l, b ≤ f x) (hB : ∀ᶠ x in l, f x ≤ B) (hg : Tendsto g l (𝓝 0)) :
  Tendsto (fun x ↦ f x * g x) l (𝓝 0)

Full source

/-- If `g` tends to zero and there exist constants `b B : 𝕜` such that eventually `b ≤ f x| ≤ B`,
  then the product `f * g` tends to zero. -/
theorem bdd_le_mul_tendsto_zero {f g : α → 𝕜} {b B : 𝕜} (hb : ∀ᶠ x in l, b ≤ f x)
    (hB : ∀ᶠ x in l, f x ≤ B) (hg : Tendsto g l (𝓝 0)) :
    Tendsto (fun x ↦ f x * g x) l (𝓝 0) := by
  set C := max |b| |B|
  have hbC : -C ≤ b := neg_le.mpr (le_max_of_le_left (neg_le_abs b))
  have hBC : B ≤ C := le_max_of_le_right (le_abs_self B)
  apply bdd_le_mul_tendsto_zero' C _ hg
  filter_upwards [hb, hB]
  exact fun x hbx hBx ↦ abs_le.mpr ⟨hbC.trans hbx, hBx.trans hBC⟩

Bounded function multiplied by zero-tending function tends to zero

Informal description

Let $\mathbb{K}$ be a linearly ordered field with order topology, and let $f, g : \alpha \to \mathbb{K}$ be functions. If there exist constants $b, B \in \mathbb{K}$ such that eventually $b \leq f(x) \leq B$ for all $x$ in a filter $l$ on $\alpha$, and $g$ tends to $0$ along $l$, then the product function $f \cdot g$ tends to $0$ along $l$.

tendsto_bdd_div_atTop_nhds_zero theorem

 {f g : α → 𝕜} {b B : 𝕜} (hb : ∀ᶠ x in l, b ≤ f x) (hB : ∀ᶠ x in l, f x ≤ B) (hg : Tendsto g l atTop) :
  Tendsto (fun x => f x / g x) l (𝓝 0)

Full source

/-- If `g` tends to `atTop` and there exist constants `b B : 𝕜` such that eventually
  `b ≤ f x| ≤ B`, then the quotient `f / g` tends to zero. -/
theorem tendsto_bdd_div_atTop_nhds_zero {f g : α → 𝕜} {b B : 𝕜}
    (hb : ∀ᶠ x in l, b ≤ f x) (hB : ∀ᶠ x in l, f x ≤ B) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x / g x) l (𝓝 0) := by
  simp only [div_eq_mul_inv]
  exact bdd_le_mul_tendsto_zero hb hB hg.inv_tendsto_atTop

Bounded function divided by infinity-tending function tends to zero

Informal description

Let $\mathbb{K}$ be a linearly ordered field with order topology, and let $f, g : \alpha \to \mathbb{K}$ be functions. If there exist constants $b, B \in \mathbb{K}$ such that eventually $b \leq f(x) \leq B$ for all $x$ in a filter $l$ on $\alpha$, and $g$ tends to $+\infty$ along $l$, then the quotient function $f / g$ tends to $0$ along $l$.

tendsto_pow_neg_atTop theorem

{n : ℕ} (hn : n ≠ 0) : Tendsto (fun x : 𝕜 => x ^ (-(n : ℤ))) atTop (𝓝 0)

Full source

/-- The function `x^(-n)` tends to `0` at `+∞` for any positive natural `n`.
A version for positive real powers exists as `tendsto_rpow_neg_atTop`. -/
theorem tendsto_pow_neg_atTop {n : ℕ} (hn : n ≠ 0) :
    Tendsto (fun x : 𝕜 => x ^ (-(n : ℤ))) atTop (𝓝 0) := by
  simpa only [zpow_neg, zpow_natCast] using (tendsto_pow_atTop (α := 𝕜) hn).inv_tendsto_atTop

Limit of Negative Power at Infinity: $x^{-n} \to 0$ as $x \to +\infty$ for $n > 0$

Informal description

For any positive natural number $n$, the function $x \mapsto x^{-n}$ tends to $0$ as $x$ tends to $+\infty$ in a linearly ordered field $\mathbb{K}$.

tendsto_zpow_atTop_zero theorem

{n : ℤ} (hn : n < 0) : Tendsto (fun x : 𝕜 => x ^ n) atTop (𝓝 0)

Full source

theorem tendsto_zpow_atTop_zero {n : ℤ} (hn : n < 0) :
    Tendsto (fun x : 𝕜 => x ^ n) atTop (𝓝 0) := by
  lift -n to ℕ using le_of_lt (neg_pos.mpr hn) with N h
  rw [← neg_pos, ← h, Nat.cast_pos] at hn
  simpa only [h, neg_neg] using tendsto_pow_neg_atTop hn.ne'

Limit of Negative Integer Power at Infinity: $x^n \to 0$ as $x \to +\infty$ for $n < 0$

Informal description

For any negative integer $n$ and any linearly ordered field $\mathbb{K}$ with the order topology, the function $x \mapsto x^n$ tends to $0$ as $x$ tends to $+\infty$.

tendsto_const_mul_zpow_atTop_zero theorem

{n : ℤ} {c : 𝕜} (hn : n < 0) : Tendsto (fun x => c * x ^ n) atTop (𝓝 0)

Full source

theorem tendsto_const_mul_zpow_atTop_zero {n : ℤ} {c : 𝕜} (hn : n < 0) :
    Tendsto (fun x => c * x ^ n) atTop (𝓝 0) :=
  mul_zero c ▸ Filter.Tendsto.const_mul c (tendsto_zpow_atTop_zero hn)

Limit of $c \cdot x^n$ at infinity: $c \cdot x^n \to 0$ as $x \to +\infty$ for $n < 0$

Informal description

For any negative integer $n$ and any constant $c$ in a linearly ordered field $\mathbb{K}$ with the order topology, the function $x \mapsto c \cdot x^n$ tends to $0$ as $x$ tends to $+\infty$.

tendsto_const_mul_pow_nhds_iff' theorem

{n : ℕ} {c d : 𝕜} : Tendsto (fun x : 𝕜 => c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

Full source

theorem tendsto_const_mul_pow_nhds_iff' {n : ℕ} {c d : 𝕜} :
    TendstoTendsto (fun x : 𝕜 => c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d := by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp [tendsto_const_nhds_iff]
  rcases lt_trichotomy c 0 with (hc | rfl | hc)
  · have := tendsto_const_mul_pow_atBot_iff.2 ⟨hn, hc⟩
    simp [not_tendsto_nhds_of_tendsto_atBot this, hc.ne, hn]
  · simp [tendsto_const_nhds_iff]
  · have := tendsto_const_mul_pow_atTop_iff.2 ⟨hn, hc⟩
    simp [not_tendsto_nhds_of_tendsto_atTop this, hc.ne', hn]

Limit of $c \cdot x^n$ at Infinity is $d$ iff ($c = 0$ or $n = 0$) and $c = d$

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology, and let $c, d \in \mathbb{K}$. For any natural number $n$, the function $f(x) = c \cdot x^n$ tends to $d$ as $x$ tends to infinity if and only if either $c = 0$ or $n = 0$, and $c = d$.

tendsto_const_mul_pow_nhds_iff theorem

{n : ℕ} {c d : 𝕜} (hc : c ≠ 0) : Tendsto (fun x : 𝕜 => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d

Full source

theorem tendsto_const_mul_pow_nhds_iff {n : ℕ} {c d : 𝕜} (hc : c ≠ 0) :
    TendstoTendsto (fun x : 𝕜 => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d := by
  simp [tendsto_const_mul_pow_nhds_iff', hc]

Limit of $c \cdot x^n$ at Infinity is $d$ iff $n=0$ and $c=d$

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology, and let $c, d \in \mathbb{K}$ with $c \neq 0$. For any natural number $n$, the function $f(x) = c \cdot x^n$ tends to $d$ as $x$ tends to infinity if and only if $n = 0$ and $c = d$.

tendsto_const_mul_zpow_atTop_nhds_iff theorem

 {n : ℤ} {c d : 𝕜} (hc : c ≠ 0) : Tendsto (fun x : 𝕜 => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0

Full source

theorem tendsto_const_mul_zpow_atTop_nhds_iff {n : ℤ} {c d : 𝕜} (hc : c ≠ 0) :
    TendstoTendsto (fun x : 𝕜 => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0 := by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · cases n with
    | ofNat n =>
      left
      simpa [tendsto_const_mul_pow_nhds_iff hc] using h
    | negSucc n =>
      have hn := Int.negSucc_lt_zero n
      exact Or.inr ⟨hn, tendsto_nhds_unique h (tendsto_const_mul_zpow_atTop_zero hn)⟩
  · rcases h with h | h
    · simp only [h.left, h.right, zpow_zero, mul_one]
      exact tendsto_const_nhds
    · exact h.2.symm ▸ tendsto_const_mul_zpow_atTop_zero h.1

Limit of $c \cdot x^n$ at Infinity: $c \cdot x^n \to d$ iff ($n=0$ and $c=d$) or ($n<0$ and $d=0$)

Informal description

Let $\mathbb{K}$ be a linearly ordered field with the order topology, and let $c, d \in \mathbb{K}$ with $c \neq 0$. For any integer $n$, the function $f(x) = c \cdot x^n$ tends to $d$ as $x$ tends to infinity if and only if either: 1. $n = 0$ and $c = d$, or 2. $n < 0$ and $d = 0$.

IsStrictOrderedRing.toHasContinuousInv₀ instance

 {𝕜} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [ContinuousMul 𝕜] :
  HasContinuousInv₀ 𝕜

Full source

instance (priority := 100) IsStrictOrderedRing.toHasContinuousInv₀ {𝕜}
    [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
    [TopologicalSpace 𝕜] [OrderTopology 𝕜] [ContinuousMul 𝕜] :
    HasContinuousInv₀ 𝕜 := .of_nhds_one <| tendsto_order.2 <| by
  refine ⟨fun x hx => ?_, fun x hx => ?_⟩
  · obtain ⟨x', h₀, hxx', h₁⟩ : ∃ x', 0 < x' ∧ x ≤ x' ∧ x' < 1 :=
      ⟨max x (1 / 2), one_half_pos.trans_le (le_max_right _ _), le_max_left _ _,
        max_lt hx one_half_lt_one⟩
    filter_upwards [Ioo_mem_nhds one_pos ((one_lt_inv₀ h₀).2 h₁)] with y hy
    exact hxx'.trans_lt <| lt_inv_of_lt_inv₀ hy.1 hy.2
  · filter_upwards [Ioi_mem_nhds (inv_lt_one_of_one_lt₀ hx)] with y hy
    exact inv_lt_of_inv_lt₀ (by positivity) hy

Continuity of Inversion in Strictly Ordered Semifields

Informal description

For any linearly ordered semifield $\mathbb{K}$ with a strict ordered ring structure and the order topology, if multiplication is continuous, then the inversion operation $x \mapsto x^{-1}$ is continuous at all nonzero points.

IsStrictOrderedRing.toIsTopologicalDivisionRing instance

: IsTopologicalDivisionRing 𝕜

Full source

instance (priority := 100) IsStrictOrderedRing.toIsTopologicalDivisionRing :
    IsTopologicalDivisionRing 𝕜 := ⟨⟩

Strictly Ordered Semifields as Topological Division Rings

Informal description

Every strictly ordered semifield $\mathbb{K}$ with the order topology is a topological division ring, meaning that the operations of addition, multiplication, and inversion (away from zero) are continuous with respect to the order topology.

comap_mulLeft_nhdsGT_zero theorem

{x : 𝕜} (hx : 0 < x) : comap (x * ·) (𝓝[>] 0) = 𝓝[>] 0

Full source

theorem comap_mulLeft_nhdsGT_zero {x : 𝕜} (hx : 0 < x) : comap (x * ·) (𝓝[>] 0) = 𝓝[>] 0 := by
  rw [nhdsWithin, comap_inf, comap_principal, preimage_const_mul_Ioi _ hx, zero_div]
  congr 1
  refine ((Homeomorph.mulLeft₀ x hx.ne').comap_nhds_eq _).trans ?_
  simp

Preimage of Right-Neighborhood Filter at Zero under Positive Scaling Equals Itself

Informal description

For any positive element $x$ in a linearly ordered semifield $\mathbb{K}$ with the order topology, the preimage of the right-neighborhood filter at zero under the left multiplication map $y \mapsto x \cdot y$ is equal to the right-neighborhood filter at zero itself. That is, $$(x \cdot )^{-1}(\mathcal{N}_{>0}) = \mathcal{N}_{>0}.$$

eventually_nhdsGT_zero_mul_left theorem

{x : 𝕜} (hx : 0 < x) {p : 𝕜 → Prop} (h : ∀ᶠ ε in 𝓝[>] 0, p ε) : ∀ᶠ ε in 𝓝[>] 0, p (x * ε)

Full source

theorem eventually_nhdsGT_zero_mul_left {x : 𝕜} (hx : 0 < x) {p : 𝕜 → Prop}
    (h : ∀ᶠ ε in 𝓝[>] 0, p ε) : ∀ᶠ ε in 𝓝[>] 0, p (x * ε) := by
  rw [← comap_mulLeft_nhdsGT_zero hx]
  exact h.comap fun ε => x * ε

Preservation of Eventual Properties under Positive Scaling in Right-Neighborhood Filter at Zero

Informal description

Let $\mathbb{K}$ be a linearly ordered semifield with the order topology. For any positive element $x \in \mathbb{K}$ and any predicate $p : \mathbb{K} \to \text{Prop}$, if $p$ holds eventually in the right-neighborhood filter at zero $\mathcal{N}_{>0}$, then the predicate $p$ also holds eventually in $\mathcal{N}_{>0}$ when composed with the left multiplication map $y \mapsto x \cdot y$. That is, if $\forallᶠ \varepsilon \text{ in } \mathcal{N}_{>0}, p(\varepsilon)$, then $\forallᶠ \varepsilon \text{ in } \mathcal{N}_{>0}, p(x \cdot \varepsilon)$.