Documentation

Mathlib.Analysis.NormedSpace.BallAction

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.

instance mulActionClosedBallBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} :

MulAction ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)

Equations

mulActionClosedBallBall = MulAction.mk ⋯ ⋯

instance continuousSMul_closedBall_ball {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} :

ContinuousSMul ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)

Equations

⋯ = ⋯

instance mulActionClosedBallClosedBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} :

MulAction ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)

Equations

mulActionClosedBallClosedBall = MulAction.mk ⋯ ⋯

instance continuousSMul_closedBall_closedBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} :

ContinuousSMul ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)

Equations

⋯ = ⋯

instance mulActionSphereBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} :

MulAction ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)

Equations

mulActionSphereBall = MulAction.mk ⋯ ⋯

instance continuousSMul_sphere_ball {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} :

ContinuousSMul ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)

Equations

⋯ = ⋯

instance mulActionSphereClosedBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} :

MulAction ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)

Equations

mulActionSphereClosedBall = MulAction.mk ⋯ ⋯

instance continuousSMul_sphere_closedBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} :

ContinuousSMul ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)

Equations

⋯ = ⋯

instance mulActionSphereSphere {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} :

MulAction ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)

Equations

mulActionSphereSphere = MulAction.mk ⋯ ⋯

instance continuousSMul_sphere_sphere {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} :

ContinuousSMul ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)

Equations

⋯ = ⋯

instance isScalarTower_closedBall_closedBall_closedBall {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] :

IsScalarTower ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)

Equations

⋯ = ⋯

instance isScalarTower_closedBall_closedBall_ball {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] :

IsScalarTower ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)

Equations

⋯ = ⋯

instance isScalarTower_sphere_closedBall_closedBall {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] :

IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)

Equations

⋯ = ⋯

instance isScalarTower_sphere_closedBall_ball {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] :

IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)

Equations

⋯ = ⋯

instance isScalarTower_sphere_sphere_closedBall {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] :

IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)

Equations

⋯ = ⋯

instance isScalarTower_sphere_sphere_ball {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] :

IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)

Equations

⋯ = ⋯

instance isScalarTower_sphere_sphere_sphere {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] :

IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)

Equations

⋯ = ⋯

instance isScalarTower_sphere_ball_ball {𝕜 : Type u_1} {𝕜' : Type u_2} [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] :

IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.ball 0 1) ↑(Metric.ball 0 1)

Equations

⋯ = ⋯

instance isScalarTower_closedBall_ball_ball {𝕜 : Type u_1} {𝕜' : Type u_2} [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] :

IsScalarTower ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 1) ↑(Metric.ball 0 1)

Equations

⋯ = ⋯

instance instSMulCommClass_closedBall_closedBall_closedBall {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] :

SMulCommClass ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)

Equations

⋯ = ⋯

instance instSMulCommClass_closedBall_closedBall_ball {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] :

SMulCommClass ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)

Equations

⋯ = ⋯

instance instSMulCommClass_sphere_closedBall_closedBall {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] :

SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)

Equations

⋯ = ⋯

instance instSMulCommClass_sphere_closedBall_ball {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] :

SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)

Equations

⋯ = ⋯

instance instSMulCommClass_sphere_ball_ball {𝕜 : Type u_1} {𝕜' : Type u_2} [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] :

SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.ball 0 1) ↑(Metric.ball 0 1)

Equations

⋯ = ⋯

instance instSMulCommClass_sphere_sphere_closedBall {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] :

SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)

Equations

⋯ = ⋯

instance instSMulCommClass_sphere_sphere_ball {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] :

SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)

Equations

⋯ = ⋯

instance instSMulCommClass_sphere_sphere_sphere {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] :

SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)

Equations

⋯ = ⋯

theorem ne_neg_of_mem_sphere (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CharZero 𝕜] {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} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CharZero 𝕜] (x : ↑(Metric.sphere 0 1)) :

x ≠ -x