[ 3 / biz / cgl / ck / diy / fa / ic / jp / lit / sci / vr / vt ] [ index / top / reports ] [ become a patron ] [ status ]
2023-11: Warosu is now out of extended maintenance.

/sci/ - Science & Math


View post   

File: 635 KB, 868x654, 1561985999183.png [View same] [iqdb] [saucenao] [google]
11043085 No.11043085 [Reply] [Original]

>infinite sets
edition

>> No.11043089

old:
>>11030534

>> No.11043092
File: 326 KB, 1222x695, log.png [View same] [iqdb] [saucenao] [google]
11043092

>>11043077
>The Reals aren't computable, how does this gain you anything in analysis?
If you got any Turing complete system, you also get non-computability issues, so that's not the issue at hand. There's a dozens of constructions of the reals, but trying to avoid the law of excluded middle (LEM) gives you a lot (although it makes proofs harder, since you don't have "make believe" axioms such as LEM). Pic related, especially the last paragraph.

>> No.11043096
File: 324 KB, 882x889, 1550710493285.png [View same] [iqdb] [saucenao] [google]
11043096

1st for fuck cantor and fuck 20th century "math"

>> No.11043104

>>11043096
type theory, homotopy theory and topos theory are 20th century math.

>> No.11043105
File: 69 KB, 828x930, 1570136553263.jpg [View same] [iqdb] [saucenao] [google]
11043105

>>11043096
now this is based

>> No.11043109
File: 258 KB, 868x958, whitesuit.png [View same] [iqdb] [saucenao] [google]
11043109

Posting from other thread.

>>11043058
>But I am talking about "geometric" object, not a function
You were asking for the definition of continuous function, no?
>But in that case you are LITERALLY doing nothing but calling things by different names.
Types are fundamentally different in that everything you talk about must have a single* unique type. In set theory [math]x\inX[/math] is a proposition; it can be either true or false. In type theory [math]x:X[/math] is not a proposition; x doesn't even make sense without a type.
The type theoretic approach has disadvantages (subtypes are less neat than subsets, quotient types require additional axioms) but most of the maths still works and it is much easier for computers to reason about.

*strictly with universes this isn't true but it doesn't really matter


>>11043077
>The Reals aren't computable, how does this gain you anything in analysis?
The reals aren't computable, but facts about them are. Computer systems are no more working with representations of the reals than you are. They use axioms just like you. Computers can already prove "basic" facts of analysis by heuristic graph search.

>>11043096
based

>> No.11043110

>>11043077
Regarding the domain, you what do you use the domain for? To take things from it and work with them.
In a relatively small set like some Neumann universe that's smaller than of level omega squared, any set you consider is really in correspondence with some predicate anyway
[math] P \leftrightarrow \{x | P(x)\} [/math]
To check if a term is of a set is to check if the term fulfills the predicate.

>> No.11043122

I, for one, am disgusted at the new OP.

>> No.11043125 [DELETED] 

>>11043092
None of that andwe>>11043110
>To take things from it and work with them.
No, you usually investigate them as a geometric object.

>> No.11043128
File: 62 KB, 570x653, 1570241141850.jpg [View same] [iqdb] [saucenao] [google]
11043128

>>11043092
>constructive analysis
Has been reformulating and reproving first-year calculus theorems again and again for a hundred years. When they're not doing that, they're reinventing wheels from other kinds of constructive/computable mathematics or Soviet mathematics. An absolute shit-tier, anti-aesthetic, and in the cases of wheel reinvention, borderline fraudulent field.

>> No.11043131

>>11043110
>To take things from it and work with them.
No, you usually investigate them as a geometric object.

>> No.11043132

>>11043109
>You were asking for the definition of continuous function, no?
No? I was asking about Continuous or Lipschitz boundaries, as they often come up in analysis.

>In type theory x:X is not a proposition
How is that even true?
Can't you talk about the type of an object?
Like saying "the proposition that sqrt 2 : Rat" is false.

>x doesn't even make sense without a type.
Let me rephrase that in set theory. x doesn't make sense if it isn't specified from which set it originates from.

So, again, what is the actual point of trying to rephrase things in type theory, it won't make PDE theory any more computable than it is now.

>> No.11043135
File: 31 KB, 485x443, 1512956165259.png [View same] [iqdb] [saucenao] [google]
11043135

what the f*ck is an ordinal

>> No.11043139
File: 93 KB, 685x514, godel.jpg [View same] [iqdb] [saucenao] [google]
11043139

reminder infinite sets exist, and any one that denies this quite literally just dosent have the capacity to conceive of one. You shouldnt attack finitists, you should feel sorry for them. They are trying, but make sure to point out where they are retarded without being to harsh.

>> No.11043142

>>11043135
https://en.wikipedia.org/wiki/Ordinal_number

>> No.11043146

>>11043128
I don't think there's many people working on it and I think this style will get stronger over time, with suitable programming languages, either way.
I'm not biased against any more common math, no need for a debate.

>>11043131
I'm not seeing where the issue is exactly. My point is that you capture the same things (they are all relatively small anyway).
I agree that the primitives may not be good for topology and sigma algebra kind of operations.

>>11043132
>Like saying "the proposition that sqrt 2 : Rat" is false.
You can write that down and check it with a type check algoithm - in that sense you have a "truth value".
But the point is that it's not a proposition inside the language that you can use or return.
Just like the syntactically wrong expression [math] \neg \lor {\mathbb R} [/math] isn't part of the language or has a truth value in the language (but we can use our reasoning / an algorithm) to see it's nothing valid.

>So, again, what is the actual point of trying to rephrase things in type theory, it won't make PDE theory any more computable than it is now.
Yes it will, because general PDE proofs that mathematicans publish papers with don't have requirements to be constructive. The other framework would enforce this by construction (or at least highlight added axioms very explicitly)
Again, I'm not saying people stop what they do.

>>11043135
Applying "one more" and "jump somewhere else" to 0 and never stopping.

>> No.11043156
File: 493 KB, 1597x906, lc.jpg [View same] [iqdb] [saucenao] [google]
11043156

This shit blew my fucking mind

>> No.11043160

>>11043146
Sure, but then there simply is no point to actually replacing anything existing with type theory, as you would literally just say what mathematicians have been saying with types instead of sets.

I see that it is useful for constructive analysis, which seems interesting, but also nothing more than a severely crippled version.

>> No.11043162

>>11043135
https://youtu.be/EAAC9dCV9_k

>> No.11043182
File: 58 KB, 575x489, Voevodsky-Diagram.png [View same] [iqdb] [saucenao] [google]
11043182

>>11043160
Well you'd have papers that are closer to being ready to be checked by computers in that language.
Per Martin Löfs equality proposition (the thing that fleshes out the BHK interpretation and taking it from a pure logic to a math context) is from the early 80's, but was made popular by Voevodsky ((higher) homotopy theorists) after he went looking for a new subject after he won all the prices in his field and found that going higher in the higher algebra direction gets him to factually uncheckable (for human reviewers) category theory'esk constructions. I think that's roughly how the story goes with "univalent foundations".
Of course a lot of it is just bargaining for where the manpower goes.

I do agree with the more dedicated proponents (Andrej Bauer etc.), that LEM etc. makes people research kind of silly things when they could do nicer things. But of course again, this is an aestetic point.

Just giving analysist set theory axioms from the 1920's of course they're using and abusing it because it's never questions.
>For every vector space there "exists" a basis.
>Also, there are vector spaces for which we can prove that it's impossible to ever state a basis.
Yeah I mean if you don't mind those things, then sure, go ahead.
I think it's not the case that constructivism is "limiting". If would be limiting if there was infinite manpower to do math.

>> No.11043239

1. are axioms arbitrary? if true:
2. are there any properties that hold regardless of choice of axioms?

>> No.11043245

>>11043239
>are axioms arbitrary
Ye.
>are there any properties that hold regardless of choice of axioms
Ye, logic.

>> No.11043249

>tfw summerfags will never leave
>this is 4channel now forever

>> No.11043272
File: 10 KB, 180x180, GNCA-0212.jpg [View same] [iqdb] [saucenao] [google]
11043272

>>11043139
real number set isn't infinite

>> No.11043277

>>11043109
Recommend me an introductory source on type theory.

>> No.11043282
File: 175 KB, 560x420, 1558411566185.gif [View same] [iqdb] [saucenao] [google]
11043282

i can't into latex

>> No.11043307

>>11043156
The proof that Goldstein's sequence eventually goes to zero also depends on ordinal fuckery, to give a more elementary example.
The order of magnitude of the term that zeroes the sequence is also pretty damn absurd. For a starting number of twelve it takes way over Graham's number of iterations to end the sequence.

>> No.11043327
File: 56 KB, 720x410, 190214100031_1_900x600.jpg [View same] [iqdb] [saucenao] [google]
11043327

>>11043245
>Ye.
then what's the point of anything

>> No.11043370
File: 110 KB, 781x944, __remilia_scarlet_touhou_drawn_by_miyo_ranthath__25e7f172b0b0c9dbf698b6aa96b31244.jpg [View same] [iqdb] [saucenao] [google]
11043370

>>11043327
Geometry makes me hard.

>> No.11043438

>>11043245
>Ye, logic.
Logic is based on axioms.

>> No.11043441

>>11043249
>>tfw summerfags will never leave
>>this is 4channel now forever
Who are you quoting?

>> No.11043442
File: 524 KB, 1920x1080, hot-gorilla-today-150625-tease_f85bf9d67d8f7fd4a3f4af0d8e69e109.jpg [View same] [iqdb] [saucenao] [google]
11043442

>>11043370
nothing makes me hard

>> No.11043465
File: 41 KB, 350x268, TURN ON CNN.jpg [View same] [iqdb] [saucenao] [google]
11043465

https://arxiv.org/pdf/1910.02954
>Prime numbers and the Riemann hypothesis
>Tatenda Kubalalika
>(Submitted on 7 Oct 2019)

>By considering the prime zeta function, we demonstrate in this note that the Riemann zeta function zeta(s) does not vanish for Re(s)>1/2, which proves the Riemann hypothesis.

>> No.11043485

>>11043096
>>11043085
Does this nigga still make videos? I remember reading his shit back in 2011.

>> No.11043487

>>11043139
Imagine making obscure videos on Youtube about the exact same topic while being wrong about it for literally 10 years. Just imagine that.

>> No.11043510
File: 873 KB, 1046x1272, 0dca8b8abcd968b2dd3509156f584006608e454d.png [View same] [iqdb] [saucenao] [google]
11043510

>>11043442
You're never gonna get anywhere with that attitude.
>>11043485
Yes. This is from two days ago:
https://youtu.be/ZgOtcvNG9I0

>> No.11043612

How did you guys determine which topics really interested you?
I've been learning about smooth manifolds because I want to understand what Lie Groups are and how they apply to physics. I've been reading John Lee's text, but I find myself not caring all that much about a lot of the early material (like embeddings and Sard's theorem for example), so I'm wondering if perhaps this topic isn't for me.
Maybe I'm just approaching reading the text wrong and trying to be too comprehensive with it all. I'm just a hobbyist so perhaps I should try and race ahead to the material that I'm curious about so that I can decide if it's worthwhile to deepen my understanding of the fundamentals.

>> No.11043736
File: 24 KB, 568x74, hes at it again.png [View same] [iqdb] [saucenao] [google]
11043736

>>11043485

>> No.11043842

>>11043282
Just use Google, that's how I do 99% of my TeX things.

>> No.11043843

>>11043239
>1. are axioms arbitrary?
No, they are chosen very deliberately such that certain things are true.

>> No.11043855

>>11043277
Depends what you mean by introductory and what you're actually interested in.
Type theory (like set theory) is extremely dry by itself. I would suggest learning it by learning to use a theorem prover (one of the real reasons for type theory).
I learnt using lean. It has a manual that is half textbook half documentation: https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf
Also this guy's blog: https://xenaproject.wordpress.com/category/learning-lean/

>>11043282
What are you struggling with?
Have you tried any tutorials?

>>11043612
Sometimes you just see a theorem or result and you go "damn that's cool"

>> No.11043892
File: 128 KB, 496x450, yukari_suicide_hotline.png [View same] [iqdb] [saucenao] [google]
11043892

>>11043465
Stop posting links from math.GM.
>>11043612
Read Schwarz's "Quantum Field Theory and Topology". It's a short book about how topological concepts see application in physics, from defect classification with homotopy groups to solving Abelian Yang-Mills with Ray-Singer torsion. Sard's theorem also sees an appearance as spectral representation for something.
It doesn't cover much of the background, but it will definitely give you plenty of motivation to learn more topology.

>> No.11043913
File: 48 KB, 1004x777, A83DBFA2-5E4B-4E5E-9746-C2C8329CC354.jpg [View same] [iqdb] [saucenao] [google]
11043913

>all A’s in hs, minimum effort
>36 ACT
>4.0 GPA sophomore year at uni math major
>rarely pay attention in class, study the day before tests
>forget everything in 2 weeks
>tfw I’m a math major and don’t understand mathematics

>> No.11043934
File: 195 KB, 1650x1050, 1549413997689.png [View same] [iqdb] [saucenao] [google]
11043934

>>11043085

>> No.11043942

intuitionism rules OK

>> No.11044106

>>11043855
why do you shill type theory here? it's placed literally at the edge of mathematics and no one cares about it. Everyone, every book and every paper uses set theory and first-second order logic. No one cares about proof assistents either. And even if people did there is already a proof assistant based on set theory which uses first-second order logic. It is called Mizar. Studying type theory is a waste of time.

>> No.11044117

>>11043736
>>11043096
Can someone explain what the fuck is his problem? Why does he deny R? is there some short text in which I can read about all his qualms with the real numbers and other standard modern mathematical constructions? Preferably all in one place and where he gives arguments for why he believes that.
Thanks

>> No.11044118

>>11043307
>goodstein depends on ordinals
Not really. You can prove it directly by induction on the digits:
>suppose the sequence never reachrs zero
>then the ones digit changes infinitely often
>then the "tens digit" changes infinitely often
>...
>then the top digit changes infinitely often
>but this is impossible
This proof is equivalent to the ordinal thing in a specific formal way, but nowhere do you need to mystically rely on infinite sets

>> No.11044143
File: 26 KB, 128x128, 1569341345617.png [View same] [iqdb] [saucenao] [google]
11044143

>>11043277
https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf

>>11044117
He's just a finitist.
The Wikipedia pages on computable numbers as well as on definable numbers will help understand people's issues, and the note that indeed not all numbers are are definable, let alone computable. I don't say this in support of finitism.

On the other hand, people saying X is a waste of time don't make a case either.
What's not a waste of time? Making money, progressing society and getting in bed with pretty girls and making babies? There's no universal justification for the merit of that either, might as well do the music, writing or math you like. If someone wants to write down math from a finitist angle - and in high quality and stamina - then let him. Afraid those influences will take away resources from mainstream math? But you just argued it's not important, so what is it?

>> No.11044144

>>11044143
I hate her face so goddamn much.

>> No.11044161
File: 36 KB, 350x301, lick-boot.png [View same] [iqdb] [saucenao] [google]
11044161

>>11044143
>there's no such thing as a waste of time
>doing math is the same as not doing math

>> No.11044203
File: 45 KB, 909x799, Skärmklipp63.png [View same] [iqdb] [saucenao] [google]
11044203

>>11043085
How the fuck do I solve this?
ABE triangle is equilateral so it's three internal angles must be 60 and equal 180 total.
AED and BEC must be identical.
E has to be 360-60-AED-BEC.
It has to be easy, I just don't see it.
Please help

>> No.11044205

>>11044106
It's a cool refreshing take on mathematics with really nice computational applications. I also just enjoy arguing with people.
>no one cares about it
As I said, there are people teaching and practising it at my uni. I know people are doing it elsewhere too. There's also research in industry from the computer science side.
>And even if people did there is already a proof assistant based on set theory which uses first-second order logic. It is called Mizar.
Does it treat propositions and proofs as first order objects? Can I write programs and prove their correctness in it? How does it deal with a statement like [math] 6 \in \pi [/math] (this is something that is somewhat involved to disprove in set theory, yet is nonsensical in type theory).
>Studying type theory is a waste of time
Yeah, I personally think you have to be a bit bent to study either type theory or set theory. I'm glad someone does it though so I can use them to do fun maths.

>> No.11044233

>>11044205
>As I said, there are people teaching and practising it at my uni. I know people are doing it elsewhere too. There's also research in industry from the computer science side.
yeah, only people who care about type theory are from CS department. Are you from CS department? Most people from math deparments haven't even heard about type theory.
>Does it treat propositions and proofs as first order objects?
it doesn't
>Can I write programs and prove their correctness in it?
You can formalize algorithms and prove their correctness but you can't use them as a part of the system after that. Coq or Lean would be better suited for that.

>> No.11044236

>>11044203
It’s trivial.

Notice that BE=BC, so you know all angles in BCE.

>> No.11044246

>>11043736
>>11044117
It's fucking hilarious. Imagine not understanding a concept for 10 fucking years and STILL not giving up on it, despite having a PhD in mathematics.

>> No.11044247

>>11043510
Why does it feel like almost every video he makes is more or less the same complaint about infinite sets and real numbers?

>> No.11044253
File: 56 KB, 909x799, Skärmklipp63.png [View same] [iqdb] [saucenao] [google]
11044253

>>11044236
Yeah lol, thanks

>> No.11044259

>>11044233
I'll check out Mizar, it sounds pretty interesting.

>Are you from CS department?
I'm doing a maths undergrad (mostly algebraic stuff). I've done a bit of CS though. The people who do type theory in the maths department at my uni don't study it as their main thing. It's mostly a hobby/toy/gimmick for them to do other maths with. There's people people doing logic and correctness stuff in the CS department but it sounds super dry to me.
>it doesn't
For me this was one of the main appeals of type theory. You can reason about propositions (the dreaded category of propositions). You can define mathematical objects which bundle proofs with them. You can define functions of propositions, etc.
It reminds me of discovering that functions were first class objects in Haskell (but better!). It's just such an elegant, self encapsulating system. You're used to thinking of propositions as a kind of meta thing and then suddenly they're just another type.
>Coq or Lean would be better suited for that.
I'm told Lean code is still very slow. It's also still pretty painful to write proofs in imo. Theorem provers have a long way to go, but that's mainly a CS problem.

>> No.11044337

>>11044117
Purism. His approach of math is not "wrong" in itself, not completely "useless", it is just an exercice in building a consistent and somewhat worthwhile mathematic model without any references to infinite sets.

It's funny as an exercice, but it is not really useful for any practical application and further developpement of the existing theories.

At any rate he completely forgets that math is just a formal set of axioms, tools, and theorems that arise naturally from it.
Math does not exist, except maybe in the platonic realm our axioms create.

>> No.11044359

>>11043913
cringe

>> No.11044385

In my first semester I have 3 pure math classes:
Analysis 1
Linear Algebra 1
logical foundations of mathematics

After every lecture the professor uploads a full transcript of the two hours.
So now I want to know, how do I get the most out of the lectures?
I tried copying everything the professor wrote on the board, but I ended up mindlessly writing down everything without really grasping everything.

>> No.11044426

>>11044337
>but it is not really useful for any practical application and further developpement of the existing theories.
I'm not so sure about that, we could couple it with a constructive theorem-prover and learn which theorems of Peano arithmetic remain valid over finite structures (though not necessarily with a constructive proof), and which theorems hold only in infinite models.
I could see these kinds of reverse-mathematics results having applications in cryptography, where the fact that all our _physical_ models of arithmetic are necessarily finite is significant (roughly speaking, they'd tell you what you can brute-force, what remains out of reach of brute force, and what you can get without needing brute force, where "brute force" refers to some kind of unbounded search).

>> No.11044437

>>11044385
Do exercices. You can't really hope to grasp everything the proof does in class ; just focus on what he emphasises.
(If a prof stops to repeat something, it's definitively worth noting)

>> No.11044444

>>11044426
All models of Peano arithmetic are infinite.

>> No.11044449

>>11044426
I am absolutely not versed enough in arithmetic to think of that, honnestly. But I guess you're right
In my ""fields of interests" (probabilities, stats, mathematical physics...) his approach doesn't seem very useful.

>> No.11044465

>>11044337
>he completely forgets that math is just a formal set of axioms, tools, and theorems that arise naturally from it
Exactly. This is what still bothers me about him. Nobody is claiming that a particular set of axioms are "true". Nobody. Yet this man spends 10+ years of his life and likely thousands of hours trying to "prove" that infinite sets are "false". I used to think he was funny but I can see him aging in his videos now and I just feel kind of bad for him.

>> No.11044486

>>11044465
>Nobody is claiming that a particular set of axioms are "true". Nobody.
I am.

>> No.11044494
File: 56 KB, 1024x576, 1564880719620m.jpg [View same] [iqdb] [saucenao] [google]
11044494

>>11044444
>[math]\forall \mathcal{M}\in\emptyset~~\mathcal{M}[/math] is infinite
But anon, this requires some version of the law of excluded middle...

>> No.11044497

>>11044444
>All models of Peano arithmetic are infinite.
Well yes, but I was referring to a finite structure embedding into an infinite one, on which the PA signature is definable, such that the infinite structure becomes a model of PA.
This isn't my area of expertise so I might not have gotten the terminology quite right, but what I had in mind was the structures discussed in http://www1.cs.columbia.edu/~tl2383/arith.pdf (tl;dr: < and | (divisibility) can define PA's * and +, so a finite structure of signature (<,|) can simulate PA).

>> No.11044517

Do award winning mathematicians browse /mg/?

>> No.11044529 [DELETED] 

>>11044465
>I can see him aging in his videos now and I just feel kind of bad for him
this. he's gonna die a crank who, at some point in his life, taught a bunch of niggers some algebraic topology

>> No.11044544

>>11044529
Someone ought to make a before/after ultrafinitism meme with Wildberger

>> No.11044582

>>11044117
He has terminal Platonist AIDS and is in denial about his homofaggotry just like all platonists.
>>11044144
t. neurotypical herd animal
>>11044385
>i have 3 math classes
You have listed 2 math classes and a scam course castrati undergrads and their faggot parents are willing to pay for.

>> No.11044586

>>11043441
newfag

>> No.11044603

>>11044582
>pay
Tution is free where I live

Yes the logic foundations is just 2 hours per week without any mandatory exercises. Its just there to supplement the other two main classes and during the second part of the semester its very basic logic stuff.

>> No.11044697

>platonic realm
Cringe

>> No.11044878

>>11044582
This is a top tier post. This is why I come to /mg/.

>> No.11045065
File: 134 KB, 1279x708, 1568833186457.jpg [View same] [iqdb] [saucenao] [google]
11045065

>>11043096
This

>> No.11045186

>>11043096
Does he lurk /sci/?

>> No.11045271
File: 40 KB, 733x297, hensel&#039;s lemma.png [View same] [iqdb] [saucenao] [google]
11045271

>>11043085
Comm Alg bros, I know the endgame of this problem. I just don't understand how you get [math]g_{k+1},h_{k+1}[/math] from [math]g_k,h_k[/math] using his hint.

>> No.11045348
File: 10 KB, 250x189, reminder.jpg [View same] [iqdb] [saucenao] [google]
11045348

Threadly reminder to work with physicists

>> No.11045353

>>11045271
What practical applications does this have?

>> No.11045357
File: 451 KB, 822x904, yukari_pose.png [View same] [iqdb] [saucenao] [google]
11045357

>>11045348
Yeah a physicist probably wouldn't have posted a thumbnail

>> No.11045428

https://people.math.gatech.edu/~mbaker/pdf/ANTBook.pdf

Is this a good resource for studying Algebraic Number Theory?

>> No.11045496

>>11045428
Why don't you read it and find out?

>> No.11045560
File: 9 KB, 225x225, index.jpg [View same] [iqdb] [saucenao] [google]
11045560

*ting ting ting*
a-HEM fuck the axiom of choice and fuck LEM

>> No.11045572

>>11045560
agreed. I mean how can anyone think it's a true axiom, it leads to banach tarski for god's sake

>> No.11045589

>>11045357
i blame my third world internet, can only load the thumbnail
FeelsOkayMan.png

>> No.11045637

>>11045572
>Banach tarski is his objection
Nice try, high schooler

>> No.11045693

>>11045496
I am reading it

>> No.11045765

What book would you recommend for a review of calculus up to vector calculus, and linear algebra. And directions to go after that, say statistics? Also has self learning helped any of you with your career?
Im a biochem grad but dont want to spend my life waiting, purifying proteins and running gels. I'm hoping to join a comp bio lab. So maybe anything useful for CS and stats?

>> No.11045792

>dropped out of high school to go full NEET mode
>didn't get past algebra 1
>going back to CC since I'm not mentally ill anymore
>got placed into COLLEGE ALGEBRA
>everybody is complaining about the amount of homework and how we're going too fast
>I find it easy and finish the HW (usually 4-5 sections) in under an hour
>they're complaining about spending 8 hours on a single section
I'm a brainlet myself so just how stupid is the average person if they struggle with this? One of these people works at a bank.

>> No.11045821

>>11045765
>>11045792
>>>/sci/sqt

>> No.11045878

>>11045821
>>>/lgbt/discord

>> No.11045900
File: 9 KB, 402x155, Capture.png [View same] [iqdb] [saucenao] [google]
11045900

>>11043085

I am trying to understand proof by contradiction. Symbolically a proof by contraction should be the lemma which I have here. Shouldn't this be a tautology? Because when if you take the right most columns and say one implies the next, it's not always true. What am I missing here?

>> No.11045916

>>11045765
>>11045792
>>11045900
>>11045878
>>11045693
fuck off

>> No.11045932

>>11045916
>>11045821
go back to your containment board, butthurt discord tranny

>> No.11045969

>>11045916
>fuck off
Do you really need to swear?

>> No.11045970

>>11045900
>proof by contradiction
>>>/x/

>> No.11046001

>>11045900
[math]\neg \neg P[/math] is a weaker condition than [math]P[/math]

>> No.11046084
File: 154 KB, 1941x1846, q4h26.jpg [View same] [iqdb] [saucenao] [google]
11046084

>>11044118
>an actual math proof
>in /mg/

>> No.11046268

>>11045560
agreed. I mean how can anyone think it's a true axiom, it leads to non-measurable sets for god's sake

>> No.11046283

>>11046001
how so?

>> No.11046385

Is Khan Academy the way that math is going in general? I did a lot of algebra and calculus prep with KA and stuff in my calc textbook is way more difficult and eccentric. Why would the problems in KA be so easy?

>> No.11046503

>>11045572
>it leads to banach tarski
As much of a Paradox as Zeno's Paradox, which is to say not a Paradox at all.

>> No.11046508

>>11046283
If P holds, then its negation doesn't, so the negation's negation holds. On the other hand, if you want to be able to conclude P from its double negation, you need to postulate that "no-no" is a "yes". This can actually be approached by topology: Consider the lattice of open sets in a space, and note that an open set has the same exterior points as its closure. Using union for join, intersection for meet and "externalisation" for negation, you get a Heyting algebra out of your lattice. These can be used to formulate logic, and here not-not-U = ext(ext(U)), so x in not-not-U does not necessarily imply that x is U.

>> No.11046517

>>11046283
Only if you do not accept LEM, so nothing you should worry about.

>> No.11046534

>>11046283
schizotypical personality disorder

>> No.11046535

>>11046084
>that
>a math proof
go back to /mlg/ undergrad

>> No.11046656

Can I get a quick rundown on infinite dimensional integration and analysis?

>> No.11046666 [DELETED] 
File: 170 KB, 813x741, kripp.png [View same] [iqdb] [saucenao] [google]
11046666

>>11046001
Say you're hit on the head and when you wake up in a room without windows. You don't know for how long you were asleep. You're then asked whether it's day or night.

For a Boolean scenario, you may well argue that:
>It's either day or it's not day (D or not D)
(but you don't know which it is).

Now instead consider a modal knowledge semantics of intuitionistic logic (that ties to you as an agent). Both of the following don't apply:
>I have evidence that it's day
>I have evidence for it to be day or I have evidence for it to be not day (D or not D)
>If I don't have evidence that I don't have evidence that it's day, then I have evidence that it's day ((not(not D)) => D)
>I don't have evidence that I don't have evidence that it's day
Only the last of those four is true for you.

This is about whether you actually have a reason to believe. To put this is scope. If you model yourself as a self-aware and accurate reasoner, then you might also say
>If I have evidence that from my guard being asleep this implies it's night, then if I have evidence (reason to believe) that my guard is asleep, then I have also have evidence (reason to believe) it's night
B(X => Y) => (BX => BY)
(Here I use B for "Believe", or "Box", if you like it more abstractly)
>If I have evidence that it's day, then it's day (you know you're right if you came to some conclusion)
BX => X
>If I have evidence it's day, then I've evidence that I have evidence that it's day (you consider yours and maybe others convictions as evidence in itself)
BX => BBX
>If I have evidence that I have evidence that it's day, then it's day (similar to the third)
BBX => BX

The first 4 in pic related.

>>11045900
Classically, it's a tautology and it's not hard to see. Let's look at it semantically (with proof tables):
"not (P) or X" is "P or X" for any X
"Q and (not Q)" is F
"U implies V" is "(not X) or Y"
"not (not P)" is "P"
"P or F" is "P"
so we're left with
"P or (not (P) or Q)"
And now whatever P is, this is T

>> No.11046673
File: 170 KB, 813x741, kripp.png [View same] [iqdb] [saucenao] [google]
11046673

>>11046001
Say you're hit on the head and when you wake up in a room without windows. You don't know for how long you were asleep. You're then asked whether it's day or night.

For a Boolean scenario, you may well argue that:
>It's either day or it's not day (D or not D)
(but you don't know which it is).

Now instead consider a modal knowledge semantics of intuitionistic logic (that ties to you, as an agent).
>I have evidence that it's day
>I have evidence for it to be day or I have evidence for it to be not day (D or not D)
>If I don't have evidence that I don't have evidence that it's day, then I have evidence that it's day ((not(not D)) => D)
>I don't have evidence that I don't have evidence that it's day (not(not D))
Only the last of those four is true for you.

This is about whether you actually have a reason to believe. To put this is scope. If you model yourself as a self-aware and accurate reasoner, then you might also say
>If I have evidence that from my guard being asleep this implies it's night, then if I have evidence (reason to believe) that my guard is asleep, then I have also have evidence (reason to believe) it's night
B(X => Y) => (BX => BY)
(Here I use B for "Believe", or "Box", if you like it more abstractly)
>If I have evidence that it's day, then it's day (you know you're right if you came to some conclusion)
BX => X
>If I have evidence it's day, then I've evidence that I have evidence that it's day (you consider yours and maybe others convictions as evidence in itself)
BX => BBX
>If I have evidence that I have evidence that it's day, then it's day (similar to the third)
BBX => BX

All possible modal axioms, the first 4 in pic.

>>11045900
Classically, it's a tautology and it's not hard to see. Let's look at it semantically (with proof tables):
"not (P) or X" is "P or X" for any X
"Q and (not Q)" is F
"U implies V" is "(not X) or Y"
"not (not P)" is "P"
"P or F" is "P"
so we're left with
"P or (not (P) or Q)"
And now whatever P is, this is T

>> No.11046674

>>11045560
correct, axiom of choice is for brainlets: it makes things easier so you don't have to think in your proofs and in the end it leads you to a Banach-Tarski and well-ordering of real numbers. It's like drugs. That's why I'm working only in ZF. Can't say the same thing about LEM though because even if LEM makes things easier it does not provide any counter-intuitive results.

>> No.11046682
File: 319 KB, 760x1410, Screenshot_20191010-095032.png [View same] [iqdb] [saucenao] [google]
11046682

>>11046673
Note that when I say "the last is true for you", then I mean as part of this story scenario with you as the prisoner in the room and what you think.
I didn't want to implies that (not not P) is a tautology in intuitiinistic logic, nor do you need any other axioms about knowledge to use intuitiinistic logic. The logics studied by Gödel, Kripke etc. after the war are just richer logics that you never see in common core math that's fine with third-excluded-as-axiom (LEM, although "middle" may be misleading) semantics. In any case, even if not not P is weaker that P, it's classically equivalent and so you can just go with the former and flip it at the end. That goes with any classical statement, you can always prove them constructively (with evidence explicit) and flip it formally at the very end to get to the classical statement, i.e. you lose nothing by going with the agent centric perspective, you can prove the same statements (classically interpreted)

>> No.11046820

Threadly reminder that classical linear logic is the definitive constructive logic demystifying both classical and intuitionistic mathematics.

>> No.11046839

>>11045186
nobody lurks sci you faggot except shitty math sophomores

>> No.11046890

What does /mg/ think of the Infinitely Large Napkin?

https://venhance.github.io/napkin/Napkin.pdf

>> No.11046909

How does statistics work? Or rather why?
It seems magical.
As far as I understand, all statistics is based on the general assumption that
Y = F(X) + e
where e is the 'error'.
The error is always something you add to 'what it should be'. How did they arrive to this conclusion, that this is THE way to do it

>> No.11046912

>>11046890
there are thousands of textbooks already, why create another one

>> No.11046915

>>11043085
>What is induction

>> No.11046919

>>11046915
Its assuming that if it works for the first case, and that if you assume it works for some case you can show it works for the next case, then it must work for as many cases as you would like
which breaks down when you have an uncountable number of cases

>> No.11046926

What's a surjection between [math]\mathcal{P}(A) [/math] and [math]\mathcal{P}(B)[/math] given that [math]A\sim B[/math] ?

>> No.11046940

>>11046926
What do you mean by A~B?

>> No.11046942

>>11046940
Equipotent

>> No.11046946

>>11046942
The fuck is this retarded terminology LMAO. Just say they have the same cardinality.
And yes, to every bijection AB there corresponds a bijection P(A)P(B). Pick a bijection f: A->B and then for every subset X of A, let g(X)=image of X under f. You can easily prove that g is a bijection.

>> No.11047053

>>11046946
>Just say they have the same cardinality.
Not that guy, but that's literally the etymology of it
>equi = same
>potent = power (ie. old terminology for cardinal, as in "power of the continuum")

>> No.11047054

>>11046890
>>11046912
Because it's an index for higher level math. Very useful stuff.

>> No.11047103
File: 48 KB, 676x232, ch.png [View same] [iqdb] [saucenao] [google]
11047103

>>11046890
>>11047054
It's pretty and I like the effort.
It starts with basic vector spaces and then eventually mostly talks about algebraic topology and geometry and throws in a few dozen pages on quantum algorithms for factorization, Artin reciprocity, stuff like that. I don't imagine it's super clear and coherrent given it's under 1000 pages.
Was it edited (by a book editor)? Otherwise I'd think Algebra-Chapter-0 would be a better alternative. It's not like any first semester could really learn from it properly anyhow, even if the author may like to think so.
Cool he made an effort with colors and symbols and formatting.

>> No.11047131

>>11047103
https://dec41.user.srcf.net/notes/

I love these notetakers.

>> No.11047203

>>11047103
>We accept the Axiom of Choice, and use it freely.
Insta dropped

>> No.11047207

>tfw you feel incredibly guilty for liking graph theory
One of my professors snuck up behind me in our lounge and instead of switching to a different page I threw my laptop in the trash because I was reading a graph theory paper.

>> No.11047208

>>11047103
>>11047203
also, the author is a brainlet

>> No.11047221

>>11047207
Pretty sure he thought u wete watching porn

>> No.11047611

>>11046656
complete normed vector spaces.
measure theory.
just integrate.
many trivial results, some nontrivial ones (different forms of reisz rep, good forms of fredholm alternative, etc)

>> No.11047618

what do you think about Perelman?

>> No.11047626
File: 378 KB, 540x503, youkai_toot.png [View same] [iqdb] [saucenao] [google]
11047626

>>11046656
The "redpill", as they say, is that they are ill-defined. There is a sense in which you can perform differentiation and integration on Frechet functionals, but this is extremely constrained, and usually doesn't lend well to the usual applications where the functional integration involves a certain locus of an entire jet bundle.
In certain cases, these functional integrations can be performed implicitly. In Yang-Mills or Chern-Simons theories, for example, the partition function involves an integration of the Chern character and some symplectic form over the moduli space of [math]G[/math]-covariant connections, which can be performed implicitly by localization to saddle points fixed by the maximal torus of [math]G[/math] (Atiyah-Bott). In [math]G[/math]-TQFTs for finite [math]G[/math], on the other hand, the partition function [math]Z= \int e^{S} t^*s[/math] can be expressed as a "push-pull formalism" of maps between bordism groupoids carrying a Giibbs kernel, and localization can be similarly be performed. These are extremely special cases, however, and a general formulation for theories with non-trivial dynamics is still elusive.

>> No.11047628

>>11047626
>they are ill-defined
That's modern “physics'' summed up for you.

>> No.11047633

>>11047618
An absolute lad. His proof of the soul conjecture is kino.
10/10 would discuss waifus and geometry with him.

>> No.11047636

>>11047626
Thx for redpilling us.

What do you mean by "implicit" integration?
Also, can you say something general about limits of quotients of integrals (thinking of expectations here)

>> No.11047692
File: 1.05 MB, 764x1046, yukari13.png [View same] [iqdb] [saucenao] [google]
11047692

>>11047636
>What do you mean by "implicit" integration?
I meant that no actual integration has been performed, but only argued that it has the effect of "smearing out" contributions from non-saddle points so we just write down the saddle-point contribution. For equivariant fibre integration on oriented vector bundles, this is the essence of Atiyah-Bott.
>can you say something general about expectations
If you can find sequences of measures [math]d\mu_n[/math] that converges to the Gibbs measure [math]d\mu = D[\phi]e^{S}[/math] then it's definitely possible to regularize expressions like [math]\langle A(\phi)\rangle = \lim_n \frac{\int d\mu_n A(\phi)}{\int d\mu_n}[/math]. However, typically these measures are just better behaved (regularity-wise) and are still infinite-dimensional. You can try to section out finite-dimensional subspaces in the measure, but then convergence is extremely ill-behaved.
In certain special cases such as in CFT, we can again circumvent these difficulties by defining correlations geometrically by inserting primaries [math]\phi_i(z)[/math] into marked points of a Riemannian surface [math]\Sigma[/math]. By expressing the partition function [math]Z(\overline{q},q)[/math] (as a section of a V-bundle on moduli space of Riemann surfaces) in terms of the nome [math]q[/math] of the punctures you open up at the marked points, you can directly evaluate [math]\langle \prod_i \phi_i(z)\rangle[/math] by just "counting Virasoro weights" on [math]\overline{q},q[/math] using the factorization algebra. This is also an "implicit" evaluation similar to the Atiyah-Bott localization.

>> No.11047836

>>11046926
Let [math]f:A\to B[/math] be the bijection. Then define [math]\phi:\mathcal P(A)\to\mathcal P(B)[/math] by [math]E\subseteq A \mapsto f|_E (A)[/math], the restriction

>> No.11047837

>>11047836
correction, I meant [math]f|_E(E)[/math], of course

>> No.11047901

>>11047836
>>11047837
what a horrible post
the question was already answered AND you got it wrong once AND THEN you posted a fix that still was worse than the first answer that was given, which is just E \mapsto f(E). why the fuck are you restricting it you idiot.
jesus christ.

>> No.11047983

>>11047901
retard

>> No.11048048

What's the most mathematically elegant way to commit suicide?
I'm thinking it should use intuitionistic logic, but perhaps there's some absurd non-constructive method using choice.

>> No.11048068

What's the best linear algebra book that is more difficult and extensive than Axler, and more rigorous/explicit than Lang?

>> No.11048093

>>11048068
Lax, Kostikin and Manin, Roman. I can’t believe you read both Axler and Lang

>> No.11048172

>>11048068
I WILL WRITE A LINEAR ALGEBRA BOOK
IT WILL HAVE THE BEST GEOMETRY AND THE LEAST RIGOR
>>11048093
I've read Lang and a book with a baboon on the cover. Tragic shit.
Found out about Roman later, tho.

>> No.11048174

>>11048068
bourbaki

>> No.11048182

>>11048174
this, but completely and utterly unironically

>> No.11048560

>>11048068
>What's the best linear algebra book that is more difficult and extensive than Axler, and more rigorous/explicit than Lang?
Lang is a meme.

>> No.11048564

>>11048172
i dont care

>> No.11048962

>>11047628
Examples of "ill-defined" in modern physics?
Instant brainlet detector if you say qft path integrals.

>> No.11048966

>>11048068
A good litmus test for a linear algebra textbook is how it introduces a determinant. If it is not through exterior algebra, then the book is for brainlet engineers/social sciences.

>> No.11049083

>>11048093
I didn't, I've just tried both and didn't like either.
Thank you for the advice, I'll try those out!

>> No.11049220

>>11048048
you could choose to hurry up please

>> No.11049444

>>11048962
How's that not the canonical answer?

>> No.11049640

I hate stochastic calculus so much.
I just want to study analytic geometry.
How do people actually enjoy this dogshit?

>> No.11049696

>>11049640
study shadow calculus

>> No.11049712

Can anyone hook me up with the mathematicians tier list?

>> No.11049714

>>11048048
Just die without accomplishing anything. That's how most mathematicians die anwyway

>> No.11049726

>>11048048
study combinatorics

>> No.11049742

>>11049712
Niggas in my field>historical mathematicians>me>you lads>the rest.
>>11049726
He said he wants to die, not go to hell.

>> No.11049761

>>11045348
"No.". I don't work with animals.

>> No.11049936
File: 1.04 MB, 1163x1103, 3C00AEC1-6936-4AE2-B268-C9634FBDFC2A.jpg [View same] [iqdb] [saucenao] [google]
11049936

>Your brain in category theory.

>> No.11050016

>>11048560
No, Lang's Algebra and Lang's Basic Mathematics are memes. Lang's Linear Algebra is one of the best texts ever written.

>> No.11050020

>>11049936
Based Homo(A, B)
>The undergrad category theorist

>> No.11050111

I found a property I called "detail" that a subset of R^d can have at points. It is invariant under C1-Homeomorphisms. Is that useful?

The detail of omega at x is basically the image you would get if you infinitely zoomed into the set (It is a subset of the unit ball). So the detail of a corner of a square is a 90 degree edge, the detail on a point on a side is a line.
I defined it like this:
Detail(omega, x) =
{y: forall e > 0 exists c > 0: forall c' > c,
the e ball around y intersects with (omega - x)*c'}

Then I proved (hopefully correctly) that a C1 homeo has to conserve the detail at a point.
If anyone is interested I will post it, at the moment I only wrote it down in english and I suck at latex.

>> No.11050120

>>11050111
>90 degree edge
That isn't invariant under even smooth maps, that's a conformal invariant.

>> No.11050132

>>11050120
>>11050111
oh I forgot to mention something: the detail is unvariant up to linear isomorphism,
so what I got is that if f is the C1 homeo
Df(Detail(x)) = Detail(f(x)) (ignoring the normalization, but bc details are radially constant it doesnt matter.
So actually equivalence classes of S^d under isomorphism would be the invariants.

Not sure if it resolves the issue you mentioned though. But if you apply a smooth map to a 90 degree edge, you will locally basically apply a linear map, and thats what the detail looks at.
That's how I proved it, the C1 map is locally a linear one and then I just have to carefully play with the definitions and "how local" to get that the detail undergoes EXACTLY that linear map.

>> No.11050134

Should I study game theory? What is it good for?

>> No.11050381
File: 211 KB, 976x906, 1570484869999.png [View same] [iqdb] [saucenao] [google]
11050381

>>11046839
not true, FAG
>>11050134
lol, no. Study algebraic geometry.
>>11049936
>>11050020
BASED? BASED. "undergrad category theorist"
>>11048068
Artin.
>>11048048
Hahahahaa. Great question. Unfortunately, you are only allowed to commit suicide after you've published in a top tier journal. Now get to work, fag.
>>11047836
:(

>> No.11050416
File: 96 KB, 1170x228, 61103CB4-4D22-4621-932A-CC390FA137F8.jpg [View same] [iqdb] [saucenao] [google]
11050416

>>11050381
meme is real
https://www.twitter.com/_julesh_

>> No.11050505

>>11050416
just kill me now, this can't be real

>> No.11050522

>>11050505
He is worst and general community of Category theorist on twitter.

>> No.11050545

>>11050505
https://www.twitter.com/ququ7/status/1182638468339589120

>> No.11050555

>>11049936
So bullying category theorists get even easier, huh?

>> No.11050593
File: 3.58 MB, 640x358, both_lidar_radar.gif [View same] [iqdb] [saucenao] [google]
11050593

Motivating rant on Weierstrass factorization

https://youtu.be/SEHPs8nrqLY

>>11049712
My vote goes to Riemann

>>11049640
The bridge between stochastic processes (or the densities that capture them) and partial differential equations is pretty fascinating, and the integrals are fascinating. I agree that it's rather frustrating how there aren't to many examples once you go beyond the simple examples that have analytic situation. But on the flip-side, that stuff is actually useful. I work in tech and do nothing all day but trying to speed optimize Bayesian estimations on a Lie group.

>>11050020
>>11050522
Pretty sure that's a Scala programmer or something similar and "category theory" here means function composition and mapping over lists.
Not that I'm against the influence of those notions to the mainstream, but if category is explicitly declared just the means, then it doesn't fit the meme.

>> No.11050623
File: 6 KB, 724x176, fml.png [View same] [iqdb] [saucenao] [google]
11050623

just fuck my shit up fampai
>can't fail out of grad school if you can't get in

>> No.11050631

>>11050623
Well you wouldn’t have done yourself much good had you been allowed in anyways.

>> No.11050648

>>11050631
>remembering complex variables from 6 years ago correlates with your success in a phd program
fuck off

>> No.11050659

>>11043182
What in the fuck is that

>> No.11050819
File: 47 KB, 786x372, help.png [View same] [iqdb] [saucenao] [google]
11050819

Can someone help me explaining how he get those conclusion in these 3 red lines?

>> No.11050858

>>11050819
If A and B are subsets of C with at least 3/4 of elements, then at most 1/4 of B aren't already in A. In other words, the intersection is at least 1/2.
For the second one, you might find out why upon trying to find a counterexample to the claim.

>> No.11050906

>>11050623
GRE score has barely any effect on whether you get into a grad program. You did make sure to do undergrad research and get good letters of rec, right?

>> No.11051097

>>11050906
>GRE score has barely any effect on whether you get into a grad program
I wouldn't go that far. It's technically true that you can still get into _a_ grad program with any GRE score, but it does matter.
Sure, it's not the most important portion of your application, but it will raise eyebrows everywhere if you absolutely fucking tank it (can this guy not do calculus?), and most actually competitive schools have a soft cutoff to filter out the majority of applicants beneath like the 70th-80th percentile, unless there's an exceptional reason to keep them in the pool.

>> No.11051177 [DELETED] 
File: 353 KB, 450x600, 1570833445841.png [View same] [iqdb] [saucenao] [google]
11051177

>>11043110
>>11043146
>>11043182
>>11043612
>>11043855
>>11044106
>>11044118
>>11044143
>>11044203
>>11044205
>>11044233
>>11044236
>>11044246
>>11044247
>>11044259
>>11044337
>>11044385
>>11044426
>>11044444
>>11044465
>>11044486
>>11044494
>>11044497
>>11045271
>>11045765
>>11046001
>>11046503
>>11046508
>>11046673
>>11046674
>>11046682
>>11046909
>>11046926
>>11047103
>>11047692
>>11047836
>>11047837
>>11050111
>>11050132
>>11050593
>>11050819
>>11050858
>>11051097
what?

>> No.11051206

you know the deal, do not reply

>> No.11051213
File: 100 KB, 882x617, 1245873878383.jpg [View same] [iqdb] [saucenao] [google]
11051213

>>11051177

>> No.11051238

Damnit lad, what part of not replying didn't you get?
>>11050648
>complex variables from 6 years ago
You studied complex variables in high school?
>>11050545
>topologists invented some of it
>some
What did they mean by this?

>> No.11051284

I just had to show you the epic pic I had saved!

>> No.11051296
File: 371 KB, 775x581, 1551211960018.jpg [View same] [iqdb] [saucenao] [google]
11051296

someone explain finitists to me? what do they mean by infinite sets "dont exist"?

>> No.11051300

>>11051177
please explain your action

>> No.11051316

>>11043465
>Tatenda Kubalalika, University of Zimbabwe

Fucking kek

>> No.11051339

>>11051238
>You studied complex variables in high school?
no, i studied them my second year of undergrad. i've been in industry for 3 years.

>> No.11051385

>>11051339
yes ((((

>> No.11051427
File: 91 KB, 814x858, p1.png [View same] [iqdb] [saucenao] [google]
11051427

>>11050111
find mistake plz

>> No.11051438
File: 145 KB, 816x950, p2.png [View same] [iqdb] [saucenao] [google]
11051438

>>11051427

>> No.11051498 [DELETED] 
File: 273 KB, 517x396, 1538699466411.png [View same] [iqdb] [saucenao] [google]
11051498

>>11050111
>>11051427
>I defined some shit with a complicated formula
>is it useful??
It looks like your formula just says, if [math]\Omega[/math] in [math]\mathbb{R}[/math], then [math]Z(\Omega,0)[/math] is the set of directions [math]v[/math] where every small cone going out from 0 and centered around that cone intersects [math]\Omega[/math]. And [math]Z(\Omega,x)[/math] is the same thing after you shift [math]\Omega[/math] by [math]-x[/math]. So since it's something to do with directions, certainly you can express it in projective-geometry terms.

But it took a lot of work to figure even that much out. It would be easier if you explained what it's supposed to be for?? You claim at the top that something is invariant under homeomorphisms of [math]\mathbb{R}[/math], is that Z? Or is it this thing on page 2 called A? What is D in your Theorem 1?

>> No.11051511
File: 38 KB, 720x720, 1da7de4dfb70c5d55c9af4887a69151e6c57fa01d9f63ed29ae528855632873d.jpg [View same] [iqdb] [saucenao] [google]
11051511

>>11050111
>>11051427
>I defined some shit with a complicated formula
>is it useful??
It looks like your formula just says, if [math]\Omega[/math] is a subset of [math]R^d[/math], then [math]Z(\Omega,0)[/math] is the set of directions [math]v[/math] where every small cone going out from 0 and centred around that direction intersects [math]\Omega[/math]. And [math]Z(\Omega,x)[/math] is the same thing after you shift [math]\Omega[/math] over by [math]−x[/math]. So since it's something to do with directions, certainly you can express it in projective-geometry terms.

But it took a lot of work to figure even that much out. It would be easier if you explained what it's supposed to be for?? You claim at the top that something is invariant under homeomorphisms of [math]R^d[/math], is that [math]Z[/math]? But [math]Z[/math] isn't even invariant under rotations. Or is it this thing on page 2 called [math]A[/math]? What is [math]D[/math] supposed to be in your Theorem 1?

>> No.11051730

>>11050381
>le undergrad category theorist meme
>DO ALGEBRAIC GEOMETRY
you are the thing you hate

>> No.11051742

>>11049712
Well? Make your own.
https://tiermaker.com/create/mathematicians-48833
I'll make one too and post it.

>> No.11051748

>>11051730
No he isn't. Undergrads (often CS) buy into hype and try to study cat theory and be smug about it, but there is literally no point in categories if you already don't understand modules, rings, homology and cohomology, homotopy, etc.
If you read algtop properly then cat theory is necessary to move forward, it's what it was designed for afterall.

Oh, and you are a brainlet, in case you had any doubts.

>> No.11051757
File: 19 KB, 220x268, grothendieck.jpg [View same] [iqdb] [saucenao] [google]
11051757

>>11051748
>stumbling over herself to defend sucking off abstract nonsense to """"generalize"""" trivial topological invariants such as homology
you are the thing you hate

>> No.11051767

>>11051757
>abstract nonsense
Ah, so you are one of those who just parrots wikipedia but has no idea what he's talking about, good to know.

>> No.11051778

>>11045560
brainlet question. Why doesn't this work? I define a function that maps each real to a natural number by just picking an arbitrary real (which i can do because of meme axiom) and then (if i havent already assinged it to a number) map it to the lowest natural number with no numbers mapped to it. This is a bijection so R is countable.

>> No.11051779
File: 567 KB, 1166x676, math tierlist.png [View same] [iqdb] [saucenao] [google]
11051779

>>11049712
>>11051742
here you are.

>> No.11051782

>>11051778
you can't pick all the reals that way, you'll run out of natural numbers. cantor's diagonalization proof literally starts off by doing what you say and then finding a real which is not on your list.

>> No.11051788

>>11051782
i know that cantors diagonalization argument shows the reals have a greater cardinality than the naturals, but why cant I pick reals that way? Is there a better reason than "it just doesnt work because |R|>|N| so it cant work"

>> No.11051793

>>11051788
lol

>> No.11051794

>>11051767
no, i know full well what i'm talking about, and have used quite a bit of category theory myself in learning some elementary modern algebraic geometry and algebraic topology. i by no means claim to be an expert in either realm. at the same time, i have more than enough experience to know that the formalism is needlessly obscuring for anyone who thinks even the least bit geometrically, and distills something which should be a fine wine, juicy geometry with a refreshing kick of algebra, into a disgusting purely algebraic rubbing alcohol.

>> No.11051798

>>11051788
yes, that's why it doesn't work. no, you can't just do this. if you want to inductively pick elements of R to assign to elements of N, you'll need to use transfinite induction up to the ordinal of the continuum, and you'll run out of things to choose in N by the time you hit the first infinite ordinal. you obviously have no clue what transfinite induction is and how your little process is implicitly using it.

>> No.11051799
File: 101 KB, 785x731, soy2.jpg [View same] [iqdb] [saucenao] [google]
11051799

>>11051793
*I began choosing reals*
"HAHAHAHAAHA LOOK AT THIS RETARD"
*i reach 10*
"ok you can stop now this is retarded and pointless"
*i hit 50*
"please stop you cant count the reals"
*i have chosen 20 trillion reals and im still going*
NOOO SOMEBODY STOP HIM HES GOING TO COUNT THEM ALL

>> No.11051800

>>11051794
Well, category theory is definitely not needed to understand a sizeable bulk of algebraic topology and geometry, yes. But it's really invaluable in further reading, when many things are just defined as, say, a derived functor.

So I agree with you in a sense that, unless you are a pure mathematician aiming to get a phd, cat theory is unnecessary.

>> No.11051808

>>11051800
>unless you are a pure mathematician aiming to get a phd
no, unless you are a pure mathematician aiming to get a phd in specifically the fields of modern algebraic geometry or algebraic topology. or i suppose some moronic type theory thing, but no one gives a shit about that. and probably also arithmetic geometry.
and sure, i get the value of having it to just say "this is the thing which we see everywhere," but in my opinion wanting a language for that instead of just accepting yeah of course it's similar like a normal person is the kind of mentality which is ruining mathematics.

>> No.11051819

Infinite sets: That which has been found/expressed before will do so again.

>> No.11051838

>>11051808
Basically all modern pure math research requires understanding of cat theory.
Source: I read arxiv.org every day for a living.

>> No.11051841

>>11051838
>could use
sure
>requires
you need to branch out and read some papers from different fields then

>> No.11051855

>>11051841
There is no point in arguing with you since you are not familiar with what is actually published on arxiv. You can define Hochschild homologies of schemes without cat theory all you want.

Again, it's not my area of interest, it's the contents of around 90% of all recent papers. You completely miss the point and very obviously have an agenda/are biased against it.

>> No.11051872

>>11051778
youre going through the reals one by one
so youre starting from the assumption that the reals are countable, to prove that the reals are countable

>> No.11051905

>>11051855
ah yes, i'm sure all the analysis, combinatorics, dynamics, and number theory papers on arxiv right now make absolutely required use of category theory. you're a fucking hack.

>> No.11051954

>>11051778
Random pickup elements doesn't make for a function, however

>> No.11052027

>>11051757
>homologies
>trivial
Uuuh

>> No.11052029

>>11051788
Because an irrational number has no finite period. You can't write it down explictly in decimal form.

>> No.11052095

Has anyone got any good recommendations for (short) introductions to asymptotics? I never really looked into them

>> No.11052129

>>11047692
Is it true that in string theory (in CFT in general) the path integral somehow gets "finite-dimensional"? Can't express the details, sorry

>> No.11052133

>>11051511
>first paragraph
I considered if the definition by a cone is equivalent too, but I dont think it is so because your definition can be satisfied if omega has a sequence of points converging to x from the direction v, will ir doed not suffice in my definition bc for epsilon small enough and the right "zoom" you should be able to fit the Ball inside a gap in the sequence.

>second paragraph
I should've added more explanation ok.
Df(x) is the total derivative in x as a matrix of function
The theorem basically states that for Diffeomorphisms f:
Df(x) (Z(omega,x)) is in Z(f(Omega),f(x)).
I only introduced the A, because Df has to be normalized to safely map into B1(0).

And then the corollary does the same for the reverse direction with (Df)^-1 = D(f^-1) giving you that the isomorphism equivalence class of Z(omega, x) is the invariant that cant be changed by a Diffeomorphism.

This is useful because now you proved, for example, that a sauare is not diffeomorphic to a circle because the Detail in a corner of the square is not isomorphic to the Detail on the side of a circle (90° corner vs straight line).

But the theorem immediately shows this for all kinds of arbitrarily dimensional objects. I didnt even need to specify any regularity on Omega!
So if you have a set of volumes connected by surfaces and lines (in non differentiable fashion, i.e. with corners) then you can compute the details and possibly find it can not be diffeomorphic to another set.

>> No.11052134
File: 203 KB, 1080x1920, Screenshot_20191012-112000_Drive.jpg [View same] [iqdb] [saucenao] [google]
11052134

>>11052133

>> No.11052172
File: 273 KB, 517x396, 1538699466411.png [View same] [iqdb] [saucenao] [google]
11052172

>>11052133
>omega has a sequence of points converging to x from the direction v, will ir doed not suffice in my definition bc for epsilon small enough and the right "zoom" you should be able to fit the Ball inside a gap in the sequence
But then a bigger value of [math]\lambda[/math] will put the next element of the sequence into the ball.
>D is the derivative matrix
Then what is the type of [math] D f (x_0) \cdot x[/math]? It looks like a dot product, but I guess it's a function application?

Anyway, I believe your theorem, it makes sense. And I have enough information to tell you where to go looking for uses for it. Ask a professor about differential geometry. If you'd rather look in a book, try "Smooth Manifolds" by John Lee. That setting is more general than [math]\mathbb{R}^d[/math], however. I'm no expert myself and can't tell you whether they use this Detail or not.

>> No.11052202

>>11052172
>first
I didnt think about it thoroughly but the non-emptiness in the definition has to be true for all lambda after some point, so that's why choosing another lambda such that the sequence coincides with the ball again wouldn't work I think.
>Df
Df(x) = (del_ij f(x))ij so the matrix, but I used it interchangably as a function soo
So Df(x)*h = Df(x)(h). My analysis prof used this notation, maybe it's uncommon.

>manifolds
Yea I would be surprised if geometers haven't thought of that, but I'm not quite sure that manifolds are the right object to apply this on, because the details of differentiable shapes are generally boring.
I think what is much more interesting is that algebraic Varieties are exactly the kind of shape where the Detail is useful.
(x^2+y^2 - 1)*(z) = 0? You get a surface intersected by a line and the interesting detail "line intersects plane" in 0.
So maybe these details are algebraically computable and could help see what varieties are morphismic or smth like that (polynomial functions are C1-homeos).

Im going to be a faggot though and ask my prof if it's correct. I hope I'm not a cringeworthy undergrad.

>> No.11052273
File: 219 KB, 588x548, 68fd9311a46cca44836059a706bebde940dd56ccf26c3538d1e0a7dc970bb09f.gif [View same] [iqdb] [saucenao] [google]
11052273

>>11052202
>holes in the sequence can escape
Oh yeah, I guess you're right. Although since you're interested in smooth things, maybe a simpler definition with cones or whatever would equivalent enough, and easier to communicate.
>the details of differentiable shapes are generally boring.
I agree, but of course don't go around saying that IRL.
>(x^2+y^2 - 1)*(z) = 0? You get a surface intersected by a line
Looks like two surfaces unioned together desu. Anyway I think I see where you're going, and agree you'll need to ask an expert. A piece of advice for approaching: don't email or bring that latex along, just ask if he can help you with something you're not sure you're the inventor of, and explain it using a chalkboard. This will help avoid the "cringeworthiness" you're worried about.

>> No.11052298

>>11052273
>don't email or bring that latex along
oh well too late, thanks for the advice though

>> No.11052304

>>11043085
We can prove that there are infinite sets, based on our axioms. Now it's true that our axioms may be inconsistent, but no one has been able to find any inconsistency so we just hope they aren't.

>> No.11052308
File: 42 KB, 543x405, 1xop2q.jpg [View same] [iqdb] [saucenao] [google]
11052308

What is meant by "mathematical maturity"?

>> No.11052317

>>11052304
> We can prove that there are infinite sets, based on our axioms
What axioms? ZFC has an infinity axiom actually

>> No.11052325

>>11052308
Experience. Some combination of actual mathematical skills, and just, like, "noncommutative rings? oh yeah, I've seen something like that before except it was groups instead of rings, so I have an idea where this is going"

>> No.11052326
File: 99 KB, 280x210, 1236207118069.gif [View same] [iqdb] [saucenao] [google]
11052326

>>11052304
nobody has been able to get you laid, so let's just hope you never do

>> No.11052348

>>11052304
I don't think the consistency of ZFC is relevant to the discussion

>> No.11052496
File: 113 KB, 640x624, 71920902_981209168883886_2204431834853408768_n.jpg [View same] [iqdb] [saucenao] [google]
11052496

I don't understand the case (2) of the proof - does he not assume the result concerning the transcendence degree?

>choose a transcendence basis {e_1,...,e_r} of L/k such that a subset of it is a transcendence basis of M/k
>equivalently, trdeg L >= trdeg M

>> No.11052507

>>11052308
The ability to understand and extract the big picture from the small details, and vice versa

>> No.11052527
File: 308 KB, 708x448, adc5a4a011663b94e9d3852c510a512a.png [View same] [iqdb] [saucenao] [google]
11052527

which one of you did this, confess

>> No.11052581
File: 9 KB, 222x326, Cantor.jpg [View same] [iqdb] [saucenao] [google]
11052581

It is relatively consistent with ZFC that there exists an uncountable set of reals whose cardinality is strictly less than the continuum. We cannot explicitly construct a set with this property, since CH is independent of ZFC.

My question, however, is: assuming only ZFC, does there exist a "definable" set [math]X \subset \mathbb R[/math] which is provably uncountable, yet it is independent of ZFC whether [math]|X|=|\mathbb R|[/math]?

>> No.11052663 [DELETED] 
File: 198 KB, 1080x1349, 56337569_312634609449870_7002017531381367656_n.jpg [View same] [iqdb] [saucenao] [google]
11052663

>>11052581
I'd think so.
The ordinal-smallest such set of which we don't know if it's 2^w would be
https://en.wikipedia.org/wiki/First_uncountable_ordinal
Now all countable ordinal types are codable by subsets of N, i.e. elements of 2^w.
With that approach, if I understand you correctly, you're then asking whether they can all be coded at once (and we disregard isomorphic types) and gathered together to form a set in bijection with the the above.

>> No.11052667
File: 198 KB, 1080x1349, 56337569_312634609449870_7002017531381367656_n.jpg [View same] [iqdb] [saucenao] [google]
11052667

>>11052581
I'd think so.
The ordinal-smallest such set of which we don't know if its cardinality is |2^w0| would be w1.
https://en.wikipedia.org/wiki/First_uncountable_ordinal

Now all countable ordinal types are codable by subsets of w0, i.e. elements of 2^w0.
With the approach of gathering together all ordinal types to get w1, if I understand you correctly, you're then asking whether the types can all be coded at once (and we disregard isomorphic ones).

>> No.11052700

In every book it says that we look for derivative only in interiour points because otherwise the uniqueness might fail
>no one ever gives an example of that
WTF

>> No.11052706

>>11052700
y = |x|

left limit gives -1, right limit gives +1 derivative at 0

>> No.11052712

>>11052700
>>11052706
that of course, counts as a counterexample if you consider the function y=|x| on (0,1), for example

you cant define a slope if you dont have other points nearby in every direction to 'measure it against'

>> No.11052716

eg, how do you define the slope on a function [math]f:\{a\}\to\mathbb R[/math]?

>> No.11052720
File: 10 KB, 300x180, 2699.jpg [View same] [iqdb] [saucenao] [google]
11052720

>>11052667
I looked around a bit, and it seems you can embed the countable ordinals in Q and then enumerate those in w, so that you can then map those to R, and that's possible or all such ordinals

https://math.stackexchange.com/questions/123969/embedding-ordinals-in-mathbbq
followed by
https://math.stackexchange.com/questions/99589/injection-from-the-set-of-countable-ordinals-omega-into-mathbbr
A related construction is
https://en.wikipedia.org/wiki/Aronszajn_tree#Construction_of_a_special_Aronszajn_tree
but w.r.t. niceness, be aware that of course
https://en.wikipedia.org/wiki/Church%E2%80%93Kleene_ordinal
is among the countable still.

>> No.11052760

>>11052706
>>11052712
you should learn some logic, you can meaningfully define a derivative as long as the point where you are defining the derivative is a limit point of a domain of a function f
>>11052716
here a is not a limit point of {a}

>> No.11052764

>>11052720
Interesting, I'll look into it. Cheers anon

>> No.11052778

>>11043085
Hey, pls help me with the following ling alg. Proof.

Let [math] \boldsymbol{a,b,c} \in \mathbb{R}^n [/math] , show that:
[eqn]
\boldsymbol{a} \times ( \boldsymbol{b} \times \boldsymbol{c} ) = \boldsymbol{b} ( \boldsymbol{a} \dot \boldsymbol{c} ) - \boldsymbol{c} ( \boldsymbol{a} \dot \boldsymbol{b} ) [/eqn]
Pls help senpai

>> No.11052785

>>11052778
what have you tried?

>> No.11052789

>>11052778
Ffs
[math] \boldsymbol{a} \times ( \boldsymbol{b} \times \boldsymbol{c} ) = \boldsymbol{b} ( \boldsymbol{a} \dot \boldsymbol{c} ) - \boldsymbol{c} ( \boldsymbol{a} \dot \boldsymbol{b} ) [/math]

>> No.11052792
File: 12 KB, 200x200, bead9ff6ddc7c095d18968ec950edb4d.jpg [View same] [iqdb] [saucenao] [google]
11052792

I'm currently playing around in the area of holomorphic functions and am in this moment checking out pic related's papers on what he calls Coherent Spaces, which is essentially a rewrite of the theory of reproducing kernel Hilbert spaces where he really puts the vector space last
https://arxiv.org/pdf/1804.01402.pdf

If you look at his archive (I've linked it before here a few weeks ago), he published a book and I think the last 5 additions on the archive are those books in chapters - it's a technical critique of quantum mechanics interpretations (his thermal approach is to is, I think, one where expectations play the central role, over states and observables (there's an axiomatization of probability in terms of expectation values instead of densities (Kolmogorov)))
https://arxiv.org/search/?query=Arnold+Neumaier&searchtype=all

>>11052764
np, report back your findings

>> No.11052802

>>11052785
Idk why the tex code doesn't compile properly, it compiles just fine on texstudio.
Its ax(bxc) = b(a•b) - c(a•b)

>What have you tried
Ive tried using the identities but to no avail, everything is just too damn general, theres also no point in trying to brute force it. Even proving the R^3 particular case by brute force is an algebra nightmare.

>> No.11052808

>>11052792
amazing guy
https://www.physicsforums.com/insights/interview-mathematician-physicist-arnold-neumaier/

>> No.11052818

>>11052802
but cross-product is defined only in R^3
just checking that example by computing each sides should suffice, it's not as bad as you think, all vectors just have 3 coordinates you know how to compute scalar and cross products in R^3 so just do it.

>> No.11052820

[math]\mathbb{R} \in \geq[/math]

>> No.11052821

>>11052027
>the set of n-dimensional commutative loopy things in a topological space is so complicated! oh man!!!!
maybe if you're a fucking sophomore undergraduate
homotopy is literally obvious, and homology is the obvious way to improve it

>> No.11052840
File: 23 KB, 326x432, sector conformal.jpg [View same] [iqdb] [saucenao] [google]
11052840

>>11050111
i'll be honest, i haven't really read what you're doing in detail, but i'm curious about what happens when you look at, say, the open unit disk and a quarter plane in C. these are conformally equivalent, so C1 diffeomorphic and in fact smoothly diffeomorphic, but they would seem to have different detail at the origin on the quarter plane / at the corr. point on the disk. so do you only care about details of points in the set? or are these in fact the same detail?
on a similar note, your C1-ness reminds me of the flat torus in R^3, which is a C1-embedding with fractal structure. it seems a little tough to me to understand what the detail is, and why it's locally flat. maybe i just don't understand it well enough.
http://hevea-project.fr/ENPageToreDossierDePresse.html

>> No.11052845

>>11052700
check out sin(1/x) defined on (0, infinity)
it's perfectly differentiable, since it has a derivative at every point where it's defined.
but what should the derivative at 0 be?
this is stupid and gross, and no one wants to deal with it.

>> No.11052873

>>11052818
>Cross product is only defined in R^3
Technically, the "hard" definition it exist in only R^3 and R^7, but its defined in all other Rs with less strong conditions.

>> No.11052878
File: 75 KB, 500x572, 121112-knot9.jpg [View same] [iqdb] [saucenao] [google]
11052878

>>11052808
Nice read, thx.
Is physics forums worth it? Or is it just /sci/ with 3 more good people added?

>> No.11052890

>>11052818
>he doesn't know about the seven-dimensional cross product
Sad!

>> No.11052913

>>11052873
is it not in [math] \mathbb{R}^{2^n - 1} [/math] ?
I always just assumed there was one in R^15.

>> No.11052914
File: 27 KB, 274x424, Georg_Cantor3.jpg [View same] [iqdb] [saucenao] [google]
11052914

>>11043139
>>11043487
>Imagine making obscure videos on Youtube about the exact same topic while being wrong about it for literally 10 years. Just imagine that.
Imagine being wrong for literally 100 years.
>>11043139
reminder that "infinite sets" are a parlor trick that preoccupy those with neuroses and inferiority complexes

>> No.11052915

>>11051427
>>11051438
I improved the definition and texed it.
>counterexample
I don't fully understand what you mean, it seems like you'd say a full disk and a quarter disk are diffeomorphic.
Details are only supposed to be invariant up to isomorphism, and I Id say there is no linear function that takes a quarter disk (detail of quarter disk in 0) to a full disk (detail of full disk in 0), so that would disprove my theorem.

A further comment: I have to precise more that the way I used diffeomorphic is not entirely correct, I only proved the theorem for whole-R^d diffeomorphisms that take one set to a different one. If the diffeomorphism ends at the border of the set, I cant do my proof.

>flat torus
If something is wavy then the detail will not "converge".
Imagine sth like cos(1/x).
At 0 if you zoom in you will see oscillating waves. All the points in your B1(0) "view" that are touched will just not be in the detail. So the detail here would actually be a point I think.
As you can see details dont work as nicely as one hopes. But I just happened to find a (possible) proof for a useful theorem where *this* definition of detail is good enough.


Stronger definitions of detail could be made.
For example you might require that every point in B1(0) is in the detail of omega or the detail of R^d\omega. So there are no points which keep oscillating between inside and outside as you zoom in.

The ultimate killer would be to use the details of a set and their "configuration" to create a property that, if equal, implies diffeomorphic.
Then diffeimirohism classes = detail configs
But this would probably require a stronger definition of detail and many regularities in the sets and functions.
Would still be awesome though.

>> No.11052924

>>11052915
when you say isomorphism do you mean linear isomorphism?
an open disk and a quarter plane (and a quarter disk) are definitely diffeomorphic, but i doubt they are if you need something which extends to be diffeomorphic on all of R^d. i haven't proven it but that seems stupid.

>> No.11052933

>>11052924
Yea then the whole R'd diffeo is an important distinction.
I think what you could say is.
If the diffeomorphism can be extened to the closed hull distance epsilon from the boundary, then the whole thing works.
Or restricting to closed sets.

>> No.11052934

>>11052924
yes linear isomorphism

>> No.11052939

>>11052496
>choose a transcendence basis {e_1,...,e_r} of L/k such that a subset of it is a transcendence basis of M/k
Start by choosing the transcendence basis of M/k. Then you can extend it to a transcendence basis of L/k: this is probably implicit in an earlier result, since you already have a notion of transcendence degree. You're right that this appears to be part of the theorem they're proving, but you can write it off as (slightly) sloppy writing. Also, not relevant but:
>(e_1,...,e_r)
those "e"s are the Greek lower-case letter xi.

>> No.11052942

>>11052913
>R^{2^n-1}
Yeah, because of the quaternion-octonion-sedenion etc thing.
It just degenerates really fast, so by the time you reach R^15 it's already absolute dogshit.

>> No.11052953

>>11052924
The whole thing is basically just doing this heuristic rigorously:
C1-functions are locally linear.
The Detail in a point is the ultimate infinitely local behaviour of the set there.
So the detail behaves exactly like the total derivative of the function in the point!

>> No.11052966

>>11052933
yeah that definition should work. you probably don't want to have a diffeo between closed sets because a smooth map of closed sets is defined as one which can be extended to one on open sets containing the closed sets. but it does work - the condition you want comes up a lot in topology, the condition of "it is defined on an open set and can be extended to an open set which contains the closure of the domain"
this is some sort of remnant of local compactness.

>> No.11052969

>>11052953
yeah that makes a lot of sense
sounds like something a differential geometer/topologist would care about
>>11052942
oh shit i forgot about that garbage.
>nonassociative algebras

>> No.11052972

>>11052878
>physics forums worth it?
Today Stack sites Math and Physics outperformance it.

>> No.11052974

>reading a probability book
>it keeps giving new names for literally everything in real analysis
FUCK PROBABILITY THEORISTS
DO THEY HAVE SOME SORT OF MENTAL PROBLEM

>> No.11052978

>>11052974
anyone who decides to redo basic measure theory with le funny "normalize finite measure spaces to have measure 1 :)" meme is not right in the head

>> No.11052985
File: 22 KB, 749x155, intermediate_value_dream.jpg [View same] [iqdb] [saucenao] [google]
11052985

>>11052972
Well yeah I do have a SE account and it's helpful, but I didn't mean so much in terms of question-answer quality, but getting to know what's hot in fields I don't rigorously check.
There's no Neumaier types (actual profs) posting here (I assume)

>>11043139
>>11052914
Am I the only one enjoying this meme culture?

>> No.11053015

>>11044337
>>11044582
> lmao I love ANALysis I wish I could bugger weierstrass and suck on cantor's balls
> wildberger is a platonist
As if there weren't enough evidence that brainlets on sci don't know what they're talking about.

>> No.11053063

Why the fuck have we not formalized all mathematics in a database with some language to proof check new theorems automatically.
>hurr durr it takes too long to formalize
Bullshit, that's like saying creating software is impossible because it's just too slow to write everything in assembly.
A good language should have powerful tools to create and apply definitions and theorems. The time to write a proof formally will be 3-6 times longer than informally, but it will safe everyone a FUCKton of time and money because proof checking basically becomes unnecessary.
It would also allow us to start creating algorithms that create and prove new theorems. If you have a massive database you can use ML and it could do all the annoying details of the proof for you. It doesnt matter if its wrong, then you just do it yourself, but if it's right you will KNOW it's right because the proof works. It's like programming but you get a free green arrow when your program is 100% bug free, how amazing would that be.

>> No.11053066

>>11053063
please go away csnigger
>>11053015
please have iq

>> No.11053088
File: 138 KB, 1080x1349, sween.jpg [View same] [iqdb] [saucenao] [google]
11053088

>>11053063
The biggest such system for proof hording is the Polish Mizar project from the 80's++, but afaik it's pretty dead. And it's in a mildly typed setty language using Grothendieck universes (large cardinal universes around any set exists).

More realistically speaking, the Agda guys have a theorem library (if you want to describe it brutally, a dependently typed Haskell dialect)

https://en.wikipedia.org/wiki/Mizar_system
https://en.wikipedia.org/wiki/Agda_(programming_language)

>> No.11053090

>>11053066
tell me why it wouldn't work.
99% of mathematics are like this

def theorem(the objects that appear)
the statement
proof:
create variables, do transformations
some info = use(lemma)(objects you
want to use it on)
further steps
so statement

def definition "somespace" (some
objects)
definition
proof:
definition is well defined bc blabla

>> No.11053092

>>11053088
yea but these are not large scale efforts, they are more like side projects.
Also why does everyone focus so much on the logical aspect of what a language is based on, if the language is actually good it should allow you to do mathematics the same way you do them normally (mostly set theory I guess)

>> No.11053099
File: 13 KB, 255x255, a38b3b2ebaa75d3ce5610f363686019dfd921e46388fbf38ecb734e7d555c26c.jpg [View same] [iqdb] [saucenao] [google]
11053099

>>11052978
>probability theory is newer than measure theory and the latter was invented in a vacuum or perhaps in the service of abstract functional analysis
[DEEBLY GONZERNED]

>> No.11053100

>>11053090
you disgust me so deeply

>> No.11053103

>>11053063
>Why the fuck have we not formalized all mathematics in a database with some language to proof check new theorems automatically.
We effectively have. Lean has a library on GitHub.

>> No.11053106

>>11053092
Mathematics done by mathematicians isn't actually formal.
On the other hand, formal proofs are ludicrously long and mostly not helpful to humans.

>> No.11053119

>>11053106
maybe I am underestimating how informal research maths is, but it would not take long at all to formalize the typical all of undergrad Analysis textbook for example. The proofs of theorems arent insanely long when done rigorously. All the necessary epsilons and subset, properties and theorems used are stated usually.

>> No.11053121

>>11053099
yes, everything you posted is true.

>> No.11053138

>>11053119
>but it would not take long at all to formalize the typical all of undergrad Analysis textbook for example
Yeah maybe.
I mean I see your point that if you just want to get at the first 3 undergrad years, for computer affine inclined people to learn it quickly, to have a reference implementation.

>maybe I am underestimating how informal research maths is
It's reference to _versions of_ other theorems that other mathematicians know, and it's freely switching between isomorphic structures. It's glossing over any boring detail of equivalence relations (gigantic sets), which is a huge pain in formalization.

>> No.11053142

>have to take trig before i can do precalculus
jdimsa

>> No.11053150

>>11053090
gtfo

>> No.11053152

>>11053138
But if you express everything via universal properties to avoid the isomorphism issue, then every facet is defined via an adjoint functor and you end up with the undergrad cat theorists

And if you literally make equivalences into equalities, you end up with HoTT Twitter trannies

>> No.11053153

>>11053142
this is usually taught in precalculus, did you nof have enough hs math credits? see if you can test out of it (and also precalc), just pick up any precalculus book they cover everything on those placement tests, and if you work hard you can start calc right away.

>> No.11053157

>>11053138
>for computer affine people
no it's supposed to make research mathematics faster by solving proof checking

>isomorphisms
I can imagine this being a problem, but as far as I have seen yet isomorphisms are not specified to just save on notation. And the extra effort to specify as what kind of object you are interpreting some thing would be manageable.
In the end I cant know because im notns researcher, but all the mathematics I have seen so far were absolutely formalizeable with some effort. The deepest I am in any field is sobolev inequalities or things up to Nullstellensatz. The proof here would all be only a few times longer in code than they the way we did them.

>> No.11053166

>>11053157
>The deepest I am in any field is sobolev inequalities or things up to Nullstellensatz. The proof here would all be only a few times longer in code than they the way we did them.
You can literally look at the proofs people have made in formal systems such as coq, they're always pretty long (although this is normally because a single math-English sentence is doing a bunch of things at once when you look closely enough and formally enough)

Check out the model-theoretic proof of Nullstellensatz, by the way, it's kind of cool and not really the same as the normal one

>> No.11053171

>>11053157
You underestimate how messy mathematical objects are

https://en.m.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

Here on the top right you see a slick proof that n+m=m+n for naturals. Needs a lot of axioms, such as n+0=n.
Now look at the clusterfuck definition of the real numbers e.g. each are infinite sets of sequences with some properties, or infinite subsets of the rational and try go get anywhere.
It's an active field of research, patience.
Not going with sets, First order direct axiomatizations of the reals aren't categorical (no unique model) and so if you want to tie it to anything useful like your spaces, you need more morphisms and embeddings

>> No.11053173

>>11053157
>things up to Nullstellensatz
Even I know more algebraic geometry than that, and I hate the fucking shitty subject.
Christ, lad.

>> No.11053186

>>11053171
Or here's choice: Either your logic has subdomain (and thus your have no completeness, as you'd have for first order logic (which set theory is usually written in))
or you use the conventional logic and your theory has extra numbers (beyond all the ones you know) that nobody ever talks about
https://en.m.wikipedia.org/wiki/Non-standard_model_of_arithmetic

There's arbitrary much math out there, and some people are formalizing some. Anything that smells like point set topology will be hard to capture concisely

>> No.11053201

have you guys ever gone back to baby rudin to try to prove some of the theorems on your own?
They can be pretty hard, but I am a brainlet.

>> No.11053203

More advanced question this.

So modularity theorem associates every elliptic curve over the rationals with a weight 2 cusp form. The Langlands conjectures say basically every other object that is similar to a modular form is associated with an object which is similar to an elliptic curve.

My question is do we have any idea about what? Are there examples of weight 4 cusp forms (for example) which are associated with certain algebraic varieties? How about weight 0 Maass forms? Or Hilbert modular forms?

Do we have individual cases of association, and we conjecture that everything is associated, or do we have no associations whatsoever, but because they're there for elliptic curves and weight 2 cusp forms we feel there should be similar for other forms?

>> No.11053225

hey /mg/, uh... well...
what's [math]e^{log(0)}[/math] ?

>> No.11053228

>>11053225
log(0) is not defined.

>> No.11053230

>>11053225
undefined. Though the limit of e^(log(z)) as z tends to 0 (along anything other than the negative real line) is 0.

>> No.11053233

>>11053203
rusty on this subject but here's a partial answer starting from the non-analytic side:

the most well known case:
elliptic curves over Q are associated with modular forms of weight 2

generalizing the dimension of the geometric object:
singular K3 surfaces over Q are associated with modular forms of weight 3'
rigid Calabi-Yau manifolds over Q are associated with modular forms of weight 4

generalizing the field of definition:
elliptic curves over real quadratic fields are associated with certain forms

>> No.11053238

>>11053228
>>11053230
I get that it's not defined but doesn't the fact that we can use the identity [math]e^{log(x)} = x[/math] mean that we can easily conclude that it's equal to zero, moreover following the fact that the limit approaching it is 0 as well?

>> No.11053252

>>11053238
That identity does not hold true for every x.
Just because something has a limit doesn't mean it equals that limit, otherwise there'd be no point of limits in the first place.

>> No.11053254

>>11053233
Thanks for this. Wish I could find an example-heavy survey of these associations somewhere.

>>11053238
No. log(z) is not defined on any non-positive real number. The function exp(log(z)) therefore looks exactly like z but is undefined on the non-positive reals.
What you are noticing is that there is only one way to analytically extend the function onto the points where it's undefined. If we say f is an analytic function which we define as exp(log(z)) everywhere other than the non-positive reals, then f(0)=0.

>> No.11053256

>>11053063
you have no fucking idea how much money it would cost to maintain such a database, no one will ever fund that. And without the money fuck off, will ya

>> No.11053270

>>11053252
>>11053254
alright but the inverse identity [math]log(exp(x)) = x[/math] is certainly defined for [math]x = 0[/math] under the form of [math]log(1) = 0[/math]
I get that the standard definition of the first one is for [math]x > 0[/math], but doesn't the existence of its inverse prove that we can safely extend it to the 0 as well and conclude that [math]exp(log(0)) = 0[/math]?
Again, I get that you're trying to stay away from extending the standard definition to include the zero, all I'm asking is if nothing breaks and if the inverse has already been extended to [math]x = 0[/math] "safely", then what's the problem? The implication that [math]p^q = 0[/math] finally has a solution which breaks math?

>> No.11053272

>>11053256
I am certain that once you have such a database and ML has advanced by 10 years, you will be able to write proofs in Latey and 90% of it will be formalized automatically. The good thing is also that the program can know if it did somwthing correctly, bc it can check proofs.
Proof Assistance is exactly the kind of task where ML is better than hand written algorithms if given enough data.
It will be glorious, in 2040 you'll tell your computer some heuristic you came up with and it will try to formalize it, doing all the messy work. And it can do it any ugly way it wants to, if the proof is verified to work, it works.

>> No.11053280

>>11053270
"we can safely extend." Yes, we can. As I said, if you say "f is an analytic function defined as exp(log(z)) everywhere other than the non-positive reals" then f(0)=0.

However, if we just say "f(z)=exp(log(z))" then it is not defined at 0.

>> No.11053281

>>11053270
You shouldn't think of those two functions as inverses because exp(log(x)) is not defined on every point in the image of log(exp(x)).
>doesn't the existence of its inverse prove that we can safely extend it to the 0 as well and conclude that exp(log(0))=0?
You're going to have to clarify what you mean by "safely"

>> No.11053283

>>11053254
>Thanks for this. Wish I could find an example-heavy survey of these associations somewhere.
If you meant examples of associations, this may help when generalizing the geometric object:
https://arxiv.org/pdf/1212.4308.pdf

these aren't surveys, but when changing the field of definition, see the work of Siksek, looks like they've also shown it for totally real cubic fields:
https://arxiv.org/abs/1310.7088
https://arxiv.org/abs/1901.03436

If you want examples of specific curves or specific forms, try LMFDB,
http://www.lmfdb.org/EllipticCurve/Q/490160/h/3 (associated modular form is given)
http://www.lmfdb.org/EllipticCurve/2.2.5.1/4105.2/a/1 (associated Hilbert modular form is given)

>> No.11053307

>>11053272
what, ML advanced by 10 years will be able to finish people thoughts? It will be able to understand what people want to say even if people themselves do not know exactly what they want to say? You're dreaming, brother, this is some artificial intelligence shit right there and there's no guarantee it will exist at all, especially in 2040.

>> No.11053338

I've read somewhere that there does not exists a linear(?) ordering on C but isn't split it into cocentric circles with center at 0 and then say two complex numbers z1, z2: z1 <= z2 iff z1,z2 belong to two diffrent circles and radius of z1 circle is < radius of z2 or z1,z2 belong to the same sircle and by moving counterclockwise starting from the "real line" (x,0) the point we meet first will be a lesser one. Wouldn't that be a linear ordering on C?

>> No.11053346

>>11053173
congratulations you know literally the most elementary nontrivial result in alg geo, which a child could prove given a few hours

>> No.11053348

>>11053201
if you read the proofs in rudin the first time though instead of doing them yourself, you were never going to make it

>> No.11053351

>>11053338
no because then i <= 1 and i >= 1, but i is not equal to 1

>> No.11053352

Hey /mg/ how do I go about this?

Let [math] \sigma [/math] be a surface on spherical coordinates such that [math] r = 4, 20° \leq \theta \leq 180° , 45° \leq \phi \leq 125° [/math] find the flux of [math] \vec{F}(r, \theta, \phi) = [1/r^3 , 0, 0] [/math] thru [math] \sigma [/math]

>> No.11053353

>>11053338
>doesn't exist a linear ordering on C
It's literally bijective with R, which admits the usual linear ordering. Maybe there was some requirement on it?
The one you posted should also work.
>>11053346
I said more, ESL.

>> No.11053354

>>11053338
that is,
z1 <= z2 iff |z1| < |z2| or (|z1| = |z2| and Arg(z1) <= Arg(z2))

>> No.11053357

>>11053338
>>11053351
wait i fucked up, just kidding. didn't see the later part of your post. no, this is not a linear order because you're saying -1 > 0, which would then mean 0 > 1 when we add 1 to both sides.

>> No.11053358

>>11053351
i is not <= 1 because we meet 1 first
>>11053353
weird, I definitely remember there was something about "... does not exists ... ordering on C" what's the matter and I clrearly remember people all the time say "we can't compare complex numbers" Well, I'll look it up in a second

>> No.11053362

>>11053357
hmm, why should it be consistent with addition? I don't remember that being asked in a definition of ordering

>> No.11053363

>>11053307
If I write "My favourite burger recipe is this: " then current text completion algorithms can generate a fairly reasonable burger recipe.
And in the same way possibly in the future when I write "It is enough to prove it for f in Cinf with compact support" an AI can generate the details necessary to approximate f. All that's needed is lots and lots of data.

>> No.11053364

>>11053353
congratulations you defined an algebraically worthless order
and how much more? fucking idiot. i bet not much.
>>11053358
yeah i fixed it you idiot
there does not exist an order on C which respects the field structure

>> No.11053365

>>11053362
AN ORDERED FIELD HAS AN ORDER WHICH RESPECTS ADDITION
OTHERWISE IT IS WORTHLESS
IF YOU DO NOT CARE ABOUT ANYTHING BESIDES THE SET STRUCTURE OF C, CONGRATULATIONS, YOU ARE JUST LOOKING AT THE FUCKING CONTINUUM
HOLY SHIT.

>> No.11053371

>>11053352
integrate and use one of the big 3 theorems you learnt in class

>> No.11053372

>>11053364
>>11053365
You might want to calm down, lad.
>how much more
General theory of coherent sheaves on schemes.
Needed it for analytic geometry and GAGA results.

>> No.11053373

>>11053365
chill, bro, I just wanted to enumerate eigenvalues

>> No.11053403

>>11053371
The field is discontinous in r = 0 so I cant use gauß, stokes doesn't even apply here. How do I find a surface differential if the surface is so ill defined?

>> No.11053434

>>11053403
There is literally a contradiction in your assumptions, undergradfriend.

>> No.11053479

>>11053272
You are absolutely delusional, do you have any clue how much work something like this would take?

Firstly, there is no standardized tool for this, there are a many small projects with extremely limited cover.
Secondly, the effort to formalize mathematics is enormous, it isn't "twice as long" going from paper to machine formalizing something like most of linear algebra might reasonably take hundreds of thousands to millions of hours.
Thirdly computer proofs have little to do with LaTeX, or "Latey" as CS idiots say, so that pipe dream something that is never going to happen.
Fourthly, nobody care. For Companies it is beyond uninteresting, the general public couldn't be less interested and most mathematicians are smart enough to realize that they will be long dead before these things have any effect on their field, so there is only a tiny amount of people who have any interest in this.
Fifthly you are far too optimistic about this, try opening Lean, Coq, whatever and try to prove something trivial, like sqrt of 2 not being rational, also ML will have an EXTREMELY hard time with this because it basically fulfills everything which makes ML hard and useless, tiny sample size, no measure of optimality, very rigorous constraints.
Sixthly write proper English bc if u write like this you expose yourself as the idiot you are.

>> No.11053760

>>11053434
Pls explain

>> No.11054554
File: 114 KB, 1024x577, france.jpg [View same] [iqdb] [saucenao] [google]
11054554

>>11053372
>need it for GAGA
Into the trash it goes.

>> No.11054826

>>11053354
Using Arg is problematic because of the discontinuity at the negative real line. Better to do the same thing but using Cartesian coordinates, i.e.
z1 <= z2 iff Im(z1) < Im(z2) or (Im(z1) = Im(z2) and Re(z1) <= Re(z2))
That avoids the issues with Arg and has the added advantage of preserving the ordering of the reals. But as >>11053364 notes, the main issue with trying to order C is
> respects the field structure
An ordered field requires that
a<b => a+c<b+c
a>0∧b>0=>a·b>0
and there's no way to define such an ordering for C. Whatever ordering you come up with, either i>0 or -i>0, but i·i=-1 and (-i)·(-i)=-1.

>> No.11054831

yet again you NIGGERS are not going to link the new thread