mathlib documentation

analysis.normed_space.ball_action

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.

@[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 : } :
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[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 : } :
Equations
@[protected, instance]
@[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 : } :
Equations
@[protected, instance]
@[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 : } :
Equations
@[protected, instance]
@[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] :
@[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] :
@[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] :
@[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] :
@[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] :
@[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] :
@[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] :
@[protected, instance]
def is_scalar_tower_sphere_ball_ball {𝕜 : Type u_1} {𝕜' : Type u_2} [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] :
@[protected, instance]
def is_scalar_tower_closed_ball_ball_ball {𝕜 : Type u_1} {𝕜' : Type u_2} [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] :
@[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] :
@[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] :
@[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] :
@[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] :
@[protected, instance]
def smul_comm_class_sphere_ball_ball {𝕜 : Type u_1} {𝕜' : Type u_2} [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] :
@[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] :
@[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] :
@[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] :
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)) :
x -x
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)) :
x -x