# Topologies on linear ordered fields #

In this file we prove that a linear ordered field with order topology has continuous multiplication and division (apart from zero in the denominator). We also prove theorems like Filter.Tendsto.mul_atTop: if f tends to a positive number and g tends to positive infinity, then f * g tends to positive infinity.

theorem TopologicalRing.of_norm {R : Type u_1} {π : Type u_2} [] [] (norm : R β π) (norm_nonneg : β (x : R), 0 β€ norm x) (norm_mul_le : β (x y : R), norm (x * y) β€ norm x * norm y) (nhds_basis : (nhds 0).HasBasis (fun (x : π) => 0 < x) fun (Ξ΅ : π) => {x : R | norm x < Ξ΅}) :

If a (possibly non-unital and/or non-associative) ring R admits a submultiplicative nonnegative norm norm : R β π, where π is a linear ordered field, and the open balls { x | norm x < Ξ΅ }, Ξ΅ > 0, form a basis of neighborhoods of zero, then R is a topological ring.

@[instance 100]
instance LinearOrderedField.topologicalRing {π : Type u_1} [] [TopologicalSpace π] [OrderTopology π] :
Equations
• β― = β―
theorem Filter.Tendsto.atTop_mul {π : Type u_1} {Ξ± : Type u_2} [] [TopologicalSpace π] [OrderTopology π] {l : Filter Ξ±} {f : Ξ± β π} {g : Ξ± β π} {C : π} (hC : 0 < C) (hf : Filter.Tendsto f l Filter.atTop) (hg : Filter.Tendsto g l (nhds C)) :
Filter.Tendsto (fun (x : Ξ±) => f x * g x) l Filter.atTop

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.mul_atTop {π : Type u_1} {Ξ± : Type u_2} [] [TopologicalSpace π] [OrderTopology π] {l : Filter Ξ±} {f : Ξ± β π} {g : Ξ± β π} {C : π} (hC : 0 < C) (hf : Filter.Tendsto f l (nhds C)) (hg : Filter.Tendsto g l Filter.atTop) :
Filter.Tendsto (fun (x : Ξ±) => f x * g x) l Filter.atTop

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.atTop_mul_neg {π : Type u_1} {Ξ± : Type u_2} [] [TopologicalSpace π] [OrderTopology π] {l : Filter Ξ±} {f : Ξ± β π} {g : Ξ± β π} {C : π} (hC : C < 0) (hf : Filter.Tendsto f l Filter.atTop) (hg : Filter.Tendsto g l (nhds C)) :
Filter.Tendsto (fun (x : Ξ±) => f x * g x) l Filter.atBot

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.neg_mul_atTop {π : Type u_1} {Ξ± : Type u_2} [] [TopologicalSpace π] [OrderTopology π] {l : Filter Ξ±} {f : Ξ± β π} {g : Ξ± β π} {C : π} (hC : C < 0) (hf : Filter.Tendsto f l (nhds C)) (hg : Filter.Tendsto g l Filter.atTop) :
Filter.Tendsto (fun (x : Ξ±) => f x * g x) l Filter.atBot

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.atBot_mul {π : Type u_1} {Ξ± : Type u_2} [] [TopologicalSpace π] [OrderTopology π] {l : Filter Ξ±} {f : Ξ± β π} {g : Ξ± β π} {C : π} (hC : 0 < C) (hf : Filter.Tendsto f l Filter.atBot) (hg : Filter.Tendsto g l (nhds C)) :
Filter.Tendsto (fun (x : Ξ±) => f x * g x) l Filter.atBot

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_neg {π : Type u_1} {Ξ± : Type u_2} [] [TopologicalSpace π] [OrderTopology π] {l : Filter Ξ±} {f : Ξ± β π} {g : Ξ± β π} {C : π} (hC : C < 0) (hf : Filter.Tendsto f l Filter.atBot) (hg : Filter.Tendsto g l (nhds C)) :
Filter.Tendsto (fun (x : Ξ±) => f x * g x) l Filter.atTop

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.mul_atBot {π : Type u_1} {Ξ± : Type u_2} [] [TopologicalSpace π] [OrderTopology π] {l : Filter Ξ±} {f : Ξ± β π} {g : Ξ± β π} {C : π} (hC : 0 < C) (hf : Filter.Tendsto f l (nhds C)) (hg : Filter.Tendsto g l Filter.atBot) :
Filter.Tendsto (fun (x : Ξ±) => f x * g x) l Filter.atBot

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.neg_mul_atBot {π : Type u_1} {Ξ± : Type u_2} [] [TopologicalSpace π] [OrderTopology π] {l : Filter Ξ±} {f : Ξ± β π} {g : Ξ± β π} {C : π} (hC : C < 0) (hf : Filter.Tendsto f l (nhds C)) (hg : Filter.Tendsto g l Filter.atBot) :
Filter.Tendsto (fun (x : Ξ±) => f x * g x) l Filter.atTop

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.

@[simp]
theorem inv_atTopβ {π : Type u_1} [] [TopologicalSpace π] [OrderTopology π] :
Filter.atTopβ»ΒΉ = nhdsWithin 0 ()
@[simp]
theorem inv_nhdsWithin_Ioi_zero {π : Type u_1} [] [TopologicalSpace π] [OrderTopology π] :
(nhdsWithin 0 ())β»ΒΉ = Filter.atTop
theorem tendsto_inv_zero_atTop {π : Type u_1} [] [TopologicalSpace π] [OrderTopology π] :
Filter.Tendsto (fun (x : π) => ) (nhdsWithin 0 ()) Filter.atTop

The function x β¦ xβ»ΒΉ tends to +β on the right of 0.

theorem tendsto_inv_atTop_zero' {π : Type u_1} [] [TopologicalSpace π] [OrderTopology π] :
Filter.Tendsto (fun (r : π) => ) Filter.atTop (nhdsWithin 0 ())

The function r β¦ rβ»ΒΉ tends to 0 on the right as r β +β.

theorem tendsto_inv_atTop_zero {π : Type u_1} [] [TopologicalSpace π] [OrderTopology π] :
Filter.Tendsto (fun (r : π) => ) Filter.atTop (nhds 0)
theorem Filter.Tendsto.div_atTop {π : Type u_1} {Ξ± : Type u_2} [] [TopologicalSpace π] [OrderTopology π] {l : Filter Ξ±} {f : Ξ± β π} {g : Ξ± β π} {a : π} (h : Filter.Tendsto f l (nhds a)) (hg : Filter.Tendsto g l Filter.atTop) :
Filter.Tendsto (fun (x : Ξ±) => f x / g x) l (nhds 0)
theorem Filter.Tendsto.inv_tendsto_atTop {π : Type u_1} {Ξ± : Type u_2} [] [TopologicalSpace π] [OrderTopology π] {l : Filter Ξ±} {f : Ξ± β π} (h : Filter.Tendsto f l Filter.atTop) :
theorem Filter.Tendsto.inv_tendsto_zero {π : Type u_1} {Ξ± : Type u_2} [] [TopologicalSpace π] [OrderTopology π] {l : Filter Ξ±} {f : Ξ± β π} (h : Filter.Tendsto f l (nhdsWithin 0 ())) :
Filter.Tendsto l Filter.atTop
theorem tendsto_pow_neg_atTop {π : Type u_1} [] [TopologicalSpace π] [OrderTopology π] {n : β} (hn : n β  0) :
Filter.Tendsto (fun (x : π) => x ^ (-βn)) Filter.atTop (nhds 0)

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_zpow_atTop_zero {π : Type u_1} [] [TopologicalSpace π] [OrderTopology π] {n : β€} (hn : n < 0) :
Filter.Tendsto (fun (x : π) => x ^ n) Filter.atTop (nhds 0)
theorem tendsto_const_mul_zpow_atTop_zero {π : Type u_1} [] [TopologicalSpace π] [OrderTopology π] {n : β€} {c : π} (hn : n < 0) :
Filter.Tendsto (fun (x : π) => c * x ^ n) Filter.atTop (nhds 0)
theorem tendsto_const_mul_pow_nhds_iff' {π : Type u_1} [] [TopologicalSpace π] [OrderTopology π] {n : β} {c : π} {d : π} :
Filter.Tendsto (fun (x : π) => c * x ^ n) Filter.atTop (nhds d) β (c = 0 β¨ n = 0) β§ c = d
theorem tendsto_const_mul_pow_nhds_iff {π : Type u_1} [] [TopologicalSpace π] [OrderTopology π] {n : β} {c : π} {d : π} (hc : c β  0) :
Filter.Tendsto (fun (x : π) => c * x ^ n) Filter.atTop (nhds d) β n = 0 β§ c = d
theorem tendsto_const_mul_zpow_atTop_nhds_iff {π : Type u_1} [] [TopologicalSpace π] [OrderTopology π] {n : β€} {c : π} {d : π} (hc : c β  0) :
Filter.Tendsto (fun (x : π) => c * x ^ n) Filter.atTop (nhds d) β n = 0 β§ c = d β¨ n < 0 β§ d = 0
@[instance 100]
instance LinearOrderedSemifield.toHasContinuousInvβ {π : Type u_3} [] [TopologicalSpace π] [OrderTopology π] [ContinuousMul π] :
Equations
• β― = β―
@[instance 100]
instance LinearOrderedField.toTopologicalDivisionRing {π : Type u_1} [] [TopologicalSpace π] [OrderTopology π] :
Equations
• β― = β―
theorem nhdsWithin_pos_comap_mul_left {π : Type u_1} [] [TopologicalSpace π] [OrderTopology π] {x : π} (hx : 0 < x) :
Filter.comap (fun (x_1 : π) => x * x_1) (nhdsWithin 0 ()) = nhdsWithin 0 ()
theorem eventually_nhdsWithin_pos_mul_left {π : Type u_1} [] [TopologicalSpace π] [OrderTopology π] {x : π} (hx : 0 < x) {p : π β Prop} (h : βαΆ  (Ξ΅ : π) in nhdsWithin 0 (), p Ξ΅) :
βαΆ  (Ξ΅ : π) in nhdsWithin 0 (), p (x * Ξ΅)