Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(analysis/normed*): add instances about balls and spheres (#14808)
Non-bc change: `has_inv.inv` on the unit circle is now defined using `has_inv.inv` instead of complex conjugation.
- Loading branch information
Showing
7 changed files
with
272 additions
and
54 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,107 @@ | ||
/- | ||
Copyright (c) 2022 Yury Kudryashov. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Yury Kudryashov, Heather Macbeth | ||
-/ | ||
import analysis.normed.field.basic | ||
import analysis.normed.group.ball_sphere | ||
|
||
/-! | ||
# Algebraic structures on unit balls and spheres | ||
In this file we define algebraic structures (`semigroup`, `comm_semigroup`, `monoid`, `comm_monoid`, | ||
`group`, `comm_group`) on `metric.ball (0 : 𝕜) 1`, `metric.closed_ball (0 : 𝕜) 1`, and | ||
`metric.sphere (0 : 𝕜) 1`. In each case we use the weakest possible typeclass assumption on `𝕜`, | ||
from `non_unital_semi_normed_ring` to `normed_field`. | ||
-/ | ||
|
||
open set metric | ||
|
||
variables {𝕜 : Type*} | ||
|
||
/-- Unit ball in a non unital semi normed ring as a bundled `subsemigroup`. -/ | ||
def subsemigroup.unit_ball (𝕜 : Type*) [non_unital_semi_normed_ring 𝕜] : | ||
subsemigroup 𝕜 := | ||
{ carrier := ball (0 : 𝕜) 1, | ||
mul_mem' := λ x y hx hy, | ||
begin | ||
rw [mem_ball_zero_iff] at *, | ||
exact (norm_mul_le x y).trans_lt (mul_lt_one_of_nonneg_of_lt_one_left (norm_nonneg _) | ||
hx hy.le) | ||
end } | ||
|
||
instance [non_unital_semi_normed_ring 𝕜] : semigroup (ball (0 : 𝕜) 1) := | ||
mul_mem_class.to_semigroup (subsemigroup.unit_ball 𝕜) | ||
|
||
instance [non_unital_semi_normed_ring 𝕜] : has_continuous_mul (ball (0 : 𝕜) 1) := | ||
⟨continuous_subtype_mk _ $ continuous.mul (continuous_subtype_val.comp continuous_fst) | ||
(continuous_subtype_val.comp continuous_snd)⟩ | ||
|
||
instance [semi_normed_comm_ring 𝕜] : comm_semigroup (ball (0 : 𝕜) 1) := | ||
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) | ||
|
||
/-- 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 𝕜 := | ||
{ carrier := closed_ball 0 1, | ||
mul_mem' := λ x y hx hy, | ||
begin | ||
rw [mem_closed_ball_zero_iff] at *, | ||
exact (norm_mul_le x y).trans (mul_le_one hx (norm_nonneg _) hy) | ||
end } | ||
|
||
instance [non_unital_semi_normed_ring 𝕜] : semigroup (closed_ball (0 : 𝕜) 1) := | ||
mul_mem_class.to_semigroup (subsemigroup.unit_closed_ball 𝕜) | ||
|
||
instance [non_unital_semi_normed_ring 𝕜] : has_distrib_neg (closed_ball (0 : 𝕜) 1) := | ||
subtype.coe_injective.has_distrib_neg (coe : closed_ball (0 : 𝕜) 1 → 𝕜) (λ _, rfl) (λ _ _, rfl) | ||
|
||
instance [non_unital_semi_normed_ring 𝕜] : has_continuous_mul (closed_ball (0 : 𝕜) 1) := | ||
⟨continuous_subtype_mk _ $ continuous.mul (continuous_subtype_val.comp continuous_fst) | ||
(continuous_subtype_val.comp continuous_snd)⟩ | ||
|
||
/-- 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 𝕜 := | ||
{ carrier := closed_ball 0 1, | ||
one_mem' := mem_closed_ball_zero_iff.2 norm_one.le, | ||
.. subsemigroup.unit_closed_ball 𝕜 } | ||
|
||
instance [semi_normed_ring 𝕜] [norm_one_class 𝕜] : monoid (closed_ball (0 : 𝕜) 1) := | ||
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 𝕜) | ||
|
||
/-- 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_distrib_neg (sphere (0 : 𝕜) 1) := | ||
subtype.coe_injective.has_distrib_neg (coe : sphere (0 : 𝕜) 1 → 𝕜) (λ _, rfl) (λ _ _, 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) | ||
|
||
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), | ||
continuous_inv := continuous_subtype_mk _ $ | ||
continuous_subtype_coe.inv₀ ne_zero_of_mem_unit_sphere } | ||
|
||
instance [normed_field 𝕜] : comm_group (sphere (0 : 𝕜) 1) := | ||
{ .. metric.sphere.group, | ||
.. submonoid_class.to_comm_monoid (submonoid.unit_sphere 𝕜) } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,56 @@ | ||
/- | ||
Copyright (c) 2022 Yury Kudryashov. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Yury Kudryashov, Heather Macbeth | ||
-/ | ||
import analysis.normed.group.basic | ||
|
||
/-! | ||
# Negation on spheres and balls | ||
In this file we define `has_involutive_neg` instances for spheres, open balls, and closed balls in a | ||
semi normed group. | ||
-/ | ||
|
||
open metric set | ||
|
||
variables {E : Type*} [semi_normed_group E] {r : ℝ} | ||
|
||
/-- We equip the sphere, in a seminormed group, with a formal operation of negation, namely the | ||
antipodal map. -/ | ||
instance : has_involutive_neg (sphere (0 : E) r) := | ||
{ neg := λ w, ⟨-↑w, by simp⟩, | ||
neg_neg := λ x, subtype.ext $ neg_neg x } | ||
|
||
@[simp] lemma coe_neg_sphere {r : ℝ} (v : sphere (0 : E) r) : | ||
↑(-v) = (-v : E) := | ||
rfl | ||
|
||
instance : has_continuous_neg (sphere (0 : E) r) := | ||
⟨continuous_subtype_mk _ continuous_subtype_coe.neg⟩ | ||
|
||
/-- We equip the ball, in a seminormed group, with a formal operation of negation, namely the | ||
antipodal map. -/ | ||
instance {r : ℝ} : has_involutive_neg (ball (0 : E) r) := | ||
{ neg := λ w, ⟨-↑w, by simpa using w.coe_prop⟩, | ||
neg_neg := λ x, subtype.ext $ neg_neg x } | ||
|
||
@[simp] lemma coe_neg_ball {r : ℝ} (v : ball (0 : E) r) : | ||
↑(-v) = (-v : E) := | ||
rfl | ||
|
||
instance : has_continuous_neg (ball (0 : E) r) := | ||
⟨continuous_subtype_mk _ continuous_subtype_coe.neg⟩ | ||
|
||
/-- We equip the closed ball, in a seminormed group, with a formal operation of negation, namely the | ||
antipodal map. -/ | ||
instance {r : ℝ} : has_involutive_neg (closed_ball (0 : E) r) := | ||
{ neg := λ w, ⟨-↑w, by simpa using w.coe_prop⟩, | ||
neg_neg := λ x, subtype.ext $ neg_neg x } | ||
|
||
@[simp] lemma coe_neg_closed_ball {r : ℝ} (v : closed_ball (0 : E) r) : | ||
↑(-v) = (-v : E) := | ||
rfl | ||
|
||
instance : has_continuous_neg (closed_ball (0 : E) r) := | ||
⟨continuous_subtype_mk _ continuous_subtype_coe.neg⟩ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,94 @@ | ||
/- | ||
Copyright (c) 2022 Yury Kudryashov. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Yury Kudryashov, Heather Macbeth | ||
-/ | ||
import analysis.normed.field.unit_ball | ||
import analysis.normed_space.basic | ||
|
||
/-! | ||
# Multiplicative actions of/on balls and spheres | ||
Let `E` be a normed vector space over a normed field `𝕜`. In this file we define the following | ||
multiplicative actions. | ||
- The closed unit ball in `𝕜` acts on open balls and closed balls centered at `0` in `E`. | ||
- 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 : ℝ} | ||
|
||
section closed_ball | ||
|
||
instance mul_action_closed_ball_ball : mul_action (closed_ball (0 : 𝕜) 1) (ball (0 : E) r) := | ||
{ smul := λ c x, ⟨(c : 𝕜) • x, mem_ball_zero_iff.2 $ | ||
by simpa only [norm_smul, one_mul] | ||
using mul_lt_mul' (mem_closed_ball_zero_iff.1 c.2) (mem_ball_zero_iff.1 x.2) | ||
(norm_nonneg _) one_pos⟩, | ||
one_smul := λ x, subtype.ext $ one_smul 𝕜 _, | ||
mul_smul := λ c₁ c₂ x, subtype.ext $ mul_smul _ _ _ } | ||
|
||
instance has_continuous_smul_closed_ball_ball : | ||
has_continuous_smul (closed_ball (0 : 𝕜) 1) (ball (0 : E) r) := | ||
⟨continuous_subtype_mk _ $ (continuous_subtype_val.comp continuous_fst).smul | ||
(continuous_subtype_val.comp continuous_snd)⟩ | ||
|
||
instance mul_action_closed_ball_closed_ball : | ||
mul_action (closed_ball (0 : 𝕜) 1) (closed_ball (0 : E) r) := | ||
{ smul := λ c x, ⟨(c : 𝕜) • x, mem_closed_ball_zero_iff.2 $ | ||
by simpa only [norm_smul, one_mul] | ||
using mul_le_mul (mem_closed_ball_zero_iff.1 c.2) (mem_closed_ball_zero_iff.1 x.2) | ||
(norm_nonneg _) zero_le_one⟩, | ||
one_smul := λ x, subtype.ext $ one_smul 𝕜 _, | ||
mul_smul := λ c₁ c₂ x, subtype.ext $ mul_smul _ _ _ } | ||
|
||
instance has_continuous_smul_closed_ball_closed_ball : | ||
has_continuous_smul (closed_ball (0 : 𝕜) 1) (closed_ball (0 : E) r) := | ||
⟨continuous_subtype_mk _ $ (continuous_subtype_val.comp continuous_fst).smul | ||
(continuous_subtype_val.comp continuous_snd)⟩ | ||
|
||
end closed_ball | ||
|
||
section sphere | ||
|
||
instance mul_action_sphere_ball : mul_action (sphere (0 : 𝕜) 1) (ball (0 : E) r) := | ||
{ smul := λ c x, inclusion sphere_subset_closed_ball c • x, | ||
one_smul := λ x, subtype.ext $ one_smul _ _, | ||
mul_smul := λ c₁ c₂ x, subtype.ext $ mul_smul _ _ _ } | ||
|
||
instance has_continuous_smul_sphere_ball : | ||
has_continuous_smul (sphere (0 : 𝕜) 1) (ball (0 : E) r) := | ||
⟨continuous_subtype_mk _ $ (continuous_subtype_val.comp continuous_fst).smul | ||
(continuous_subtype_val.comp continuous_snd)⟩ | ||
|
||
instance mul_action_sphere_closed_ball : mul_action (sphere (0 : 𝕜) 1) (closed_ball (0 : E) r) := | ||
{ smul := λ c x, inclusion sphere_subset_closed_ball c • x, | ||
one_smul := λ x, subtype.ext $ one_smul _ _, | ||
mul_smul := λ c₁ c₂ x, subtype.ext $ mul_smul _ _ _ } | ||
|
||
instance has_continuous_smul_sphere_closed_ball : | ||
has_continuous_smul (sphere (0 : 𝕜) 1) (closed_ball (0 : E) r) := | ||
⟨continuous_subtype_mk _ $ (continuous_subtype_val.comp continuous_fst).smul | ||
(continuous_subtype_val.comp continuous_snd)⟩ | ||
|
||
instance mul_action_sphere_sphere : mul_action (sphere (0 : 𝕜) 1) (sphere (0 : E) r) := | ||
{ smul := λ c x, ⟨(c : 𝕜) • x, mem_sphere_zero_iff_norm.2 $ | ||
by rw [norm_smul, mem_sphere_zero_iff_norm.1 c.coe_prop, mem_sphere_zero_iff_norm.1 x.coe_prop, | ||
one_mul]⟩, | ||
one_smul := λ x, subtype.ext $ one_smul _ _, | ||
mul_smul := λ c₁ c₂ x, subtype.ext $ mul_smul _ _ _ } | ||
|
||
instance has_continuous_smul_sphere_sphere : | ||
has_continuous_smul (sphere (0 : 𝕜) 1) (sphere (0 : E) r) := | ||
⟨continuous_subtype_mk _ $ (continuous_subtype_val.comp continuous_fst).smul | ||
(continuous_subtype_val.comp continuous_snd)⟩ | ||
|
||
end sphere | ||
|
||
variables (𝕜) [char_zero 𝕜] | ||
|
||
lemma ne_neg_of_mem_sphere {r : ℝ} (hr : r ≠ 0) (x : sphere (0:E) r) : x ≠ - x := | ||
λ h, ne_zero_of_mem_sphere hr x ((self_eq_neg 𝕜 _).mp (by { conv_lhs {rw h}, simp })) | ||
|
||
lemma ne_neg_of_mem_unit_sphere (x : sphere (0:E) 1) : x ≠ - x := | ||
ne_neg_of_mem_sphere 𝕜 one_ne_zero x |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters