feat(analysis/normed*): add instances and lemmas (#15515)

* Add some `coe_*` lemmas.
* Add `is_scalar_tower` and `is_smul_class` instances.

src/algebra/group/units.lean

@@ -218,7 +218,7 @@ by rw [←mul_inv_eq_one, inv_inv]
 @[to_additive] lemma mul_eq_one_iff_inv_eq {a : α} : ↑u * a = 1 ↔ ↑u⁻¹ = a :=
 by rw [←inv_mul_eq_one, inv_inv]
 
-lemma inv_unique {u₁ u₂ : αˣ} (h : (↑u₁ : α) = ↑u₂) : (↑u₁⁻¹ : α) = ↑u₂⁻¹ :=
+@[to_additive] lemma inv_unique {u₁ u₂ : αˣ} (h : (↑u₁ : α) = ↑u₂) : (↑u₁⁻¹ : α) = ↑u₂⁻¹ :=
 units.inv_eq_of_mul_eq_one_right $ by rw [h, u₂.mul_inv]
 
 end units

src/algebra/hom/units.lean

@@ -70,6 +70,9 @@ variables [division_monoid α]
 @[simp, norm_cast, to_additive] lemma coe_inv : ∀ u : αˣ, ↑u⁻¹ = (u⁻¹ : α) :=
 (units.coe_hom α).map_inv
 
+@[simp, norm_cast, to_additive] lemma coe_div : ∀ u₁ u₂ : αˣ, ↑(u₁ / u₂) = (u₁ / u₂ : α) :=
+(units.coe_hom α).map_div
+
 @[simp, norm_cast, to_additive] lemma coe_zpow : ∀ (u : αˣ) (n : ℤ), ((u ^ n : αˣ) : α) = u ^ n :=
 (units.coe_hom α).map_zpow
 

src/analysis/normed/field/unit_ball.lean

@@ -43,6 +43,9 @@ mul_mem_class.to_comm_semigroup (subsemigroup.unit_ball 𝕜)
 instance [non_unital_semi_normed_ring 𝕜] : has_distrib_neg (ball (0 : 𝕜) 1) :=
 subtype.coe_injective.has_distrib_neg (coe : ball (0 : 𝕜) 1 → 𝕜) (λ _, rfl) (λ _ _, rfl)
 
+@[simp, norm_cast] lemma coe_mul_unit_ball [non_unital_semi_normed_ring 𝕜] (x y : ball (0 : 𝕜) 1) :
+  ↑(x * y) = (x * y : 𝕜) := rfl
+
 /-- Closed unit ball in a non unital semi normed ring as a bundled `subsemigroup`. -/
 def subsemigroup.unit_closed_ball (𝕜 : Type*) [non_unital_semi_normed_ring 𝕜] :
   subsemigroup 𝕜 :=
@@ -63,6 +66,10 @@ instance [non_unital_semi_normed_ring 𝕜] : has_continuous_mul (closed_ball (0
 ⟨continuous_subtype_mk _ $ continuous.mul (continuous_subtype_val.comp continuous_fst)
   (continuous_subtype_val.comp continuous_snd)⟩
 
+@[simp, norm_cast]
+lemma coe_mul_unit_closed_ball [non_unital_semi_normed_ring 𝕜] (x y : closed_ball (0 : 𝕜) 1) :
+  ↑(x * y) = (x * y : 𝕜) := rfl
+
 /-- Closed unit ball in a semi normed ring as a bundled `submonoid`. -/
 def submonoid.unit_closed_ball (𝕜 : Type*) [semi_normed_ring 𝕜] [norm_one_class 𝕜] :
   submonoid 𝕜 :=
@@ -76,26 +83,79 @@ submonoid_class.to_monoid (submonoid.unit_closed_ball 𝕜)
 instance [semi_normed_comm_ring 𝕜] [norm_one_class 𝕜] : comm_monoid (closed_ball (0 : 𝕜) 1) :=
 submonoid_class.to_comm_monoid (submonoid.unit_closed_ball 𝕜)
 
+@[simp, norm_cast]
+lemma coe_one_unit_closed_ball [semi_normed_ring 𝕜] [norm_one_class 𝕜] :
+  ((1 : closed_ball (0 : 𝕜) 1) : 𝕜) = 1 := rfl
+
+@[simp, norm_cast]
+lemma coe_pow_unit_closed_ball [semi_normed_ring 𝕜] [norm_one_class 𝕜]
+  (x : closed_ball (0 : 𝕜) 1) (n : ℕ) :
+  ↑(x ^ n) = (x ^ n : 𝕜) := rfl
+
 /-- Unit sphere in a normed division ring as a bundled `submonoid`. -/
 def submonoid.unit_sphere (𝕜 : Type*) [normed_division_ring 𝕜] : submonoid 𝕜 :=
 { carrier := sphere (0 : 𝕜) 1,
   mul_mem' := λ x y hx hy, by { rw [mem_sphere_zero_iff_norm] at *, simp * },
   one_mem' := mem_sphere_zero_iff_norm.2 norm_one }
 
-instance [normed_division_ring 𝕜] : group (sphere (0 : 𝕜) 1) :=
-{ inv := λ x, ⟨x⁻¹, mem_sphere_zero_iff_norm.2 $
-    by rw [norm_inv, mem_sphere_zero_iff_norm.1 x.coe_prop, inv_one]⟩,
-  mul_left_inv := λ x, subtype.coe_injective $ inv_mul_cancel $ ne_zero_of_mem_unit_sphere x,
-  .. submonoid_class.to_monoid (submonoid.unit_sphere 𝕜) }
+instance [normed_division_ring 𝕜] : has_inv (sphere (0 : 𝕜) 1) :=
+⟨λ x, ⟨x⁻¹, mem_sphere_zero_iff_norm.2 $
+  by rw [norm_inv, mem_sphere_zero_iff_norm.1 x.coe_prop, inv_one]⟩⟩
 
-instance [normed_division_ring 𝕜] : has_distrib_neg (sphere (0 : 𝕜) 1) :=
-subtype.coe_injective.has_distrib_neg (coe : sphere (0 : 𝕜) 1 → 𝕜) (λ _, rfl) (λ _ _, rfl)
+@[simp, norm_cast]
+lemma coe_inv_unit_sphere [normed_division_ring 𝕜] (x : sphere (0 : 𝕜) 1) : ↑x⁻¹ = (x⁻¹ : 𝕜) := rfl
+
+instance [normed_division_ring 𝕜] : has_div (sphere (0 : 𝕜) 1) :=
+⟨λ x y, ⟨x / y, mem_sphere_zero_iff_norm.2 $ by rw [norm_div, mem_sphere_zero_iff_norm.1 x.coe_prop,
+  mem_sphere_zero_iff_norm.1 y.coe_prop, div_one]⟩⟩
+
+@[simp, norm_cast]
+lemma coe_div_unit_sphere [normed_division_ring 𝕜] (x y : sphere (0 : 𝕜) 1) :
+  ↑(x / y) = (x / y : 𝕜) := rfl
+
+instance [normed_division_ring 𝕜] : has_pow (sphere (0 : 𝕜) 1) ℤ :=
+⟨λ x n, ⟨x ^ n, by rw [mem_sphere_zero_iff_norm, norm_zpow,
+    mem_sphere_zero_iff_norm.1 x.coe_prop, one_zpow]⟩⟩
+
+@[simp, norm_cast]
+lemma coe_zpow_unit_sphere [normed_division_ring 𝕜] (x : sphere (0 : 𝕜) 1) (n : ℤ) :
+  ↑(x ^ n) = (x ^ n : 𝕜) := rfl
+
+instance [normed_division_ring 𝕜] : monoid (sphere (0 : 𝕜) 1) :=
+submonoid_class.to_monoid (submonoid.unit_sphere 𝕜)
+
+@[simp, norm_cast]
+lemma coe_one_unit_sphere [normed_division_ring 𝕜] : ((1 : sphere (0 : 𝕜) 1) : 𝕜) = 1 := rfl
+
+@[simp, norm_cast]
+lemma coe_mul_unit_sphere [normed_division_ring 𝕜] (x y : sphere (0 : 𝕜) 1) :
+  ↑(x * y) = (x * y : 𝕜) := rfl
+
+@[simp, norm_cast]
+lemma coe_pow_unit_sphere [normed_division_ring 𝕜] (x : sphere (0 : 𝕜) 1) (n : ℕ) :
+  ↑(x ^ n) = (x ^ n : 𝕜) := rfl
 
 /-- Monoid homomorphism from the unit sphere to the group of units. -/
 def unit_sphere_to_units (𝕜 : Type*) [normed_division_ring 𝕜] : sphere (0 : 𝕜) 1 →* units 𝕜 :=
 units.lift_right (submonoid.unit_sphere 𝕜).subtype (λ x, units.mk0 x $ ne_zero_of_mem_unit_sphere _)
   (λ x, rfl)
 
+@[simp] lemma unit_sphere_to_units_apply_coe [normed_division_ring 𝕜] (x : sphere (0 : 𝕜) 1) :
+  (unit_sphere_to_units 𝕜 x : 𝕜) = x := rfl
+
+lemma unit_sphere_to_units_injective [normed_division_ring 𝕜] :
+  function.injective (unit_sphere_to_units 𝕜) :=
+λ x y h, subtype.eq $ by convert congr_arg units.val h
+
+instance [normed_division_ring 𝕜] : group (sphere (0 : 𝕜) 1) :=
+unit_sphere_to_units_injective.group (unit_sphere_to_units 𝕜) (units.ext rfl)
+  (λ x y, units.ext rfl) (λ x, units.ext rfl) (λ x y, units.ext $ div_eq_mul_inv _ _)
+  (λ x n, units.ext (units.coe_pow (unit_sphere_to_units 𝕜 x) n).symm)
+  (λ x n, units.ext (units.coe_zpow (unit_sphere_to_units 𝕜 x) n).symm)
+
+instance [normed_division_ring 𝕜] : has_distrib_neg (sphere (0 : 𝕜) 1) :=
+subtype.coe_injective.has_distrib_neg (coe : sphere (0 : 𝕜) 1 → 𝕜) (λ _, rfl) (λ _ _, rfl)
+
 instance [normed_division_ring 𝕜] : topological_group (sphere (0 : 𝕜) 1) :=
 { continuous_mul := continuous_subtype_mk _ $ (continuous_subtype_val.comp continuous_fst).mul
     (continuous_subtype_val.comp continuous_snd),

src/analysis/normed_space/ball_action.lean

@@ -16,7 +16,8 @@ multiplicative actions.
 - The unit sphere in `𝕜` acts on open balls, closed balls, and spheres centered at `0` in `E`.
 -/
 open metric set
-variables {𝕜 E : Type*} [normed_field 𝕜] [semi_normed_group E] [normed_space 𝕜 E] {r : ℝ}
+variables {𝕜 𝕜' E : Type*} [normed_field 𝕜] [normed_field 𝕜']
+  [semi_normed_group E] [normed_space 𝕜 E] [normed_space 𝕜' E] {r : ℝ}
 
 section closed_ball
 
@@ -85,6 +86,86 @@ instance has_continuous_smul_sphere_sphere :
 
 end sphere
 
+section is_scalar_tower
+
+variables [normed_algebra 𝕜 𝕜'] [is_scalar_tower 𝕜 𝕜' E]
+
+instance is_scalar_tower_closed_ball_closed_ball_closed_ball :
+  is_scalar_tower (closed_ball (0 : 𝕜) 1) (closed_ball (0 : 𝕜') 1) (closed_ball (0 : E) r) :=
+⟨λ a b c, subtype.ext $ smul_assoc (a : 𝕜) (b : 𝕜') (c : E)⟩
+
+instance is_scalar_tower_closed_ball_closed_ball_ball :
+  is_scalar_tower (closed_ball (0 : 𝕜) 1) (closed_ball (0 : 𝕜') 1) (ball (0 : E) r) :=
+⟨λ a b c, subtype.ext $ smul_assoc (a : 𝕜) (b : 𝕜') (c : E)⟩
+
+instance is_scalar_tower_sphere_closed_ball_closed_ball :
+  is_scalar_tower (sphere (0 : 𝕜) 1) (closed_ball (0 : 𝕜') 1) (closed_ball (0 : E) r) :=
+⟨λ a b c, subtype.ext $ smul_assoc (a : 𝕜) (b : 𝕜') (c : E)⟩
+
+instance is_scalar_tower_sphere_closed_ball_ball :
+  is_scalar_tower (sphere (0 : 𝕜) 1) (closed_ball (0 : 𝕜') 1) (ball (0 : E) r) :=
+⟨λ a b c, subtype.ext $ smul_assoc (a : 𝕜) (b : 𝕜') (c : E)⟩
+
+instance is_scalar_tower_sphere_sphere_closed_ball :
+  is_scalar_tower (sphere (0 : 𝕜) 1) (sphere (0 : 𝕜') 1) (closed_ball (0 : E) r) :=
+⟨λ a b c, subtype.ext $ smul_assoc (a : 𝕜) (b : 𝕜') (c : E)⟩
+
+instance is_scalar_tower_sphere_sphere_ball :
+  is_scalar_tower (sphere (0 : 𝕜) 1) (sphere (0 : 𝕜') 1) (ball (0 : E) r) :=
+⟨λ a b c, subtype.ext $ smul_assoc (a : 𝕜) (b : 𝕜') (c : E)⟩
+
+instance is_scalar_tower_sphere_sphere_sphere :
+  is_scalar_tower (sphere (0 : 𝕜) 1) (sphere (0 : 𝕜') 1) (sphere (0 : E) r) :=
+⟨λ a b c, subtype.ext $ smul_assoc (a : 𝕜) (b : 𝕜') (c : E)⟩
+
+instance is_scalar_tower_sphere_ball_ball :
+  is_scalar_tower (sphere (0 : 𝕜) 1) (ball (0 : 𝕜') 1) (ball (0 : 𝕜') 1) :=
+⟨λ a b c, subtype.ext $ smul_assoc (a : 𝕜) (b : 𝕜') (c : 𝕜')⟩
+
+instance is_scalar_tower_closed_ball_ball_ball :
+  is_scalar_tower (closed_ball (0 : 𝕜) 1) (ball (0 : 𝕜') 1) (ball (0 : 𝕜') 1) :=
+⟨λ a b c, subtype.ext $ smul_assoc (a : 𝕜) (b : 𝕜') (c : 𝕜')⟩
+
+end is_scalar_tower
+
+section smul_comm_class
+
+variables [smul_comm_class 𝕜 𝕜' E]
+
+instance smul_comm_class_closed_ball_closed_ball_closed_ball :
+  smul_comm_class (closed_ball (0 : 𝕜) 1) (closed_ball (0 : 𝕜') 1) (closed_ball (0 : E) r) :=
+⟨λ a b c, subtype.ext $ smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩
+
+instance smul_comm_class_closed_ball_closed_ball_ball :
+  smul_comm_class (closed_ball (0 : 𝕜) 1) (closed_ball (0 : 𝕜') 1) (ball (0 : E) r) :=
+⟨λ a b c, subtype.ext $ smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩
+
+instance smul_comm_class_sphere_closed_ball_closed_ball :
+  smul_comm_class (sphere (0 : 𝕜) 1) (closed_ball (0 : 𝕜') 1) (closed_ball (0 : E) r) :=
+⟨λ a b c, subtype.ext $ smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩
+
+instance smul_comm_class_sphere_closed_ball_ball :
+  smul_comm_class (sphere (0 : 𝕜) 1) (closed_ball (0 : 𝕜') 1) (ball (0 : E) r) :=
+⟨λ a b c, subtype.ext $ smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩
+
+instance smul_comm_class_sphere_ball_ball [normed_algebra 𝕜 𝕜'] :
+  smul_comm_class (sphere (0 : 𝕜) 1) (ball (0 : 𝕜') 1) (ball (0 : 𝕜') 1) :=
+⟨λ a b c, subtype.ext $ smul_comm (a : 𝕜) (b : 𝕜') (c : 𝕜')⟩
+
+instance smul_comm_class_sphere_sphere_closed_ball :
+  smul_comm_class (sphere (0 : 𝕜) 1) (sphere (0 : 𝕜') 1) (closed_ball (0 : E) r) :=
+⟨λ a b c, subtype.ext $ smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩
+
+instance smul_comm_class_sphere_sphere_ball :
+  smul_comm_class (sphere (0 : 𝕜) 1) (sphere (0 : 𝕜') 1) (ball (0 : E) r) :=
+⟨λ a b c, subtype.ext $ smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩
+
+instance smul_comm_class_sphere_sphere_sphere :
+  smul_comm_class (sphere (0 : 𝕜) 1) (sphere (0 : 𝕜') 1) (sphere (0 : E) r) :=
+⟨λ a b c, subtype.ext $ smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩
+
+end smul_comm_class
+
 variables (𝕜) [char_zero 𝕜]
 
 lemma ne_neg_of_mem_sphere {r : ℝ} (hr : r ≠ 0) (x : sphere (0:E) r) : x ≠ - x :=