Equivariant child-evaluation test map #
An arbitrary nice multivalued function is evaluated on all equal-area children. The resulting coordinate vector is continuous and transforms by coordinate relabelling.
noncomputable def
NRR.PrimeConfigurationModel.childTestMap
{p : ℕ}
{hp : Nat.Prime p}
{K : Geometry.ConvexBody Geometry.Plane}
{A : ℝ}
(M : PrimeConfigurationModel hp)
(hA : 0 < A)
(φ : NiceMV (BodySpace K (A / ↑p)))
:
Evaluate the multivalued observable on every equal-area child body and interval parameter.
Equations
- M.childTestMap hA φ z i = φ.eval (NRR.EMP.VariableBody.child M.sites hA ⋯ z.1 i) z.2
Instances For
theorem
NRR.PrimeConfigurationModel.continuous_childTestMap
{p : ℕ}
{hp : Nat.Prime p}
{K : Geometry.ConvexBody Geometry.Plane}
{A : ℝ}
(M : PrimeConfigurationModel hp)
(hA : 0 < A)
(φ : NiceMV (BodySpace K (A / ↑p)))
:
Continuous (M.childTestMap hA φ)
theorem
NRR.PrimeConfigurationModel.childTestMap_smul
{p : ℕ}
{hp : Nat.Prime p}
{K : Geometry.ConvexBody Geometry.Plane}
{A : ℝ}
(M : PrimeConfigurationModel hp)
(hA : 0 < A)
(φ : NiceMV (BodySpace K (A / ↑p)))
(g : ↥(PrimeSymmetry p))
(z : (BodySpace K A × M.Point) × ↑SignedInterval)
:
def
NRR.PrimeConfigurationModel.allChildrenZeroSet
{p : ℕ}
{hp : Nat.Prime p}
{K : Geometry.ConvexBody Geometry.Plane}
{A : ℝ}
(M : PrimeConfigurationModel hp)
(hA : 0 < A)
(φ : NiceMV (BodySpace K (A / ↑p)))
:
The simultaneous child-zero set.
Equations
- M.allChildrenZeroSet hA φ = {z : (NRR.BodySpace K A × M.Point) × ↑NRR.SignedInterval | M.childTestMap hA φ z = 0}
Instances For
theorem
NRR.PrimeConfigurationModel.mem_allChildrenZeroSet_iff
{p : ℕ}
{hp : Nat.Prime p}
{K : Geometry.ConvexBody Geometry.Plane}
{A : ℝ}
(M : PrimeConfigurationModel hp)
(hA : 0 < A)
(φ : NiceMV (BodySpace K (A / ↑p)))
(z : (BodySpace K A × M.Point) × ↑SignedInterval)
:
z ∈ M.allChildrenZeroSet hA φ ↔ ∀ (i : Fin p), φ.Zero (EMP.VariableBody.child M.sites hA ⋯ z.1 i) z.2
theorem
NRR.PrimeConfigurationModel.isClosed_allChildrenZeroSet
{p : ℕ}
{hp : Nat.Prime p}
{K : Geometry.ConvexBody Geometry.Plane}
{A : ℝ}
(M : PrimeConfigurationModel hp)
(hA : 0 < A)
(φ : NiceMV (BodySpace K (A / ↑p)))
:
IsClosed (M.allChildrenZeroSet hA φ)
theorem
NRR.PrimeConfigurationModel.allChildrenZeroSet_invariant
{p : ℕ}
{hp : Nat.Prime p}
{K : Geometry.ConvexBody Geometry.Plane}
{A : ℝ}
(M : PrimeConfigurationModel hp)
(hA : 0 < A)
(φ : NiceMV (BodySpace K (A / ↑p)))
(g : ↥(PrimeSymmetry p))
(z : (BodySpace K A × M.Point) × ↑SignedInterval)
:
z ∈ M.allChildrenZeroSet hA φ → M.smulBodyPointInterval g z ∈ M.allChildrenZeroSet hA φ