Local zero-free homotopies for the child-map family

The frozen child coordinate map depends continuously on the parent body and signed-interval parameter. Compactness of the order-complex realization upgrades this to a local uniform estimate. Consequently, outside the projected full-zero set, nearby frozen child maps are joined by a zero-free straight-line homotopy.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.childFamilyMap {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) : C((BodySpace K A × ↑SignedInterval) × Realization p, Fin p → ℝ)

Joint child coordinate map, with the parent/interval parameter left variable.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.childFamilyMap_apply {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (z : BodySpace K A × ↑SignedInterval) (x : Realization p) : (childFamilyMap hp hA phi) (z, x) = (childMap hp hA phi z) x

theorem NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.exists_childMap_norm_margin {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (z : BodySpace K A × ↑SignedInterval) (hz : z ∈ ((orderComplexModel hp).projectedAllChildrenZeroSet hA phi)ᶜ) : ∃ (m : ℝ), 0 < m ∧ ∀ (x : Realization p), m ≤ ‖(childMap hp hA phi z) x‖

Uniform positive norm margin of one frozen zero-free child map.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.exists_uniform_childMap_neighborhood {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (z : BodySpace K A × ↑SignedInterval) {eps : ℝ} (heps : 0 < eps) : ∃ (U : Set (BodySpace K A × ↑SignedInterval)), IsOpen U ∧ z ∈ U ∧ ∀ w ∈ U, ∀ (x : Realization p), ‖(childMap hp hA phi w) x - (childMap hp hA phi z) x‖ < eps

Nearby parameters give uniformly close frozen child maps.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.segment_ne_zero_of_norm_sub_lt {p : ℕ} {v w : Fin p → ℝ} {m : ℝ} (hm : m ≤ ‖v‖) (hclose : ‖w - v‖ < m) (t : ↑(Set.Icc 0 1)) : (1 - ↑t) • v + ↑t • w ≠ 0

A vector segment stays nonzero when its moving endpoint remains closer than the norm margin.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantCoordinateHomotopy.exists_local_zeroFreeHomotopy {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (z : BodySpace K A × ↑SignedInterval) (hz : z ∈ ((orderComplexModel hp).projectedAllChildrenZeroSet hA phi)ᶜ) : ∃ (U : Set (BodySpace K A × ↑SignedInterval)) (hUout : U ⊆ ((orderComplexModel hp).projectedAllChildrenZeroSet hA phi)ᶜ), IsOpen U ∧ z ∈ U ∧ ∀ (w : BodySpace K A × ↑SignedInterval) (hw : w ∈ U), Nonempty (ZeroFreeHomotopy hp (childZeroFreeMap hp hA phi z hz) (childZeroFreeMap hp hA phi w ⋯))

Outside the projected zero set, nearby frozen child maps are joined by a zero-free equivariant straight-line homotopy.