Endpoint orthants

The strict endpoint signs of a nice multivalued function place the child test map in the negative orthant at -1 and the positive orthant at 1.

def NRR.negativeOrthant (p : ℕ) : Set (Fin p → ℝ)

Strictly negative coordinate orthant.

Equations

• NRR.negativeOrthant p = {v : Fin p → ℝ | ∀ (i : Fin p), v i < 0}

def NRR.positiveOrthant (p : ℕ) : Set (Fin p → ℝ)

Strictly positive coordinate orthant.

Equations

• NRR.positiveOrthant p = {v : Fin p → ℝ | ∀ (i : Fin p), 0 < v i}

theorem NRR.isOpen_negativeOrthant {p : ℕ} : IsOpen (negativeOrthant p)

theorem NRR.isOpen_positiveOrthant {p : ℕ} : IsOpen (positiveOrthant p)

theorem NRR.negativeOrthant_invariant (p : ℕ) : IsPrimeInvariant (negativeOrthant p)

theorem NRR.positiveOrthant_invariant (p : ℕ) : IsPrimeInvariant (positiveOrthant p)

theorem NRR.zero_not_mem_negativeOrthant {p : ℕ} (hp : Nat.Prime p) : 0 ∉ negativeOrthant p

theorem NRR.zero_not_mem_positiveOrthant {p : ℕ} (hp : Nat.Prime p) : 0 ∉ positiveOrthant p

theorem NRR.PrimeConfigurationModel.childTestMap_left_mem_negative {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (hA : 0 < A) (φ : NiceMV (BodySpace K (A / ↑p))) (C : BodySpace K A) (x : M.Point) : M.childTestMap hA φ ((C, x), SignedInterval.left) ∈ negativeOrthant p

theorem NRR.PrimeConfigurationModel.childTestMap_right_mem_positive {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (hA : 0 < A) (φ : NiceMV (BodySpace K (A / ↑p))) (C : BodySpace K A) (x : M.Point) : M.childTestMap hA φ ((C, x), SignedInterval.right) ∈ positiveOrthant p

def NRR.PrimeConfigurationModel.leftBoundary {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (K : Geometry.ConvexBody Geometry.Plane) (A : ℝ) : Set ((BodySpace K A × M.Point) × ↑SignedInterval)

Left endpoint boundary.

Equations

• M.leftBoundary K A = {z : (NRR.BodySpace K A × M.Point) × ↑NRR.SignedInterval | z.2 = NRR.SignedInterval.left}

def NRR.PrimeConfigurationModel.rightBoundary {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (K : Geometry.ConvexBody Geometry.Plane) (A : ℝ) : Set ((BodySpace K A × M.Point) × ↑SignedInterval)

Right endpoint boundary.

Equations

• M.rightBoundary K A = {z : (NRR.BodySpace K A × M.Point) × ↑NRR.SignedInterval | z.2 = NRR.SignedInterval.right}

theorem NRR.PrimeConfigurationModel.allChildrenZeroSet_disjoint_left {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (hA : 0 < A) (φ : NiceMV (BodySpace K (A / ↑p))) : Disjoint (M.allChildrenZeroSet hA φ) (M.leftBoundary K A)

theorem NRR.PrimeConfigurationModel.allChildrenZeroSet_disjoint_right {p : ℕ} {hp : Nat.Prime p} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (M : PrimeConfigurationModel hp) (hA : 0 < A) (φ : NiceMV (BodySpace K (A / ↑p))) : Disjoint (M.allChildrenZeroSet hA φ) (M.rightBoundary K A)