Mathlib.Analysis.Convex.EGauge

egauge definition

(𝕜 : Type*) [ENorm 𝕜] {E : Type*} [SMul 𝕜 E] (s : Set E) (x : E) : ℝ≥0∞

Full source

/-- The Minkowski functional for vector spaces over normed fields.
Given a set `s` in a vector space over a normed field `𝕜`,
`egauge s` is the functional which sends `x : E`
to the infimum of `‖c‖ₑ` over `c` such that `x` belongs to `s` scaled by `c`.

The definition only requires `𝕜` to have a `ENorm` instance
and `(· • ·) : 𝕜 → E → E` to be defined.
This way the definition applies, e.g., to `𝕜 = ℝ≥0`.
For `𝕜 = ℝ≥0`, the function is equal (up to conversion to `ℝ`)
to the usual Minkowski functional defined in `gauge`. -/
noncomputable def egauge (𝕜 : Type*) [ENorm 𝕜] {E : Type*} [SMul 𝕜 E] (s : Set E) (x : E) : ℝ≥0∞ :=
  ⨅ (c : 𝕜) (_ : x ∈ c • s), ‖c‖ₑ

Minkowski functional for normed fields

Informal description

Given a normed field $\mathbb{K}$ with an extended norm $\|\cdot\|_e$, a vector space $E$ over $\mathbb{K}$ with a scalar multiplication operation, and a subset $s \subseteq E$, the Minkowski functional (or gauge) $\text{egauge}_{\mathbb{K}}(s, x)$ of $s$ at a point $x \in E$ is defined as the infimum of the extended norms $\|c\|_e$ over all $c \in \mathbb{K}$ such that $x$ belongs to the scaled set $c \cdot s$. In other words: \[ \text{egauge}_{\mathbb{K}}(s, x) = \inf \{\|c\|_e \mid c \in \mathbb{K}, x \in c \cdot s\} \] This functional generalizes the notion of the Minkowski functional to vector spaces over normed fields, including cases like $\mathbb{K} = \mathbb{R}_{\geq 0}$. The result takes values in the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

Set.MapsTo.egauge_le theorem

 {E' F : Type*} [SMul 𝕜 E'] [FunLike F E E'] [MulActionHomClass F 𝕜 E E'] (f : F) {t : Set E'} (h : MapsTo f s t)
  (x : E) : egauge 𝕜 t (f x) ≤ egauge 𝕜 s x

Full source

lemma Set.MapsTo.egauge_le {E' F : Type*} [SMul 𝕜 E'] [FunLike F E E'] [MulActionHomClass F 𝕜 E E']
    (f : F) {t : Set E'} (h : MapsTo f s t) (x : E) : egauge 𝕜 t (f x) ≤ egauge 𝕜 s x :=
  iInf_mono fun c ↦ iInf_mono' fun hc ↦ ⟨h.smul_set c hc, le_rfl⟩

Minkowski Functional Inequality under Equivariant Maps: $\text{egauge}_{\mathbb{K}}(t, f(x)) \leq \text{egauge}_{\mathbb{K}}(s, x)$

Informal description

Let $\mathbb{K}$ be a normed field with an extended norm, and let $E$ and $E'$ be vector spaces over $\mathbb{K}$ with scalar multiplication operations. Let $F$ be a type of $\mathbb{K}$-equivariant maps from $E$ to $E'$, and let $f \in F$ be such that $f$ maps a subset $s \subseteq E$ into a subset $t \subseteq E'$. Then, for any $x \in E$, the Minkowski functional of $t$ at $f(x)$ is less than or equal to the Minkowski functional of $s$ at $x$, i.e., \[ \text{egauge}_{\mathbb{K}}(t, f(x)) \leq \text{egauge}_{\mathbb{K}}(s, x). \]

egauge_anti theorem

(h : s ⊆ t) (x : E) : egauge 𝕜 t x ≤ egauge 𝕜 s x

Full source

@[mono, gcongr]
lemma egauge_anti (h : s ⊆ t) (x : E) : egauge 𝕜 t x ≤ egauge 𝕜 s x :=
  MapsTo.egauge_le _ (MulActionHom.id ..) h _

Monotonicity of Minkowski Functional: $\text{egauge}_{\mathbb{K}}(t, x) \leq \text{egauge}_{\mathbb{K}}(s, x)$ for $s \subseteq t$

Informal description

For any subsets $s$ and $t$ of a vector space $E$ over a normed field $\mathbb{K}$ with $s \subseteq t$, and for any point $x \in E$, the Minkowski functional of $t$ at $x$ is less than or equal to the Minkowski functional of $s$ at $x$, i.e., \[ \text{egauge}_{\mathbb{K}}(t, x) \leq \text{egauge}_{\mathbb{K}}(s, x). \]

egauge_empty theorem

(x : E) : egauge 𝕜 ∅ x = ∞

Full source

@[simp] lemma egauge_empty (x : E) : egauge 𝕜 ∅ x = ∞ := by simp [egauge]

Minkowski Functional of Empty Set is Infinity

Informal description

For any vector space $E$ over a normed field $\mathbb{K}$ and any point $x \in E$, the Minkowski functional of the empty set $\emptyset$ evaluated at $x$ is equal to infinity, i.e., \[ \text{egauge}_{\mathbb{K}}(\emptyset, x) = \infty. \]

egauge_le_of_mem_smul theorem

(h : x ∈ c • s) : egauge 𝕜 s x ≤ ‖c‖ₑ

Full source

lemma egauge_le_of_mem_smul (h : x ∈ c • s) : egauge 𝕜 s x ≤ ‖c‖ₑ := iInf₂_le c h

Upper Bound for Minkowski Functional via Scaled Set Membership

Informal description

For any element $x$ in a vector space $E$ over a normed field $\mathbb{K}$ with extended norm $\|\cdot\|_e$, if $x$ belongs to the scaled set $c \cdot s$ for some $c \in \mathbb{K}$ and subset $s \subseteq E$, then the Minkowski functional (gauge) of $s$ at $x$ satisfies $\text{egauge}_{\mathbb{K}}(s, x) \leq \|c\|_e$.

le_egauge_iff theorem

: r ≤ egauge 𝕜 s x ↔ ∀ c : 𝕜, x ∈ c • s → r ≤ ‖c‖ₑ

Full source

lemma le_egauge_iff : r ≤ egauge 𝕜 s x ↔ ∀ c : 𝕜, x ∈ c • s → r ≤ ‖c‖ₑ := le_iInf₂_iff

Characterization of Lower Bound for Minkowski Functional

Informal description

For any extended nonnegative real number $r$, the Minkowski functional $\text{egauge}_{\mathbb{K}}(s, x)$ satisfies $r \leq \text{egauge}_{\mathbb{K}}(s, x)$ if and only if for every $c \in \mathbb{K}$ such that $x \in c \cdot s$, we have $r \leq \|c\|_e$. In other words: \[ r \leq \inf\{\|c\|_e \mid c \in \mathbb{K}, x \in c \cdot s\} \leftrightarrow \forall c \in \mathbb{K}, (x \in c \cdot s \rightarrow r \leq \|c\|_e) \]

egauge_eq_top theorem

: egauge 𝕜 s x = ∞ ↔ ∀ c : 𝕜, x ∉ c • s

Full source

lemma egauge_eq_top : egaugeegauge 𝕜 s x = ∞ ↔ ∀ c : 𝕜, x ∉ c • s := by simp [egauge]

Minkowski Functional Equals Infinity if and only if No Scalar Multiple Contains the Point

Informal description

For a subset $s$ of a vector space $E$ over a normed field $\mathbb{K}$ and a point $x \in E$, the Minkowski functional $\text{egauge}_{\mathbb{K}}(s, x)$ equals infinity if and only if there does not exist any scalar $c \in \mathbb{K}$ such that $x$ belongs to the scaled set $c \cdot s$. In other words: \[ \text{egauge}_{\mathbb{K}}(s, x) = \infty \leftrightarrow \forall c \in \mathbb{K}, \, x \notin c \cdot s \]

egauge_lt_iff theorem

: egauge 𝕜 s x < r ↔ ∃ c : 𝕜, x ∈ c • s ∧ ‖c‖ₑ < r

Full source

lemma egauge_lt_iff : egaugeegauge 𝕜 s x < r ↔ ∃ c : 𝕜, x ∈ c • s ∧ ‖c‖ₑ < r := by
  simp [egauge, iInf_lt_iff]

Characterization of Minkowski Functional via Strict Inequality

Informal description

For a normed field $\mathbb{K}$ with extended norm $\|\cdot\|_e$, a vector space $E$ over $\mathbb{K}$, a subset $s \subseteq E$, and a point $x \in E$, the Minkowski functional $\text{egauge}_{\mathbb{K}}(s, x)$ is strictly less than $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ if and only if there exists $c \in \mathbb{K}$ such that $x \in c \cdot s$ and $\|c\|_e < r$. In other words: \[ \text{egauge}_{\mathbb{K}}(s, x) < r \iff \exists c \in \mathbb{K}, (x \in c \cdot s) \land (\|c\|_e < r) \]

egauge_union theorem

(s t : Set E) (x : E) : egauge 𝕜 (s ∪ t) x = egauge 𝕜 s x ⊓ egauge 𝕜 t x

Full source

lemma egauge_union (s t : Set E) (x : E) : egauge 𝕜 (s ∪ t) x = egaugeegauge 𝕜 s x ⊓ egauge 𝕜 t x := by
  unfold egauge
  simp [smul_set_union, iInf_or, iInf_inf_eq]

Minkowski Functional of Union is Minimum of Individual Functionals

Informal description

For any subsets $s$ and $t$ of a vector space $E$ over a normed field $\mathbb{K}$ and any point $x \in E$, the Minkowski functional of the union $s \cup t$ at $x$ equals the infimum of the Minkowski functionals of $s$ and $t$ at $x$. In other words: \[ \text{egauge}_{\mathbb{K}}(s \cup t, x) = \min \left( \text{egauge}_{\mathbb{K}}(s, x), \text{egauge}_{\mathbb{K}}(t, x) \right) \]

le_egauge_inter theorem

(s t : Set E) (x : E) : egauge 𝕜 s x ⊔ egauge 𝕜 t x ≤ egauge 𝕜 (s ∩ t) x

Full source

lemma le_egauge_inter (s t : Set E) (x : E) :
    egaugeegauge 𝕜 s x ⊔ egauge 𝕜 t x ≤ egauge 𝕜 (s ∩ t) x :=
  max_le (egauge_anti _ inter_subset_left _) (egauge_anti _ inter_subset_right _)

Minkowski Functional Inequality for Set Intersection: $\max(\text{egauge}_{\mathbb{K}}(s, x), \text{egauge}_{\mathbb{K}}(t, x)) \leq \text{egauge}_{\mathbb{K}}(s \cap t, x)$

Informal description

For any subsets $s$ and $t$ of a vector space $E$ over a normed field $\mathbb{K}$, and for any point $x \in E$, the maximum of the Minkowski functionals of $s$ and $t$ at $x$ is less than or equal to the Minkowski functional of their intersection $s \cap t$ at $x$. In other words: \[ \max \left( \text{egauge}_{\mathbb{K}}(s, x), \text{egauge}_{\mathbb{K}}(t, x) \right) \leq \text{egauge}_{\mathbb{K}}(s \cap t, x) \]

le_egauge_pi theorem

 {ι : Type*} {E : ι → Type*} [∀ i, SMul 𝕜 (E i)] {I : Set ι} {i : ι} (hi : i ∈ I) (s : ∀ i, Set (E i)) (x : ∀ i, E i) :
  egauge 𝕜 (s i) (x i) ≤ egauge 𝕜 (I.pi s) x

Full source

lemma le_egauge_pi {ι : Type*} {E : ι → Type*} [∀ i, SMul 𝕜 (E i)] {I : Set ι} {i : ι}
    (hi : i ∈ I) (s : ∀ i, Set (E i)) (x : ∀ i, E i) :
    egauge 𝕜 (s i) (x i) ≤ egauge 𝕜 (I.pi s) x :=
  MapsTo.egauge_le _ (Pi.evalMulActionHom i) (fun x hx ↦ by exact hx i hi) _

Minkowski Functional Inequality for Product Sets: $\text{egauge}_{\mathbb{K}}(s_i, x_i) \leq \text{egauge}_{\mathbb{K}}(\prod_{i \in I} s_i, x)$

Informal description

Let $\mathbb{K}$ be a normed field with extended norm, and let $\{E_i\}_{i \in \iota}$ be a family of vector spaces over $\mathbb{K}$ equipped with scalar multiplication. For any index set $I \subseteq \iota$ and any index $i \in I$, given a family of subsets $s_i \subseteq E_i$ and a point $x = (x_i)_{i \in \iota}$ in the product space $\prod_{i \in \iota} E_i$, the Minkowski functional of $s_i$ at $x_i$ is less than or equal to the Minkowski functional of the product set $\prod_{i \in I} s_i$ at $x$. In other words: \[ \text{egauge}_{\mathbb{K}}(s_i, x_i) \leq \text{egauge}_{\mathbb{K}}\left(\prod_{i \in I} s_i, x\right) \]

le_egauge_prod theorem

(s : Set E) (t : Set F) (a : E) (b : F) : max (egauge 𝕜 s a) (egauge 𝕜 t b) ≤ egauge 𝕜 (s ×ˢ t) (a, b)

Full source

lemma le_egauge_prod (s : Set E) (t : Set F) (a : E) (b : F) :
    max (egauge 𝕜 s a) (egauge 𝕜 t b) ≤ egauge 𝕜 (s ×ˢ t) (a, b) :=
  max_le (mapsTo_fst_prod.egauge_le 𝕜 (MulActionHom.fst 𝕜 E F) (a, b))
    (MapsTo.egauge_le 𝕜 (MulActionHom.snd 𝕜 E F) mapsTo_snd_prod (a, b))

Minkowski Functional Inequality for Cartesian Products: $\max(\text{egauge}_{\mathbb{K}}(s, a), \text{egauge}_{\mathbb{K}}(t, b)) \leq \text{egauge}_{\mathbb{K}}(s \times t, (a, b))$

Informal description

Let $\mathbb{K}$ be a normed field with an extended norm, and let $E$ and $F$ be vector spaces over $\mathbb{K}$. For any subsets $s \subseteq E$ and $t \subseteq F$, and any elements $a \in E$ and $b \in F$, the maximum of the Minkowski functionals of $s$ at $a$ and of $t$ at $b$ is less than or equal to the Minkowski functional of the Cartesian product $s \times t$ at the point $(a, b)$. In other words: \[ \max \left( \text{egauge}_{\mathbb{K}}(s, a), \text{egauge}_{\mathbb{K}}(t, b) \right) \leq \text{egauge}_{\mathbb{K}}(s \times t, (a, b)) \]

egauge_zero_left_eq_top theorem

: egauge 𝕜 0 x = ∞ ↔ x ≠ 0

Full source

@[simp] lemma egauge_zero_left_eq_top : egaugeegauge 𝕜 0 x = ∞ ↔ x ≠ 0 := by
  simp [egauge_eq_top]

Minkowski Functional of Zero Set is Infinite for Nonzero Vectors

Informal description

For any normed field $\mathbb{K}$ with extended norm $\|\cdot\|_e$, vector space $E$ over $\mathbb{K}$, and nonzero element $x \in E$, the Minkowski functional of the zero set at $x$ is infinite, i.e., $\text{egauge}_{\mathbb{K}}(0, x) = \infty$ if and only if $x \neq 0$.

egauge_le_of_smul_mem_of_ne theorem

(h : c • x ∈ s) (hc : c ≠ 0) : egauge 𝕜 s x ≤ (‖c‖₊⁻¹ : ℝ≥0)

Full source

/-- If `c • x ∈ s` and `c ≠ 0`, then `egauge 𝕜 s x` is at most `(‖c‖₊⁻¹ : ℝ≥0)`.

See also `egauge_le_of_smul_mem`. -/
lemma egauge_le_of_smul_mem_of_ne (h : c • x ∈ s) (hc : c ≠ 0) : egauge 𝕜 s x ≤ (‖c‖₊‖c‖₊⁻¹ : ℝ≥0) := by
  rw [← nnnorm_inv]
  exact egauge_le_of_mem_smul <| (mem_inv_smul_set_iff₀ hc _ _).2 h

Upper Bound for Minkowski Functional via Nonzero Scaled Membership: $\text{egauge}_{\mathbb{K}}(s, x) \leq \|c\|^{-1}$

Informal description

Let $\mathbb{K}$ be a normed field, $E$ a vector space over $\mathbb{K}$, and $s \subseteq E$. For any $x \in E$ and $c \in \mathbb{K}$ with $c \neq 0$, if $c \cdot x \in s$, then the Minkowski functional $\text{egauge}_{\mathbb{K}}(s, x)$ satisfies $\text{egauge}_{\mathbb{K}}(s, x) \leq \|c\|_{\mathbb{R}_{\geq 0}}^{-1}$.

egauge_le_of_smul_mem theorem

(h : c • x ∈ s) : egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹

Full source

/-- If `c • x ∈ s`, then `egauge 𝕜 s x` is at most `‖c‖ₑ⁻¹`.

See also `egauge_le_of_smul_mem_of_ne`. -/
lemma egauge_le_of_smul_mem (h : c • x ∈ s) : egauge 𝕜 s x ≤ ‖c‖ₑ‖c‖ₑ⁻¹ := by
  rcases eq_or_ne c 0 with rfl | hc
  · simp
  · exact (egauge_le_of_smul_mem_of_ne h hc).trans ENNReal.coe_inv_le

Upper Bound for Minkowski Functional via Scaled Membership: $\text{egauge}_{\mathbb{K}}(s, x) \leq \|c\|_e^{-1}$

Informal description

For any normed field $\mathbb{K}$ with extended norm $\|\cdot\|_e$, vector space $E$ over $\mathbb{K}$, subset $s \subseteq E$, and $x \in E$, if there exists $c \in \mathbb{K}$ such that $c \cdot x \in s$, then the Minkowski functional $\text{egauge}_{\mathbb{K}}(s, x)$ satisfies $\text{egauge}_{\mathbb{K}}(s, x) \leq \|c\|_e^{-1}$.

mem_smul_of_egauge_lt theorem

(hs : Balanced 𝕜 s) (hc : egauge 𝕜 s x < ‖c‖ₑ) : x ∈ c • s

Full source

lemma mem_smul_of_egauge_lt (hs : Balanced 𝕜 s) (hc : egauge 𝕜 s x < ‖c‖ₑ) : x ∈ c • s :=
  let ⟨a, hxa, ha⟩ := egauge_lt_iff.1 hc
  hs.smul_mono (by simpa [enorm] using ha.le) hxa

Membership in Scaled Set via Minkowski Functional: $\text{egauge}_{\mathbb{K}}(s, x) < \|c\|_e \implies x \in c \cdot s$

Informal description

Let $\mathbb{K}$ be a normed field, $E$ a vector space over $\mathbb{K}$, and $s \subseteq E$ a balanced set. For any $x \in E$ and $c \in \mathbb{K}$, if the Minkowski functional $\text{egauge}_{\mathbb{K}}(s, x)$ satisfies $\text{egauge}_{\mathbb{K}}(s, x) < \|c\|_e$, then $x$ belongs to the scaled set $c \cdot s$. In other words: \[ \text{If } s \text{ is balanced and } \text{egauge}_{\mathbb{K}}(s, x) < \|c\|_e, \text{ then } x \in c \cdot s. \]

mem_of_egauge_lt_one theorem

(hs : Balanced 𝕜 s) (hx : egauge 𝕜 s x < 1) : x ∈ s

Full source

lemma mem_of_egauge_lt_one (hs : Balanced 𝕜 s) (hx : egauge 𝕜 s x < 1) : x ∈ s :=
  one_smul 𝕜 s ▸ mem_smul_of_egauge_lt hs (by simpa)

Membership in Set via Minkowski Functional: $\text{egauge}_{\mathbb{K}}(s, x) < 1 \implies x \in s$

Informal description

Let $\mathbb{K}$ be a normed field, $E$ a vector space over $\mathbb{K}$, and $s \subseteq E$ a balanced set. For any $x \in E$, if the Minkowski functional $\text{egauge}_{\mathbb{K}}(s, x)$ satisfies $\text{egauge}_{\mathbb{K}}(s, x) < 1$, then $x$ belongs to $s$. In other words: \[ \text{If } s \text{ is balanced and } \text{egauge}_{\mathbb{K}}(s, x) < 1, \text{ then } x \in s. \]

egauge_eq_zero_iff theorem

: egauge 𝕜 s x = 0 ↔ ∃ᶠ c : 𝕜 in 𝓝 0, x ∈ c • s

Full source

lemma egauge_eq_zero_iff : egaugeegauge 𝕜 s x = 0 ↔ ∃ᶠ c : 𝕜 in 𝓝 0, x ∈ c • s := by
  refine (iInf₂_eq_bot _).trans ?_
  rw [(nhds_basis_uniformity uniformity_basis_edist).frequently_iff]
  simp [and_comm]

Minkowski Functional Vanishes if and only if Zero is a Limit Point of Scalars Mapping $x$ into $s$

Informal description

For a normed field $\mathbb{K}$ and a subset $s$ of a vector space $E$ over $\mathbb{K}$, the Minkowski functional $\text{egauge}_{\mathbb{K}}(s, x)$ evaluated at $x \in E$ equals zero if and only if there exists a net of scalars $c \in \mathbb{K}$ converging to zero such that $x$ belongs to $c \cdot s$ frequently (i.e., for every neighborhood of zero, there exists such a $c$ in that neighborhood). In other words: \[ \text{egauge}_{\mathbb{K}}(s, x) = 0 \leftrightarrow \text{For every neighborhood } U \text{ of } 0 \text{ in } \mathbb{K}, \exists c \in U \text{ such that } x \in c \cdot s. \]

egauge_univ theorem

[(𝓝[≠] (0 : 𝕜)).NeBot] : egauge 𝕜 univ x = 0

Full source

@[simp]
lemma egauge_univ [(𝓝[≠] (0 : 𝕜)).NeBot] : egauge 𝕜 univ x = 0 := by
  rw [egauge_eq_zero_iff]
  refine (frequently_iff_neBot.2 ‹_›).mono fun c hc ↦ ?_
  simp_all [smul_set_univ₀]

Minkowski Functional of Universal Set Vanishes Everywhere

Informal description

For any normed field $\mathbb{K}$ where the punctured neighborhood filter at zero is non-trivial, the Minkowski functional of the universal set $\text{univ}$ in a vector space $E$ over $\mathbb{K}$ evaluated at any point $x \in E$ is zero, i.e., $\text{egauge}_{\mathbb{K}}(\text{univ}, x) = 0$.

egauge_zero_right theorem

(hs : s.Nonempty) : egauge 𝕜 s 0 = 0

Full source

@[simp]
lemma egauge_zero_right (hs : s.Nonempty) : egauge 𝕜 s 0 = 0 := by
  have : 0 ∈ (0 : 𝕜) • s := by simp [zero_smul_set hs]
  simpa using egauge_le_of_mem_smul this

Minkowski Functional of Nonempty Set at Zero is Zero

Informal description

For any nonempty subset $s$ of a vector space $E$ over a normed field $\mathbb{K}$, the Minkowski functional (gauge) of $s$ evaluated at the zero vector is zero, i.e., $\text{egauge}_{\mathbb{K}}(s, 0) = 0$.

egauge_zero_zero theorem

: egauge 𝕜 (0 : Set E) 0 = 0

Full source

lemma egauge_zero_zero : egauge 𝕜 (0 : Set E) 0 = 0 := by simp

Minkowski Functional of Zero Set at Zero is Zero

Informal description

For any normed field $\mathbb{K}$ and vector space $E$ over $\mathbb{K}$, the Minkowski functional (gauge) of the zero set evaluated at the zero vector is zero, i.e., $\text{egauge}_{\mathbb{K}}(\{0\}, 0) = 0$.

egauge_le_one theorem

(h : x ∈ s) : egauge 𝕜 s x ≤ 1

Full source

lemma egauge_le_one (h : x ∈ s) : egauge 𝕜 s x ≤ 1 := by
  rw [← one_smul 𝕜 s] at h
  simpa using egauge_le_of_mem_smul h

Upper bound of Minkowski functional for elements in the set

Informal description

For any element $x$ in a subset $s$ of a vector space $E$ over a normed field $\mathbb{K}$, the Minkowski functional (gauge) of $s$ at $x$ satisfies $\text{egauge}_{\mathbb{K}}(s, x) \leq 1$.

le_egauge_smul_left theorem

(c : 𝕜) (s : Set E) (x : E) : egauge 𝕜 s x / ‖c‖ₑ ≤ egauge 𝕜 (c • s) x

Full source

lemma le_egauge_smul_left (c : 𝕜) (s : Set E) (x : E) :
    egauge 𝕜 s x / ‖c‖ₑ ≤ egauge 𝕜 (c • s) x := by
  simp_rw [le_egauge_iff, smul_smul]
  rintro a ⟨x, hx, rfl⟩
  apply ENNReal.div_le_of_le_mul
  rw [← enorm_mul]
  exact egauge_le_of_mem_smul <| smul_mem_smul_set hx

Lower Bound for Scaled Minkowski Functional: $\text{egauge}(s, x) / \|c\|_e \leq \text{egauge}(c \cdot s, x)$

Informal description

For any element $x$ in a vector space $E$ over a normed field $\mathbb{K}$ with extended norm $\|\cdot\|_e$, and for any subset $s \subseteq E$ and scalar $c \in \mathbb{K}$, the Minkowski functional (gauge) satisfies the inequality: \[ \frac{\text{egauge}_{\mathbb{K}}(s, x)}{\|c\|_e} \leq \text{egauge}_{\mathbb{K}}(c \cdot s, x) \] where $c \cdot s$ denotes the scaled set $\{c \cdot y \mid y \in s\}$.

egauge_smul_left theorem

(hc : c ≠ 0) (s : Set E) (x : E) : egauge 𝕜 (c • s) x = egauge 𝕜 s x / ‖c‖ₑ

Full source

lemma egauge_smul_left (hc : c ≠ 0) (s : Set E) (x : E) :
    egauge 𝕜 (c • s) x = egauge 𝕜 s x / ‖c‖ₑ := by
  refine le_antisymm ?_ (le_egauge_smul_left _ _ _)
  rw [ENNReal.le_div_iff_mul_le (by simp [*]) (by simp)]
  calc
    egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ := by
      rw [enorm_inv (by simpa), div_eq_mul_inv, inv_inv]
    _ ≤ egauge 𝕜 (c⁻¹ • c • s) x := le_egauge_smul_left _ _ _
    _ = egauge 𝕜 s x := by rw [inv_smul_smul₀ hc]

Minkowski Functional Scaling Identity: $\text{egauge}(c \cdot s, x) = \text{egauge}(s, x) / \|c\|_e$ for $c \neq 0$

Informal description

For any nonzero scalar $c$ in a normed field $\mathbb{K}$ with extended norm $\|\cdot\|_e$, any subset $s$ of a vector space $E$ over $\mathbb{K}$, and any vector $x \in E$, the Minkowski functional satisfies: \[ \text{egauge}_{\mathbb{K}}(c \cdot s, x) = \frac{\text{egauge}_{\mathbb{K}}(s, x)}{\|c\|_e} \] where $c \cdot s$ denotes the scaled set $\{c \cdot y \mid y \in s\}$.

le_egauge_smul_right theorem

(c : 𝕜) (s : Set E) (x : E) : ‖c‖ₑ * egauge 𝕜 s x ≤ egauge 𝕜 s (c • x)

Full source

lemma le_egauge_smul_right (c : 𝕜) (s : Set E) (x : E) :
    ‖c‖ₑ * egauge 𝕜 s x ≤ egauge 𝕜 s (c • x) := by
  rw [le_egauge_iff]
  rintro a ⟨y, hy, hxy⟩
  rcases eq_or_ne c 0 with rfl | hc
  · simp
  · refine ENNReal.mul_le_of_le_div' <| le_trans ?_ ENNReal.coe_div_le
    rw [div_eq_inv_mul, ← nnnorm_inv, ← nnnorm_mul]
    refine egauge_le_of_mem_smul ⟨y, hy, ?_⟩
    simp only [mul_smul, hxy, inv_smul_smul₀ hc]

Lower Bound for Minkowski Functional under Scalar Multiplication: $\|c\|_e \cdot \text{egauge}(s, x) \leq \text{egauge}(s, c \cdot x)$

Informal description

For any scalar $c$ in a normed field $\mathbb{K}$ with extended norm $\|\cdot\|_e$, any subset $s$ of a vector space $E$ over $\mathbb{K}$, and any vector $x \in E$, the Minkowski functional satisfies the inequality: \[ \|c\|_e \cdot \text{egauge}_{\mathbb{K}}(s, x) \leq \text{egauge}_{\mathbb{K}}(s, c \cdot x). \]

egauge_smul_right theorem

(h : c = 0 → s.Nonempty) (x : E) : egauge 𝕜 s (c • x) = ‖c‖ₑ * egauge 𝕜 s x

Full source

lemma egauge_smul_right (h : c = 0 → s.Nonempty) (x : E) :
    egauge 𝕜 s (c • x) = ‖c‖ₑ * egauge 𝕜 s x := by
  refine le_antisymm ?_ (le_egauge_smul_right c s x)
  rcases eq_or_ne c 0 with rfl | hc
  · simp [egauge_zero_right _ (h rfl)]
  · rw [mul_comm, ← ENNReal.div_le_iff_le_mul (.inl <| by simpa) (.inl enorm_ne_top),
      ENNReal.div_eq_inv_mul, ← enorm_inv (by simpa)]
    refine (le_egauge_smul_right _ _ _).trans_eq ?_
    rw [inv_smul_smul₀ hc]

Minkowski Functional Scaling Identity: $\text{egauge}(s, c \cdot x) = \|c\|_e \cdot \text{egauge}(s, x)$ under Nonemptiness Condition

Informal description

For any scalar $c$ in a normed field $\mathbb{K}$ with extended norm $\|\cdot\|_e$, any subset $s$ of a vector space $E$ over $\mathbb{K}$, and any vector $x \in E$, if $c = 0$ implies that $s$ is nonempty, then the Minkowski functional satisfies: \[ \text{egauge}_{\mathbb{K}}(s, c \cdot x) = \|c\|_e \cdot \text{egauge}_{\mathbb{K}}(s, x). \]

egauge_prod_mk theorem

 {F : Type*} [AddCommGroup F] [Module 𝕜 F] {U : Set E} {V : Set F} (hU : Balanced 𝕜 U) (hV : Balanced 𝕜 V) (a : E)
  (b : F) : egauge 𝕜 (U ×ˢ V) (a, b) = max (egauge 𝕜 U a) (egauge 𝕜 V b)

Full source

/-- The extended gauge of a point `(a, b)` with respect to the product of balanced sets `U` and `V`
is equal to the maximum of the extended gauges of `a` with respect to `U`
and `b` with respect to `V`.
-/
theorem egauge_prod_mk {F : Type*} [AddCommGroup F] [Module 𝕜 F] {U : Set E} {V : Set F}
    (hU : Balanced 𝕜 U) (hV : Balanced 𝕜 V) (a : E) (b : F) :
    egauge 𝕜 (U ×ˢ V) (a, b) = max (egauge 𝕜 U a) (egauge 𝕜 V b) := by
  refine le_antisymm (le_of_forall_lt' fun r hr ↦ ?_) (le_egauge_prod _ _ _ _)
  simp only [max_lt_iff, egauge_lt_iff, smul_set_prod, mk_mem_prod] at hr ⊢
  rcases hr with ⟨⟨x, hx, hxr⟩, ⟨y, hy, hyr⟩⟩
  cases le_total ‖x‖ ‖y‖ with
  | inl hle => exact ⟨y, ⟨hU.smul_mono hle hx, hy⟩, hyr⟩
  | inr hle => exact ⟨x, ⟨hx, hV.smul_mono hle hy⟩, hxr⟩

Minkowski Functional of Product Set Equals Maximum of Component Functionals

Informal description

Let $\mathbb{K}$ be a normed field, $E$ and $F$ be vector spaces over $\mathbb{K}$, and $U \subseteq E$, $V \subseteq F$ be balanced sets. For any elements $a \in E$ and $b \in F$, the Minkowski functional of the product set $U \times V$ at the point $(a, b)$ equals the maximum of the Minkowski functionals of $U$ at $a$ and of $V$ at $b$. That is: \[ \text{egauge}_{\mathbb{K}}(U \times V, (a, b)) = \max \left( \text{egauge}_{\mathbb{K}}(U, a), \text{egauge}_{\mathbb{K}}(V, b) \right). \]

egauge_add_add_le theorem

 {U V : Set E} (hU : Balanced 𝕜 U) (hV : Balanced 𝕜 V) (a b : E) :
  egauge 𝕜 (U + V) (a + b) ≤ max (egauge 𝕜 U a) (egauge 𝕜 V b)

Full source

theorem egauge_add_add_le {U V : Set E} (hU : Balanced 𝕜 U) (hV : Balanced 𝕜 V) (a b : E) :
    egauge 𝕜 (U + V) (a + b) ≤ max (egauge 𝕜 U a) (egauge 𝕜 V b) := by
  rw [← egauge_prod_mk hU hV a b, ← add_image_prod]
  exact MapsTo.egauge_le 𝕜 (LinearMap.fst 𝕜 E E + LinearMap.snd 𝕜 E E) (mapsTo_image _ _) (a, b)

Subadditivity of Minkowski Functional for Balanced Sets: $\text{egauge}_{\mathbb{K}}(U + V, a + b) \leq \max(\text{egauge}_{\mathbb{K}}(U, a), \text{egauge}_{\mathbb{K}}(V, b))$

Informal description

Let $\mathbb{K}$ be a normed field, $E$ a vector space over $\mathbb{K}$, and $U, V \subseteq E$ balanced sets. For any elements $a, b \in E$, the Minkowski functional of the Minkowski sum $U + V$ at the point $a + b$ satisfies the inequality: \[ \text{egauge}_{\mathbb{K}}(U + V, a + b) \leq \max \left( \text{egauge}_{\mathbb{K}}(U, a), \text{egauge}_{\mathbb{K}}(V, b) \right). \]

egauge_pi' theorem

 {I : Set ι} (hI : I.Finite) {U : ∀ i, Set (E i)} (hU : ∀ i ∈ I, Balanced 𝕜 (U i)) (x : ∀ i, E i)
  (hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ (𝓝[≠] (0 : 𝕜)).NeBot) : egauge 𝕜 (I.pi U) x = ⨆ i ∈ I, egauge 𝕜 (U i) (x i)

Full source

/-- The extended gauge of a point `x` in an indexed product
with respect to a product of finitely many balanced sets `U i`, `i ∈ I`,
(and the whole spaces for the other indices)
is the supremum of the extended gauges of the components of `x`
with respect to the corresponding balanced set.

This version assumes the following technical condition:
- either `I` is the universal set;
- or one of `x i`, `i ∈ I`, is nonzero;
- or `𝕜` is nontrivially normed.
-/
theorem egauge_pi' {I : Set ι} (hI : I.Finite)
    {U : ∀ i, Set (E i)} (hU : ∀ i ∈ I, Balanced 𝕜 (U i))
    (x : ∀ i, E i) (hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ (𝓝[≠] (0 : 𝕜)).NeBot) :
    egauge 𝕜 (I.pi U) x = ⨆ i ∈ I, egauge 𝕜 (U i) (x i) := by
  refine le_antisymm ?_ (iSup₂_le fun i hi ↦ le_egauge_pi hi _ _)
  refine le_of_forall_lt' fun r hr ↦ ?_
  have : ∀ i ∈ I, ∃ c : 𝕜, x i ∈ c • U i ∧ ‖c‖ₑ < r := fun i hi ↦
    egauge_lt_iff.mp <| (le_iSup₂ i hi).trans_lt hr
  choose! c hc hcr using this
  obtain ⟨c₀, hc₀, hc₀I, hc₀r⟩ :
      ∃ c₀ : 𝕜, (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r := by
    have hr₀ : 0 < r := hr.bot_lt
    rcases I.eq_empty_or_nonempty with rfl | hIne
    · obtain hι | hbot : IsEmptyIsEmpty ι ∨ (𝓝[≠] (0 : 𝕜)).NeBot := by simpa [@eq_comm _ ∅] using hI₀
      · use 0
        simp [@eq_comm _ ∅, hι, hr₀]
      · rcases exists_enorm_lt 𝕜 hr₀.ne' with ⟨c₀, hc₀, hc₀r⟩
        exact ⟨c₀, .inl hc₀, by simp, hc₀r⟩
    · obtain ⟨i₀, hi₀I, hc_max⟩ : ∃ i₀ ∈ I, IsMaxOn (‖c ·‖ₑ) I i₀ :=
        exists_max_image _ (‖c ·‖ₑ) hI hIne
      by_cases H : c i₀ ≠ 0 ∨ I = univ
      · exact ⟨c i₀, H, fun i hi ↦ by simpa [enorm] using hc_max hi, hcr _ hi₀I⟩
      · push_neg at H
        have hc0 (i : ι) (hi : i ∈ I) : c i = 0 := by simpa [H] using hc_max hi
        have heg0 (i : ι) (hi : i ∈ I) : x i = 0 :=
          zero_smul_set_subset (α := 𝕜) (U i) (hc0 i hi ▸ hc i hi)
        have : (𝓝[≠] (0 : 𝕜)).NeBot := (hI₀.resolve_left H.2).resolve_left (by simpa)
        rcases exists_enorm_lt 𝕜 hr₀.ne' with ⟨c₁, hc₁, hc₁r⟩
        refine ⟨c₁, .inl hc₁, fun i hi ↦ ?_, hc₁r⟩
        simp [hc0 i hi]
  refine egauge_lt_iff.2 ⟨c₀, ?_, hc₀r⟩
  rw [smul_set_pi₀' hc₀]
  intro i hi
  exact (hU i hi).smul_mono (hc₀I i hi) (hc i hi)

Minkowski Functional of Product Set: $\text{egauge}_{\mathbb{K}}(\prod_{i \in I} U_i, x) = \sup_{i \in I} \text{egauge}_{\mathbb{K}}(U_i, x_i)$ under Technical Conditions

Informal description

Let $\mathbb{K}$ be a normed field, $\{E_i\}_{i \in \iota}$ a family of vector spaces over $\mathbb{K}$, and $I \subseteq \iota$ a finite subset. For each $i \in I$, let $U_i \subseteq E_i$ be a balanced set. Given a point $x = (x_i)_{i \in \iota} \in \prod_{i \in \iota} E_i$, the Minkowski functional of the product set $\prod_{i \in I} U_i$ at $x$ satisfies \[ \text{egauge}_{\mathbb{K}}\left(\prod_{i \in I} U_i, x\right) = \sup_{i \in I} \text{egauge}_{\mathbb{K}}(U_i, x_i), \] provided that either: 1. $I$ is the universal set (i.e., $I = \iota$), or 2. there exists $i \in I$ such that $x_i \neq 0$, or 3. the punctured neighborhood filter of $0$ in $\mathbb{K}$ is nontrivial (i.e., $\mathbb{K}$ is a nontrivially normed field).

egauge_univ_pi theorem

 [Finite ι] {U : ∀ i, Set (E i)} (hU : ∀ i, Balanced 𝕜 (U i)) (x : ∀ i, E i) :
  egauge 𝕜 (univ.pi U) x = ⨆ i, egauge 𝕜 (U i) (x i)

Full source

/-- The extended gauge of a point `x` in an indexed product with finite index type
with respect to a product of balanced sets `U i`,
is the supremum of the extended gauges of the components of `x`
with respect to the corresponding balanced set.
-/
theorem egauge_univ_pi [Finite ι] {U : ∀ i, Set (E i)} (hU : ∀ i, Balanced 𝕜 (U i)) (x : ∀ i, E i) :
    egauge 𝕜 (univ.pi U) x = ⨆ i, egauge 𝕜 (U i) (x i) :=
  egauge_pi' finite_univ (fun i _ ↦ hU i) x (.inl rfl) |>.trans <| by simp

Minkowski Functional of Universal Product Set: $\text{egauge}_{\mathbb{K}}(\prod_{i} U_i, x) = \sup_i \text{egauge}_{\mathbb{K}}(U_i, x_i)$ for Finite Index Sets

Informal description

Let $\mathbb{K}$ be a normed field, $\{E_i\}_{i \in \iota}$ a finite family of vector spaces over $\mathbb{K}$, and for each $i \in \iota$, let $U_i \subseteq E_i$ be a balanced set. Given a point $x = (x_i)_{i \in \iota} \in \prod_{i \in \iota} E_i$, the Minkowski functional of the product set $\prod_{i \in \iota} U_i$ at $x$ satisfies \[ \text{egauge}_{\mathbb{K}}\left(\prod_{i \in \iota} U_i, x\right) = \sup_{i \in \iota} \text{egauge}_{\mathbb{K}}(U_i, x_i). \]

egauge_pi theorem

 [(𝓝[≠] (0 : 𝕜)).NeBot] {I : Set ι} {U : ∀ i, Set (E i)} (hI : I.Finite) (hU : ∀ i ∈ I, Balanced 𝕜 (U i))
  (x : ∀ i, E i) : egauge 𝕜 (I.pi U) x = ⨆ i ∈ I, egauge 𝕜 (U i) (x i)

Full source

/-- The extended gauge of a point `x` in an indexed product
with respect to a product of finitely many balanced sets `U i`, `i ∈ I`,
(and the whole spaces for the other indices)
is the supremum of the extended gauges of the components of `x`
with respect to the corresponding balanced set.

This version assumes that `𝕜` is a nontrivially normed division ring.
See also `egauge_univ_pi` for when `s = univ`,
and `egauge_pi'` for a version with more choices of the technical assumptions.
-/
theorem egauge_pi [(𝓝[≠] (0 : 𝕜)).NeBot] {I : Set ι} {U : ∀ i, Set (E i)}
    (hI : I.Finite) (hU : ∀ i ∈ I, Balanced 𝕜 (U i)) (x : ∀ i, E i) :
    egauge 𝕜 (I.pi U) x = ⨆ i ∈ I, egauge 𝕜 (U i) (x i) :=
  egauge_pi' hI hU x <| .inr <| .inr inferInstance

Minkowski Functional of Finite Product of Balanced Sets: $\text{egauge}_{\mathbb{K}}(\prod_{i \in I} U_i, x) = \sup_{i \in I} \text{egauge}_{\mathbb{K}}(U_i, x_i)$ for Nontrivially Normed $\mathbb{K}$

Informal description

Let $\mathbb{K}$ be a nontrivially normed division ring, $\{E_i\}_{i \in \iota}$ a family of vector spaces over $\mathbb{K}$, and $I \subseteq \iota$ a finite subset. For each $i \in I$, let $U_i \subseteq E_i$ be a balanced set. Given a point $x = (x_i)_{i \in \iota} \in \prod_{i \in \iota} E_i$, the Minkowski functional of the product set $\prod_{i \in I} U_i$ at $x$ satisfies \[ \text{egauge}_{\mathbb{K}}\left(\prod_{i \in I} U_i, x\right) = \sup_{i \in I} \text{egauge}_{\mathbb{K}}(U_i, x_i). \]

div_le_egauge_closedBall theorem

(r : ℝ≥0) (x : E) : ‖x‖ₑ / r ≤ egauge 𝕜 (closedBall 0 r) x

Full source

lemma div_le_egauge_closedBall (r : ℝ≥0) (x : E) : ‖x‖ₑ / r ≤ egauge 𝕜 (closedBall 0 r) x := by
  rw [le_egauge_iff]
  rintro c ⟨y, hy, rfl⟩
  rw [mem_closedBall_zero_iff, ← coe_nnnorm, NNReal.coe_le_coe] at hy
  rw [enorm_smul]
  apply ENNReal.div_le_of_le_mul
  gcongr
  rwa [enorm_le_coe]

Ratio of Extended Norm to Radius is Bounded by Minkowski Functional of Closed Ball

Informal description

For any non-negative real number $r$ and any vector $x$ in a normed space $E$ over a normed field $\mathbb{K}$, the ratio of the extended norm $\|x\|_e$ to $r$ is bounded above by the Minkowski functional of the closed ball $\overline{B}(0, r)$ centered at the origin with radius $r$ evaluated at $x$. In other words: \[ \frac{\|x\|_e}{r} \leq \text{egauge}_{\mathbb{K}}(\overline{B}(0, r), x). \]

le_egauge_closedBall_one theorem

(x : E) : ‖x‖ₑ ≤ egauge 𝕜 (closedBall 0 1) x

Full source

lemma le_egauge_closedBall_one (x : E) : ‖x‖ₑ ≤ egauge 𝕜 (closedBall 0 1) x := by
  simpa using div_le_egauge_closedBall 𝕜 1 x

Extended Norm Bounded by Minkowski Functional of Closed Unit Ball

Informal description

For any vector $x$ in a normed space $E$ over a normed field $\mathbb{K}$, the extended norm $\|x\|_e$ is bounded above by the Minkowski functional of the closed unit ball $\overline{B}(0, 1)$ evaluated at $x$, i.e., \[ \|x\|_e \leq \text{egauge}_{\mathbb{K}}(\overline{B}(0, 1), x). \]

div_le_egauge_ball theorem

(r : ℝ≥0) (x : E) : ‖x‖ₑ / r ≤ egauge 𝕜 (ball 0 r) x

Full source

lemma div_le_egauge_ball (r : ℝ≥0) (x : E) : ‖x‖ₑ / r ≤ egauge 𝕜 (ball 0 r) x :=
  (div_le_egauge_closedBall 𝕜 r x).trans <| egauge_anti _ ball_subset_closedBall _

Ratio of Extended Norm to Radius is Bounded by Minkowski Functional of Open Ball

Informal description

For any non-negative real number $r$ and any vector $x$ in a normed space $E$ over a normed field $\mathbb{K}$, the ratio of the extended norm $\|x\|_e$ to $r$ is bounded above by the Minkowski functional of the open ball $B(0, r)$ centered at the origin with radius $r$ evaluated at $x$. In other words: \[ \frac{\|x\|_e}{r} \leq \text{egauge}_{\mathbb{K}}(B(0, r), x). \]

le_egauge_ball_one theorem

(x : E) : ‖x‖ₑ ≤ egauge 𝕜 (ball 0 1) x

Full source

lemma le_egauge_ball_one (x : E) : ‖x‖ₑ ≤ egauge 𝕜 (ball 0 1) x := by
  simpa using div_le_egauge_ball 𝕜 1 x

Extended Norm Bounded by Minkowski Functional of Open Unit Ball

Informal description

For any vector $x$ in a normed space $E$ over a normed field $\mathbb{K}$, the extended norm $\|x\|_e$ is bounded above by the Minkowski functional of the open unit ball $B(0, 1)$ evaluated at $x$, i.e., \[ \|x\|_e \leq \text{egauge}_{\mathbb{K}}(B(0, 1), x). \]

egauge_ball_le_of_one_lt_norm theorem

(hc : 1 < ‖c‖) (h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0) : egauge 𝕜 (ball 0 r) x ≤ ‖c‖ₑ * ‖x‖ₑ / r

Full source

lemma egauge_ball_le_of_one_lt_norm (hc : 1 < ‖c‖) (h₀ : r ≠ 0r ≠ 0 ∨ ‖x‖ ≠ 0) :
    egauge 𝕜 (ball 0 r) x ≤ ‖c‖ₑ * ‖x‖ₑ / r := by
  letI : NontriviallyNormedField 𝕜 := ⟨c, hc⟩
  rcases (zero_le r).eq_or_lt with rfl | hr
  · rw [ENNReal.coe_zero, ENNReal.div_zero (mul_ne_zero _ _)]
    · apply le_top
    · simpa using one_pos.trans hc
    · simpa [enorm, ← NNReal.coe_eq_zero] using h₀
  · rcases eq_or_ne ‖x‖ 0 with hx | hx
    · have hx' : ‖x‖ₑ = 0 := by simpa [enorm, ← coe_nnnorm, NNReal.coe_eq_zero] using hx
      simp only [hx', mul_zero, ENNReal.zero_div, nonpos_iff_eq_zero, egauge_eq_zero_iff]
      refine (frequently_iff_neBot.2 (inferInstance : NeBot (𝓝[≠] (0 : 𝕜)))).mono fun c hc ↦ ?_
      simp [mem_smul_set_iff_inv_smul_mem₀ hc, norm_smul, hx, hr]
    · rcases rescale_to_shell_semi_normed hc hr hx with ⟨a, ha₀, har, -, hainv⟩
      calc
        egauge 𝕜 (ball 0 r) x ≤ ↑(‖a‖₊‖a‖₊⁻¹) :=
          egauge_le_of_smul_mem_of_ne (mem_ball_zero_iff.2 har) ha₀
        _ ≤ ↑(‖c‖₊ * ‖x‖₊ / r) := by rwa [ENNReal.coe_le_coe, div_eq_inv_mul, ← mul_assoc]
        _ ≤ ‖c‖ₑ * ‖x‖ₑ / r := ENNReal.coe_div_le.trans <| by simp [ENNReal.coe_mul, enorm]

Upper Bound for Minkowski Functional of Ball: $\text{egauge}_{\mathbb{K}}(\text{ball}(0, r), x) \leq \|c\|_e \cdot \frac{\|x\|_e}{r}$

Informal description

Let $\mathbb{K}$ be a normed field and $E$ a vector space over $\mathbb{K}$. For any $c \in \mathbb{K}$ with $\|c\| > 1$, any $r \in \mathbb{R}_{\geq 0}$ with $r \neq 0$ or $\|x\| \neq 0$, and any $x \in E$, the Minkowski functional of the open ball $\text{ball}(0, r)$ satisfies: \[ \text{egauge}_{\mathbb{K}}(\text{ball}(0, r), x) \leq \|c\|_e \cdot \frac{\|x\|_e}{r} \] where $\|\cdot\|_e$ denotes the extended norm on $\mathbb{K}$.

egauge_ball_one_le_of_one_lt_norm theorem

(hc : 1 < ‖c‖) (x : E) : egauge 𝕜 (ball 0 1) x ≤ ‖c‖ₑ * ‖x‖ₑ

Full source

lemma egauge_ball_one_le_of_one_lt_norm (hc : 1 < ‖c‖) (x : E) :
    egauge 𝕜 (ball 0 1) x ≤ ‖c‖ₑ * ‖x‖ₑ := by
  simpa using egauge_ball_le_of_one_lt_norm hc (.inl one_ne_zero)

Upper Bound for Minkowski Functional of Unit Ball: $\text{egauge}_{\mathbb{K}}(\text{ball}(0, 1), x) \leq \|c\|_e \cdot \|x\|_e$

Informal description

Let $\mathbb{K}$ be a normed field and $E$ a vector space over $\mathbb{K}$. For any $c \in \mathbb{K}$ with $\|c\| > 1$ and any $x \in E$, the Minkowski functional of the unit open ball $\text{ball}(0, 1)$ satisfies: \[ \text{egauge}_{\mathbb{K}}(\text{ball}(0, 1), x) \leq \|c\|_e \cdot \|x\|_e \] where $\|\cdot\|_e$ denotes the extended norm on $\mathbb{K}$.