feat(analysis/convex): the gauge as a seminorm over is_R_or_C (#14879)

Constructs the gauge for a set on a vector spaces over `is_R_or_C` assuming that the set is convex, balanced and absorbing.

The main part of this PR is to show that if a set is balanced then the corresponding gauge has the correct scaling behavior.

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>



Co-authored-by: YaelDillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Moritz Doll <doll@uni-bremen.de>

src/analysis/convex/gauge.lean

@@ -6,6 +6,7 @@ Authors: Yaël Dillies, Bhavik Mehta
 import analysis.convex.star
 import analysis.normed_space.pointwise
 import analysis.seminorm
+import data.complex.is_R_or_C
 import tactic.congrm
 
 /-!
@@ -40,7 +41,7 @@ open_locale pointwise
 
 noncomputable theory
 
-variables {E : Type*}
+variables {𝕜 E F : Type*}
 
 section add_comm_group
 variables [add_comm_group E] [module ℝ E]
@@ -239,18 +240,6 @@ begin
     exact smul_mem_smul_set hx }
 end
 
-/-- In textbooks, this is the homogeneity of the Minkowksi functional. -/
-lemma gauge_smul [module α E] [is_scalar_tower α ℝ (set E)] {s : set E}
-  (symmetric : ∀ x ∈ s, -x ∈ s) (r : α) (x : E) :
-  gauge s (r • x) = abs r • gauge s x :=
-begin
-  rw ←gauge_smul_of_nonneg (abs_nonneg r),
-  obtain h | h := abs_choice r,
-  { rw h },
-  { rw [h, neg_smul, gauge_neg symmetric] },
-  { apply_instance }
-end
-
 lemma gauge_smul_left_of_nonneg [mul_action_with_zero α E] [smul_comm_class α ℝ ℝ]
   [is_scalar_tower α ℝ ℝ] [is_scalar_tower α ℝ E] {s : set E} {a : α} (ha : 0 ≤ a) :
   gauge (a • s) = a⁻¹ • gauge s :=
@@ -292,6 +281,26 @@ end
 
 end linear_ordered_field
 
+section is_R_or_C
+variables [is_R_or_C 𝕜] [module 𝕜 E] [is_scalar_tower ℝ 𝕜 E]
+
+lemma gauge_norm_smul (hs : balanced 𝕜 s) (r : 𝕜) (x : E) : gauge s (∥r∥ • x) = gauge s (r • x) :=
+begin
+  rw @is_R_or_C.real_smul_eq_coe_smul 𝕜,
+  obtain rfl | hr := eq_or_ne r 0,
+  { simp only [norm_zero, is_R_or_C.of_real_zero] },
+  unfold gauge,
+  congr' with θ,
+  refine and_congr_right (λ hθ, (hs.smul _).mem_smul_iff _),
+  rw [is_R_or_C.norm_of_real, norm_norm],
+end
+
+/-- If `s` is balanced, then the Minkowski functional is ℂ-homogeneous. -/
+lemma gauge_smul (hs : balanced 𝕜 s) (r : 𝕜) (x : E) : gauge s (r • x) = ∥r∥ * gauge s x :=
+by { rw [←smul_eq_mul, ←gauge_smul_of_nonneg (norm_nonneg r), gauge_norm_smul hs], apply_instance }
+
+end is_R_or_C
+
 section topological_space
 variables [topological_space E] [has_continuous_smul ℝ E]
 
@@ -365,24 +374,22 @@ begin
     mul_inv_cancel hb.ne', ←smul_add, one_div, ←mem_smul_set_iff_inv_smul_mem₀ hab.ne'] at this,
 end
 
-/-- `gauge s` as a seminorm when `s` is symmetric, convex and absorbent. -/
-@[simps] def gauge_seminorm (hs₀ : ∀ x ∈ s, -x ∈ s) (hs₁ : convex ℝ s) (hs₂ : absorbent ℝ s) :
-  seminorm ℝ E :=
-seminorm.of (gauge s) (gauge_add_le hs₁ hs₂)
-  (λ r x, by rw [gauge_smul hs₀, real.norm_eq_abs, smul_eq_mul]; apply_instance)
+section is_R_or_C
+variables [is_R_or_C 𝕜] [module 𝕜 E] [is_scalar_tower ℝ 𝕜 E]
 
-section gauge_seminorm
-variables {hs₀ : ∀ x ∈ s, -x ∈ s} {hs₁ : convex ℝ s} {hs₂ : absorbent ℝ s}
+/-- `gauge s` as a seminorm when `s` is  balanced, convex and absorbent. -/
+@[simps] def gauge_seminorm (hs₀ : balanced 𝕜 s)  (hs₁ : convex ℝ s) (hs₂ : absorbent ℝ s) :
+  seminorm 𝕜 E :=
+seminorm.of (gauge s) (gauge_add_le hs₁ hs₂) (gauge_smul hs₀)
 
-section topological_space
-variables [topological_space E] [has_continuous_smul ℝ E]
+variables {hs₀ : balanced 𝕜 s} {hs₁ : convex ℝ s} {hs₂ : absorbent ℝ s} [topological_space E]
+  [has_continuous_smul ℝ E]
 
 lemma gauge_seminorm_lt_one_of_open (hs : is_open s) {x : E} (hx : x ∈ s) :
   gauge_seminorm hs₀ hs₁ hs₂ x < 1 :=
 gauge_lt_one_of_mem_of_open hs₁ hs₂.zero_mem hs hx
 
-end topological_space
-end gauge_seminorm
+end is_R_or_C
 
 /-- Any seminorm arises as the gauge of its unit ball. -/
 @[simp] protected lemma seminorm.gauge_ball (p : seminorm ℝ E) : gauge (p.ball 0 1) = p :=
@@ -410,7 +417,7 @@ begin
 end
 
 lemma seminorm.gauge_seminorm_ball (p : seminorm ℝ E) :
-  gauge_seminorm (λ x, p.symmetric_ball_zero 1) (p.convex_ball 0 1)
+  gauge_seminorm (p.balanced_ball_zero 1) (p.convex_ball 0 1)
     (p.absorbent_ball_zero zero_lt_one) = p := fun_like.coe_injective p.gauge_ball
 
 end add_comm_group

src/analysis/locally_convex/basic.lean

@@ -3,7 +3,9 @@ Copyright (c) 2019 Jean Lo. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean Lo, Bhavik Mehta, Yaël Dillies
 -/
-import analysis.normed_space.basic
+import analysis.convex.basic
+import analysis.normed_space.lattice_ordered_group
+import analysis.normed_space.ordered
 
 /-!
 # Local convexity
@@ -341,3 +343,17 @@ lemma absorbent.zero_mem (hs : absorbent 𝕜 s) : (0 : E) ∈ s :=
 absorbs_zero_iff.1 $ absorbent_iff_forall_absorbs_singleton.1 hs _
 
 end nontrivially_normed_field
+
+section real
+variables [add_comm_group E] [module ℝ E] {s : set E}
+
+lemma balanced_iff_neg_mem (hs : convex ℝ s) : balanced ℝ s ↔ ∀ ⦃x⦄, x ∈ s → -x ∈ s :=
+begin
+  refine ⟨λ h x, h.neg_mem_iff.2, λ h a ha, smul_set_subset_iff.2 $ λ x hx, _⟩,
+  rw [real.norm_eq_abs, abs_le] at ha,
+  rw [show a = -((1 - a) / 2) + (a - -1)/2, by ring, add_smul, neg_smul, ←smul_neg],
+  exact hs (h hx) hx (div_nonneg (sub_nonneg_of_le ha.2) zero_le_two)
+    (div_nonneg (sub_nonneg_of_le ha.1) zero_le_two) (by ring),
+end
+
+end real

src/data/complex/is_R_or_C.lean

@@ -70,7 +70,7 @@ end
 
 mk_simp_attribute is_R_or_C_simps "Simp attribute for lemmas about `is_R_or_C`"
 
-variables {K : Type*} [is_R_or_C K]
+variables {K E : Type*} [is_R_or_C K]
 
 namespace is_R_or_C
 
@@ -83,6 +83,13 @@ See Note [coercion into rings], or `data/nat/cast.lean` for more details. -/
 lemma of_real_alg (x : ℝ) : (x : K) = x • (1 : K) :=
 algebra.algebra_map_eq_smul_one x
 
+lemma real_smul_eq_coe_mul (r : ℝ) (z : K) : r • z = (r : K) * z :=
+by rw [is_R_or_C.of_real_alg, ←smul_eq_mul, smul_assoc, smul_eq_mul, one_mul]
+
+lemma real_smul_eq_coe_smul [add_comm_group E] [module K E] [module ℝ E] [is_scalar_tower ℝ K E]
+  (r : ℝ) (x : E) : r • x = (r : K) • x :=
+by rw [is_R_or_C.of_real_alg, smul_one_smul]
+
 lemma algebra_map_eq_of_real : ⇑(algebra_map ℝ K) = coe := rfl
 
 @[simp, is_R_or_C_simps] lemma re_add_im (z : K) : ((re z) : K) + (im z) * I = z :=
@@ -699,9 +706,9 @@ library_note "is_R_or_C instance"
     simp [re_add_im a, algebra.smul_def, algebra_map_eq_of_real]
   end⟩⟩
 
-variables (K) (E : Type*) [normed_add_comm_group E] [normed_space K E]
+variables (K E) [normed_add_comm_group E] [normed_space K E]
 
-/-- A finite dimensional vector space Over an `is_R_or_C` is a proper metric space.
+/-- A finite dimensional vector space over an `is_R_or_C` is a proper metric space.
 
 This is not an instance because it would cause a search for `finite_dimensional ?x E` before
 `is_R_or_C ?x`. -/