Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: port Analysis.NormedSpace.BallAction (#3513)
- Loading branch information
Showing
2 changed files
with
213 additions
and
0 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,212 @@ | ||
/- | ||
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 | ||
! This file was ported from Lean 3 source module analysis.normed_space.ball_action | ||
! leanprover-community/mathlib commit 3339976e2bcae9f1c81e620836d1eb736e3c4700 | ||
! Please do not edit these lines, except to modify the commit id | ||
! if you have ported upstream changes. | ||
-/ | ||
import Mathlib.Analysis.Normed.Field.UnitBall | ||
import Mathlib.Analysis.NormedSpace.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 | ||
|
||
variable {π π' E : Type _} [NormedField π] [NormedField π'] [SeminormedAddCommGroup E] | ||
[NormedSpace π E] [NormedSpace π' E] {r : β} | ||
|
||
section ClosedBall | ||
|
||
instance mulActionClosedBallBall : MulAction (closedBall (0 : π) 1) (ball (0 : E) r) where | ||
smul c x := | ||
β¨(c : π) β’ βx, | ||
mem_ball_zero_iff.2 <| by | ||
simpa only [norm_smul, one_mul] using | ||
mul_lt_mul' (mem_closedBall_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 _ _ _ | ||
#align mul_action_closed_ball_ball mulActionClosedBallBall | ||
|
||
instance continuousSMul_closedBall_ball : ContinuousSMul (closedBall (0 : π) 1) (ball (0 : E) r) := | ||
β¨(continuous_subtype_val.fst'.smul continuous_subtype_val.snd').subtype_mk _β© | ||
#align has_continuous_smul_closed_ball_ball continuousSMul_closedBall_ball | ||
|
||
instance mulActionClosedBallClosedBall : MulAction (closedBall (0 : π) 1) (closedBall (0 : E) r) | ||
where | ||
smul c x := | ||
β¨(c : π) β’ βx, | ||
mem_closedBall_zero_iff.2 <| by | ||
simpa only [norm_smul, one_mul] using | ||
mul_le_mul (mem_closedBall_zero_iff.1 c.2) (mem_closedBall_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 _ _ _ | ||
#align mul_action_closed_ball_closed_ball mulActionClosedBallClosedBall | ||
|
||
instance continuousSMul_closedBall_closedBall : | ||
ContinuousSMul (closedBall (0 : π) 1) (closedBall (0 : E) r) := | ||
β¨(continuous_subtype_val.fst'.smul continuous_subtype_val.snd').subtype_mk _β© | ||
#align has_continuous_smul_closed_ball_closed_ball continuousSMul_closedBall_closedBall | ||
|
||
end ClosedBall | ||
|
||
section Sphere | ||
|
||
instance mulActionSphereBall : MulAction (sphere (0 : π) 1) (ball (0 : E) r) where | ||
smul c x := inclusion sphere_subset_closedBall c β’ x | ||
one_smul _ := Subtype.ext <| one_smul _ _ | ||
mul_smul _ _ _ := Subtype.ext <| mul_smul _ _ _ | ||
#align mul_action_sphere_ball mulActionSphereBall | ||
|
||
instance continuousSMul_sphere_ball : ContinuousSMul (sphere (0 : π) 1) (ball (0 : E) r) := | ||
β¨(continuous_subtype_val.fst'.smul continuous_subtype_val.snd').subtype_mk _β© | ||
#align has_continuous_smul_sphere_ball continuousSMul_sphere_ball | ||
|
||
instance mulActionSphereClosedBall : MulAction (sphere (0 : π) 1) (closedBall (0 : E) r) where | ||
smul c x := inclusion sphere_subset_closedBall c β’ x | ||
one_smul _ := Subtype.ext <| one_smul _ _ | ||
mul_smul _ _ _ := Subtype.ext <| mul_smul _ _ _ | ||
#align mul_action_sphere_closed_ball mulActionSphereClosedBall | ||
|
||
instance continuousSMul_sphere_closedBall : | ||
ContinuousSMul (sphere (0 : π) 1) (closedBall (0 : E) r) := | ||
β¨(continuous_subtype_val.fst'.smul continuous_subtype_val.snd').subtype_mk _β© | ||
#align has_continuous_smul_sphere_closed_ball continuousSMul_sphere_closedBall | ||
|
||
instance mulActionSphereSphere : MulAction (sphere (0 : π) 1) (sphere (0 : E) r) where | ||
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 _ _ _ | ||
#align mul_action_sphere_sphere mulActionSphereSphere | ||
|
||
instance continuousSMul_sphere_sphere : ContinuousSMul (sphere (0 : π) 1) (sphere (0 : E) r) := | ||
β¨(continuous_subtype_val.fst'.smul continuous_subtype_val.snd').subtype_mk _β© | ||
#align has_continuous_smul_sphere_sphere continuousSMul_sphere_sphere | ||
|
||
end Sphere | ||
|
||
section IsScalarTower | ||
|
||
variable [NormedAlgebra π π'] [IsScalarTower π π' E] | ||
|
||
instance isScalarTower_closedBall_closedBall_closedBall : | ||
IsScalarTower (closedBall (0 : π) 1) (closedBall (0 : π') 1) (closedBall (0 : E) r) := | ||
β¨fun a b c => Subtype.ext <| smul_assoc (a : π) (b : π') (c : E)β© | ||
#align is_scalar_tower_closed_ball_closed_ball_closed_ball isScalarTower_closedBall_closedBall_closedBall | ||
|
||
instance isScalarTower_closedBall_closedBall_ball : | ||
IsScalarTower (closedBall (0 : π) 1) (closedBall (0 : π') 1) (ball (0 : E) r) := | ||
β¨fun a b c => Subtype.ext <| smul_assoc (a : π) (b : π') (c : E)β© | ||
#align is_scalar_tower_closed_ball_closed_ball_ball isScalarTower_closedBall_closedBall_ball | ||
|
||
instance isScalarTower_sphere_closedBall_closedBall : | ||
IsScalarTower (sphere (0 : π) 1) (closedBall (0 : π') 1) (closedBall (0 : E) r) := | ||
β¨fun a b c => Subtype.ext <| smul_assoc (a : π) (b : π') (c : E)β© | ||
#align is_scalar_tower_sphere_closed_ball_closed_ball isScalarTower_sphere_closedBall_closedBall | ||
|
||
instance isScalarTower_sphere_closedBall_ball : | ||
IsScalarTower (sphere (0 : π) 1) (closedBall (0 : π') 1) (ball (0 : E) r) := | ||
β¨fun a b c => Subtype.ext <| smul_assoc (a : π) (b : π') (c : E)β© | ||
#align is_scalar_tower_sphere_closed_ball_ball isScalarTower_sphere_closedBall_ball | ||
|
||
instance isScalarTower_sphere_sphere_closedBall : | ||
IsScalarTower (sphere (0 : π) 1) (sphere (0 : π') 1) (closedBall (0 : E) r) := | ||
β¨fun a b c => Subtype.ext <| smul_assoc (a : π) (b : π') (c : E)β© | ||
#align is_scalar_tower_sphere_sphere_closed_ball isScalarTower_sphere_sphere_closedBall | ||
|
||
instance isScalarTower_sphere_sphere_ball : | ||
IsScalarTower (sphere (0 : π) 1) (sphere (0 : π') 1) (ball (0 : E) r) := | ||
β¨fun a b c => Subtype.ext <| smul_assoc (a : π) (b : π') (c : E)β© | ||
#align is_scalar_tower_sphere_sphere_ball isScalarTower_sphere_sphere_ball | ||
|
||
instance isScalarTower_sphere_sphere_sphere : | ||
IsScalarTower (sphere (0 : π) 1) (sphere (0 : π') 1) (sphere (0 : E) r) := | ||
β¨fun a b c => Subtype.ext <| smul_assoc (a : π) (b : π') (c : E)β© | ||
#align is_scalar_tower_sphere_sphere_sphere isScalarTower_sphere_sphere_sphere | ||
|
||
instance isScalarTower_sphere_ball_ball : | ||
IsScalarTower (sphere (0 : π) 1) (ball (0 : π') 1) (ball (0 : π') 1) := | ||
β¨fun a b c => Subtype.ext <| smul_assoc (a : π) (b : π') (c : π')β© | ||
#align is_scalar_tower_sphere_ball_ball isScalarTower_sphere_ball_ball | ||
|
||
instance isScalarTower_closedBall_ball_ball : | ||
IsScalarTower (closedBall (0 : π) 1) (ball (0 : π') 1) (ball (0 : π') 1) := | ||
β¨fun a b c => Subtype.ext <| smul_assoc (a : π) (b : π') (c : π')β© | ||
#align is_scalar_tower_closed_ball_ball_ball isScalarTower_closedBall_ball_ball | ||
|
||
end IsScalarTower | ||
|
||
section SMulCommClass | ||
|
||
variable [SMulCommClass π π' E] | ||
|
||
instance sMulCommClass_closedBall_closedBall_closedBall : | ||
SMulCommClass (closedBall (0 : π) 1) (closedBall (0 : π') 1) (closedBall (0 : E) r) := | ||
β¨fun a b c => Subtype.ext <| smul_comm (a : π) (b : π') (c : E)β© | ||
#align smul_comm_class_closed_ball_closed_ball_closed_ball sMulCommClass_closedBall_closedBall_closedBall | ||
|
||
instance sMulCommClass_closedBall_closedBall_ball : | ||
SMulCommClass (closedBall (0 : π) 1) (closedBall (0 : π') 1) (ball (0 : E) r) := | ||
β¨fun a b c => Subtype.ext <| smul_comm (a : π) (b : π') (c : E)β© | ||
#align smul_comm_class_closed_ball_closed_ball_ball sMulCommClass_closedBall_closedBall_ball | ||
|
||
instance sMulCommClass_sphere_closedBall_closedBall : | ||
SMulCommClass (sphere (0 : π) 1) (closedBall (0 : π') 1) (closedBall (0 : E) r) := | ||
β¨fun a b c => Subtype.ext <| smul_comm (a : π) (b : π') (c : E)β© | ||
#align smul_comm_class_sphere_closed_ball_closed_ball sMulCommClass_sphere_closedBall_closedBall | ||
|
||
instance sMulCommClass_sphere_closedBall_ball : | ||
SMulCommClass (sphere (0 : π) 1) (closedBall (0 : π') 1) (ball (0 : E) r) := | ||
β¨fun a b c => Subtype.ext <| smul_comm (a : π) (b : π') (c : E)β© | ||
#align smul_comm_class_sphere_closed_ball_ball sMulCommClass_sphere_closedBall_ball | ||
|
||
instance sMulCommClass_sphere_ball_ball [NormedAlgebra π π'] : | ||
SMulCommClass (sphere (0 : π) 1) (ball (0 : π') 1) (ball (0 : π') 1) := | ||
β¨fun a b c => Subtype.ext <| smul_comm (a : π) (b : π') (c : π')β© | ||
#align smul_comm_class_sphere_ball_ball sMulCommClass_sphere_ball_ball | ||
|
||
instance sMulCommClass_sphere_sphere_closedBall : | ||
SMulCommClass (sphere (0 : π) 1) (sphere (0 : π') 1) (closedBall (0 : E) r) := | ||
β¨fun a b c => Subtype.ext <| smul_comm (a : π) (b : π') (c : E)β© | ||
#align smul_comm_class_sphere_sphere_closed_ball sMulCommClass_sphere_sphere_closedBall | ||
|
||
instance sMulCommClass_sphere_sphere_ball : | ||
SMulCommClass (sphere (0 : π) 1) (sphere (0 : π') 1) (ball (0 : E) r) := | ||
β¨fun a b c => Subtype.ext <| smul_comm (a : π) (b : π') (c : E)β© | ||
#align smul_comm_class_sphere_sphere_ball sMulCommClass_sphere_sphere_ball | ||
|
||
instance sMulCommClass_sphere_sphere_sphere : | ||
SMulCommClass (sphere (0 : π) 1) (sphere (0 : π') 1) (sphere (0 : E) r) := | ||
β¨fun a b c => Subtype.ext <| smul_comm (a : π) (b : π') (c : E)β© | ||
#align smul_comm_class_sphere_sphere_sphere sMulCommClass_sphere_sphere_sphere | ||
|
||
end SMulCommClass | ||
|
||
variable (π) | ||
|
||
variable [CharZero π] | ||
|
||
theorem ne_neg_of_mem_sphere {r : β} (hr : r β 0) (x : sphere (0 : E) r) : x β -x := fun h => | ||
ne_zero_of_mem_sphere hr x ((self_eq_neg π _).mp (by conv_lhs => rw [h])) | ||
#align ne_neg_of_mem_sphere ne_neg_of_mem_sphere | ||
|
||
theorem ne_neg_of_mem_unit_sphere (x : sphere (0 : E) 1) : x β -x := | ||
ne_neg_of_mem_sphere π one_ne_zero x | ||
#align ne_neg_of_mem_unit_sphere ne_neg_of_mem_unit_sphere |