Multiplicative actions of/on balls and spheres #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 at0inE. - The unit sphere in
𝕜acts on open balls, closed balls, and spheres centered at0inE.
@[protected, instance]
def
mul_action_closed_ball_ball
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{r : ℝ} :
mul_action ↥(metric.closed_ball 0 1) ↥(metric.ball 0 r)
Equations
- mul_action_closed_ball_ball = {to_has_smul := {smul := λ (c : ↥(metric.closed_ball 0 1)) (x : ↥(metric.ball 0 r)), ⟨↑c • ↑x, _⟩}, one_smul := _, mul_smul := _}
@[protected, instance]
def
has_continuous_smul_closed_ball_ball
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{r : ℝ} :
has_continuous_smul ↥(metric.closed_ball 0 1) ↥(metric.ball 0 r)
@[protected, instance]
def
mul_action_closed_ball_closed_ball
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{r : ℝ} :
mul_action ↥(metric.closed_ball 0 1) ↥(metric.closed_ball 0 r)
Equations
- mul_action_closed_ball_closed_ball = {to_has_smul := {smul := λ (c : ↥(metric.closed_ball 0 1)) (x : ↥(metric.closed_ball 0 r)), ⟨↑c • ↑x, _⟩}, one_smul := _, mul_smul := _}
@[protected, instance]
def
has_continuous_smul_closed_ball_closed_ball
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{r : ℝ} :
@[protected, instance]
def
mul_action_sphere_ball
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{r : ℝ} :
mul_action ↥(metric.sphere 0 1) ↥(metric.ball 0 r)
Equations
- mul_action_sphere_ball = {to_has_smul := {smul := λ (c : ↥(metric.sphere 0 1)) (x : ↥(metric.ball 0 r)), set.inclusion mul_action_sphere_ball._proof_1 c • x}, one_smul := _, mul_smul := _}
@[protected, instance]
def
has_continuous_smul_sphere_ball
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{r : ℝ} :
has_continuous_smul ↥(metric.sphere 0 1) ↥(metric.ball 0 r)
@[protected, instance]
def
mul_action_sphere_closed_ball
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{r : ℝ} :
mul_action ↥(metric.sphere 0 1) ↥(metric.closed_ball 0 r)
Equations
- mul_action_sphere_closed_ball = {to_has_smul := {smul := λ (c : ↥(metric.sphere 0 1)) (x : ↥(metric.closed_ball 0 r)), set.inclusion mul_action_sphere_closed_ball._proof_1 c • x}, one_smul := _, mul_smul := _}
@[protected, instance]
def
has_continuous_smul_sphere_closed_ball
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{r : ℝ} :
has_continuous_smul ↥(metric.sphere 0 1) ↥(metric.closed_ball 0 r)
@[protected, instance]
def
mul_action_sphere_sphere
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{r : ℝ} :
mul_action ↥(metric.sphere 0 1) ↥(metric.sphere 0 r)
Equations
- mul_action_sphere_sphere = {to_has_smul := {smul := λ (c : ↥(metric.sphere 0 1)) (x : ↥(metric.sphere 0 r)), ⟨↑c • ↑x, _⟩}, one_smul := _, mul_smul := _}
@[protected, instance]
def
has_continuous_smul_sphere_sphere
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
{r : ℝ} :
has_continuous_smul ↥(metric.sphere 0 1) ↥(metric.sphere 0 r)
@[protected, instance]
def
is_scalar_tower_closed_ball_closed_ball_closed_ball
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[normed_field 𝕜]
[normed_field 𝕜']
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space 𝕜' E]
{r : ℝ}
[normed_algebra 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' E] :
is_scalar_tower ↥(metric.closed_ball 0 1) ↥(metric.closed_ball 0 1) ↥(metric.closed_ball 0 r)
@[protected, instance]
def
is_scalar_tower_closed_ball_closed_ball_ball
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[normed_field 𝕜]
[normed_field 𝕜']
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space 𝕜' E]
{r : ℝ}
[normed_algebra 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' E] :
is_scalar_tower ↥(metric.closed_ball 0 1) ↥(metric.closed_ball 0 1) ↥(metric.ball 0 r)
@[protected, instance]
def
is_scalar_tower_sphere_closed_ball_closed_ball
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[normed_field 𝕜]
[normed_field 𝕜']
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space 𝕜' E]
{r : ℝ}
[normed_algebra 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' E] :
is_scalar_tower ↥(metric.sphere 0 1) ↥(metric.closed_ball 0 1) ↥(metric.closed_ball 0 r)
@[protected, instance]
def
is_scalar_tower_sphere_closed_ball_ball
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[normed_field 𝕜]
[normed_field 𝕜']
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space 𝕜' E]
{r : ℝ}
[normed_algebra 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' E] :
is_scalar_tower ↥(metric.sphere 0 1) ↥(metric.closed_ball 0 1) ↥(metric.ball 0 r)
@[protected, instance]
def
is_scalar_tower_sphere_sphere_closed_ball
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[normed_field 𝕜]
[normed_field 𝕜']
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space 𝕜' E]
{r : ℝ}
[normed_algebra 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' E] :
is_scalar_tower ↥(metric.sphere 0 1) ↥(metric.sphere 0 1) ↥(metric.closed_ball 0 r)
@[protected, instance]
def
is_scalar_tower_sphere_sphere_ball
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[normed_field 𝕜]
[normed_field 𝕜']
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space 𝕜' E]
{r : ℝ}
[normed_algebra 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' E] :
is_scalar_tower ↥(metric.sphere 0 1) ↥(metric.sphere 0 1) ↥(metric.ball 0 r)
@[protected, instance]
def
is_scalar_tower_sphere_sphere_sphere
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[normed_field 𝕜]
[normed_field 𝕜']
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space 𝕜' E]
{r : ℝ}
[normed_algebra 𝕜 𝕜']
[is_scalar_tower 𝕜 𝕜' E] :
is_scalar_tower ↥(metric.sphere 0 1) ↥(metric.sphere 0 1) ↥(metric.sphere 0 r)
@[protected, instance]
def
is_scalar_tower_sphere_ball_ball
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[normed_field 𝕜]
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜'] :
is_scalar_tower ↥(metric.sphere 0 1) ↥(metric.ball 0 1) ↥(metric.ball 0 1)
@[protected, instance]
def
is_scalar_tower_closed_ball_ball_ball
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[normed_field 𝕜]
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜'] :
is_scalar_tower ↥(metric.closed_ball 0 1) ↥(metric.ball 0 1) ↥(metric.ball 0 1)
@[protected, instance]
def
smul_comm_class_closed_ball_closed_ball_closed_ball
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[normed_field 𝕜]
[normed_field 𝕜']
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space 𝕜' E]
{r : ℝ}
[smul_comm_class 𝕜 𝕜' E] :
smul_comm_class ↥(metric.closed_ball 0 1) ↥(metric.closed_ball 0 1) ↥(metric.closed_ball 0 r)
@[protected, instance]
def
smul_comm_class_closed_ball_closed_ball_ball
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[normed_field 𝕜]
[normed_field 𝕜']
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space 𝕜' E]
{r : ℝ}
[smul_comm_class 𝕜 𝕜' E] :
smul_comm_class ↥(metric.closed_ball 0 1) ↥(metric.closed_ball 0 1) ↥(metric.ball 0 r)
@[protected, instance]
def
smul_comm_class_sphere_closed_ball_closed_ball
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[normed_field 𝕜]
[normed_field 𝕜']
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space 𝕜' E]
{r : ℝ}
[smul_comm_class 𝕜 𝕜' E] :
smul_comm_class ↥(metric.sphere 0 1) ↥(metric.closed_ball 0 1) ↥(metric.closed_ball 0 r)
@[protected, instance]
def
smul_comm_class_sphere_closed_ball_ball
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[normed_field 𝕜]
[normed_field 𝕜']
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space 𝕜' E]
{r : ℝ}
[smul_comm_class 𝕜 𝕜' E] :
smul_comm_class ↥(metric.sphere 0 1) ↥(metric.closed_ball 0 1) ↥(metric.ball 0 r)
@[protected, instance]
def
smul_comm_class_sphere_ball_ball
{𝕜 : Type u_1}
{𝕜' : Type u_2}
[normed_field 𝕜]
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜'] :
smul_comm_class ↥(metric.sphere 0 1) ↥(metric.ball 0 1) ↥(metric.ball 0 1)
@[protected, instance]
def
smul_comm_class_sphere_sphere_closed_ball
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[normed_field 𝕜]
[normed_field 𝕜']
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space 𝕜' E]
{r : ℝ}
[smul_comm_class 𝕜 𝕜' E] :
smul_comm_class ↥(metric.sphere 0 1) ↥(metric.sphere 0 1) ↥(metric.closed_ball 0 r)
@[protected, instance]
def
smul_comm_class_sphere_sphere_ball
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[normed_field 𝕜]
[normed_field 𝕜']
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space 𝕜' E]
{r : ℝ}
[smul_comm_class 𝕜 𝕜' E] :
smul_comm_class ↥(metric.sphere 0 1) ↥(metric.sphere 0 1) ↥(metric.ball 0 r)
@[protected, instance]
def
smul_comm_class_sphere_sphere_sphere
{𝕜 : Type u_1}
{𝕜' : Type u_2}
{E : Type u_3}
[normed_field 𝕜]
[normed_field 𝕜']
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[normed_space 𝕜' E]
{r : ℝ}
[smul_comm_class 𝕜 𝕜' E] :
smul_comm_class ↥(metric.sphere 0 1) ↥(metric.sphere 0 1) ↥(metric.sphere 0 r)
theorem
ne_neg_of_mem_sphere
(𝕜 : Type u_1)
{E : Type u_3}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[char_zero 𝕜]
{r : ℝ}
(hr : r ≠ 0)
(x : ↥(metric.sphere 0 r)) :
theorem
ne_neg_of_mem_unit_sphere
(𝕜 : Type u_1)
{E : Type u_3}
[normed_field 𝕜]
[seminormed_add_comm_group E]
[normed_space 𝕜 E]
[char_zero 𝕜]
(x : ↥(metric.sphere 0 1)) :