NRR.Multivalued.ZeroSet — zero sets, fibers, and existence of zeros

The graph of a nice multivalued function is the zero set of its scalar observable. This module defines the zero predicate, the total zero set on X × SignedInterval, and the vertical zero fiber over a base point. It records that these sets are closed, that fibers are compact and nonempty, and that the total zero set is compact when X is compact.

Existence of a zero in every vertical fiber follows from the intermediate value theorem: the observable is strictly negative at the left endpoint and strictly positive at the right endpoint, and the signed interval is connected, so the continuous image contains 0. No zero selector is introduced; only existence is proved. Zeros never occur at either endpoint, by the strict signs.

def NRR.NiceMV.Zero {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) (y : ↑SignedInterval) : Prop

A point (x, y) is a zero of φ when the observable vanishes there.

Equations

• φ.Zero x y = (φ.eval x y = 0)

def NRR.NiceMV.zeroSet {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) : Set (X × ↑SignedInterval)

The total zero set (graph) of φ inside X × SignedInterval.

Equations

• φ.zeroSet = {z : X × ↑NRR.SignedInterval | φ.Zero z.1 z.2}

def NRR.NiceMV.zeroFiber {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) : Set ↑SignedInterval

The vertical zero fiber of φ over a base point x.

Equations

• φ.zeroFiber x = {y : ↑NRR.SignedInterval | φ.Zero x y}

@[simp]

theorem NRR.NiceMV.zero_iff {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) (y : ↑SignedInterval) : φ.Zero x y ↔ φ.eval x y = 0

theorem NRR.NiceMV.continuous_eval_fiber {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) : Continuous fun (y : ↑SignedInterval) => φ.eval x y

Continuity of the observable along a single vertical fiber.

theorem NRR.NiceMV.isClosed_zeroSet {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) : IsClosed φ.zeroSet

theorem NRR.NiceMV.isClosed_zeroFiber {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) : IsClosed (φ.zeroFiber x)

theorem NRR.NiceMV.isCompact_zeroFiber {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) : IsCompact (φ.zeroFiber x)

theorem NRR.NiceMV.exists_zero {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) : ∃ (y : ↑SignedInterval), φ.Zero x y

theorem NRR.NiceMV.zeroFiber_nonempty {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) : (φ.zeroFiber x).Nonempty

theorem NRR.NiceMV.isCompact_zeroSet {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (φ : NiceMV X) : IsCompact φ.zeroSet

theorem NRR.NiceMV.not_zero_left {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) : ¬φ.Zero x SignedInterval.left

theorem NRR.NiceMV.not_zero_right {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) : ¬φ.Zero x SignedInterval.right