NRR.Multivalued.Operations — constructors and transformations of nice multivalued functions

This module provides the reusable operations on nice multivalued functions used later in the prime-refinement argument:

• NiceMV.pullback along a continuous base map;
• NiceMV.ofObservable, the canonical nice multivalued function φ(x, y) = y - f x attached to a bounded continuous observable f with |f x| < 1;
• NiceMV.scale by a strictly positive real constant;
• NiceMV.reflect, the interval-reflection operation that reverses the sign convention through interval negation without changing the represented zero relation.

The signed-interval negation SignedInterval.neg is introduced first, together with its coercion and continuity lemmas. Each operation records its evaluation law and the corresponding zero-set/zero relation identity.

def NRR.SignedInterval.neg (t : ↑SignedInterval) : ↑SignedInterval

Negation on the signed interval: reflection t ↦ -t through the center 0.

Equations

• NRR.SignedInterval.neg t = ⟨-↑t, ⋯⟩

@[simp]

theorem NRR.SignedInterval.coe_neg (t : ↑SignedInterval) : ↑(neg t) = -↑t

theorem NRR.SignedInterval.continuous_neg : Continuous neg

@[simp]

theorem NRR.SignedInterval.neg_left : neg left = right

@[simp]

theorem NRR.SignedInterval.neg_right : neg right = left

def NRR.NiceMV.pullback {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (φ : NiceMV X) (f : C(Y, X)) : NiceMV Y

Pull back a nice multivalued function φ on X along a continuous map f : Y → X, giving a nice multivalued function on Y evaluated by (φ.pullback f).eval y t = φ.eval (f y) t.

Equations

• φ.pullback f = NRR.NiceMV.ofFunction (fun (y : Y) (t : ↑NRR.SignedInterval) => φ.eval (f y) t) ⋯ ⋯ ⋯

theorem NRR.NiceMV.pullback_eval {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (φ : NiceMV X) (f : C(Y, X)) (y : Y) (t : ↑SignedInterval) : (φ.pullback f).eval y t = φ.eval (f y) t

theorem NRR.NiceMV.pullback_zeroSet {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (φ : NiceMV X) (f : C(Y, X)) : (φ.pullback f).zeroSet = (fun (z : Y × ↑SignedInterval) => (f z.1, z.2)) ⁻¹' φ.zeroSet

def NRR.NiceMV.ofObservable {X : Type u_1} [TopologicalSpace X] (f : C(X, ℝ)) (hbound : ∀ (x : X), |f x| < 1) : NiceMV X

The canonical nice multivalued function attached to a bounded continuous observable f with |f x| < 1: it evaluates by (t : ℝ) - f x, so its zero set is the graph t = f x.

Equations

• NRR.NiceMV.ofObservable f hbound = NRR.NiceMV.ofFunction (fun (x : X) (t : ↑NRR.SignedInterval) => ↑t - f x) ⋯ ⋯ ⋯

theorem NRR.NiceMV.ofObservable_eval {X : Type u_1} [TopologicalSpace X] (f : C(X, ℝ)) (hbound : ∀ (x : X), |f x| < 1) (x : X) (t : ↑SignedInterval) : (ofObservable f hbound).eval x t = ↑t - f x

theorem NRR.NiceMV.ofObservable_zero_iff {X : Type u_1} [TopologicalSpace X] (f : C(X, ℝ)) (hbound : ∀ (x : X), |f x| < 1) (x : X) (t : ↑SignedInterval) : (ofObservable f hbound).Zero x t ↔ ↑t = f x

def NRR.NiceMV.scale {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (c : ℝ) (hc : 0 < c) : NiceMV X

Rescale a nice multivalued function by a strictly positive constant c; scaling preserves the strict endpoint signs, hence yields a nice multivalued function evaluated by c * φ.eval x t.

Equations

• φ.scale c hc = NRR.NiceMV.ofFunction (fun (x : X) (t : ↑NRR.SignedInterval) => c * φ.eval x t) ⋯ ⋯ ⋯

theorem NRR.NiceMV.scale_eval {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (c : ℝ) (hc : 0 < c) (x : X) (t : ↑SignedInterval) : (φ.scale c hc).eval x t = c * φ.eval x t

theorem NRR.NiceMV.scale_zeroSet {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (c : ℝ) (hc : 0 < c) : (φ.scale c hc).zeroSet = φ.zeroSet

def NRR.NiceMV.reflect {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) : NiceMV X

Reflect a nice multivalued function through interval negation: reflect negates both the observable and the interval coordinate. It preserves the zero relation under SignedInterval.neg, so it reverses the sign convention without changing the represented zero relation.

Equations

• φ.reflect = NRR.NiceMV.ofFunction (fun (x : X) (t : ↑NRR.SignedInterval) => -φ.eval x (NRR.SignedInterval.neg t)) ⋯ ⋯ ⋯

theorem NRR.NiceMV.reflect_eval {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) (t : ↑SignedInterval) : φ.reflect.eval x t = -φ.eval x (SignedInterval.neg t)

theorem NRR.NiceMV.reflect_zero_iff {X : Type u_1} [TopologicalSpace X] (φ : NiceMV X) (x : X) (t : ↑SignedInterval) : φ.reflect.Zero x t ↔ φ.Zero x (SignedInterval.neg t)