Site family and explicit parameter actions

The body and signed-interval coordinates are fixed; only the model point is moved by the prime symmetry group. Named maps are used instead of global product-action instances.

def NRR.PrimeConfigurationModel.sites {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) : EMP.VariableBody.SiteFamily M.Point p

The model configuration map as the compact site family used by the variable-body partition construction.

Equations

• M.sites = M.toConfig

@[simp]

theorem NRR.PrimeConfigurationModel.sites_apply {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (x : M.Point) : M.sites x = M.toConfig x

theorem NRR.PrimeConfigurationModel.sites_equivariant {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) : IsPrimeEquivariant ⇑M.sites

def NRR.PrimeConfigurationModel.smulBodyPoint {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (g : ↥(PrimeSymmetry p)) (z : BodySpace K A × M.Point) : BodySpace K A × M.Point

Action on a body/model-point parameter, fixing the body.

Equations

• M.smulBodyPoint g z = (z.1, g • z.2)

def NRR.PrimeConfigurationModel.smulBodyPointInterval {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (g : ↥(PrimeSymmetry p)) (z : (BodySpace K A × M.Point) × ↑SignedInterval) : (BodySpace K A × M.Point) × ↑SignedInterval

Action on a body/model-point/interval parameter, fixing body and interval.

Equations

• M.smulBodyPointInterval g z = ((z.1.1, g • z.1.2), z.2)

@[simp]

theorem NRR.PrimeConfigurationModel.smulBodyPoint_one {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (z : BodySpace K A × M.Point) : M.smulBodyPoint 1 z = z

theorem NRR.PrimeConfigurationModel.smulBodyPoint_mul {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (g h : ↥(PrimeSymmetry p)) (z : BodySpace K A × M.Point) : M.smulBodyPoint (g * h) z = M.smulBodyPoint g (M.smulBodyPoint h z)

@[simp]

theorem NRR.PrimeConfigurationModel.smulBodyPointInterval_one {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (z : (BodySpace K A × M.Point) × ↑SignedInterval) : M.smulBodyPointInterval 1 z = z

theorem NRR.PrimeConfigurationModel.smulBodyPointInterval_mul {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (g h : ↥(PrimeSymmetry p)) (z : (BodySpace K A × M.Point) × ↑SignedInterval) : M.smulBodyPointInterval (g * h) z = M.smulBodyPointInterval g (M.smulBodyPointInterval h z)

theorem NRR.PrimeConfigurationModel.continuous_smulBodyPoint {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (g : ↥(PrimeSymmetry p)) : Continuous (M.smulBodyPoint g)

theorem NRR.PrimeConfigurationModel.continuous_smulBodyPointInterval {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (g : ↥(PrimeSymmetry p)) : Continuous (M.smulBodyPointInterval g)