NRR.Multivalued.Separator.SignedDistance — signed distance to the carrier

For a top–bottom separator S over a metric space X, the signed distance assigns to each point of X × SignedInterval its distance to the carrier, negated on the lower region:

signedDistance z = if z ∈ S.lower then -infDist z S.carrier else infDist z S.carrier

Its absolute value is the ordinary distance to the carrier, its zero set is exactly the carrier, it is strictly negative on the lower region and strictly positive on the upper region, and it takes the corresponding strict signs at the bottom and top boundaries. The carrier-point estimate bounds the absolute value by the distance to any chosen carrier point. Continuity is not treated here.

The carrier is nonempty because X is nonempty (via the vertical-fiber theorem), and it is closed by the separator structure; these two facts drive the sign laws through the Metric.infDist wrappers.

noncomputable def NRR.TopBottomSeparator.signedDistance {X : Type u_1} [MetricSpace X] (S : TopBottomSeparator X) (z : X × ↑SignedInterval) : ℝ

The signed distance to the carrier: the distance to the carrier, negated on the lower region.

Equations

• S.signedDistance z = if z ∈ S.lower then -Metric.infDist z S.carrier else Metric.infDist z S.carrier

theorem NRR.TopBottomSeparator.abs_signedDistance {X : Type u_1} [MetricSpace X] (S : TopBottomSeparator X) (z : X × ↑SignedInterval) : |S.signedDistance z| = Metric.infDist z S.carrier

The absolute value of the signed distance is the distance to the carrier.

theorem NRR.TopBottomSeparator.signedDistance_eq_zero_iff {X : Type u_1} [MetricSpace X] [Nonempty X] (S : TopBottomSeparator X) (z : X × ↑SignedInterval) : S.signedDistance z = 0 ↔ z ∈ S.carrier

The zero set of the signed distance is exactly the carrier.

theorem NRR.TopBottomSeparator.signedDistance_eq_zero_of_mem {X : Type u_1} [MetricSpace X] [Nonempty X] (S : TopBottomSeparator X) {z : X × ↑SignedInterval} (hz : z ∈ S.carrier) : S.signedDistance z = 0

The signed distance vanishes on the carrier.

theorem NRR.TopBottomSeparator.signedDistance_neg_of_mem_lower {X : Type u_1} [MetricSpace X] [Nonempty X] (S : TopBottomSeparator X) {z : X × ↑SignedInterval} (hz : z ∈ S.lower) : S.signedDistance z < 0

The signed distance is strictly negative on the lower region.

theorem NRR.TopBottomSeparator.signedDistance_pos_of_mem_upper {X : Type u_1} [MetricSpace X] [Nonempty X] (S : TopBottomSeparator X) {z : X × ↑SignedInterval} (hz : z ∈ S.upper) : 0 < S.signedDistance z

The signed distance is strictly positive on the upper region.

theorem NRR.TopBottomSeparator.signedDistance_left_neg {X : Type u_1} [MetricSpace X] [Nonempty X] (S : TopBottomSeparator X) (x : X) : S.signedDistance (x, SignedInterval.left) < 0

At the bottom boundary point the signed distance is strictly negative.

theorem NRR.TopBottomSeparator.signedDistance_right_pos {X : Type u_1} [MetricSpace X] [Nonempty X] (S : TopBottomSeparator X) (x : X) : 0 < S.signedDistance (x, SignedInterval.right)

At the top boundary point the signed distance is strictly positive.

theorem NRR.TopBottomSeparator.abs_signedDistance_le_dist_of_mem {X : Type u_1} [MetricSpace X] (S : TopBottomSeparator X) {z s : X × ↑SignedInterval} (hs : s ∈ S.carrier) : |S.signedDistance z| ≤ dist z s

The absolute value of the signed distance is bounded by the distance to any carrier point.

theorem NRR.TopBottomSeparator.continuous_signedDistance {X : Type u_1} [MetricSpace X] [Nonempty X] (S : TopBottomSeparator X) : Continuous S.signedDistance

The signed distance to the carrier is continuous on the whole product.

noncomputable def NRR.TopBottomSeparator.signedDistanceMap {X : Type u_1} [MetricSpace X] [Nonempty X] (S : TopBottomSeparator X) : C(X × ↑SignedInterval, ℝ)

The signed distance packaged as a bundled continuous map.

Equations

• S.signedDistanceMap = { toFun := S.signedDistance, continuous_toFun := ⋯ }

@[simp]

theorem NRR.TopBottomSeparator.signedDistanceMap_apply {X : Type u_1} [MetricSpace X] [Nonempty X] (S : TopBottomSeparator X) (z : X × ↑SignedInterval) : S.signedDistanceMap z = S.signedDistance z