Scalar Transport

Approximation numbers under a scalar transport

TauCeti.ScalarTransport renames the scalar field of a Hilbert space without touching its vectors, its norm, or its topology. Everything an approximation number sees is therefore unchanged, and this file says so: ScalarTransport.approximationNumber_clm.

The payoff is ContinuousLinearMap.hasMinMaxLowerBoundEverywhere, the instance at an arbitrary RCLike field. That property was the one input to the approximation-number localization theory that depended on the scalar field, with instances at ℝ and at ℂ and nothing in between; RCLike has exactly those two models, so the case split closes it.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: none. Written directly here, 2026-09-01.
• Extraction class: new. It completes MinMaxReal: that module carries the min--max lower bound over ℝ by complexification, and this one carries it from ℝ and ℂ to every RCLike field, which is what makes ContinuousLinearMap.HasMinMaxLowerBoundEverywhere an instance rather than a hypothesis.
• Namespaces: TauCeti.ScalarTransport for the transport lemmas, and ContinuousLinearMap for the instance, which is a fact about a ContinuousLinearMap.
• Original authors / copyright: Jon Crall, Claude Opus 5; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none.

theorem TauCeti.ScalarTransport.approximationNumber_clm {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : (clm T).approximationNumber n = T.approximationNumber n

The transport does not change an approximation number: it is an infimum of operator norms over the maps of bounded rank, and the transport is a rank-preserving, norm-preserving bijection of those.

theorem TauCeti.ScalarTransport.linearIndependent_of_iff {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_1} (v : ι → E) : (LinearIndependent 𝕂 fun (i : ι) => of (v i)) ↔ LinearIndependent 𝕜 v

Linear independence is unchanged: the two scalar actions differ by e.

theorem TauCeti.ScalarTransport.span_of {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_1} (v : ι → E) : Submodule.span 𝕂 (Set.range fun (i : ι) => of (v i)) = submodule (Submodule.span 𝕜 (Set.range v))

Spans are unchanged: the transported span has the original carrier.

theorem ContinuousLinearMap.hasMinMaxLowerBound_of_transport {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : TauCeti.RCLikeIso 𝕜 𝕂) {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (h : HasMinMaxLowerBound 𝕂 (TauCeti.ScalarTransport e E) (TauCeti.ScalarTransport e F)) : HasMinMaxLowerBound 𝕜 E F

The min--max lower-bound property transports along an isomorphism of RCLike fields: it mentions only approximation numbers, norms, linear independence and spans, and the transport changes none of them.

theorem ContinuousLinearMap.hasMinMaxLowerBound_rclike (𝕜 : Type u) [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] : HasMinMaxLowerBound 𝕜 E F

The min--max lower-bound property holds at every RCLike field.

RCLike is an open class, but RCLike.I_eq_zero_or_im_I_eq_one says it has exactly two models. Transporting a 𝕜-Hilbert space to the corresponding ℝ- or ℂ-Hilbert space changes no vector, no norm, no approximation number, no linear independence and no span, so the two fixed-field instances give the general one.

This removes [HasMinMaxLowerBoundEverywhere 𝕜] from every downstream statement that carried it as a hypothesis.

instance ContinuousLinearMap.hasMinMaxLowerBoundEverywhere (𝕜 : Type u) [RCLike 𝕜] : HasMinMaxLowerBoundEverywhere 𝕜

The single-universe class form of hasMinMaxLowerBound_rclike, so that the statements carrying [HasMinMaxLowerBoundEverywhere 𝕜] resolve it by instance search rather than by hypothesis.

theorem ContinuousLinearMap.kyFanGauge_add_le {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (S T : E →L[𝕜] F) (k : ℕ) : (S + T).kyFanGauge k ≤ S.kyFanGauge k + T.kyFanGauge k

Ky Fan subadditivity on Hilbert spaces over any RCLike field.

The min--max localization is an internal theorem, not a public capability hypothesis.