NRR.Multivalued.ChildEvaluation — nice multivalued functions on continuous children

This module combines the continuous variable power-partition children on the lower-area convex-body hyperspace with an arbitrary nice multivalued function φ on that hyperspace.

For a parameter z = ((C, x), t) with base body C, site parameter x, and signed-interval coordinate t, and for a site index i, the child evaluation φ.childEval evaluates φ at the canonical child child sites hA hn (C, x) i and the interval coordinate t. The child depends continuously on (C, x) and the interval coordinate is continuous, so each coordinate evaluation is continuous; the whole vector of coordinate evaluations is continuous by continuous_pi.

The simultaneous-zero set collects the parameters at which φ vanishes on every child at once. It is a finite intersection of coordinate zero sets, hence closed, and membership is exactly the vanishing of every child evaluation coordinate.

The output is kept in Fin n → ℝ; no projection to a zero-sum representation is performed here, and no common zero, equivariance, or obstruction result is assumed.

noncomputable def NRR.NiceMV.childEval {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} {X : Type u_1} [MetricSpace X] (sites : EMP.VariableBody.SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (φ : NiceMV (BodySpace K (A / ↑n))) (z : (BodySpace K A × X) × ↑SignedInterval) (i : Fin n) : ℝ

The child evaluation of a nice multivalued function φ at parameter z = ((C, x), t) and site index i: evaluate φ at the canonical child child sites hA hn (C, x) i and the signed interval coordinate t.

Equations

• NRR.NiceMV.childEval sites hA hn φ z i = φ.eval (NRR.EMP.VariableBody.child sites hA hn z.1 i) z.2

theorem NRR.NiceMV.continuous_childEval {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} {X : Type u_1} [MetricSpace X] [CompactSpace X] (sites : EMP.VariableBody.SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (φ : NiceMV (BodySpace K (A / ↑n))) (i : Fin n) : Continuous fun (z : (BodySpace K A × X) × ↑SignedInterval) => childEval sites hA hn φ z i

Continuity of a child evaluation coordinate. The child depends continuously on (C, x) via EMP.VariableBody.continuous_child, the interval coordinate is continuous, and φ.continuous_eval composes the two.

theorem NRR.NiceMV.continuous_childEvalVec {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} {X : Type u_1} [MetricSpace X] [CompactSpace X] (sites : EMP.VariableBody.SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (φ : NiceMV (BodySpace K (A / ↑n))) : Continuous fun (z : (BodySpace K A × X) × ↑SignedInterval) (i : Fin n) => childEval sites hA hn φ z i

Continuity of the child evaluation vector. The whole finite family of coordinate evaluations depends continuously on the parameter, by continuous_pi.

def NRR.NiceMV.allChildrenZeroSet {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} {X : Type u_1} [MetricSpace X] (sites : EMP.VariableBody.SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (φ : NiceMV (BodySpace K (A / ↑n))) : Set ((BodySpace K A × X) × ↑SignedInterval)

The simultaneous child-zero set: the parameters at which φ vanishes on every child at once.

Equations

• NRR.NiceMV.allChildrenZeroSet sites hA hn φ = {z : (NRR.BodySpace K A × X) × ↑NRR.SignedInterval | ∀ (i : Fin n), φ.Zero (NRR.EMP.VariableBody.child sites hA hn z.1 i) z.2}

theorem NRR.NiceMV.mem_allChildrenZeroSet_iff {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} {X : Type u_1} [MetricSpace X] (sites : EMP.VariableBody.SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (φ : NiceMV (BodySpace K (A / ↑n))) (z : (BodySpace K A × X) × ↑SignedInterval) : z ∈ allChildrenZeroSet sites hA hn φ ↔ ∀ (i : Fin n), childEval sites hA hn φ z i = 0

Membership in the simultaneous child-zero set is exactly the vanishing of every child evaluation coordinate.

theorem NRR.NiceMV.isClosed_allChildrenZeroSet {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} {X : Type u_1} [MetricSpace X] [CompactSpace X] (sites : EMP.VariableBody.SiteFamily X n) (hA : 0 < A) (hn : 0 < n) (φ : NiceMV (BodySpace K (A / ↑n))) : IsClosed (allChildrenZeroSet sites hA hn φ)

Closedness of the simultaneous child-zero set. It is the finite intersection over i of the coordinate zero sets, each closed as the zero set of a continuous coordinate evaluation.