Route B: measurability of the complete mixed-face bad set

The existential witness ranges over the compact standard simplex. Strict positivity is exhausted by countably many closed threshold conditions. Each threshold relation is closed in parameter space times the simplex, and its projection is closed because the simplex is compact. Hence the complete bad set is a countable union of closed sets.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.jointAffineCoordinate {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (z : MovableParameterSpace hp C × StandardSimplex p) (j : Fin p) : ℝ

One coordinate of the joint affine value as a function of the movable assignment and the simplex witness.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.jointDeviation {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (z : MovableParameterSpace hp C × StandardSimplex p) (r : Fin (p - 1)) : ℝ

Joint deviation coordinate.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.jointMean {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (z : MovableParameterSpace hp C × StandardSimplex p) : ℝ

Joint mean coordinate.

Equations

• One or more equations did not get rendered due to their size.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.continuous_jointAffineCoordinate {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (j : Fin p) : Continuous fun (z : MovableParameterSpace hp C × StandardSimplex p) => jointAffineCoordinate hp C base κ z j

Joint affine coordinates are continuous in both the movable parameters and the simplex witness.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.continuous_jointDeviation {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (r : Fin (p - 1)) : Continuous fun (z : MovableParameterSpace hp C × StandardSimplex p) => jointDeviation hp C base κ z r

Joint deviations are continuous.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.continuous_jointMean {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) : Continuous fun (z : MovableParameterSpace hp C × StandardSimplex p) => jointMean hp C base κ z

The joint mean is continuous.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.mixedFaceThresholdRelation {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (n m : ℕ) : Set (MovableParameterSpace hp C × StandardSimplex p)

Closed threshold relation. The natural numbers replace the two strict positivity conditions by positive lower bounds.

Equations

• One or more equations did not get rendered due to their size.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.isClosed_mixedFaceThresholdRelation {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (n m : ℕ) : IsClosed (mixedFaceThresholdRelation hp C base κ n m)

Every threshold relation is closed.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.mixedFaceThresholdBadSet {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (n m : ℕ) : Set (MovableParameterSpace hp C)

Projection of one closed threshold relation to movable parameter space.

Equations

• One or more equations did not get rendered due to their size.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.isClosed_mixedFaceThresholdBadSet {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) (n m : ℕ) : IsClosed (mixedFaceThresholdBadSet hp C base κ n m)

Compactness of the simplex makes every threshold projection closed.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.mixedFaceBadSet_eq_iUnion_threshold {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) : mixedFaceBadSet hp C base κ = ⋃ (n : ℕ), ⋃ (m : ℕ), mixedFaceThresholdBadSet hp C base κ n m

The complete existential bad set is exhausted by the closed threshold projections.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.measurableSet_mixedFaceBadSet {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (κ : MixedFaceCase hp C) : MeasurableSet (mixedFaceBadSet hp C base κ)

The complete mixed-face bad set is measurable.