Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help


slug: dedania-patel-2024-spatial-numerical-range-convexity bibkey: dedaniapatel2024spatial doi: null url: https://arxiv.org/abs/2306.16172v1 triage: theorem motivation_gids:

  • D5/S3/Analytic/NumericalRange/SpatialNumericalRangeNonconvex.result

Convexity of the spatial numerical range in non-unital normed algebras

Problem

H. V. Dedania and A. B. Patel, Spatial numerical range in non-unital, normed algebras and their unitizations, arXiv:2306.16172v1, Sarajevo Journal of Mathematics 20(2) (2024), §1, p. 2, write:

Let be the unit sphere in . Let be the Banach space dual of . Let for each . Further, let for and . Then is the spatial numerical range (SNR) … It is still open problem wether is always convex? This problem is discussed in [5].

The question is whether is convex as a subset of the real vector space underlying , for every element of every complex non-unital normed algebra.

Motivation

Convexity would allow norming functionals at different unit vectors to contribute a common convex range. Classical convexity of the algebra numerical range in unital normed algebras, as treated by Bonsall–Duncan, does not directly settle the spatial definition above without a unit. An explicit counterexample separates the universal assertion from the specific convexity results in the companion paper.

Gap

The authors state that the question is open. The abstract of their companion paper, On the convexity of the spatial numerical range in non-unital normed algebras, likewise says that they believe it is still open and that the answer seems to be negative, while establishing convexity in several specific non-unital Banach algebras. Their account presents no known non-convex example. This is the gap stated by the authors; whether older books or the general Banach-space-operator literature already contain a transferable counterexample remains ASSUMED-UNVERIFIED.

Route

On with its supremum norm, define

Give the product and norm

The Lean carrier Alg is ℂ × (Fin 2 → ℂ), with rescaled scalar coordinate and the ordinary product supremum norm. Its multiplication mulDef is

The lemma P_sq proves idempotence. The algebra instances use the associativity, distributivity, scalar compatibility and submultiplicative norm lemmas. The norm proof uses the sufficient bound ; it does not assert the exact operator norm of .

Let , represented by e = (3, 0) in Lean. The lemma e_mul gives . The unit vectors

and the coordinate functionals phi0 and phi1 are norming pairs. The lemma z_points proves

For a hypothetical norming pair producing their midpoint, write

Testing on the coefficient phases gives (coeff_sum_le_one). The norming equation and the coordinate bounds make the three diagonal products real (support_im_zero). Consequently

At height , equality forces , , diagonal products , , and cross products , . The identity

then gives . For the proposed midpoint, its real part additionally forces , a contradiction. This is the argument in midpoint_not_mem; nonconvex applies the convexity midpoint condition, and result refutes claim.

Falsifier

The displayed normed algebra and element falsify the universal convexity assertion. Both and belong to , whereas

The structure uses a non-unital normed ring with complex normed-space structure and both scalar compatibility instances. No completeness or commutativity premise is used in claim.

Evidence

The public declarations in D5/S3/Analytic/NumericalRange/SpatialNumericalRangeNonconvex.lean are spatialNumericalRange, claim, and result; the construction and supporting lemmas are private.

The definition spatialNumericalRange quantifies over a unit vector and a continuous complex-linear functional of norm one taking value one on that vector. The definition claim quantifies over A : Type with instances NonUnitalNormedRing A, NormedSpace ℂ A, IsScalarTower ℂ A A, and SMulCommClass ℂ A A, and over every a : A; its conclusion is Convex ℝ (spatialNumericalRange a).

The algebra instances establish the required normed-algebra structure. The private lemmas z_points, coeff_sum_le_one, support_im_zero, midpoint_not_mem, and nonconvex establish the membership and exclusion argument. The theorem D5.S3.Analytic.NumericalRange.SpatialNumericalRangeNonconvex.result has type ¬ claim.

The accepted axiom closure is , with no sorry or additional axiom. NonUnitalNormedRing does not itself assert that no identity exists; absence of a left identity is justified separately below. The module has no separate theorem classifying the entire spatial range or proving an abstract transfer principle.

Triage

What the settlement shows

  1. Proved (Lean) — the normed-algebra instance and refutation. The explicit algebra has the required non-unital normed-algebra structure, , and their midpoint is absent. Hence claim fails. The conclusion concerns spatial numerical ranges defined by norming pairs, not the classical Hilbert-space numerical range.

  2. Computed (exact hand calculation) — one-sided identity and projection norm. The product gives , so is a right identity. The nonzero vector satisfies ; every therefore satisfies , which excludes a left identity. Left multiplication by is , as also expressed by e_mul, and is proved by P_sq. The absolute row sums of are and , and , giving . The right-identity, no-left-identity and exact-norm assertions have no separate Lean theorem.

  3. Open — explanatory mechanism beyond the instance. In the classical normalized unital setting, evaluating an element on the convex set of states makes its algebra numerical range convex. The candidate explanation for failure here is that the spatial range of is a union over norming vectors of convex pieces that need not glue into a convex set. This is mathematical reasoning about the example; the comparison with states and a general criterion for gluing are not proved in the Lean module.

  4. Open — generalization and transfer. For a complex Banach space and a bounded linear idempotent , consider

    The hand derivation for gives associativity from and, with , ,

    A norming pair for extends to with and , yielding . Thus the proposed construction contains the spatial numerical range of in . These general statements are not formalized. The stronger proposed conclusion that every nonconvex spatial range of an idempotent transfers to a nonconvex algebra spatial range remains open: inclusion alone is insufficient, because other norming pairs can add points. A transfer theorem must also preserve an excluded point, as the explicit equality-case argument does here.

  5. Open — bounded approximate identities. Is convex for every element of a non-unital Banach algebra with a bounded approximate identity? The example and its Lean statement do not settle this question.

  6. Open — commutative algebras. Does convexity hold for every element of every commutative non-unital normed algebra? The universal refutation does not settle this restricted assertion.

  7. Open — unitization comparison. Does the closed convex hull of always equal the numerical range of in the unitization? This is only a question; no equality is asserted.

ASSUMED-UNVERIFIED

Whether Bonsall–Duncan, Numerical Ranges I/II, contain an element of a non-unital normed algebra with nonconvex spatial numerical range is unverified: the books have not been read for this question. The source authors cite them and still call the problem open. Their description does not replace a check of the books’ actual results and hypotheses.

The general Banach-space-operator literature on nonconvex spatial numerical ranges has not been read. Its relation to the idempotent construction and any earlier non-unital-algebra counterexample remains unverified. The exact hand calculations and proposed generalization in Triage are distinguished from the Lean results; no literature priority or general transfer theorem is claimed.