LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Topology.Algebra.Order.Field

`Filter.Tendsto.div_atTop` theorem Filter.Tendsto.div_atTop : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {a : 𝕜}, Filter.Tendsto f l (nhds a) → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x / g x) l (nhds 0) This theorem states that for any types `𝕜` and `α`, where `𝕜` is a linearly ordered field with a topological structure and an order topology, and `α` is an arbitrary type with a filter `l` and two functions `f` and `g` from `α` to `𝕜`. If the function `f` tends toward a value `a` in the neighborhood filter at `a` as we approach any point in the filter `l`, and the function `g` tends to infinity (represented by `Filter.atTop`) as we approach any point in the filter `l`, then the function that sends each point `x` in `α` to the ratio `f(x)/g(x)` tends towards 0 in the neighborhood filter at `0` as we approach any point in the filter `l`. This theorem essentially provides a condition under which the quotient of two functions tends to 0. More concisely: If `𝕜` is a linearly ordered field with a topology and `α` is a type with filter `l`, given functions `f : α → 𝕜` converging to `a` in `l` and `g : α → 𝕜` approaching infinity in `l`, then the ratio function `x ↦ f(x) / g(x)` converges to 0 in the neighborhood filter at 0 as we approach any point in `l`.
`tendsto_zpow_atTop_zero` theorem tendsto_zpow_atTop_zero : ∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] {n : ℤ}, n < 0 → Filter.Tendsto (fun x => x ^ n) Filter.atTop (nhds 0) This theorem, `tendsto_zpow_atTop_zero`, states that for any linearly ordered field `𝕜`, in the context of a topological space with order topology, if `n` is a negative integer, then the function `x ^ n` tends to 0 as `x` approaches infinity. In other words, for any neighborhood of 0 in the field, there exists a sufficiently large threshold after which the values of `x ^ n` will stay within that neighborhood, thus approaching 0 as `x` goes to infinity. More concisely: For any linearly ordered field with order topology, the function `x ^ (-n)` converges to 1 as `x` approaches infinity, hence `x ^ n` tends to 0 as `x` goes to infinity.
`Filter.Tendsto.atBot_mul_neg` theorem Filter.Tendsto.atBot_mul_neg : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜}, C < 0 → Filter.Tendsto f l Filter.atBot → Filter.Tendsto g l (nhds C) → Filter.Tendsto (fun x => f x * g x) l Filter.atTop This theorem states that in a linearly ordered field with the order topology, if a function `f` tends to negative infinity and another function `g` tends to a negative constant `C`, then the product of `f` and `g` tends to positive infinity. This is formalized as: for every type `𝕜` and `α`, given a linearly ordered field structure, a topological space structure and an order topology on `𝕜`, if `C` is less than zero, `f` tends to `Filter.atBot` at some filter `l` and `g` tends to the neighborhood of `C` at the same filter `l`, then the function that maps any `x` in `α` to the product of `f(x)` and `g(x)` tends to `Filter.atTop` at the filter `l`. More concisely: If `f` tends to negative infinity and `g` tends to a negative constant `C` in a linearly ordered field with the order topology, then their product tends to positive infinity.
`Filter.Tendsto.inv_tendsto_zero` theorem Filter.Tendsto.inv_tendsto_zero : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] {l : Filter α} {f : α → 𝕜}, Filter.Tendsto f l (nhdsWithin 0 (Set.Ioi 0)) → Filter.Tendsto f⁻¹ l Filter.atTop The theorem `Filter.Tendsto.inv_tendsto_zero` states that for any type `𝕜` that can be ordered with a linear ordering and has a topology compatible with that order, and for any filter `l` over any type `α` and any function `f` from `α` to `𝕜`, if the function `f` tends to a value in the interval `(0, ∞)` as `l` tends to 0, then the reciprocal function `1/f` tends to infinity as `l` is considered. In other words, if `f` approaches values greater than zero when its input approaches zero, then `1/f` approaches infinity when the same input filter is considered. More concisely: If a function from a filtered space to the real numbers with a compatible topology tends to a positive value as the filter tends to 0, then the reciprocal function tends to infinity with respect to that filter.
`Filter.Tendsto.inv_tendsto_atTop` theorem Filter.Tendsto.inv_tendsto_atTop : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] {l : Filter α} {f : α → 𝕜}, Filter.Tendsto f l Filter.atTop → Filter.Tendsto f⁻¹ l (nhds 0) The theorem `Filter.Tendsto.inv_tendsto_atTop` states that for any linearly ordered field 𝕜, with a corresponding topological structure and order topology, and any filter `l` on an arbitrary type α, if a function `f` from α to 𝕜 tends to infinity (i.e., for every neighborhood of infinity, the pre-image of that neighborhood under `f` is a neighborhood in `l`), then the reciprocal of the function `f`, denoted by `f⁻¹`, tends to 0 (i.e., for every neighborhood of 0, the pre-image of this neighborhood under `f⁻¹` is a neighborhood in `l`). More concisely: If a function from an arbitrary type to a linearly ordered field tends to infinity with respect to a filter, then the reciprocal function tends to 0 with respect to the same filter.
`tendsto_inv_atTop_zero` theorem tendsto_inv_atTop_zero : ∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜], Filter.Tendsto (fun r => r⁻¹) Filter.atTop (nhds 0) This theorem, `tendsto_inv_atTop_zero`, states that for any linearly ordered field `𝕜`, which is also a topological space with an order topology, the function that takes the inverse of each element (`fun r => r⁻¹`) tends to zero as the input values approach infinity (`Filter.atTop`). In other words, as we consider larger and larger values in the ordered field `𝕜`, their reciprocals get closer and closer to zero. This formalizes the intuitive notion that the inverse of a large number is a small number close to zero. More concisely: For any linearly ordered field `𝕜` with order topology, the function `r => r⁻¹` converges to zero as `r` approaches the top element.
`tendsto_inv_zero_atTop` theorem tendsto_inv_zero_atTop : ∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜], Filter.Tendsto (fun x => x⁻¹) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop The theorem `tendsto_inv_zero_atTop` states that for any type `𝕜` that is a linear ordered field with an associated topological space and order topology, the function defined as the reciprocal of `x` (`x ↦ x⁻¹`) tends to positive infinity (`+∞`) as `x` approaches 0 from the right side. This is formalized by saying that the function `x ↦ x⁻¹` has `Filter.atTop` (representing `+∞`) as its limit when the input `x` is taken from a neighborhood of 0 that lies within the interval `(0, ∞)` (`Set.Ioi 0`). This means that as `x` gets arbitrarily close to 0 from the right, the value of `x⁻¹` gets arbitrarily large. More concisely: For any linear ordered field `𝕜` with associated topological space and order topology, the reciprocal function `x ↦ x⁻¹` approaches positive infinity as `x` approaches 0 from the right in the order topology (`Set.Ioi 0`).
`tendsto_pow_neg_atTop` theorem tendsto_pow_neg_atTop : ∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] {n : ℕ}, n ≠ 0 → Filter.Tendsto (fun x => x ^ (-↑n)) Filter.atTop (nhds 0) The theorem `tendsto_pow_neg_atTop` states that for any given type `𝕜` which has a linear ordered field structure and a topological space structure, and given a natural number `n` that is not equal to zero, the function `x^(-n)` tends to `0` as `x` goes to positive infinity. Essentially, it's describing that the inverse of any positive power of `x` will approach zero when `x` is very large. This is a specific case of a more general theorem, `tendsto_rpow_neg_atTop`, which applies to positive real powers. More concisely: For any type `𝕜` with a linear ordered field structure and a topological space structure, and for any natural number `n` not equal to zero, the function `x ↦ x^(-n)` converges to `0` as `x` approaches the top of the order on `𝕜`.
`Filter.Tendsto.mul_atBot` theorem Filter.Tendsto.mul_atBot : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜}, 0 < C → Filter.Tendsto f l (nhds C) → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x * g x) l Filter.atBot This theorem states that in a linearly ordered field, equipped with the order topology, if a function `f` is approaching a positive constant `C` (i.e., the limit of `f` is `C`), and another function `g` is tending towards negative infinity, then the product of these two functions `f` and `g`, is also tending towards negative infinity. This result holds for any filter `l`. More concisely: In a linearly ordered field with order topology, if the limit of a function `f` is a positive constant `C` and the limit of another function `g` is negative infinity for any filter `l`, then the product `f * g` tends towards negative infinity.
`Filter.Tendsto.atTop_mul_neg` theorem Filter.Tendsto.atTop_mul_neg : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜}, C < 0 → Filter.Tendsto f l Filter.atTop → Filter.Tendsto g l (nhds C) → Filter.Tendsto (fun x => f x * g x) l Filter.atBot In a linearly ordered field, equipped with the order topology, the theorem states that if a function `f` tends towards infinity (represented by `Filter.atTop`) and another function `g` tends towards a negative constant `C`, then the multiplication of these two functions `f * g` tends towards negative infinity (represented by `Filter.atBot`). This is to say, as the function `f` grows very large and `g` approaches a negative constant, their product becomes increasingly negative. More concisely: In a linearly ordered field, if a function tends towards positive infinity and another function tends towards a negative constant, then their product tends towards negative infinity.
`Filter.Tendsto.mul_atTop` theorem Filter.Tendsto.mul_atTop : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜}, 0 < C → Filter.Tendsto f l (nhds C) → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x * g x) l Filter.atTop This theorem states that in a linearly ordered field with the order topology, given a function `f` that tends to a positive constant `C` and another function `g` that tends towards infinity (`Filter.atTop`), the function formed by the product of `f` and `g` also tends towards infinity. In more formal terms, for any `𝕜` which is a type representing a linearly ordered field with a topological structure and order topology, and any `l` which is a type representing a filter, if `f` and `g` are functions from `l` to `𝕜`, with `f` tending to a positive constant `C` and `g` tending to infinity, then the function defined as the product of `f` and `g` also tends to infinity. More concisely: In a linearly ordered field with the order topology, if a function tends to a positive constant and another function tends to infinity, then their product function tends to infinity.
`TopologicalRing.of_norm` theorem TopologicalRing.of_norm : ∀ {R : Type u_1} {𝕜 : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : LinearOrderedField 𝕜] [inst_2 : TopologicalSpace R] [inst_3 : TopologicalAddGroup R] (norm : R → 𝕜), (∀ (x : R), 0 ≤ norm x) → (∀ (x y : R), norm (x * y) ≤ norm x * norm y) → ((nhds 0).HasBasis (fun x => 0 < x) fun ε => {x \| norm x < ε}) → TopologicalRing R The theorem `TopologicalRing.of_norm` states that for a given non-unital and non-associative ring `R` which has a nonnegative submultiplicative norm `norm` mapping to a linear ordered field `𝕜`, if the open balls defined by `{ x \| norm x < ε }` for `ε > 0` form a basis of neighborhoods of zero, then `R` is a topological ring. Here, a norm is called submultiplicative if it satisfies the inequality `norm (x * y) ≤ norm x * norm y` for all `x, y` in `R`, and an open ball `{ x \| norm x < ε }` is a set of points in the ring whose norm is less than `ε`. More concisely: Given a non-unital and non-associative ring `R` with a nonnegative submultiplicative norm `norm` mapping to a linear ordered field, if the open balls defined by `{ x \| norm x < ε }` form a basis of neighborhoods of zero, then `R` is a topological ring.
`inv_atTop₀` theorem inv_atTop₀ : ∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜], Filter.atTop⁻¹ = nhdsWithin 0 (Set.Ioi 0) This theorem states that for any type `𝕜` that is a linearly ordered field with a topological space structure and an order topology, the inverse of the filter `atTop` (representing the limit towards positive infinity) is equal to the neighborhood within the set `(0, ∞)` at `0`. This effectively means that taking the inverse of elements going to positive infinity gives us the neighborhood of `0` excluding `0` itself and including all positive numbers. More concisely: For a linearly ordered field `𝕜` with a topology and order topology, the filter of elements going to positive infinity `atTop` equals the neighborhood filter of `0` excluding `0` in `(0, ∞)`, and their inverses are equal.
`Filter.Tendsto.neg_mul_atTop` theorem Filter.Tendsto.neg_mul_atTop : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜}, C < 0 → Filter.Tendsto f l (nhds C) → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x * g x) l Filter.atBot The theorem states that in a linearly ordered field with the order topology, if a function `f` tends to a negative constant `C`, and another function `g` tends to positive infinity (represented by `Filter.atTop`), then the function formed by their pointwise multiplication, `f * g`, tends to negative infinity (represented by `Filter.atBot`). This is defined for any filter `l` on a generic set `α`, with `f` and `g` as functions mapping elements of `α` to the linearly ordered field. More concisely: In a linearly ordered field with the order topology, if a function `f` converges to a negative constant `C` and another function `g` converges to positive infinity, then their pointwise product `f * g` converges to negative infinity.
`Filter.Tendsto.neg_mul_atBot` theorem Filter.Tendsto.neg_mul_atBot : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜}, C < 0 → Filter.Tendsto f l (nhds C) → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x * g x) l Filter.atTop This theorem states that in a linearly ordered field, equipped with a topological space structure and an order topology, if a function `f` tends to a negative constant `C` and another function `g` tends to negative infinity (represented by `Filter.atBot`), then the product of `f` and `g` tends to positive infinity (represented by `Filter.atTop`). In other words, if we have two functions such that one approaches a negative constant and the other goes to negative infinity as their inputs follow a certain filter `l`, then their pointwise product goes to positive infinity for the same filter `l`. More concisely: In a linearly ordered field with order topology, if function `f` converges to a negative constant `C` and function `g` goes to negative infinity through filter `l`, then their product `f * g` converges to positive infinity through filter `l`.
`Filter.Tendsto.atBot_mul` theorem Filter.Tendsto.atBot_mul : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜}, 0 < C → Filter.Tendsto f l Filter.atBot → Filter.Tendsto g l (nhds C) → Filter.Tendsto (fun x => f x * g x) l Filter.atBot In a linearly ordered field equipped with the order topology, this theorem states that if the function `f` approaches negative infinity (expressed as `f` tends to `Filter.atBot`) and function `g` approaches a positive constant `C` (expressed as `g` tends to the neighborhood filter at `C`, written as `nhds C`), then the product of `f` and `g` also tends to negative infinity (expressed as `f * g` tends to `Filter.atBot`). This theorem applies to any filter `l` and functions `f` and `g` that map from the filter to the field. More concisely: In a linearly ordered field, if function `f` approaches negative infinity and function `g` approaches a positive constant `C`, then their product `f g` approaches negative infinity.*
`Filter.Tendsto.atTop_mul` theorem Filter.Tendsto.atTop_mul : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜}, 0 < C → Filter.Tendsto f l Filter.atTop → Filter.Tendsto g l (nhds C) → Filter.Tendsto (fun x => f x * g x) l Filter.atTop The theorem `Filter.Tendsto.atTop_mul` states the following: Suppose 𝕜 is a linearly ordered field with a topological space structure and an order topology. Given a filter `l` and two functions `f` and `g` from α to 𝕜, and a positive constant `C`. If the function `f` tends towards infinity (`Filter.atTop`) and `g` tends towards the neighborhood of the positive constant `C`, then the function defined by the product of `f` and `g` also tends towards infinity (`Filter.atTop`). In other words, in a linearly ordered field with an order topology, if one function goes to infinity and the other goes to a positive constant, their product will also go to infinity. More concisely: If a filter converges to infinity in a linearly ordered field with an order topology and another function converges to a positive constant, then their product converges to infinity.
`tendsto_inv_atTop_zero'` theorem tendsto_inv_atTop_zero' : ∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : OrderTopology 𝕜], Filter.Tendsto (fun r => r⁻¹) Filter.atTop (nhdsWithin 0 (Set.Ioi 0)) The theorem `tendsto_inv_atTop_zero'` states that for any linearly ordered field 𝕜 equipped with a topological space and order topology structures, the function `r ↦ r⁻¹` tends to `0` on the right as `r` tends to positive infinity. In other words, as values of `r` increase without bound, the values of their reciprocal `r⁻¹` get arbitrarily close to `0` from the right. The formal variables and structures used in the theorem introduce a very general context that encompasses many specific examples, such as the field of real numbers. More concisely: For any linearly ordered field with a topology, the reciprocal function tends to 0 from the right as the input approaches positive infinity.