pith. machine review for the scientific record. sign in

arxiv: 2605.10173 · v1 · submitted 2026-05-11 · 💻 cs.LO · math.FA· math.GN

Recognition: 1 theorem link

· Lean Theorem

Just Previsions

Jean Goubault-Larrecq
Authors on Pith no claims yet

Pith reviewed 2026-05-12 03:50 UTC · model grok-4.3

classification 💻 cs.LO math.FAmath.GN
keywords previsionsublinear previsionsuperlinear previsionhyperspacehomeomorphismorthogonality relationpowerspace constructionpositively homogeneous functional
0
0 comments X

The pith

Every prevision equals the infimum of sublinear previsions and, under mild conditions, the supremum of superlinear previsions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Previsions are positively homogeneous functionals that generalize integration functionals. The paper shows that any such prevision equals the infimum of all sublinear previsions lying above it. Under mild conditions the same prevision also equals the supremum of all superlinear previsions lying below it. These two representations induce homeomorphisms between the space of previsions and certain hyperspaces built from sublinear or superlinear previsions. The hyperspaces themselves admit equivalent descriptions in terms of orthogonality relations, so the entire construction appears as a variant of a double powerspace.

Core claim

The paper claims that every prevision can be expressed as an infimum of sublinear previsions, and as a supremum of superlinear previsions under mild conditions. This extends to homeomorphisms between spaces of previsions and certain hyperspaces over spaces of sublinear or superlinear previsions, which can also be characterized in terms of orthogonality relations, making the construction a variant of a double powerspace construction.

What carries the argument

Representation of each prevision as the infimum of sublinear previsions (and supremum of superlinear previsions) together with the induced homeomorphisms to hyperspaces and the orthogonality characterizations of those hyperspaces.

Load-bearing premise

The mild conditions under which every prevision is the supremum of superlinear previsions and under which the homeomorphisms and orthogonality characterizations are valid.

What would settle it

An explicit prevision on a concrete space that cannot be recovered as the infimum of any family of sublinear previsions above it would falsify the central representation claim.

read the original abstract

Previsions are positively homogeneous functionals, and are generalized forms of integration functionals. We investigate previsions -- just previsions, not sublinear or superlinear previsions as in previous work. We show that every prevision can be expressed as an infimum of sublinear previsions, and as a supremum of superlinear previsions under mild conditions. This extends to homeomorphisms between spaces of previsions and certain hyperspaces over spaces of sublinear or superlinear previsions, which can also be characterized in terms of orthogonality relations, making the construction a variant of a double powerspace construction.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper studies previsions, defined as positively homogeneous functionals that generalize integration. It proves that every prevision equals the infimum of sublinear previsions (unconditionally) and the supremum of superlinear previsions under mild conditions. These representations induce homeomorphisms between the space of previsions and suitable hyperspaces of sublinear or superlinear previsions; the hyperspaces are further characterized via orthogonality relations, yielding a variant of a double powerspace construction.

Significance. If the derivations hold, the unconditional infimum representation and the conditional supremum representation supply a clean decomposition of previsions into extremal classes already studied in the literature. The induced homeomorphisms and orthogonality characterizations link the space of previsions to hyperspace constructions in a manner that may be useful for domain-theoretic or order-theoretic treatments of imprecise probabilities and integration functionals. The work therefore extends prior results on sublinear and superlinear previsions by removing the extremality assumption while preserving topological identifications.

minor comments (3)
  1. The abstract and introduction refer to 'mild conditions' for the supremum representation and the homeomorphisms without stating them explicitly at the outset. A single sentence or short paragraph early in the paper (e.g., after the definition of previsions) that lists the precise topological or order-theoretic hypotheses would allow readers to assess immediately whether the results apply to the examples they have in mind.
  2. The orthogonality relation used to characterize the hyperspaces is introduced without a self-contained definition or a reference to its prior appearance in the literature on previsions. Adding a brief recall of the relation (including its notation) before the homeomorphism statements would improve readability.
  3. The manuscript does not indicate whether the homeomorphisms are with respect to the same topology on the space of previsions or whether different topologies are used on the hyperspaces; a short remark clarifying the topologies involved would remove ambiguity.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary and assessment of the paper, which accurately reflects the main results on representations of previsions and the induced homeomorphisms. We appreciate the recommendation for minor revision.

Circularity Check

0 steps flagged

No circularity: claims rest on independent topological and order-theoretic constructions

full rationale

The paper derives that every prevision equals an infimum of sublinear previsions (unconditionally) and a supremum of superlinear previsions (under mild conditions), yielding homeomorphisms to hyperspaces via orthogonality relations. These are presented as theorems proved from the definitions of previsions as positively homogeneous functionals, using standard properties of infima, suprema, and hyperspaces. No step reduces a claimed result to a fitted parameter, a self-definition, or a load-bearing self-citation whose content is merely renamed; prior work on sub/superlinear previsions is referenced only to distinguish the new focus on plain previsions. The derivation chain is therefore self-contained against external mathematical benchmarks and does not collapse to its inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Based solely on the abstract, the paper relies on standard background assumptions from functional analysis and topology with no free parameters or invented entities introduced.

axioms (2)
  • domain assumption Previsions are defined as positively homogeneous functionals
    Stated directly in the abstract as the object of study.
  • domain assumption The underlying spaces admit hyperspaces and homeomorphisms
    Required for the claimed topological results.

pith-pipeline@v0.9.0 · 5384 in / 1437 out tokens · 70547 ms · 2026-05-12T03:50:08.965311+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

22 extracted references · 22 canonical work pages

  1. [1]

    Adamski.τ-smooth Borel measures on topological spaces.Mathema- tische Nachrichten, 78:97–107, 1977

    W. Adamski.τ-smooth Borel measures on topological spaces.Mathema- tische Nachrichten, 78:97–107, 1977

    work page 1977

  2. [2]

    Birkhoff.Lattice Theory

    G. Birkhoff.Lattice Theory. American Mathematical Society, 1940. Second edition, 1948. Third edition, 1967

    work page 1940

  3. [3]

    de Brecht, J

    M. de Brecht, J. Goubault-Larrecq, X. Jia, and Z. Lyu. Domain-complete and LCS-complete spaces.Electronic Notes in Theoretical Computer Sci- ence, 345:3–35, 2019. Proc. 8th International Symposium on Domain The- ory (ISDT’19)

    work page 2019

  4. [4]

    de Brecht and T

    M. de Brecht and T. Kawai. On the commutativity of the powerspace constructions.Logical Methods in Computer Science, 15(3), 2019

    work page 2019

  5. [5]

    K. E. Flannery and J. J. Martin. The Hoare and Smyth power domain constructorscommuteundercomposition.Journal of Computer and System Sciences, 40:125–135, 1990

    work page 1990

  6. [6]

    Goubault-Larrecq

    J. Goubault-Larrecq. Continuous previsions. In J. Duparc and Th. A. Henzinger, editors,Proceedings of the 16th Annual EACSL Conference on Computer Science Logic (CSL’07), volume 4646 ofLecture Notes in Com- puter Science, pages 542–557, Lausanne, Switzerland, Sept. 2007. Springer

    work page 2007

  7. [7]

    Goubault-Larrecq.Non-Hausdorff Topology and Domain Theory— Selected Topics in Point-Set Topology, volume 22 ofNew Mathematical Monographs

    J. Goubault-Larrecq.Non-Hausdorff Topology and Domain Theory— Selected Topics in Point-Set Topology, volume 22 ofNew Mathematical Monographs. Cambridge University Press, 2013

    work page 2013

  8. [8]

    Goubault-Larrecq

    J. Goubault-Larrecq. Isomorphism theorems between models of mixed choice.Mathematical Structures in Computer Science, 27(6):1032–1067, Sept. 2017. Revised version on arXiv:2411.13500 [cs.LO]. 32

    work page arXiv 2017

  9. [9]

    isomorphism theorems between models of mixed choice,

    J. Goubault-Larrecq. Errata to “isomorphism theorems between models of mixed choice,” fixes and consequences.Mathematical Structures in Com- puter Science, 35:e23, 2025

    work page 2025

  10. [10]

    Goubault-Larrecq and X

    J. Goubault-Larrecq and X. Jia. Algebras of the extended probabilistic powerdomain monad.Electronic Notes in Theoretical Computer Science, 345:37–61, 2019. Proc. 8th International Symposium on Domain Theory (ISDT’19)

    work page 2019

  11. [11]

    Goubault-Larrecq and K

    J. Goubault-Larrecq and K. Keimel. Choquet-Kendall-Matheron theorems for non-Hausdorff spaces.Mathematical Structures in Computer Science, 21(3):511–561, June 2011

    work page 2011

  12. [12]

    Heckmann

    R. Heckmann. Lower and upper power domain constructions commute on all dcpos.Information Processing Letters, 40:7–11, 1991

    work page 1991

  13. [13]

    Jones.Probabilistic Non-Determinism

    C. Jones.Probabilistic Non-Determinism. PhD thesis, University of Edin- burgh, 1990. Technical Report ECS-LFCS-90-105

    work page 1990

  14. [14]

    Jones and G

    C. Jones and G. Plotkin. A probabilistic powerdomain of evaluations. In Proceedings of the 4th Annual Symposium on Logic in Computer Science, pages 186–195. IEEE Computer Society Press, 1989

    work page 1989

  15. [15]

    A. Jung. Stably compact spaces and the probabilistic powerspace con- struction. In J. Desharnais and P. Panangaden, editors,Domain-theoretic Methods in Probabilistic Processes, volume 87 ofElectronic Lecture Notes in Computer Science, pages 5–20, Amsterdam, The Netherlands, The Nether- lands, 2004. Elsevier Science Publishers B. V. 15pp

    work page 2004

  16. [16]

    K. Keimel. Topological cones: Functional analysis in aT0-setting.Semi- group Forum, 77(1):109–142, 2008

    work page 2008

  17. [17]

    J. D. Lawson. Valuations on continuous lattices. In R.-E. Hoffmann, edi- tor,Mathematische Arbeitspapiere, volume 27, pages 204–225, Universität Bremen, 1982

    work page 1982

  18. [18]

    Saheb-Djahromi

    N. Saheb-Djahromi. Cpo’s of measures for nondeterminism.Theoretical Computer Science, 12:19–37, 1980

    work page 1980

  19. [19]

    R. Tix. Stetige Bewertungen auf topologischen Räumen. Diplomarbeit, Technische Hochschule Darmstadt, 1995

    work page 1995

  20. [20]

    R. Tix, K. Keimel, and G. Plotkin. Semantic domains for combining prob- ability and non-determinism.Electronic Notes in Theoretical Computer Science, 222:3–99, 2009. Originally published in 2005

    work page 2009

  21. [21]

    Auniversalcharacterizationofthedouble powerlocale.Theoretical Computer Science, 316(1-3):297–321, 2004

    S.J.VickersandC.F.Townsend. Auniversalcharacterizationofthedouble powerlocale.Theoretical Computer Science, 316(1-3):297–321, 2004

    work page 2004

  22. [22]

    Walley.Statistical Reasoning with Imprecise Probabilities

    P. Walley.Statistical Reasoning with Imprecise Probabilities. Chapman and Hall, London, 1991. 33

    work page 1991