tendsto_gauge_nhds_zero
theorem tendsto_gauge_nhds_zero :
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
[inst_3 : ContinuousSMul ℝ E], s ∈ nhds 0 → Filter.Tendsto (gauge s) (nhds 0) (nhds 0)
This theorem states that for any set `s` in a real vector space `E` (where `E` is a topological space and the scalar multiplication in `E` is continuous), if `s` is a neighborhood of the origin (0), then the Minkowski functional (or `gauge`) of `s` tends towards 0 as the input approaches 0. In other words, for small vectors `x` in the neighborhood of the origin, the smallest real number `r` such that `x` lies in the scaled set `r • s` is also close to 0.
More concisely: Given a real vector space `E` with a continuous scalar multiplication, if `s` is a neighborhood of the origin in `E`, then the Minkowski functional of `s` approaches 0 as the input approaches the origin.
|
gauge_smul
theorem gauge_smul :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : RCLike 𝕜]
[inst_3 : Module 𝕜 E] [inst_4 : IsScalarTower ℝ 𝕜 E],
Balanced 𝕜 s → ∀ (r : 𝕜) (x : E), gauge s (r • x) = ‖r‖ * gauge s x
The theorem `gauge_smul` states that if a set `s` in a vector space `E` over the reals is balanced (meaning that scaling the set by any scalar `a` with norm at most 1 still contains the set), then the Minkowski functional of `s` is complex-homogeneous. This means that for any complex number `r` and any element `x` in `E`, the Minkowski functional of the scaled element `r • x` is equal to the norm of `r` times the Minkowski functional of `x`. In mathematical terms, this is expressed as `gauge s (r • x) = ‖r‖ * gauge s x`.
More concisely: If a set in a real vector space is balanced, then its Minkowski functional is complex-homogeneous, that is, gauge (s) (r • x) = ‖r��|| * gauge (s) x for all complex numbers r and elements x in the vector space.
|
gauge_pos
theorem gauge_pos :
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E} [inst_2 : TopologicalSpace E]
[inst_3 : T1Space E], Absorbent ℝ s → Bornology.IsVonNBounded ℝ s → (0 < gauge s x ↔ x ≠ 0)
The theorem `gauge_pos` states that for any real vector space `E` (endowed with an additive commutative group structure, a module over the real numbers structure, a topological space structure, and a T1 space structure), a set `s` in `E`, and an element `x` in `E`, if `s` is absorbent and von Neumann bounded, then the Minkowski functional (gauge) of `s` at `x` is greater than zero if and only if `x` is not the zero vector. In other words, the gauge of a nonzero vector under these conditions is always positive.
More concisely: For any absorbent and von Neumann bounded set `s` in a real vector space `E`, its Minkowski functional at a nonzero vector `x` is positive.
|
gauge_mono
theorem gauge_mono :
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s t : Set E},
Absorbent ℝ s → s ⊆ t → gauge t ≤ gauge s
The theorem `gauge_mono` is stating that for any type `E` that has the structure of a real vector space (i.e., `E` is an additive commutative group and a module over the real numbers), given two sets `s` and `t` of elements of `E`, if `s` is an *absorbent* set (meaning it absorbs every singleton) and `s` is a subset of `t`, then the Minkowski functional (or *gauge*) of `t` is less than or equal to the Minkowski functional of `s`. In other words, if a set `s` has these properties, any scaling of `t` needed to contain a vector `x` will be no greater than the scaling of `s` needed to contain `x`.
More concisely: If `s` is an absorbent subset of a real vector space `E` that is a subset of another set `t`, then the Minkowski functional of `t` is less than or equal to that of `s`.
|
continuous_gauge
theorem continuous_gauge :
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
[inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E], Convex ℝ s → s ∈ nhds 0 → Continuous (gauge s)
This theorem states that if `s` is a convex neighborhood of the origin in a topological real vector space `E`, then the Minkowski functional (or `gauge`) of `s` is a continuous function. If the ambient space is a normed space, the Minkowski functional is not just continuous, but Lipschitz continuous, as is shown in a separate theorem `Convex.lipschitz_gauge`.
In simpler words, the theorem highlights a property of the Minkowski functional applied to a set in the vicinity of the origin, emphasizing that under certain conditions (the set being convex and the space being a topological real vector space), the value of the Minkowski functional changes continuously as you move from point to point in the set.
More concisely: If `s` is a convex set in a topological real vector space, then the Minkowski functional of `s` is a continuous function.
|
Seminorm.gauge_ball
theorem Seminorm.gauge_ball :
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (p : Seminorm ℝ E), gauge (p.ball 0 1) = ⇑p := by
sorry
This theorem states that for any seminorm on a real vector space, the Minkowski functional (or gauge) of its unit ball is equal to that seminorm itself. In other words, for every element in the vector space, the smallest real number, which when used to scale the unit ball includes that element, is exactly the value of the seminorm at that element. This connection links the concepts of seminorms and gauges in a mathematically precise way.
More concisely: For any seminorm on a real vector space, the Minkowski functional of its unit ball equals the seminorm itself.
|
gauge_ball
theorem gauge_ball :
∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {r : ℝ},
0 ≤ r → ∀ (x : E), gauge (Metric.ball 0 r) x = ‖x‖ / r
The theorem `gauge_ball` states that for any type `E` that is a semi-normed additive commutative group and a normed space over the set of real numbers, for any real number `r` greater than or equal to zero, and for any element `x` of `E`, the Minkowski functional (gauge) of the metric ball centered at 0 with radius `r` evaluated at `x` is equal to the norm of `x` divided by `r`. In other words, the smallest scalar `r` that scales the set such that `x` belongs to the set is equal to the norm of `x` divided by `r`, where the set is a metric ball (set of all points at a distance less than `r` from the origin).
More concisely: For any semi-normed additive commutative group and normed space `E` over the real numbers, the Minkowski functional (gauge) of the metric ball centered at 0 with radius `r` is equal to the norm of `x` divided by `r` for all `x` in `E` and `r` greater than or equal to the norm of `x`.
|
gauge_le_of_mem
theorem gauge_le_of_mem :
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E} {a : ℝ},
0 ≤ a → x ∈ a • s → gauge s x ≤ a
The theorem `gauge_le_of_mem` states that for any type `E` that has the structure of a real vector space (indicated by the `AddCommGroup E` and `Module ℝ E` type classes), any set `s` of type `E`, any element `x` of type `E`, and any real number `a`, if `a` is nonnegative and `x` is an element of the set obtained by scaling `s` by `a`, then the Minkowski gauge of `s` at `x` is less than or equal to `a`. In other words, the Minkowski gauge of a point with respect to a set provides a bound on how far the point can be stretched while remaining within a scaled version of the set.
More concisely: For any real vector space `E`, set `s` of `E`, element `x` in the scaled set `a * s`, and nonnegative real number `a`, we have `gauge (s) x ≤ a`.
|
gauge_add_le
theorem gauge_add_le :
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
Convex ℝ s → Absorbent ℝ s → ∀ (x y : E), gauge s (x + y) ≤ gauge s x + gauge s y
This theorem states that the gauge functional is subadditive given a certain set and elements in a real vector space. More specifically, for any set in a real vector space, if the set is both convex and absorbent, then for any two elements in the vector space, the gauge of the sum of these elements is less than or equal to the sum of their individual gauges. This property of subadditivity essentially means that the gauge functional measures the "size" of a vector in such a way that the "size" of the sum of two vectors is at most the sum of their individual "sizes".
More concisely: For any convex and absorbent set in a real vector space, the gauge functional is subadditive, meaning the gauge of their sum is less than or equal to the sum of their individual gauges.
|
gauge_nonneg
theorem gauge_nonneg :
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} (x : E), 0 ≤ gauge s x
The theorem `gauge_nonneg` establishes that the Minkowski functional, also known as the gauge, is always nonnegative. In more precise terms, it states that for any real vector space `E`, for any additive commutative group structure on `E`, for any module structure of the real numbers over `E`, for any set `s` of elements of `E`, and for any element `x` of `E`, the value of the gauge of `s` at `x` is greater than or equal to zero. This is usually represented mathematically as: ∀ E, s, x, 0 ≤ gauge s x.
More concisely: For any real vector space E equipped with an additive commutative group structure and module structure of the real numbers, and for any set s of elements and any x in E, the gauge of s at x is nonnegative (gauge s x ≥ 0).
|
mem_closure_of_gauge_le_one
theorem mem_closure_of_gauge_le_one :
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E} [inst_2 : TopologicalSpace E]
[inst_3 : ContinuousSMul ℝ E], Convex ℝ s → 0 ∈ s → Absorbent ℝ s → gauge s x ≤ 1 → x ∈ closure s
The theorem `mem_closure_of_gauge_le_one` states that given a set `s` in a real vector space `E`, if `s` is convex, contains the origin, and is absorbent, then for any element `x` in `E`, if the Minkowski functional or gauge of `s` at `x` is less than or equal to one, `x` is in the closure of `s`. In other words, if `s` satisfies these properties, then any point scaled by `s` by a factor not exceeding one belongs to the smallest closed set containing `s`.
More concisely: If a convex, origin-containing, absorbent set `s` in a real vector space has Minkowski functional at `x` less than or equal to 1, then `x` is in the closure of `s`.
|
interior_subset_gauge_lt_one
theorem interior_subset_gauge_lt_one :
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : ContinuousSMul ℝ E] (s : Set E), interior s ⊆ {x | gauge s x < 1}
This theorem states that for any set `s` in a real vector space `E` equipped with an additive commutative group structure, a scalar multiplication module over the reals, a topological space structure and a continuous scalar multiplication, the interior of `s` is a subset of those vectors `x` for which the Minkowski functional of `s` at `x` is less than one. In other words, all vectors in the interior of `s` have their corresponding value under the Minkowski functional less than one.
More concisely: The interior of a real vector space set equipped with a topology and continuous scalar multiplication is contained in the set of vectors with Minkowski functional value strictly less than one.
|
continuousAt_gauge
theorem continuousAt_gauge :
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E} [inst_2 : TopologicalSpace E]
[inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E],
Convex ℝ s → s ∈ nhds 0 → ContinuousAt (gauge s) x
The theorem `continuousAt_gauge` states that if `s` is a convex neighborhood of the origin in a topological real vector space `E` equipped with addition (`AddCommGroup E`) and scalar multiplication (`Module ℝ E`), then the Minkowski functional (or `gauge`) of `s` is continuous at any point `x` in `E`. Here, a set `s` is convex if for any point `x` in `s`, the set `s` is star convex at `x`. The Minkowski functional or `gauge` of `s` maps any `x` in `E` to the infimum of the set of real numbers `r` such that `r` is positive and `x` is in the scaled set `r • s`. The neighborhood of the origin is with respect to a topology on `E` that makes addition and scalar multiplication continuous (`TopologicalAddGroup E` and `ContinuousSMul ℝ E`). Note that if the space `E` is also a normed space, the `gauge` is not just continuous, but Lipschitz continuous, as stated in `Convex.lipschitz_gauge`.
More concisely: If `s` is a convex neighborhood of the origin in a topological real vector space `E` with addition and scalar multiplication continuous, then the Minkowski functional of `s` is a continuous function.
|
gauge_zero
theorem gauge_zero : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E}, gauge s 0 = 0 := by
sorry
This theorem states that the Minkowski functional, or "gauge", evaluated at the zero vector is always zero. This is generally true in mathematics when the zero vector is included in the set `s`. However, in Lean, the theorem holds unconditionally due to the definition of the infimum over an empty set being set to `0`. Therefore, no matter the set `s` in the real vector space `E`, the gauge of `s` at `0` equals `0`.
More concisely: The Minkowski functional of any set in a real vector space evaluates to 0 at the zero vector.
|
gauge_def'
theorem gauge_def' :
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E},
gauge s x = sInf {r | r ∈ Set.Ioi 0 ∧ r⁻¹ • x ∈ s}
This theorem provides an alternative definition of the Minkowski functional (or gauge) for a given set `s` in a real vector space and an element `x`. In this alternative definition, the gauge of `s` at `x` is defined as the infimum (greatest lower bound) of the set of all real numbers `r` greater than 0 such that `x` is in `s` scaled by `1/r`, i.e., `x` is in the set obtained by scaling `s` by the multiplicative inverse of `r`. This contrasts with the usual definition where the gauge is defined as the infimum of the set of all `r` such that `x` is in `s` scaled by `r`.
More concisely: The Minkowski functional of a set `s` in a real vector space at an element `x` is the infimum of all `r > 0` such that `x` is in the set obtained by scaling `s` by the multiplicative inverse of `r`.
|
Absorbent.gauge_set_nonempty
theorem Absorbent.gauge_set_nonempty :
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E},
Absorbent ℝ s → {r | 0 < r ∧ x ∈ r • s}.Nonempty
The theorem states that for a given Absorbent subset 's' in a real vector space 'E', if we take any element 'x' from the space 'E', then the set of all positive real numbers 'r' such that 'x' is in the scalar multiplication of 'r' and 's' is nonempty. This property is particularly useful for proving many properties about the gauge. In simpler terms, if a set absorbs singletons, then for any element in the space, there's a positive real number which when multiplied with the set includes the element.
More concisely: Given an absorbent subset 's' of a real vector space 'E', for each 'x' in 'E', there exists a positive real number 'r' such that 'x' is contained in the scalar multiplication of 'r' and 's'.
|
continuousAt_gauge_zero
theorem continuousAt_gauge_zero :
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
[inst_3 : ContinuousSMul ℝ E], s ∈ nhds 0 → ContinuousAt (gauge s) 0
The theorem `continuousAt_gauge_zero` states that if `s` is a neighbourhood of the origin in a real vector space `E`, then the Minkowski functional `gauge s` is continuous at the origin. Here, a neighbourhood of a point is a set that contains an open set around that point, and the Minkowski functional of a set sends a vector to the smallest scalar such that the vector is in the set scaled by that scalar. The vector space `E` is assumed to have an addition operation, a scalar multiplication operation, and a topology, with the scalar multiplication being continuous.
More concisely: Given a real vector space `E` with a topology, if `s` is a neighborhood of the origin, then the Minkowski functional `gauge s` is continuous at the origin.
|
gauge_smul_of_nonneg
theorem gauge_smul_of_nonneg :
∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {α : Type u_4} [inst_2 : LinearOrderedField α]
[inst_3 : MulActionWithZero α ℝ] [inst_4 : OrderedSMul α ℝ] [inst_5 : MulActionWithZero α E]
[inst_6 : IsScalarTower α ℝ (Set E)] {s : Set E} {a : α}, 0 ≤ a → ∀ (x : E), gauge s (a • x) = a • gauge s x
This theorem, referred to as `gauge_smul_of_nonneg`, states that for any real vector space `E` with an additive commutative group structure and a scalar multiplication by real numbers, and for any ordered field `α` that acts on the reals and on `E` with scalar multiplication, if `s` is a set in `E` and `a` is a non-negative element of `α`, then for any element `x` in `E`, the Minkowski functional (or gauge) of the set `s` at a point `a` times `x` is equal to `a` times the Minkowski functional of `s` at `x`. Essentially, it states that scaling a vector by a non-negative scalar in the input of the Minkowski functional for a set corresponds to scaling the output of the functional by the same scalar.
More concisely: For any real vector space with scalar multiplication, and for any non-negative scalar `a` in an ordered field acting on the reals and the vector space, the Minkowski functional of a set `s` at the point `ax` equals `a` times the Minkowski functional of `s` at `x`.
|