Equivariance of variable-body children #
The proof is set-theoretic: normalized weights reindex by σ.symm, restricted power cells reindex
by the same convention, and extensionality lifts carrier equality to ConvexSubbody and
BodySpace.
theorem
NRR.EMP.VariableBody.normalizedWeight_relabel
{n : ℕ}
{K : Geometry.ConvexBody Geometry.Plane}
{A : ℝ}
(hA : 0 < A)
(hn : 0 < n)
(C : BodySpace K A)
(s : Config n)
(σ : Equiv.Perm (Fin n))
:
normalizedWeight hA hn C (Config.relabel σ s) = fun (i : Fin n) => normalizedWeight hA hn C s ((Equiv.symm σ) i)
theorem
NRR.EMP.VariableBody.canonicalCellSet_relabel
{n : ℕ}
{K : Geometry.ConvexBody Geometry.Plane}
{A : ℝ}
(hA : 0 < A)
(hn : 0 < n)
(C : BodySpace K A)
(s : Config n)
(σ : Equiv.Perm (Fin n))
(i : Fin n)
:
cellSet hA C (Config.relabel σ s) (normalizedWeight hA hn C (Config.relabel σ s)) i = cellSet hA C s (normalizedWeight hA hn C s) ((Equiv.symm σ) i)
theorem
NRR.PrimeConfigurationModel.child_smul
{p : ℕ}
{K : Geometry.ConvexBody Geometry.Plane}
{A : ℝ}
{hp : Nat.Prime p}
(M : PrimeConfigurationModel hp)
(hA : 0 < A)
(C : BodySpace K A)
(g : ↥(PrimeSymmetry p))
(x : M.Point)
(i : Fin p)
:
EMP.VariableBody.child M.sites hA ⋯ (C, g • x) i = EMP.VariableBody.child M.sites hA ⋯ (C, x) ((Equiv.symm ((PrimeSymmetry.toPerm p) g)) i)
theorem
NRR.PrimeConfigurationModel.child_carrier_smul
{p : ℕ}
{K : Geometry.ConvexBody Geometry.Plane}
{A : ℝ}
{hp : Nat.Prime p}
(M : PrimeConfigurationModel hp)
(hA : 0 < A)
(C : BodySpace K A)
(g : ↥(PrimeSymmetry p))
(x : M.Point)
(i : Fin p)
:
↑(EMP.VariableBody.child M.sites hA ⋯ (C, g • x) i).body.body = ↑(EMP.VariableBody.child M.sites hA ⋯ (C, x) ((Equiv.symm ((PrimeSymmetry.toPerm p) g)) i)).body.body