A characterisation of ordered abstract probabilities
This is a modal window.
Das Video konnte nicht geladen werden, da entweder ein Server- oder Netzwerkfehler auftrat oder das Format nicht unterstützt wird.
Formale Metadaten
Titel |
| |
Untertitel |
| |
Serientitel | ||
Anzahl der Teile | 56 | |
Autor | ||
Mitwirkende | ||
Lizenz | CC-Namensnennung 3.0 Deutschland: Sie dürfen das Werk bzw. den Inhalt zu jedem legalen Zweck nutzen, verändern und in unveränderter oder veränderter Form vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen. | |
Identifikatoren | 10.5446/49289 (DOI) | |
Herausgeber | ||
Erscheinungsjahr | ||
Sprache |
Inhaltliche Metadaten
Fachgebiet | |
Genre |
6
13
45
00:00
InformationsmanagementEinfacher RingGefangenendilemmaPrimzahlzwillingeFamilie <Mathematik>ComputerarchitekturXMLUMLComputeranimation
00:27
Reelle ZahlSoundverarbeitungSpeicherabzugAbstraktionsebeneSchnittmengePhysikalische TheorieMonoidAxiomRechenwerkPhysikerCartier-DivisorSchaltalgebraParametersystemQuick-SortPhysikalismusGruppenoperationZweiDivergente ReiheComputeranimation
01:11
AxiomBeweistheorieKontextbezogenes SystemComputerPhysikalische TheorieQuantisierung <Physik>ProgrammTypentheorieAbelsche KategorieKontextbezogenes SystemPhysikalische TheorieGruppenoperationInformatikQuantisierung <Physik>AxiomMailing-ListeTypentheorieKategorie <Mathematik>PunktInformationProgrammierungFormale SemantikNeuroinformatikTheoremKonstruktor <Informatik>InstantiierungGarbentheorieOpen SourceXMLComputeranimation
02:38
AxiomRechenwerkQuantisierung <Physik>AxiomDifferenteEindeutigkeitPhysikalische TheoriePerspektiveInformationGruppenoperationFolge <Mathematik>EreignishorizontInstantiierungComputeranimation
03:17
AxiomRechenwerkAxiomatikSkalarfeldFolge <Mathematik>BereichstheorieVollständigkeitFolge <Mathematik>BereichstheorieSupremum <Mathematik>ZahlenbereichAxiomUnendlichkeitProgrammierungKartesische KoordinatenNeuroinformatikPhysikalische TheorieZweiInstantiierungRelationentheorieComputeranimation
03:44
Folge <Mathematik>Statistische HypothesePhysikalische TheorieSoundverarbeitungAlgebraisches ModellPhysikerWort <Informatik>Kartesische KoordinatenFolge <Mathematik>Reelle ZahlStatistische HypotheseQuantisierung <Physik>RechenwerkPhysikalische TheorieZweiSoundverarbeitungDatenstrukturGruppenoperationMathematische PhysikDienst <Informatik>Mobiles InternetBeobachtungsstudieMathematikBus <Informatik>Computeranimation
04:21
AxiomBeweistheorieKontextbezogenes SystemDatenstrukturAdditionTotal <Mathematik>MultiplikationRechenwerkAbstraktionsebeneSchnittmengeSummierbarkeitElement <Gruppentheorie>MultiplikationAdditionReelle ZahlNichtlinearer OperatorPartielle DifferentiationAmenable GruppeXMLComputeranimation
05:15
AdditionEreignishorizontMultiplikationStochastische AbhängigkeitAxiomOrdnung <Mathematik>AdditionEreignishorizontStochastische AbhängigkeitMultiplikationEinsAssoziativgesetzGruppenoperationOrdnung <Mathematik>VisualisierungSelbst organisierendes SystemProgrammierungEindeutigkeitRichtungBus <Informatik>Computeranimation
06:04
AxiomEindeutigkeitQuantenmechanikEreignishorizontZahlensystemGruppenoperationComputeranimation
06:35
AxiomAlgebraisches ModellÄquivalenzklasseGruppenoperationEreignishorizontSoundverarbeitungMathematische PhysikDatenstrukturSoftwaretestMultiplikationsoperatorAlgebraisches ModellComputeranimation
06:56
AxiomEreignishorizontStochastische AbhängigkeitMultiplikationsoperatorURLEreignishorizontFunktorSoundverarbeitungStochastische AbhängigkeitMultiplikationMonoidAlgebraische StrukturAlgebraisches ModellBitEinfacher RingKategorie <Mathematik>GruppenoperationBeschränktheit <Mathematik>Partielle DifferentiationPhysikalischer EffektSchnittmengeMomentenproblemComputeranimation
08:04
AxiomSchreiben <Datenverarbeitung>ÄquivalenzklasseFolge <Mathematik>Ordnung <Mathematik>SummierbarkeitFolge <Mathematik>VollständigkeitDatenstrukturElement <Gruppentheorie>MonoidGruppenoperationSoundverarbeitungExistenzaussageGüte der AnpassungComputeranimation
08:43
Formation <Mathematik>Algebraisches ModellZahlenbereichPunktElement <Gruppentheorie>CASE <Informatik>Minkowski-MetrikAnalytische FortsetzungDifferenteFunktionalAlgebraisches ModellTouchscreenMomentenproblemMonoidMultiplikationBoolesche AlgebraSigma-AlgebraSoundverarbeitungSupremum <Mathematik>AdditionComputeranimation
09:11
Funktion <Mathematik>Stetige FunktionHausdorff-RaumMinkowski-MetrikMultiplikationSystemaufrufProdukt <Mathematik>MonoidSchnittmengeAlgebraisches ModellTheoremSummierbarkeitNichtlinearer OperatorStetige FunktionFunktionalKompakter RaumMultiplikationBoolesche AlgebraMinkowski-MetrikAlgebraisch abgeschlossener KörperAdditionAnalytische FortsetzungRechenwerkProzess <Informatik>EntscheidungstheorieComputeranimation
10:20
TheoremAlgebraisches ModellMinkowski-MetrikHausdorff-RaumMinkowski-MetrikMonoidKartesisches ProduktBoolesche AlgebraSoundverarbeitungBildschirmmaskeStetige FunktionKompakter RaumStützpunkt <Mathematik>FunktionalProdukt <Mathematik>AssoziativgesetzNeuroinformatikExistenzsatzComputeranimation
10:44
TheoremAlgebraisches ModellMinkowski-MetrikHausdorff-RaumDualitätstheoriePunktMinkowski-MetrikReelle ZahlTheoremMonoidTeilmengeRechenwerkAxiomBoolesche AlgebraKompakter RaumSoundverarbeitungFunktionalSchaltalgebraStetige FunktionTopologischer RaumGruppenoperationMomentenproblemComputeranimation
11:44
AxiomTheoremProdukt <Mathematik>GruppenoperationPunktSchnittmengeStochastische AbhängigkeitMonoidSoundverarbeitungFaserbündelRechenwerkBoolesche AlgebraAxiomStörungstheorieAusnahmebehandlungComputeranimation
12:14
TheoremAxiomBeweistheorieRechenwerkSchaltalgebraMailing-ListeGruppenoperationÜberlagerung <Mathematik>Computeranimation
12:31
AxiomBeweistheorieKontextbezogenes SystemBoolesche AlgebraLemma <Logik>PunktgitterDivisionTheoremGruppenoperationKonvexe MengeAlgebraisches ModellVektorraumMinkowski-MetrikRechenwerkMereologieBeweistheorieMailing-ListeAlgebraisches ModellSoundverarbeitungResultanteVektorraumGruppenoperationReelle ZahlRechenwerkRoutingSoftwaretestOrdnung <Mathematik>ZweiQuick-SortXMLComputeranimation
13:20
VektorraumRechenwerkMinkowski-MetrikTheoremPunktgitterNormierter RaumStetige FunktionMonoidMereologieMinkowski-MetrikSoundverarbeitungPunktgitterKompakter RaumGruppenoperationAlgebraisches ModellOrdnung <Mathematik>Quick-SortMomentenproblemVollständiger VerbandComputeranimation
14:07
PunktgitterApproximationInternetworkingApproximationProdukt <Mathematik>TermMultiplikationsoperatorPunktgitterComputeranimation
14:53
PunktgitterElement <Gruppentheorie>VierzigKomplex <Algebra>RechenwerkWhiteboardMereologieKonvexe MengeSoundverarbeitungIdempotentMonoidComputeranimation
15:19
Element <Gruppentheorie>IdempotentBoolesche AlgebraAlgebraisches ModellIdempotentCASE <Informatik>Boolesche AlgebraQuadratzahlSchnittmengeElement <Gruppentheorie>Analytische FortsetzungStetige FunktionBestimmtheitsmaßMinimumFamilie <Mathematik>FunktionalOffice-PaketComputeranimation
15:46
IdempotentBoolesche AlgebraAlgebraisches ModellSoundverarbeitungMereologieMonoidBoolesche AlgebraElement <Gruppentheorie>MultiplikationsoperatorBildschirmmaskeDifferenteComputeranimation
16:21
Rationale ZahlRechenwerkElektronisches ForumGruppenoperationSpeicherabzugTermMultiplikationMultiplikationsoperatorWasserdampftafelElement <Gruppentheorie>IdempotentComputeranimation
16:59
MaßerweiterungKonvexe MengeGruppenoperationMultiplikationAlgebraisches ModellAnalytische FortsetzungMultiplikationReelle ZahlRechenwerkGruppenoperationRationale ZahlSoundverarbeitungMinkowski-MetrikDatenstrukturFunktionalAdressraumARM <Computerarchitektur>MinimumPhysikalisches SystemURLGrenzschichtablösungEinfügungsdämpfungQuellcodeComputeranimation
17:31
ParametersystemIsomorphieklasseMultiplikationIdempotentIsomorphieklasseSoundverarbeitungStetige FunktionMonoidFunktionalComputeranimation
17:49
ParametersystemIsomorphieklasseIdempotentMultiplikationOrthogonalitätBoolesche AlgebraLemma <Logik>Boolesche AlgebraStetige FunktionProdukt <Mathematik>KonditionszahlMaßerweiterungZeitzoneWeb SiteMinimumSchnittmengeIdempotentOrthogonalitätLokales MinimumComputeranimation
18:36
Kompakter RaumHausdorff-RaumMinkowski-MetrikOrthogonalitätBoolesche AlgebraEinbettung <Mathematik>Algebraisches ModellLemma <Logik>SoundverarbeitungProdukt <Mathematik>IdempotentMultiplikationSchnittmengeMonoidElement <Gruppentheorie>OrthogonalitätBoolesche AlgebraAlgebraisches ModellOrtsoperatorMultiplikationsoperatorFolge <Mathematik>Stetige FunktionAnalytische FortsetzungTheoremStreaming <Kommunikationstechnik>Office-PaketARM <Computerarchitektur>FunktionalMereologieOrdnung <Mathematik>Spezielle unitäre GruppeComputeranimation
19:42
MultiplikationStetige FunktionDivisionIsomorphieklasseIdempotentMultiplikationSupremum <Mathematik>InverseIdempotentOrdnung <Mathematik>VollständigkeitDivisionAusdruck <Logik>MultiplikationsoperatorFreier LadungsträgerIsomorphieklasseElement <Gruppentheorie>Entropie <Informationstheorie>Güte der AnpassungBildverstehenComputeranimation
20:26
DivisionElementargeometrieArithmetische FolgeSoundverarbeitungAnalytische FortsetzungElement <Gruppentheorie>Rechter WinkelPunktReelle ZahlSummierbarkeitElektronische PublikationRechenwerkDifferenteNatürliche ZahlMomentenproblemStetige FunktionQuick-SortAbstandComputeranimation
21:06
TeilbarkeitSoundverarbeitungElement <Gruppentheorie>Kontextbezogenes SystemSoundverarbeitungVollständigkeitEindeutigkeitElement <Gruppentheorie>MultiplikationsoperatorFunktionalProzess <Informatik>QuellcodeComputeranimation
21:41
SoundverarbeitungTeilbarkeitDivisorDivisionMonoidVollständigkeitSoundverarbeitungGruppenoperationBayes-EntscheidungstheorieAnalytische FortsetzungComputeranimation
22:12
SoundverarbeitungTeilbarkeitDivisorComputeranimation
Transkript: Englisch(automatisch erzeugt)
00:13
Good afternoon. My name is Bas Asteban, and I would like to present today our characterization of absurd probabilities.
00:22
This is joint work with my twin brother, Ron Mesteban and Jonathan Laitring. So what is this all about? The core question is why is the set of probabilities always the real unit interval? Even when physicists have their crazy toy theories of physics, it's always the real unit interval.
00:44
We tried to find something else, something different, but we couldn't, and we might have figured out why. We'd like to present the argument. If we have an abstract set of probabilities that obey some reasonable axioms, then it must be either the two-element Boolean algebra or the real unit interval.
01:05
For those impatient, the axioms are non-trivial omega-complete effect monoid without zero divisors. Before I explain these axioms, I want to give some context. How did we get to this? We were trying to find a computer scientist's reconstruction of quantum theory.
01:24
What is that? A reconstruction of quantum theory is a list of axioms that a physical theory could obey, that if it does, then it must be quantum theory to begin with. The point is that these axioms of the reconstruction are quite different from the usual axioms of quantum theory, so we learned something about it.
01:46
Examples are axioms about how information is preserved, for instance, in one of the reconstructions. We were trying to find a reconstruction from a computer scientist's perspective, where we're looking at what are the behaviour of quantum types and the semantics of quantum programs to reconstruct quantum theory.
02:06
So, we were looking for axioms to axiomatize the category of quantum types and programs. While doing that, we were naturally led to axioms on the probabilities in the category.
02:21
These axioms on the probabilities are the axioms we're discussing today. And I wanted to explain this, because it's not that these axioms were chosen to make the theorem work. These axioms were, so to say, forced upon us. Okay, about these reconstructions, there's not just one reconstruction.
02:42
There are many different reconstructions of quantum theory, and they vary wildly in their axioms, the way they talk about, and they give different perspectives about quantum theory itself. We wouldn't say that one of the reconstructions is the correct one, or the simplest one.
03:01
All these reconstructions usually have one axiom that's not that obvious, and which carries the brunt of the work. For instance, essential uniqueness of purification with none of them. Similarly, our reconstruction also has one axiom that carries the brunt of the work. This axiom is sequential completeness.
03:21
If we have an ascending sequence of probabilities, we assume that there is a supremum. This is not at all obvious, but it is very useful. For instance, when you do domain theory. If you have a probabilistic program, and you have a while loop, and you want to compute a probability that it terminates, it is nice to be able to sum those infinite number of probabilities together.
03:45
Because of this, we thought about using the title, a characterization of sequentially complete ordered abstract probabilities, but that's a lot of words. Now I want to talk about applications. The primary application is a reconstruction of quantum theory, which does not
04:01
presuppose the real unit interval as probabilities, which will appear in John's thesis. A second application is an advanced and effective theory. A third application is in the theory of sequential effect algebras, which are structures studied by mathematical physicists for already 20 years.
04:21
Given the context, I want to move on to the actions. But what are we axiomatizing? We are axiomatizing a set of abstract probabilities with two distinguished elements, a 0 and a 1. And two operations, a partial addition and a total multiplication. The partial addition is written with a v to make you think of a disjunction.
04:45
I want to stress that the addition is partial, so the sum of two probabilities does not always exist. But the multiplication is always total, so it always exists. What is the interpretation? In the real unit interval, the addition is the regular addition, but it is only defined when the sum is actually below 1.
05:07
The multiplication is the usual one, and if you multiply two elements in the real unit interval, then it stays in the real unit interval. So how do we interpret these two operations?
05:20
Addition is used to add probabilities of mutually exclusive events. Multiplication gives the probability of the intersection of independent events. So, we can express our first two actions. For each of the actions, I'll first give an informal reason why it's reasonable.
05:41
So first, the order of adding probabilities of disjoint events shouldn't matter. So, if a plus b is defined, then so should b plus ab, and they should be equal. Similarly, if we have three events, then the order in which we add them should not matter, so we have a partial associativity.
06:04
The third action is that every probability should have a unique complementary probability. If we have an event, then there's also the complementary event that doesn't happen, and its probability should add up to 1 with the original probability. So, for every a, there's a unique a-perp, with a plus a-perp is 1.
06:23
I hope you excuse the idiosyncratic notation here. It comes from our contact with quantum mechanics. I hope it's not too distracting. The fourth action is that only 0 is subable to 1. So, if a plus 1 is defined, then a should have been 0.
06:46
The first four actions are equivalent to the fact that M is in effect algebra, which is a structure studied by mathematical physicists. The fifth action is that intersecting with a probability 1 event does not change the
07:01
overall probability, and that entails that a times 1 is 1 times a is a. The next action is that the intersection of independent events should distribute over the union of disjoint events. And from this it follows that multiplication should distribute over addition.
07:23
These first six actions are to say that M is in effect monoid. Perhaps effect ring would have been a more appropriate name, as you have a multiplication and an addition. But it's called an effect monoid because it's a monoid in the category of effect algebras.
07:40
About these effect algebras, by the way, they might seem a bit unnatural to some because of the partiality. They're not nice algebraic structures in a sense. But I'd like to mention that there are, in fact, L and Br more algebras for the left adjoint to the forgetful functor of the modular posets to bounded posets.
08:06
Now, our next action is the sequential completeness. But first I have to say what is the order. We say that a is less than b if a sums to b with some element c. And so we can state our sequential completeness, every ascending sequence should have a supremum.
08:28
These seven actions are to say that M is an omega-complete effect monoid. These are not yet all our actions. But I would like to give already a few examples of all the structures that obey these actions.
08:43
If I have an omega-complete Boolean algebra, then this is an omega-complete effect monoid. Namely, as multiplication with the infimum. Addition is defined if two elements are disjoint, i.e. if their infimum is zero. And in that case, their addition is given by the supremum.
09:05
In particular, any sigma algebra is also an omega-effect monoid. Another example is that of an algebra of continuous functions. If I have a basically disconnected compact Hausdorff space X, then the set
09:21
of continuous functions from X to the unit interval is an omega-effect monoid. Where the multiplication is point-wise, the zero is the constant zero function, the one is the constant one function. Addition is point-wise and is defined if point-wise sums up to something less than one.
09:41
So what is basically disconnected? In general, the continuous functions on a compact Hausdorff space are not omega-completes. Basically, disconnected is equivalent to the fact that the continuous functions on the space are omega-completes. For who wants to know, it is that the closure of a call zero set is open again.
10:01
Another example includes a Cartesian product. If I take such a Boolean algebra and such an algebra of continuous function, then I can look at the pairs. I take the Cartesian product and do the operation point-wise. But this is all. There are no other examples. And that is the main theorem of our paper.
10:21
For any omega-complete effect monoid M, there exists an omega-complete Boolean algebra B and a basically disconnected compact Hausdorff space X, such that M embeds injectively into the continuous functions on X Cartesian product with the Boolean algebra. So all omega-effect monoids are of this form.
10:45
I'd like to mention that the Boolean algebra itself, by its own duality, is isomorphic to the continuous functions from some other basically disconnected compact Hausdorff space to now the two-element Boolean algebra. Together, for any omega-effect monoid,
11:02
we can find one big basically disconnected compact Hausdorff space and the clopen, such that our omega-complete effect monoid embeds into the continuous functions from this big basically disconnected Hausdorff space to the real unit interval with the proviso that the functions should be zero-one valued on this specific clopen.
11:25
So you can see an omega-effect monoid M as probabilities varying over topological space where on a certain subset you have to be zero-one valued. This theorem is the brunt of the work. The remaining axioms are just to pick out a single point.
11:45
So what is it? The intersection of non-measurable independent events should be not measurable. So that means that if I have a product which is zero, then one of them should have been zero. And this picks out a single point, or non-point.
12:02
And from it this follows that M, if it satisfies our first eight axioms, it must either be the real unit interval, the two-element Boolean algebra, or the trivial effect monoid where zero is equal to one. Thus, if I have any set of probabilities that satisfies our first eight axioms and zero is not equal to one,
12:21
then M must be isomorphic to the two-element Boolean algebra or to the real unit interval. Okay, so now I want to give some highlights from the proof. It's quite a winding long proof and I can't give you all the details, but there are some interesting parts to it which I would like to highlight.
12:42
Here is a list of the things I will cover, but I won't come back to them. First I would like to start with the two classical results upon which we built. If we have an effect algebra, so that means the first four actions, then if this effect algebra is convex, which means that it has an action of the real unit interval,
13:02
so we can define like an eighth of a probability, then this effect algebra can be extended to a vector space. And if this effect algebra is omega-complete, then so is this vector space we construct. A second classic result is that of Yoshida, which says that an ordered vector space,
13:25
such as the one we just constructed, is isomorphic to the continuous functions on a compact housing space if and only if it is lattice ordered, Archimedean and order-norm-complete. I will not tell you what is Archimedean and order-norm-complete,
13:41
but I will tell you that this follows automatically if V is omega-complete. Thus, if we have a part of our effect monoid, which is convex, so it has this action of the real, and our effect monoid is lattice ordered, then we can show that this part of the effect monoid is actually an algebra of continuous functions.
14:04
So, is our effect monoid lattice ordered? If it is lattice ordered, then a times b is less than the infimum of a and b. Why? a times b is less than a times 1 is less than a, and also a times b is less than b, so indeed it is less than the infimum.
14:21
So a times b is a good first approximation. If we subtract a times b from it, then we can pull it into the infimum, and we get a minus a times b infimum a minus b minus a times b. So this is again an infimum, and we can use the product as an approximation to it.
14:42
What we get now is a second approximation given by a times b plus a times b perp times b times a perp. And we can continue this. Repeating this, we get the following candidate definition for an infimum. It's quite surprising that this actually works, but it does.
15:02
Also, consider this just for the real unit interval, then it's not obvious at all. Okay, now we know that every omega effect monoid is a lattice, the next part is looking at which parts are convex. But what is a part? We need idempotence for this.
15:20
An element is called an idempotent if its square is itself. So in the case of continuous functions, this is a zero-one valued continuous function. A set of idempotents form a Boolean algebra. An idempotent is called Boolean if all the idempotents below it are Boolean.
15:42
So that's basically the opposite of being convex. Okay, so how can we make the part? If I have an idempotent, then we can look at this corner. Given my effect monoid, I look at all elements of the form p times a, a from the effect monoid. This is called a corner by p, and it is again an omega effect monoid in an obvious way.
16:06
By the way, if I have an idempotent, then it's Boolean if and only if the corner by p is a Boolean algebra. Okay, so how do we see which parts are convex?
16:21
If I have an element, I say it's halfable if there exists an element, which if you sum it to itself, you get an element a. So h is a half a. If I have such a half, then I can look at h times h, and this behaves like a quarter, at least for an idempotent.
16:43
In this way, we can define an action for all rationals. Or well, the unit interval of the rationals. So if I have an idempotent p, which is halfable, then we can define for every a in its corner, n over ma. If the multiplication preserves suprema, and we'll get back to that, then we can extend
17:05
this to an action of the full real unit interval to the corner of p, by approximating wheels by rationals in a standard way. Thus the corner is isomorphic by Yoshida to the algebra of continuous functions, at least as effect algebras.
17:25
Because Yoshida only says something about the additive structure, not about the multiplication. But with a separate argument, we can show that this isomorphism also preserves the multiplication. And thus, if p is halfable, a halfable idempotent, then its corner must be isomorphic to the continuous functions on some space.
17:45
As omega effect monoids. So now we know that if we have halfable idempotents, we get continuous functions. And if we have Boolean idempotents, we get Boolean algebras. How do we stitch these together?
18:01
We raise our hands to the heavens and say Zorn. Using Zorn's lemma, we can find a maximal set of orthogonal idempotents which are all halfable. If we have an idempotent now, which is orthogonal to all the halfable idempotents we just constructed, then it can be shown that this idempotent must be Boolean.
18:24
Then, invoking Zorn again, we can extend this to a maximal set of orthogonal idempotents, where each of the idempotents is either halfable or Boolean. What we do now is that for each of them, we can create a corner.
18:40
So we have this E, this set of orthogonal idempotents, this maximal set. For each of them, we can make the corner. And all the corners we can put together, stitch together with a Cartesian product into one big omega effect monoid. In general, this is not isomorphic to M itself.
19:00
This big effect monoid is nice because in it, all the Boolean idempotents have a sum. And also all the halfable idempotents have a sum. And so this big Cartesian product is itself isomorphic to the Cartesian product of one big Boolean algebra and one algebra of continuous functions.
19:24
Our original effect monoid embeds into this in the standard way, namely an element a we send to the sequence which in the p-th position is given by a times p. And so we have our main theorem.
19:40
I still have to say something about the continuity of the multiplication. That the multiplication preserves countable supremum follows from the fact that an order interval from 0 to b where b is an arbitrary element is order isomorphic to the corner by the ceiling of b. The ceiling of b is the least idempotent above b.
20:03
It's like the carrier idempotent of b. This isomorphism from the corner to the order interval is given by you set a to a times b. This order isomorphism, its inverse is a partial division. And I want to talk about it.
20:22
By the way, below there is a formula for the ceiling using omega completeness. In an omega effect monoid, we can define for elements a and b, with a less than b and that's important, we can define a divided by b as follows. If you think about real numbers for the moment, then we can pull o to the a
20:41
and what's left on the right is a geometric progression. This geometric progression sums to 1 over b and so indeed a over b is a over b. In the situation of continuous functions, then f over g on the point x is also just f over x divided by g over x, at least if g over x is not 0.
21:04
If it is, then it is 0. This turns our effect monoid into an effect divisoid. a over b is the unique element of M such that a over b is less than b over b and a over b times b is a. Again, note that a over b is only defined if a is less than or equal to b.
21:22
Also a is less than a over a and a over a over itself is a over a. Quite interesting, by the way, is that in this context, 0 divided by 0 is 0. I wanted to mention these effect divisoids because they are quite close to omega completeness.
21:42
In fact, if I have an algebra of continuous functions, then it is an effect divisoid if and only if it is omega complete. Unfortunately, there does exist an effect monoid that is an effect divisoid, but it is not omega complete. So unfortunately, we cannot use the effect divisoid as the actions.
22:03
And that would have been nice, because the action of an effect divisoid is quite close to what you do when you compute Bayesian updating. Anyway, that's what I wanted to highlight from the proof, and I thank you for your attention.