It is not a structure since the base set is not abstract so you don't need to use the structure builder to define it.
Anyway my direction now for probabilities is to define the measure integral.
The long-awaited (at least for me :-) ) update on probability theory and general measure theory was recently delivered by Thierry Arnoux and that got me into thinking.
At some point, the direct product of RR with itself is considered and studied from the standpoint of topology, then, as I understand, some steps are taken into proving facts about dyadic squares on RR^2. When finished that will provide a Borel sigma algebra on RR^2 and then finally area can be defined.
While RR^2 as a set of pairs must fit well into the already developed framework (for example, the product of two sigma-algebras seems to be defined), it looks like not constraining yourself to products of two sigma-algebras only seems like a good idea. Proving the results about dyadic cubes in the case of RR^N should be doable and will yield a smoother development process in case if we ever go as far as developing calculus on RR^N.
So with that in mind, I suggest to try fixing a more or less coordinated definition of RR^N. I know that this question has been risen before a few times without any definite results, but when so much work is being put into the probability branch, not having an "official" version of RR^N seems to be a sad omission which may make us pay later, when some parts depending on a specific construction of RR^2 will have to be rewritten into a more general framework.
I suggest the following definition:
df-rrtn $a |- RRn = ( n e. NN |-> ( ( CCfld |`s RR ) freeLMod ( 1 ... n ) ) ) $.
Virtually the only quality this definition of RR^N lacks is the Hilbert space structure. df-prds doesn't seem to define the inner product for a structure product (btw, it would be great if a comment for df-prds listed structures it can work with and the ways it generalizes operations), but probably it can be changed. Another option is artificially augmenting RRn with an inner product, but that makes treating RRn as a free left module a bit harder.
Another variation of this definition is dropping the ( 1 ... n ) part and using an arbitrary set there. Maybe it makes it more general, but I feel that writing ( 1 ... n ) in every usage of RR^N will get a bit tedious.
Combining all the recommendations in the previous email would look something like:
df-rrx $a |- RR^ = ( i e. _V |-> ( ( CCfld |`s RR ) ^s i ) ) $.df-prds $a |- Xs_ = ... u. { <. ( .i ` ndx ) , ( f e. v , g e. v |->
( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. }
df-sra $a |- subringAlg = ... sSet <. ( .i ` ndx ) , ( .r ` w ) >.
You mean your own recommendations in your previous email.
df-rrx $a |- RR^ = ( i e. _V |-> ( ( CCfld |`s RR ) ^s i ) ) $.
df-prds $a |- Xs_ = ... u. { <. ( .i ` ndx ) , ( f e. v , g e. v |->
( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. }
df-sra $a |- subringAlg = ... sSet <. ( .i ` ndx ) , ( .r ` w ) >.
My main reference is this website pointed to by David: www.math.uah.edu/stat/index.html
Besides, I have been picking among "Probability: Theory and Examples" from Rick Durrett, "Measure Theory", from Donald L. Cohn, and "Measure Theory" from Vladimir I. Bogachev.
How could I add them to the Bibliography?
My main reference is this website pointed to by David: www.math.uah.edu/stat/index.html
Besides, I have been picking among "Probability: Theory and Examples" from Rick Durrett, "Measure Theory", from Donald L. Cohn, and "Measure Theory" from Vladimir I. Bogachev.
Everyone else: Would these proposed definitions work? I'm sure there are many ways to do this, but are there *serious* technical problems with the ones outlined by Mario (if so, what are the problems and what is the better alternative)? Or tweaks that would improve it? I'd just like to eventually move to a rough consensus.
My main reference is this website pointed to by David: www.math.uah.edu/stat/index.html
Besides, I have been picking among "Probability: Theory and Examples" from Rick Durrett, "Measure Theory", from Donald L. Cohn, and "Measure Theory" from Vladimir I. Bogachev.
How could I add them to the Bibliography?
- For Hilbert spaces, it is not the product, but the direct sum, which is important (of course, it is the same for finite sums/products, but it looks like you wanted to treat the general case; actually, I even doubt that the product exists in general). (And just to clear a possible confusion from the original post: a free module is a direct sum, that is, a coproduct, not a product.)
> df-sra $a |- subringAlg = ... sSet <. ( .i ` ndx ) , ( .r ` w ) >.
I don't understand anything to this line (I haven't looked it up in set.mm), but to anyone new to metamath (or at least, new to set.mm), "sSet" means "simplicial set" (which it probably doesn't, here), so maybe a more meaningful name could be found ?
- The field of real numbers seems central enough in mathematics to deserve its own definition: RRfld = CCfld |`s RR.
Cool! Can you show an example of how those definitions would be used together? (No need to write a proof, I just want to see them used together.)
> On Tue, Oct 17, 2017 at 1:20 PM, David A. Wheeler wrote:
> > Cool! Can you show an example of how those definitions would be used
> > together? (No need to write a proof, I just want to see them used together.)
On Tue, 17 Oct 2017 21:27:56 -0400, Mario Carneiro <di....@gmail.com> wrote:
> I guess ( toCHil ` ( ( ringLMod ` ( CCfld |`s RR ) ) ^s ( 1 ... N ) ) ) is
> an example?
No, I meant an example of how these definitions would be *used* :-).
For a trivial example, this would be a correct (and common) use of RR^ , yes?:
( RR^ ` ( 1 ... N ) )
Also, I presume the use of Xs_ (per df-prds) would stay the same,
e.g., in prdsmndd we have:
Y = ( S Xs_ R )
and in df-pws we would still have:
$a |- ^s = ( r e. _V , i e. _V |->
( ( Scalar ` r ) Xs_ ( i X. { r } ) ) ) $.
(thinking again) Oh, I guess this theorem doesn't work for infinite I, because the basis vectors don't actually form a basis. Maybe it would make more sense to use freeLMod after all, since as previously mentioned a few of the slots will be trashed for infinite I, and it would be nice to have all those statements like (RR^ ` I) e. CHil hold for all I, not just the finite ones.
(thinking again) Oh, I guess this theorem doesn't work for infinite I, because the basis vectors don't actually form a basis. Maybe it would make more sense to use freeLMod after all, since as previously mentioned a few of the slots will be trashed for infinite I, and it would be nice to have all those statements like (RR^ ` I) e. CHil hold for all I, not just the finite ones.
Won't it confuse people, though? For example, Munkres in his book on topology distinguishes between R^omega (a countable product of copies of R) and R^inf (a finitely supported subspace of R^omega).
Probably theorems that mention infinite I should call this out, but I don't see any good notational way to indicate this that isn't confusing in the finite case.
Probably theorems that mention infinite I should call this out, but I don't see any good notational way to indicate this that isn't confusing in the finite case.
My point is that probably there are not a lot of interesting theorems about the infinite case anyway. The only sane use for R^omega I can think of is defining l_p spaces, but in this case finitely supported sequences won't work.
So it's not so much that there are no interesting theorems about R^omega but rather that there are no *new* theorems - almost all the old theorems about finite dimensional vector spaces generalize without having to do anything extra, which is the kind of generalization I like to see (no extra work, just don't unnaturally limit yourself).
Okay, so it looks like there are a few issues with MY previous proposal in MY previous email.
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.
df-rrx $a |- RR^ = ( i e. _V |-> ( toCHil ` ( ( ringLMod ` ( CCfld |`s RR ) ) ^s i ) ) ) $.
df-rrxf $a |- RR^() = ( i e. _V |-> ( ( RR^ ` i ) |`s { f e. ( RR ^m i ) | ( `' f ( _V \ { 0 } ) ) e. Fin } ) ) $.
Then we will have ( RR^() ` I ) e. CHil for all I, and ( RR^() ` I ) = ( RR^ ` I ) for finite I
I'm not a big fan of addStruct because that's an awfully large token for a binary operator, even if it's not used really often. How about ":=s"? This is reminiscent of the := assignment operator in some languages, with an "s" subscript like the other structure operators. An alternative is something based on the [ A / x ] ph notation, because it is very similar in spirit, taking an existing thing and modifying just one part of it to set it to something else.
I'll have more time to elaborate tonight, but just for now, I suggest:
- define |- RRfld = ( CCfld |`s RR ) (why wait? you cannot go wrong with this one)
- df-rrx $a |- RR^ = ( i e. _V |-> ( ( ringLMod ` RRfld ) ) ^s i ) ) $. (Mario's one-but-last proposal)
- deal with inner products later
In particular, do NOT define RR^ with the free module function (Mario's last proposal). The notation \R^I is completely standard and does NOT mean "direct sum". A common notation for direct sum is \R^{(I)} so maybe one could define " RR^() " and then write "( RR^() ` I )" for the wanted direct sum.
Both structures are important: direct sum (which is the coproduct for modules) and direct product (which is the product for modules), both are natural for different kinds of problems, and there are important theorems for both. You won't have RR^ I e. Hilb but you'll have to live with that: many categories lack products. (Even more: two objects can have different products when considered in different categories, which shows the limits of df-prds.)
As for "sSet": since it "adds an additional structure", maybe "addStruct" ?
--
Benoit
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
df-rrx $a |- RR^ = ( i e. _V |-> ( toCHil ` ( ( ringLMod ` ( CCfld |`s RR ) ) ^s i ) ) ) $.
Ok. (But I still think RRfld is worth it.)df-rrxf $a |- RR^() = ( i e. _V |-> ( ( RR^ ` i ) |`s { f e. ( RR ^m i ) | ( `' f ( _V \ { 0 } ) ) e. Fin } ) ) $.
It would be more natural to use freeLmod, here (same definition as RR^, with freeLmod replacing ^s).Then we will have ( RR^() ` I ) e. CHil for all I, and ( RR^() ` I ) = ( RR^ ` I ) for finite I
Yes, and this is even a characterization of finiteness.I'm not a big fan of addStruct because that's an awfully large token for a binary operator, even if it's not used really often. How about ":=s"? This is reminiscent of the := assignment operator in some languages, with an "s" subscript like the other structure operators. An alternative is something based on the [ A / x ] ph notation, because it is very similar in spirit, taking an existing thing and modifying just one part of it to set it to something else.
Maybe (with "s" being displayed as a subscript):
class [ C / B ]s A
|- [ C / B ]s A = ( ( A |` ( _V \ ( B ` ndx ) ) u. { <. ( B ` ndx ) , C >. } )
Norm: ok, I have no strong opinion on this sSet issue (apart from finding another name) and I agree with the advantages you mention of defining new things as class constants whenever possible. Actually, I think the whole extensible structure thing is a clever hack but is very "unmathematical", and the current discussion about sSet is an illustration of this.
--
FL
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
df-rrx $a |- RR^ = ( i e. _V |-> ( toCHil ` ( ( ringLMod ` ( CCfld |`s RR ) ) ^s i ) ) ) $.
Ok. (But I still think RRfld is worth it.)df-rrxf $a |- RR^() = ( i e. _V |-> ( ( RR^ ` i ) |`s { f e. ( RR ^m i ) | ( `' f ( _V \ { 0 } ) ) e. Fin } ) ) $.
It would be more natural to use freeLmod, here (same definition as RR^, with freeLmod replacing ^s).
Norm: ok, I have no strong opinion on this sSet issue (apart from finding another name) and I agree with the advantages you mention of defining new things as class constants whenever possible. Actually, I think the whole extensible structure thing is a clever hack but is very "unmathematical", and the current discussion about sSet is an illustration of this.
Regarding the field of real numbers, I would be delighted for it to have its own definition.Construction of the reals is a pretty famous connection between set theory and traditional mathematics. It seems to me that RRfld having its own definition would feel most natural for people orienting themselves to Metamath. I know I was a bit disappointed to have to look at complex numbers to get to real numbers.
That moment when you realize that formal theorem proving is more like engineering than mathematics. :)
Of course, a mathematical object is necessarily different from its representation in a computer, but extensible structures are a bit of a stretch. If you ask around what a group is, you'll get: "it's a set with a binary operation such that..." (or better, "it's a set with a binary operation, a constant, and a unary operation such that..."), but you won't have many "it's a function f from a subset of \N to classes such that f(0) is a set, f(1) is a binary operation on f(0), f(2) \in f(0)...".
Of course, a mathematical object is necessarily different from its representation in a computer, but extensible structures are a bit of a stretch. If you ask around what a group is, you'll get: "it's a set with a binary operation such that..." (or better, "it's a set with a binary operation, a constant, and a unary operation such that..."), but you won't have many "it's a function f from a subset of \N to classes such that f(0) is a set, f(1) is a binary operation on f(0), f(2) \in f(0)...".
What does it mean to be a set with a binary operation?
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
On Wednesday, October 18, 2017 at 9:27:19 AM UTC-4, Benoit wrote:
Maybe (with "s" being displayed as a subscript):
class [ C / B ]s A
|- [ C / B ]s A = ( ( A |` ( _V \ ( B ` ndx ) ) u. { <. ( B ` ndx ) , C >. } )Just a general remark.We have always encouraged new definitions to be class constants instead of new syntax structures with arguments,
If a group is just a pair, then it can't have any additional data beyond what is relevant for group theory
but this is limiting if you want to say that a ring is a group because it's not technically true
- you have to say something much more cumbersome likeIf <A,B,C> is a ring, then <A,B> is a group
The problem with the textbook definition is that on the one hand it is claimed that every ring is a group
but I don't see how there could be anything simpler that would let us say, "every ring is a group"
If a group is just a pair, then it can't have any additional data beyond what is relevant for group theory
Yes, that's the point.but this is limiting if you want to say that a ring is a group because it's not technically true
Yes, and this is fortunate: indeed, a ring is not a group.- you have to say something much more cumbersome likeIf <A,B,C> is a ring, then <A,B> is a group
Indeed, my idea was to define the (object component of the) appropriate functors, e.g., in pseudo-metamath,
$a |- RingToGroup = ( <. x , y , z >. e. Ring |-> <. x , y >. )
$p |- RingToGroup : Ring --> Group
I realize it is more cumbersome and makes life harder, but it also looks neater. I also understand your point of view, and maybe my suggestion would hamper too much further development of set.mm (but again: what are the objectives of this development?).
> maximize the use of the "identity coercion" to produce hierarchies of literal subclasses Monoid C_ Group C_ Ring C_ DivRing C_ Field etc.
You probably meant it in the other direction, but the inclusion Ring C_ Group is abusive.
Perhaps that is a hack, but I don't see how there could be anything simpler that would let us say, "every ring is a group" and thus reuse for rings all of the theorems we developed for groups.
The problem with the textbook definition is that on the one hand it is claimed that every ring is a group
Then we have not been reading the same textbooks ! The phrase "the additive group of a/the ring" is pretty common, and this is what I implemented with the function RingToGroup (the object component of a functor).
What does it mean to be a set with a binary operation?
You can read in most textbooks: "A group is a couple (G, * ) where G is a set and * is a binary operation on G such that...".
And what's a couple but a function with domain (1, 2)?
Of course we are always looking for better names for things and appreciate your input. For example, I have come to think that Carrier might be a better word than Base. I can't remember now why I picked Base.