The Future of Mathematics? [video] | Hacker News

october 2019 by nhaliday

https://news.ycombinator.com/item?id=20909404

Kevin Buzzard (the Lean guy)

- general reflection on proof asssistants/theorem provers

- Kevin Hale's formal abstracts project, etc

- thinks of available theorem provers, Lean is "[the only one currently available that may be capable of formalizing all of mathematics eventually]" (goes into more detail right at the end, eg, quotient types)

hn
commentary
discussion
video
talks
presentation
math
formal-methods
expert-experience
msr
frontier
state-of-art
proofs
rigor
education
higher-ed
optimism
prediction
lens
search
meta:research
speculation
exocortex
skunkworks
automation
research
math.NT
big-surf
software
parsimony
cost-benefit
intricacy
correctness
programming
pls
python
functional
haskell
heavyweights
research-program
review
reflection
multi
pdf
slides
oly
experiment
span-cover
git
vcs
teaching
impetus
academia
composition-decomposition
coupling-cohesion
database
trust
types
plt
lifts-projections
induction
critique
beauty
truth
elegance
aesthetics
Kevin Buzzard (the Lean guy)

- general reflection on proof asssistants/theorem provers

- Kevin Hale's formal abstracts project, etc

- thinks of available theorem provers, Lean is "[the only one currently available that may be capable of formalizing all of mathematics eventually]" (goes into more detail right at the end, eg, quotient types)

october 2019 by nhaliday

When is proof by contradiction necessary? | Gowers's Weblog

nibble org:bleg gowers mathtariat math proofs contradiction volo-avolo structure math.CA math.NT algebra parsimony elegance minimalism efficiency technical-writing necessity-sufficiency degrees-of-freedom simplification-normalization

october 2019 by nhaliday

nibble org:bleg gowers mathtariat math proofs contradiction volo-avolo structure math.CA math.NT algebra parsimony elegance minimalism efficiency technical-writing necessity-sufficiency degrees-of-freedom simplification-normalization

october 2019 by nhaliday

Purpose of proof: semi-formal methods : Inside 245-5D

techtariat reflection rhetoric contrarianism programming engineering formal-methods rigor proofs communication collaboration c(pp) concurrency plt correctness pragmatic math lens abstraction flux-stasis flexibility documentation system-design impetus ends-means technical-writing trust

august 2019 by nhaliday

techtariat reflection rhetoric contrarianism programming engineering formal-methods rigor proofs communication collaboration c(pp) concurrency plt correctness pragmatic math lens abstraction flux-stasis flexibility documentation system-design impetus ends-means technical-writing trust

august 2019 by nhaliday

big list - Are there proofs that you feel you did not "understand" for a long time? - MathOverflow

nibble q-n-a overflow soft-question big-list math proofs expert-experience heavyweights gowers mathtariat reflection learning intricacy grokkability intuition algebra math.GR motivation math.GN topology synthesis math.CT computation tcs logic iteration-recursion math.CA extrema smoothness span-cover grokkability-clarity

august 2019 by nhaliday

nibble q-n-a overflow soft-question big-list math proofs expert-experience heavyweights gowers mathtariat reflection learning intricacy grokkability intuition algebra math.GR motivation math.GN topology synthesis math.CT computation tcs logic iteration-recursion math.CA extrema smoothness span-cover grokkability-clarity

august 2019 by nhaliday

galois theory - Existence of irreducible polynomial of arbitrary degree over finite field without use of primitive element theorem? - Mathematics Stack Exchange

nibble q-n-a overflow math math.CA algebra multiplicative tidbits proofs existence pigeonhole-markov estimate fields identity measure

july 2019 by nhaliday

nibble q-n-a overflow math math.CA algebra multiplicative tidbits proofs existence pigeonhole-markov estimate fields identity measure

july 2019 by nhaliday

The Existential Risk of Math Errors - Gwern.net

july 2019 by nhaliday

How big is this upper bound? Mathematicians have often made errors in proofs. But it’s rarer for ideas to be accepted for a long time and then rejected. But we can divide errors into 2 basic cases corresponding to type I and type II errors:

1. Mistakes where the theorem is still true, but the proof was incorrect (type I)

2. Mistakes where the theorem was false, and the proof was also necessarily incorrect (type II)

Before someone comes up with a final answer, a mathematician may have many levels of intuition in formulating & working on the problem, but we’ll consider the final end-product where the mathematician feels satisfied that he has solved it. Case 1 is perhaps the most common case, with innumerable examples; this is sometimes due to mistakes in the proof that anyone would accept is a mistake, but many of these cases are due to changing standards of proof. For example, when David Hilbert discovered errors in Euclid’s proofs which no one noticed before, the theorems were still true, and the gaps more due to Hilbert being a modern mathematician thinking in terms of formal systems (which of course Euclid did not think in). (David Hilbert himself turns out to be a useful example of the other kind of error: his famous list of 23 problems was accompanied by definite opinions on the outcome of each problem and sometimes timings, several of which were wrong or questionable5.) Similarly, early calculus used ‘infinitesimals’ which were sometimes treated as being 0 and sometimes treated as an indefinitely small non-zero number; this was incoherent and strictly speaking, practically all of the calculus results were wrong because they relied on an incoherent concept - but of course the results were some of the greatest mathematical work ever conducted6 and when later mathematicians put calculus on a more rigorous footing, they immediately re-derived those results (sometimes with important qualifications), and doubtless as modern math evolves other fields have sometimes needed to go back and clean up the foundations and will in the future.7

...

Isaac Newton, incidentally, gave two proofs of the same solution to a problem in probability, one via enumeration and the other more abstract; the enumeration was correct, but the other proof totally wrong and this was not noticed for a long time, leading Stigler to remark:

...

TYPE I > TYPE II?

“Lefschetz was a purely intuitive mathematician. It was said of him that he had never given a completely correct proof, but had never made a wrong guess either.”

- Gian-Carlo Rota13

Case 2 is disturbing, since it is a case in which we wind up with false beliefs and also false beliefs about our beliefs (we no longer know that we don’t know). Case 2 could lead to extinction.

...

Except, errors do not seem to be evenly & randomly distributed between case 1 and case 2. There seem to be far more case 1s than case 2s, as already mentioned in the early calculus example: far more than 50% of the early calculus results were correct when checked more rigorously. Richard Hamming attributes to Ralph Boas a comment that while editing Mathematical Reviews that “of the new results in the papers reviewed most are true but the corresponding proofs are perhaps half the time plain wrong”.

...

Gian-Carlo Rota gives us an example with Hilbert:

...

Olga labored for three years; it turned out that all mistakes could be corrected without any major changes in the statement of the theorems. There was one exception, a paper Hilbert wrote in his old age, which could not be fixed; it was a purported proof of the continuum hypothesis, you will find it in a volume of the Mathematische Annalen of the early thirties.

...

Leslie Lamport advocates for machine-checked proofs and a more rigorous style of proofs similar to natural deduction, noting a mathematician acquaintance guesses at a broad error rate of 1/329 and that he routinely found mistakes in his own proofs and, worse, believed false conjectures30.

[more on these "structured proofs":

https://academia.stackexchange.com/questions/52435/does-anyone-actually-publish-structured-proofs

https://mathoverflow.net/questions/35727/community-experiences-writing-lamports-structured-proofs

]

We can probably add software to that list: early software engineering work found that, dismayingly, bug rates seem to be simply a function of lines of code, and one would expect diseconomies of scale. So one would expect that in going from the ~4,000 lines of code of the Microsoft DOS operating system kernel to the ~50,000,000 lines of code in Windows Server 2003 (with full systems of applications and libraries being even larger: the comprehensive Debian repository in 2007 contained ~323,551,126 lines of code) that the number of active bugs at any time would be… fairly large. Mathematical software is hopefully better, but practitioners still run into issues (eg Durán et al 2014, Fonseca et al 2017) and I don’t know of any research pinning down how buggy key mathematical systems like Mathematica are or how much published mathematics may be erroneous due to bugs. This general problem led to predictions of doom and spurred much research into automated proof-checking, static analysis, and functional languages31.

[related:

https://mathoverflow.net/questions/11517/computer-algebra-errors

I don't know any interesting bugs in symbolic algebra packages but I know a true, enlightening and entertaining story about something that looked like a bug but wasn't.

Define sinc𝑥=(sin𝑥)/𝑥.

Someone found the following result in an algebra package: ∫∞0𝑑𝑥sinc𝑥=𝜋/2

They then found the following results:

...

So of course when they got:

∫∞0𝑑𝑥sinc𝑥sinc(𝑥/3)sinc(𝑥/5)⋯sinc(𝑥/15)=(467807924713440738696537864469/935615849440640907310521750000)𝜋

hmm:

Which means that nobody knows Fourier analysis nowdays. Very sad and discouraging story... – fedja Jan 29 '10 at 18:47

--

Because the most popular systems are all commercial, they tend to guard their bug database rather closely -- making them public would seriously cut their sales. For example, for the open source project Sage (which is quite young), you can get a list of all the known bugs from this page. 1582 known issues on Feb.16th 2010 (which includes feature requests, problems with documentation, etc).

That is an order of magnitude less than the commercial systems. And it's not because it is better, it is because it is younger and smaller. It might be better, but until SAGE does a lot of analysis (about 40% of CAS bugs are there) and a fancy user interface (another 40%), it is too hard to compare.

I once ran a graduate course whose core topic was studying the fundamental disconnect between the algebraic nature of CAS and the analytic nature of the what it is mostly used for. There are issues of logic -- CASes work more or less in an intensional logic, while most of analysis is stated in a purely extensional fashion. There is no well-defined 'denotational semantics' for expressions-as-functions, which strongly contributes to the deeper bugs in CASes.]

...

Should such widely-believed conjectures as P≠NP or the Riemann hypothesis turn out be false, then because they are assumed by so many existing proofs, a far larger math holocaust would ensue38 - and our previous estimates of error rates will turn out to have been substantial underestimates. But it may be a cloud with a silver lining, if it doesn’t come at a time of danger.

https://mathoverflow.net/questions/338607/why-doesnt-mathematics-collapse-down-even-though-humans-quite-often-make-mista

more on formal methods in programming:

https://www.quantamagazine.org/formal-verification-creates-hacker-proof-code-20160920/

https://intelligence.org/2014/03/02/bob-constable/

https://softwareengineering.stackexchange.com/questions/375342/what-are-the-barriers-that-prevent-widespread-adoption-of-formal-methods

Update: measured effort

In the October 2018 issue of Communications of the ACM there is an interesting article about Formally verified software in the real world with some estimates of the effort.

Interestingly (based on OS development for military equipment), it seems that producing formally proved software requires 3.3 times more effort than with traditional engineering techniques. So it's really costly.

On the other hand, it requires 2.3 times less effort to get high security software this way than with traditionally engineered software if you add the effort to make such software certified at a high security level (EAL 7). So if you have high reliability or security requirements there is definitively a business case for going formal.

WHY DON'T PEOPLE USE FORMAL METHODS?: https://www.hillelwayne.com/post/why-dont-people-use-formal-methods/

You can see examples of how all of these look at Let’s Prove Leftpad. HOL4 and Isabelle are good examples of “independent theorem” specs, SPARK and Dafny have “embedded assertion” specs, and Coq and Agda have “dependent type” specs.6

If you squint a bit it looks like these three forms of code spec map to the three main domains of automated correctness checking: tests, contracts, and types. This is not a coincidence. Correctness is a spectrum, and formal verification is one extreme of that spectrum. As we reduce the rigour (and effort) of our verification we get simpler and narrower checks, whether that means limiting the explored state space, using weaker types, or pushing verification to the runtime. Any means of total specification then becomes a means of partial specification, and vice versa: many consider Cleanroom a formal verification technique, which primarily works by pushing code review far beyond what’s humanly possible.

...

The question, then: “is 90/95/99% correct significantly cheaper than 100% correct?” The answer is very yes. We all are comfortable saying that a codebase we’ve well-tested and well-typed is mostly correct modulo a few fixes in prod, and we’re even writing more than four lines of code a day. In fact, the vast… [more]

ratty
gwern
analysis
essay
realness
truth
correctness
reason
philosophy
math
proofs
formal-methods
cs
programming
engineering
worse-is-better/the-right-thing
intuition
giants
old-anglo
error
street-fighting
heuristic
zooming
risk
threat-modeling
software
lens
logic
inference
physics
differential
geometry
estimate
distribution
robust
speculation
nonlinearity
cost-benefit
convexity-curvature
measure
scale
trivia
cocktail
history
early-modern
europe
math.CA
rigor
news
org:mag
org:sci
miri-cfar
pdf
thesis
comparison
examples
org:junk
q-n-a
stackex
pragmatic
tradeoffs
cracker-prog
techtariat
invariance
DSL
chart
ecosystem
grokkability
heavyweights
CAS
static-dynamic
lower-bounds
complexity
tcs
open-problems
big-surf
ideas
certificates-recognition
proof-systems
PCP
mediterranean
SDP
meta:prediction
epistemic
questions
guessing
distributed
overflow
nibble
soft-question
track-record
big-list
hmm
frontier
state-of-art
move-fast-(and-break-things)
grokkability-clarity
technical-writing
trust
1. Mistakes where the theorem is still true, but the proof was incorrect (type I)

2. Mistakes where the theorem was false, and the proof was also necessarily incorrect (type II)

Before someone comes up with a final answer, a mathematician may have many levels of intuition in formulating & working on the problem, but we’ll consider the final end-product where the mathematician feels satisfied that he has solved it. Case 1 is perhaps the most common case, with innumerable examples; this is sometimes due to mistakes in the proof that anyone would accept is a mistake, but many of these cases are due to changing standards of proof. For example, when David Hilbert discovered errors in Euclid’s proofs which no one noticed before, the theorems were still true, and the gaps more due to Hilbert being a modern mathematician thinking in terms of formal systems (which of course Euclid did not think in). (David Hilbert himself turns out to be a useful example of the other kind of error: his famous list of 23 problems was accompanied by definite opinions on the outcome of each problem and sometimes timings, several of which were wrong or questionable5.) Similarly, early calculus used ‘infinitesimals’ which were sometimes treated as being 0 and sometimes treated as an indefinitely small non-zero number; this was incoherent and strictly speaking, practically all of the calculus results were wrong because they relied on an incoherent concept - but of course the results were some of the greatest mathematical work ever conducted6 and when later mathematicians put calculus on a more rigorous footing, they immediately re-derived those results (sometimes with important qualifications), and doubtless as modern math evolves other fields have sometimes needed to go back and clean up the foundations and will in the future.7

...

Isaac Newton, incidentally, gave two proofs of the same solution to a problem in probability, one via enumeration and the other more abstract; the enumeration was correct, but the other proof totally wrong and this was not noticed for a long time, leading Stigler to remark:

...

TYPE I > TYPE II?

“Lefschetz was a purely intuitive mathematician. It was said of him that he had never given a completely correct proof, but had never made a wrong guess either.”

- Gian-Carlo Rota13

Case 2 is disturbing, since it is a case in which we wind up with false beliefs and also false beliefs about our beliefs (we no longer know that we don’t know). Case 2 could lead to extinction.

...

Except, errors do not seem to be evenly & randomly distributed between case 1 and case 2. There seem to be far more case 1s than case 2s, as already mentioned in the early calculus example: far more than 50% of the early calculus results were correct when checked more rigorously. Richard Hamming attributes to Ralph Boas a comment that while editing Mathematical Reviews that “of the new results in the papers reviewed most are true but the corresponding proofs are perhaps half the time plain wrong”.

...

Gian-Carlo Rota gives us an example with Hilbert:

...

Olga labored for three years; it turned out that all mistakes could be corrected without any major changes in the statement of the theorems. There was one exception, a paper Hilbert wrote in his old age, which could not be fixed; it was a purported proof of the continuum hypothesis, you will find it in a volume of the Mathematische Annalen of the early thirties.

...

Leslie Lamport advocates for machine-checked proofs and a more rigorous style of proofs similar to natural deduction, noting a mathematician acquaintance guesses at a broad error rate of 1/329 and that he routinely found mistakes in his own proofs and, worse, believed false conjectures30.

[more on these "structured proofs":

https://academia.stackexchange.com/questions/52435/does-anyone-actually-publish-structured-proofs

https://mathoverflow.net/questions/35727/community-experiences-writing-lamports-structured-proofs

]

We can probably add software to that list: early software engineering work found that, dismayingly, bug rates seem to be simply a function of lines of code, and one would expect diseconomies of scale. So one would expect that in going from the ~4,000 lines of code of the Microsoft DOS operating system kernel to the ~50,000,000 lines of code in Windows Server 2003 (with full systems of applications and libraries being even larger: the comprehensive Debian repository in 2007 contained ~323,551,126 lines of code) that the number of active bugs at any time would be… fairly large. Mathematical software is hopefully better, but practitioners still run into issues (eg Durán et al 2014, Fonseca et al 2017) and I don’t know of any research pinning down how buggy key mathematical systems like Mathematica are or how much published mathematics may be erroneous due to bugs. This general problem led to predictions of doom and spurred much research into automated proof-checking, static analysis, and functional languages31.

[related:

https://mathoverflow.net/questions/11517/computer-algebra-errors

I don't know any interesting bugs in symbolic algebra packages but I know a true, enlightening and entertaining story about something that looked like a bug but wasn't.

Define sinc𝑥=(sin𝑥)/𝑥.

Someone found the following result in an algebra package: ∫∞0𝑑𝑥sinc𝑥=𝜋/2

They then found the following results:

...

So of course when they got:

∫∞0𝑑𝑥sinc𝑥sinc(𝑥/3)sinc(𝑥/5)⋯sinc(𝑥/15)=(467807924713440738696537864469/935615849440640907310521750000)𝜋

hmm:

Which means that nobody knows Fourier analysis nowdays. Very sad and discouraging story... – fedja Jan 29 '10 at 18:47

--

Because the most popular systems are all commercial, they tend to guard their bug database rather closely -- making them public would seriously cut their sales. For example, for the open source project Sage (which is quite young), you can get a list of all the known bugs from this page. 1582 known issues on Feb.16th 2010 (which includes feature requests, problems with documentation, etc).

That is an order of magnitude less than the commercial systems. And it's not because it is better, it is because it is younger and smaller. It might be better, but until SAGE does a lot of analysis (about 40% of CAS bugs are there) and a fancy user interface (another 40%), it is too hard to compare.

I once ran a graduate course whose core topic was studying the fundamental disconnect between the algebraic nature of CAS and the analytic nature of the what it is mostly used for. There are issues of logic -- CASes work more or less in an intensional logic, while most of analysis is stated in a purely extensional fashion. There is no well-defined 'denotational semantics' for expressions-as-functions, which strongly contributes to the deeper bugs in CASes.]

...

Should such widely-believed conjectures as P≠NP or the Riemann hypothesis turn out be false, then because they are assumed by so many existing proofs, a far larger math holocaust would ensue38 - and our previous estimates of error rates will turn out to have been substantial underestimates. But it may be a cloud with a silver lining, if it doesn’t come at a time of danger.

https://mathoverflow.net/questions/338607/why-doesnt-mathematics-collapse-down-even-though-humans-quite-often-make-mista

more on formal methods in programming:

https://www.quantamagazine.org/formal-verification-creates-hacker-proof-code-20160920/

https://intelligence.org/2014/03/02/bob-constable/

https://softwareengineering.stackexchange.com/questions/375342/what-are-the-barriers-that-prevent-widespread-adoption-of-formal-methods

Update: measured effort

In the October 2018 issue of Communications of the ACM there is an interesting article about Formally verified software in the real world with some estimates of the effort.

Interestingly (based on OS development for military equipment), it seems that producing formally proved software requires 3.3 times more effort than with traditional engineering techniques. So it's really costly.

On the other hand, it requires 2.3 times less effort to get high security software this way than with traditionally engineered software if you add the effort to make such software certified at a high security level (EAL 7). So if you have high reliability or security requirements there is definitively a business case for going formal.

WHY DON'T PEOPLE USE FORMAL METHODS?: https://www.hillelwayne.com/post/why-dont-people-use-formal-methods/

You can see examples of how all of these look at Let’s Prove Leftpad. HOL4 and Isabelle are good examples of “independent theorem” specs, SPARK and Dafny have “embedded assertion” specs, and Coq and Agda have “dependent type” specs.6

If you squint a bit it looks like these three forms of code spec map to the three main domains of automated correctness checking: tests, contracts, and types. This is not a coincidence. Correctness is a spectrum, and formal verification is one extreme of that spectrum. As we reduce the rigour (and effort) of our verification we get simpler and narrower checks, whether that means limiting the explored state space, using weaker types, or pushing verification to the runtime. Any means of total specification then becomes a means of partial specification, and vice versa: many consider Cleanroom a formal verification technique, which primarily works by pushing code review far beyond what’s humanly possible.

...

The question, then: “is 90/95/99% correct significantly cheaper than 100% correct?” The answer is very yes. We all are comfortable saying that a codebase we’ve well-tested and well-typed is mostly correct modulo a few fixes in prod, and we’re even writing more than four lines of code a day. In fact, the vast… [more]

july 2019 by nhaliday

What's the expected level of paper for top conferences in Computer Science - Academia Stack Exchange

june 2019 by nhaliday

Top. The top level.

My experience on program committees for STOC, FOCS, ITCS, SODA, SOCG, etc., is that there are FAR more submissions of publishable quality than can be accepted into the conference. By "publishable quality" I mean a well-written presentation of a novel, interesting, and non-trivial result within the scope of the conference.

...

There are several questions that come up over and over in the FOCS/STOC review cycle:

- How surprising / novel / elegant / interesting is the result?

- How surprising / novel / elegant / interesting / general are the techniques?

- How technically difficult is the result? Ironically, FOCS and STOC committees have a reputation for ignoring the distinction between trivial (easy to derive from scratch) and nondeterministically trivial (easy to understand after the fact).

- What is the expected impact of this result? Is this paper going to change the way people do theoretical computer science over the next five years?

- Is the result of general interest to the theoretical computer science community? Or is it only of interest to a narrow subcommunity? In particular, if the topic is outside the STOC/FOCS mainstream—say, for example, computational topology—does the paper do a good job of explaining and motivating the results to a typical STOC/FOCS audience?

nibble
q-n-a
overflow
academia
tcs
cs
meta:research
publishing
scholar
lens
properties
cost-benefit
analysis
impetus
increase-decrease
soft-question
motivation
proofs
search
complexity
analogy
problem-solving
elegance
synthesis
hi-order-bits
novelty
discovery
My experience on program committees for STOC, FOCS, ITCS, SODA, SOCG, etc., is that there are FAR more submissions of publishable quality than can be accepted into the conference. By "publishable quality" I mean a well-written presentation of a novel, interesting, and non-trivial result within the scope of the conference.

...

There are several questions that come up over and over in the FOCS/STOC review cycle:

- How surprising / novel / elegant / interesting is the result?

- How surprising / novel / elegant / interesting / general are the techniques?

- How technically difficult is the result? Ironically, FOCS and STOC committees have a reputation for ignoring the distinction between trivial (easy to derive from scratch) and nondeterministically trivial (easy to understand after the fact).

- What is the expected impact of this result? Is this paper going to change the way people do theoretical computer science over the next five years?

- Is the result of general interest to the theoretical computer science community? Or is it only of interest to a narrow subcommunity? In particular, if the topic is outside the STOC/FOCS mainstream—say, for example, computational topology—does the paper do a good job of explaining and motivating the results to a typical STOC/FOCS audience?

june 2019 by nhaliday

Computer Scientists Close In on Unique Games Conjecture Proof | Quanta Magazine

news org:mag org:sci popsci tcs cs computation UGC complexity approximation lower-bounds hardness nibble org:inst rand-approx proofs big-surf announcement SDP optimization open-problems questions research

june 2018 by nhaliday

news org:mag org:sci popsci tcs cs computation UGC complexity approximation lower-bounds hardness nibble org:inst rand-approx proofs big-surf announcement SDP optimization open-problems questions research

june 2018 by nhaliday

gn.general topology - Pair of curves joining opposite corners of a square must intersect---proof? - MathOverflow

october 2017 by nhaliday

In his 'Ordinary Differential Equations' (sec. 1.2) V.I. Arnold says "... every pair of curves in the square joining different pairs of opposite corners must intersect".

This is obvious geometrically but I was wondering how one could go about proving this rigorously. I have thought of a proof using Brouwer's Fixed Point Theorem which I describe below. I would greatly appreciate the group's comments on whether this proof is right and if a simpler proof is possible.

...

Since the full Jordan curve theorem is quite subtle, it might be worth pointing out that theorem in question reduces to the Jordan curve theorem for polygons, which is easier.

Suppose on the contrary that the curves A,BA,B joining opposite corners do not meet. Since A,BA,B are closed sets, their minimum distance apart is some ε>0ε>0. By compactness, each of A,BA,B can be partitioned into finitely many arcs, each of which lies in a disk of diameter <ε/3<ε/3. Then, by a homotopy inside each disk we can replace A,BA,B by polygonal paths A′,B′A′,B′ that join the opposite corners of the square and are still disjoint.

Also, we can replace A′,B′A′,B′ by simple polygonal paths A″,B″A″,B″ by omitting loops. Now we can close A″A″ to a polygon, and B″B″ goes from its "inside" to "outside" without meeting it, contrary to the Jordan curve theorem for polygons.

- John Stillwell

nibble
q-n-a
overflow
math
geometry
topology
tidbits
intricacy
intersection
proofs
gotchas
oly
mathtariat
fixed-point
math.AT
manifolds
intersection-connectedness
This is obvious geometrically but I was wondering how one could go about proving this rigorously. I have thought of a proof using Brouwer's Fixed Point Theorem which I describe below. I would greatly appreciate the group's comments on whether this proof is right and if a simpler proof is possible.

...

Since the full Jordan curve theorem is quite subtle, it might be worth pointing out that theorem in question reduces to the Jordan curve theorem for polygons, which is easier.

Suppose on the contrary that the curves A,BA,B joining opposite corners do not meet. Since A,BA,B are closed sets, their minimum distance apart is some ε>0ε>0. By compactness, each of A,BA,B can be partitioned into finitely many arcs, each of which lies in a disk of diameter <ε/3<ε/3. Then, by a homotopy inside each disk we can replace A,BA,B by polygonal paths A′,B′A′,B′ that join the opposite corners of the square and are still disjoint.

Also, we can replace A′,B′A′,B′ by simple polygonal paths A″,B″A″,B″ by omitting loops. Now we can close A″A″ to a polygon, and B″B″ goes from its "inside" to "outside" without meeting it, contrary to the Jordan curve theorem for polygons.

- John Stillwell

october 2017 by nhaliday

Section 10 Chi-squared goodness-of-fit test.

october 2017 by nhaliday

- pf that chi-squared statistic for Pearson's test (multinomial goodness-of-fit) actually has chi-squared distribution asymptotically

- the gotcha: terms Z_j in sum aren't independent

- solution:

- compute the covariance matrix of the terms to be E[Z_iZ_j] = -sqrt(p_ip_j)

- note that an equivalent way of sampling the Z_j is to take a random standard Gaussian and project onto the plane orthogonal to (sqrt(p_1), sqrt(p_2), ..., sqrt(p_r))

- that is equivalent to just sampling a Gaussian w/ 1 less dimension (hence df=r-1)

QED

pdf
nibble
lecture-notes
mit
stats
hypothesis-testing
acm
probability
methodology
proofs
iidness
distribution
limits
identity
direction
lifts-projections
- the gotcha: terms Z_j in sum aren't independent

- solution:

- compute the covariance matrix of the terms to be E[Z_iZ_j] = -sqrt(p_ip_j)

- note that an equivalent way of sampling the Z_j is to take a random standard Gaussian and project onto the plane orthogonal to (sqrt(p_1), sqrt(p_2), ..., sqrt(p_r))

- that is equivalent to just sampling a Gaussian w/ 1 less dimension (hence df=r-1)

QED

october 2017 by nhaliday

self study - Looking for a good and complete probability and statistics book - Cross Validated

october 2017 by nhaliday

I never had the opportunity to visit a stats course from a math faculty. I am looking for a probability theory and statistics book that is complete and self-sufficient. By complete I mean that it contains all the proofs and not just states results.

nibble
q-n-a
overflow
data-science
stats
methodology
books
recommendations
list
top-n
confluence
proofs
rigor
reference
accretion
october 2017 by nhaliday

newtonian gravity - Newton's original proof of gravitation for non-point-mass objects - Physics Stack Exchange

september 2017 by nhaliday

This theorem is Proposition LXXI, Theorem XXXI in the Principia. To warm up, consider the more straightforward proof of the preceding theorem, that there's no inverse-square force inside of a spherical shell:

picture

The crux of the argument is that the triangles HPI and LPK are similar. The mass enclosed in the small-but-near patch of sphere HI goes like the square of the distance HP, while the mass enclosed in the large-but-far patch of sphere KL, with the same solid angle, goes like the square of the distance KP. This mass ratio cancels out the distance-squared ratio governing the strength of the force, and so the net force from those two patches vanishes.

For a point mass outside a shell, Newton's approach is essentially the same as the modern approach:

picture

One integral is removed because we're considering a thin spherical shell rather than a solid sphere. The second integral, "as the semi-circle AKB revolves about the diameter AB," trivially turns Newton's infinitesimal arcs HI and KL into annuli.

The third integral is over all the annuli in the sphere, over 0≤ϕ≤τ/20≤ϕ≤τ/2 or over R−r≤s≤R+rR−r≤s≤R+r. This one is a little bit hairy, even with the advantage of modern notation.

Newton's clever trick is to consider the relationship between the force due to the smaller, nearer annulus HI and the larger, farther annulus KL defined by the same viewing angle (in modern notation, dθdθ). If I understand correctly he argues again, based on lots of similar triangles with infinitesimal angles, that the smaller-but-nearer annulus and the larger-but-farther annulus exert the same force at P. Furthermore, he shows that the force doesn't depend on the distance PF, and thus doesn't depend on the radius of the sphere; the only parameter left is the distance PS (squared) between the particle and the sphere's center. Since the argument doesn't depend on the angle HPS, it's true for all the annuli, and the theorem is proved.

nibble
q-n-a
overflow
giants
old-anglo
the-trenches
physics
mechanics
gravity
proofs
symmetry
geometry
spatial
picture

The crux of the argument is that the triangles HPI and LPK are similar. The mass enclosed in the small-but-near patch of sphere HI goes like the square of the distance HP, while the mass enclosed in the large-but-far patch of sphere KL, with the same solid angle, goes like the square of the distance KP. This mass ratio cancels out the distance-squared ratio governing the strength of the force, and so the net force from those two patches vanishes.

For a point mass outside a shell, Newton's approach is essentially the same as the modern approach:

picture

One integral is removed because we're considering a thin spherical shell rather than a solid sphere. The second integral, "as the semi-circle AKB revolves about the diameter AB," trivially turns Newton's infinitesimal arcs HI and KL into annuli.

The third integral is over all the annuli in the sphere, over 0≤ϕ≤τ/20≤ϕ≤τ/2 or over R−r≤s≤R+rR−r≤s≤R+r. This one is a little bit hairy, even with the advantage of modern notation.

Newton's clever trick is to consider the relationship between the force due to the smaller, nearer annulus HI and the larger, farther annulus KL defined by the same viewing angle (in modern notation, dθdθ). If I understand correctly he argues again, based on lots of similar triangles with infinitesimal angles, that the smaller-but-nearer annulus and the larger-but-farther annulus exert the same force at P. Furthermore, he shows that the force doesn't depend on the distance PF, and thus doesn't depend on the radius of the sphere; the only parameter left is the distance PS (squared) between the particle and the sphere's center. Since the argument doesn't depend on the angle HPS, it's true for all the annuli, and the theorem is proved.

september 2017 by nhaliday

Physics 152: Gravity, Fluids, Waves, Heat

september 2017 by nhaliday

lots of good lecture notes with pictures, worked examples, and simulations

unit
org:edu
org:junk
course
physics
mechanics
gravity
tidbits
symmetry
calculation
examples
lecture-notes
simulation
dynamic
dynamical
visualization
visual-understanding
ground-up
fluid
waves
oscillation
thermo
stat-mech
p:whenever
accretion
math.CA
hi-order-bits
nitty-gritty
linearity
spatial
space
entropy-like
temperature
proofs
yoga
plots
september 2017 by nhaliday

Inscribed angle - Wikipedia

august 2017 by nhaliday

pf:

- for triangle w/ one side = a diameter, draw isosceles triangle and use supplementary angle identities

- otherwise draw second triangle w/ side = a diameter, and use above result twice

nibble
math
geometry
spatial
ground-up
wiki
reference
proofs
identity
levers
yoga
- for triangle w/ one side = a diameter, draw isosceles triangle and use supplementary angle identities

- otherwise draw second triangle w/ side = a diameter, and use above result twice

august 2017 by nhaliday

Separating Hyperplane Theorems

august 2017 by nhaliday

also has supporting hyperplane theorems

pdf
lecture-notes
nibble
exposition
caltech
acm
math
math.CA
curvature
optimization
proofs
existence
levers
atoms
yoga
convexity-curvature
august 2017 by nhaliday

Lecture 7: Convex Problems, Separation Theorems

august 2017 by nhaliday

Supporting Hyperplane Theorem

Separating Hyperplane Theorems

pdf
nibble
lectures
slides
exposition
proofs
acm
math
math.CA
optimization
curvature
existence
duality
levers
atoms
yoga
convexity-curvature
Separating Hyperplane Theorems

august 2017 by nhaliday

Subgradients - S. Boyd and L. Vandenberghe

august 2017 by nhaliday

If f is convex and x ∈ int dom f, then ∂f(x) is nonempty and bounded. To establish that ∂f(x) ≠ ∅, we apply the supporting hyperplane theorem to the convex set epi f at the boundary point (x, f(x)), ...

pdf
nibble
lecture-notes
acm
optimization
curvature
math.CA
estimate
linearity
differential
existence
proofs
exposition
atoms
math
marginal
convexity-curvature
august 2017 by nhaliday

Roche limit - Wikipedia

july 2017 by nhaliday

In celestial mechanics, the Roche limit (pronounced /ʁɔʃ/) or Roche radius, is the distance within which a celestial body, held together only by its own gravity, will disintegrate due to a second celestial body's tidal forces exceeding the first body's gravitational self-attraction.[1] Inside the Roche limit, orbiting material disperses and forms rings whereas outside the limit material tends to coalesce. The term is named after Édouard Roche, who is the French astronomer who first calculated this theoretical limit in 1848.[2]

space
physics
gravity
mechanics
wiki
reference
nibble
phase-transition
proofs
tidbits
identity
marginal
july 2017 by nhaliday

co.combinatorics - Classification of Platonic solids - MathOverflow

july 2017 by nhaliday

My question is very basic: where can I find a complete (and hopefully self-contained) proof of the classification of Platonic solids? In all the references that I found, they use Euler's formula v−e+f=2v−e+f=2 to show that there are exactly five possible triples (v,e,f)(v,e,f). But of course this is not a complete proof because it does not rule out the possibility of different configurations or deformations. Has anyone ever written up a complete proof of this statement?!

...

This is a classical question. Here is my reading of it: Why is there a unique polytope with given combinatorics of faces, which are all regular polygons? Of course, for simple polytopes (tetrahedron, cube, dodecahedron) this is clear, but for the octahedron and icosahedron this is less clear.

The answer lies in the Cauchy's theorem. It was Legendre, while writing his Elements of Geometry and Trigonometry, noticed that Euclid's proof is incomplete in the Elements. Curiously, Euclid finds both radii of inscribed and circumscribed spheres (correctly) without ever explaining why they exist. Cauchy worked out a proof while still a student in 1813, more or less specifically for this purpose. The proof also had a technical gap which was found and patched up by Steinitz in 1920s.

The complete (corrected) proof can be found in the celebrated Proofs from the Book, or in Marcel Berger's Geometry. My book gives a bit more of historical context and some soft arguments (ch. 19). It's worth comparing this proof with (an erroneous) pre-Steinitz exposition, say in Hadamard's Leçons de Géométrie Elémentaire II, or with an early post-Steinitz correct but tedious proof given in (otherwise, excellent) Alexandrov's monograph (see also ch.26 in my book which compares all the approaches).

P.S. Note that Coxeter in Regular Polytopes can completely avoid this issue but taking a different (modern) definition of the regular polytopes (which are symmetric under group actions). For a modern exposition and the state of art of this approach, see McMullen and Schulte's Abstract Regular Polytopes.

https://en.wikipedia.org/wiki/Platonic_solid#Classification

https://mathoverflow.net/questions/46502/on-the-number-of-archimedean-solids

q-n-a
overflow
math
topology
geometry
math.CO
history
iron-age
mediterranean
the-classics
multi
curiosity
clarity
proofs
nibble
wiki
reference
characterization
uniqueness
list
ground-up
grokkability-clarity
...

This is a classical question. Here is my reading of it: Why is there a unique polytope with given combinatorics of faces, which are all regular polygons? Of course, for simple polytopes (tetrahedron, cube, dodecahedron) this is clear, but for the octahedron and icosahedron this is less clear.

The answer lies in the Cauchy's theorem. It was Legendre, while writing his Elements of Geometry and Trigonometry, noticed that Euclid's proof is incomplete in the Elements. Curiously, Euclid finds both radii of inscribed and circumscribed spheres (correctly) without ever explaining why they exist. Cauchy worked out a proof while still a student in 1813, more or less specifically for this purpose. The proof also had a technical gap which was found and patched up by Steinitz in 1920s.

The complete (corrected) proof can be found in the celebrated Proofs from the Book, or in Marcel Berger's Geometry. My book gives a bit more of historical context and some soft arguments (ch. 19). It's worth comparing this proof with (an erroneous) pre-Steinitz exposition, say in Hadamard's Leçons de Géométrie Elémentaire II, or with an early post-Steinitz correct but tedious proof given in (otherwise, excellent) Alexandrov's monograph (see also ch.26 in my book which compares all the approaches).

P.S. Note that Coxeter in Regular Polytopes can completely avoid this issue but taking a different (modern) definition of the regular polytopes (which are symmetric under group actions). For a modern exposition and the state of art of this approach, see McMullen and Schulte's Abstract Regular Polytopes.

https://en.wikipedia.org/wiki/Platonic_solid#Classification

https://mathoverflow.net/questions/46502/on-the-number-of-archimedean-solids

july 2017 by nhaliday

Lecture 6: Nash Equilibrum Existence

june 2017 by nhaliday

pf:

- For mixed strategy profile p ∈ Δ(A), let g_ij(p) = gain for player i to switch to pure strategy j.

- Define y: Δ(A) -> Δ(A) by y_ij(p) ∝ p_ij + g_ij(p) (normalizing constant = 1 + ∑_k g_ik(p)).

- Look at fixed point of y.

pdf
nibble
lecture-notes
exposition
acm
game-theory
proofs
math
topology
existence
fixed-point
simplex
equilibrium
ground-up
- For mixed strategy profile p ∈ Δ(A), let g_ij(p) = gain for player i to switch to pure strategy j.

- Define y: Δ(A) -> Δ(A) by y_ij(p) ∝ p_ij + g_ij(p) (normalizing constant = 1 + ∑_k g_ik(p)).

- Look at fixed point of y.

june 2017 by nhaliday

Von Neumann–Morgenstern utility theorem - Wikipedia

economics micro game-theory values models existence uniqueness characterization wiki reference nibble proofs ORFE expectancy formal-values decision-making decision-theory acm definition outcome-risk linearity von-neumann giants

april 2017 by nhaliday

economics micro game-theory values models existence uniqueness characterization wiki reference nibble proofs ORFE expectancy formal-values decision-making decision-theory acm definition outcome-risk linearity von-neumann giants

april 2017 by nhaliday

Sets with Small Intersection | Academically Interesting

march 2017 by nhaliday

- nice application of LLL lemma

- reference for the "not hard to show" claim: https://homes.cs.washington.edu/~anuprao/pubs/CSE599sExtremal/lecture3.pdf

I think there are some typos, eg, inequality in last line should be reversed (we already have an upper bound on sum d(x), want a lower bound)

cf also Exercise 2.14 and Section 13.6 in Jukna's Extremal Combinatorics, and the Erdös–Ko–Rado Theorem in Alon-Spencer

more:

https://arxiv.org/abs/1404.4622

https://mathoverflow.net/questions/64596/minimal-intersecting-subsets

https://mathoverflow.net/questions/175969/an-upper-bound-on-families-of-subsets-with-a-small-pairwise-intersection

https://mathoverflow.net/questions/21245/pairwise-intersecting-sets-of-fixed-size

ratty
clever-rats
acmtariat
org:bleg
nibble
math
math.CO
tidbits
probability
probabilistic-method
intersection
rigidity
magnitude
combo-optimization
intersection-connectedness
multi
pdf
proofs
extrema
estimate
bare-hands
q-n-a
overflow
preprint
papers
pseudorandomness
tcs
complexity
- reference for the "not hard to show" claim: https://homes.cs.washington.edu/~anuprao/pubs/CSE599sExtremal/lecture3.pdf

I think there are some typos, eg, inequality in last line should be reversed (we already have an upper bound on sum d(x), want a lower bound)

cf also Exercise 2.14 and Section 13.6 in Jukna's Extremal Combinatorics, and the Erdös–Ko–Rado Theorem in Alon-Spencer

more:

https://arxiv.org/abs/1404.4622

https://mathoverflow.net/questions/64596/minimal-intersecting-subsets

https://mathoverflow.net/questions/175969/an-upper-bound-on-families-of-subsets-with-a-small-pairwise-intersection

https://mathoverflow.net/questions/21245/pairwise-intersecting-sets-of-fixed-size

march 2017 by nhaliday

Redistributing from Capitalists to Workers: An Impossibility Theorem, Garett Jones | EconLog | Library of Economics and Liberty

february 2017 by nhaliday

good comment by Ghost

http://mason.gmu.edu/~gjonesb/ChamleyJuddWorker.pdf

http://econlog.econlib.org/archives/2013/04/a_while_ago_i_w.html

http://marginalrevolution.com/marginalrevolution/2014/04/garett-jones-reviews-piketty.html

http://johnhcochrane.blogspot.com/2013/03/taxation-of-capital-and-labor.html

http://www.forbes.com/sites/timworstall/2014/04/27/contra-thomas-piketty-its-impossible-to-benefit-the-worker-by-taxing-capital/

http://www.separatinghyperplanes.com/2014/04/be-careful-how-you-wield-chamley-judd.html

http://www.nber.org/papers/w4525

http://www.dailykos.com/story/2014/4/28/1295399/-The-1-disproves-Piketty-s-book-about-Capital

The Redistribution Impossibility Theorem: http://mason.gmu.edu/~gjonesb/RedistributionImpossibilityRedux.pdf

An open economy exposition

org:econlib
econotariat
spearhead
garett-jones
economics
policy
rhetoric
thinking
analysis
no-go
redistribution
labor
taxes
cracker-econ
multi
piketty
news
org:lite
org:biz
pdf
links
political-econ
capital
simulation
operational
dynamic
explanation
time-preference
patience
wonkish
study
science-anxiety
externalities
long-short-run
models
map-territory
stylized-facts
s:*
broad-econ
chart
article
🎩
randy-ayndy
envy
bootstraps
inequality
absolute-relative
X-not-about-Y
volo-avolo
ideas
status
capitalism
nationalism-globalism
metabuch
optimate
aristos
open-closed
macro
government
proofs
equilibrium
http://mason.gmu.edu/~gjonesb/ChamleyJuddWorker.pdf

http://econlog.econlib.org/archives/2013/04/a_while_ago_i_w.html

http://marginalrevolution.com/marginalrevolution/2014/04/garett-jones-reviews-piketty.html

http://johnhcochrane.blogspot.com/2013/03/taxation-of-capital-and-labor.html

http://www.forbes.com/sites/timworstall/2014/04/27/contra-thomas-piketty-its-impossible-to-benefit-the-worker-by-taxing-capital/

http://www.separatinghyperplanes.com/2014/04/be-careful-how-you-wield-chamley-judd.html

http://www.nber.org/papers/w4525

http://www.dailykos.com/story/2014/4/28/1295399/-The-1-disproves-Piketty-s-book-about-Capital

The Redistribution Impossibility Theorem: http://mason.gmu.edu/~gjonesb/RedistributionImpossibilityRedux.pdf

An open economy exposition

february 2017 by nhaliday

Hoeffding’s Inequality

february 2017 by nhaliday

basic idea of standard pf: bound e^{tX} by line segment (convexity) then use Taylor expansion (in p = b/(b-a), the fraction of range to right of 0) of logarithm

pdf
lecture-notes
exposition
nibble
concentration-of-measure
estimate
proofs
ground-up
acm
probability
series
s:null
february 2017 by nhaliday

CS229 Supplemental Lecture notes: Hoeffding’s inequality

february 2017 by nhaliday

- weaker by a constant factor

- uses symmetrization instead of Taylor series

pdf
lecture-notes
exposition
nibble
proofs
concentration-of-measure
estimate
machine-learning
acm
probability
math
moments
ground-up
stanford
symmetry
curvature
convexity-curvature
- uses symmetrization instead of Taylor series

february 2017 by nhaliday

mg.metric geometry - What is the best way to peel fruit? - MathOverflow

q-n-a overflow nibble math acm sublinear metrics metric-space proofs math.CO tcstariat arrows reduction measure math.MG similarity multi papers survey computational-geometry cs algorithms pdf positivity msr tidbits intersection curvature convexity-curvature intersection-connectedness signum

february 2017 by nhaliday

q-n-a overflow nibble math acm sublinear metrics metric-space proofs math.CO tcstariat arrows reduction measure math.MG similarity multi papers survey computational-geometry cs algorithms pdf positivity msr tidbits intersection curvature convexity-curvature intersection-connectedness signum

february 2017 by nhaliday

inequalities - Is the Jaccard distance a distance? - MathOverflow

february 2017 by nhaliday

Steinhaus Transform

the referenced survey: http://kenclarkson.org/nn_survey/p.pdf

It's known that this transformation produces a metric from a metric. Now if you take as the base metric D the symmetric difference between two sets, what you end up with is the Jaccard distance (which actually is known by many other names as well).

q-n-a
overflow
nibble
math
acm
sublinear
metrics
metric-space
proofs
math.CO
tcstariat
arrows
reduction
measure
math.MG
similarity
multi
papers
survey
computational-geometry
cs
algorithms
pdf
positivity
msr
tidbits
intersection
curvature
convexity-curvature
intersection-connectedness
signum
the referenced survey: http://kenclarkson.org/nn_survey/p.pdf

It's known that this transformation produces a metric from a metric. Now if you take as the base metric D the symmetric difference between two sets, what you end up with is the Jaccard distance (which actually is known by many other names as well).

february 2017 by nhaliday

big list - Overarching reasons why problems are in P or BPP - Theoretical Computer Science Stack Exchange

q-n-a overflow nibble tcs complexity algorithms linear-algebra polynomials markov monte-carlo DP math.CO greedy math.NT synthesis list big-list hi-order-bits big-picture aaronson tcstariat graphs graph-theory proofs structure tricki yoga mathtariat time-complexity top-n metabuch metameta skeleton s:*** chart knowledge curvature convexity-curvature

february 2017 by nhaliday

q-n-a overflow nibble tcs complexity algorithms linear-algebra polynomials markov monte-carlo DP math.CO greedy math.NT synthesis list big-list hi-order-bits big-picture aaronson tcstariat graphs graph-theory proofs structure tricki yoga mathtariat time-complexity top-n metabuch metameta skeleton s:*** chart knowledge curvature convexity-curvature

february 2017 by nhaliday

Equivalence between counting and sampling

february 2017 by nhaliday

also: every counting problem either has FPTRAS or no approx. w/i polynomial factor

pdf
exposition
lecture-notes
berkeley
nibble
tcs
counting
sampling
characterization
complexity
approximation
rand-approx
proofs
february 2017 by nhaliday

A map of the Tricki | Tricki

gowers wiki reference math problem-solving proofs structure list top-n synthesis hi-order-bits tricks yoga scholar tricki metabuch 👳 toolkit unit duplication insight intuition meta:math better-explained metameta wisdom skeleton p:whenever s:*** chart knowledge org:mat elegance

february 2017 by nhaliday

gowers wiki reference math problem-solving proofs structure list top-n synthesis hi-order-bits tricks yoga scholar tricki metabuch 👳 toolkit unit duplication insight intuition meta:math better-explained metameta wisdom skeleton p:whenever s:*** chart knowledge org:mat elegance

february 2017 by nhaliday

Structure theorem for finitely generated modules over a principal ideal domain - Wikipedia

february 2017 by nhaliday

- finitely generative modules over PID isomorphic to sum of quotients by decreasing sequences of proper ideals

- never really understood the proof of this in Ma5b

math
algebra
characterization
levers
math.AC
wiki
reference
nibble
proofs
additive
arrows
- never really understood the proof of this in Ma5b

february 2017 by nhaliday

References for TCS proof techniques - Theoretical Computer Science Stack Exchange

q-n-a overflow tcs complexity proofs structure meta:math problem-solving yoga 👳 synthesis encyclopedic list big-list nibble tricki p:someday knowledge princeton sanjeev-arora lecture-notes elegance advanced

february 2017 by nhaliday

q-n-a overflow tcs complexity proofs structure meta:math problem-solving yoga 👳 synthesis encyclopedic list big-list nibble tricki p:someday knowledge princeton sanjeev-arora lecture-notes elegance advanced

february 2017 by nhaliday

bounds - What is the variance of the maximum of a sample? - Cross Validated

february 2017 by nhaliday

- sum of variances is always a bound

- can't do better even for iid Bernoulli

- looks like nice argument from well-known probabilist (using E[(X-Y)^2] = 2Var X), but not clear to me how he gets to sum_i instead of sum_{i,j} in the union bound?

edit: argument is that, for j = argmax_k Y_k, we have r < X_i - Y_j <= X_i - Y_i for all i, including i = argmax_k X_k

- different proof here (later pages): http://www.ism.ac.jp/editsec/aism/pdf/047_1_0185.pdf

Var(X_n:n) <= sum Var(X_k:n) + 2 sum_{i < j} Cov(X_i:n, X_j:n) = Var(sum X_k:n) = Var(sum X_k) = nσ^2

why are the covariances nonnegative? (are they?). intuitively seems true.

- for that, see https://pinboard.in/u:nhaliday/b:ed4466204bb1

- note that this proof shows more generally that sum Var(X_k:n) <= sum Var(X_k)

- apparently that holds for dependent X_k too? http://mathoverflow.net/a/96943/20644

q-n-a
overflow
stats
acm
distribution
tails
bias-variance
moments
estimate
magnitude
probability
iidness
tidbits
concentration-of-measure
multi
orders
levers
extrema
nibble
bonferroni
coarse-fine
expert
symmetry
s:*
expert-experience
proofs
- can't do better even for iid Bernoulli

- looks like nice argument from well-known probabilist (using E[(X-Y)^2] = 2Var X), but not clear to me how he gets to sum_i instead of sum_{i,j} in the union bound?

edit: argument is that, for j = argmax_k Y_k, we have r < X_i - Y_j <= X_i - Y_i for all i, including i = argmax_k X_k

- different proof here (later pages): http://www.ism.ac.jp/editsec/aism/pdf/047_1_0185.pdf

Var(X_n:n) <= sum Var(X_k:n) + 2 sum_{i < j} Cov(X_i:n, X_j:n) = Var(sum X_k:n) = Var(sum X_k) = nσ^2

why are the covariances nonnegative? (are they?). intuitively seems true.

- for that, see https://pinboard.in/u:nhaliday/b:ed4466204bb1

- note that this proof shows more generally that sum Var(X_k:n) <= sum Var(X_k)

- apparently that holds for dependent X_k too? http://mathoverflow.net/a/96943/20644

february 2017 by nhaliday

A VERY BRIEF REVIEW OF MEASURE THEORY

february 2017 by nhaliday

A brief philosophical discussion:

Measure theory, as much as any branch of mathematics, is an area where it is important to be acquainted with the basic notions and statements, but not desperately important to be acquainted with the detailed proofs, which are often rather unilluminating. One should always have in a mind a place where one could go and look if one ever did need to understand a proof: for me, that place is Rudin’s Real and Complex Analysis (Rudin’s “red book”).

gowers
pdf
math
math.CA
math.FA
philosophy
measure
exposition
synthesis
big-picture
hi-order-bits
ergodic
ground-up
summary
roadmap
mathtariat
proofs
nibble
unit
integral
zooming
p:whenever
Measure theory, as much as any branch of mathematics, is an area where it is important to be acquainted with the basic notions and statements, but not desperately important to be acquainted with the detailed proofs, which are often rather unilluminating. One should always have in a mind a place where one could go and look if one ever did need to understand a proof: for me, that place is Rudin’s Real and Complex Analysis (Rudin’s “red book”).

february 2017 by nhaliday

Could I be using proof by contradiction too much? - Mathematics Stack Exchange

february 2017 by nhaliday

One general reason to avoid proof by contradiction is the following. When you prove something by contradiction, all you learn is that the statement you wanted to prove is true. When you prove something directly, you learn every intermediate implication you had to prove along the way.

q-n-a
overflow
math
proofs
contradiction
oly
mathtariat
nibble
february 2017 by nhaliday

electromagnetism - Is Biot-Savart law obtained empirically or can it be derived? - Physics Stack Exchange

february 2017 by nhaliday

Addendum: In mathematics and science it is important to keep in mind the distinction between the historical and the logical development of a subject. Knowing the history of a subject can be useful to get a sense of the personalities involved and sometimes to develop an intuition about the subject. The logical presentation of the subject is the way practitioners think about it. It encapsulates the main ideas in the most complete and simple fashion. From this standpoint, electromagnetism is the study of Maxwell's equations and the Lorentz force law. Everything else is secondary, including the Biot-Savart law.

q-n-a
overflow
physics
electromag
synthesis
proofs
nibble
february 2017 by nhaliday

Cauchy-Schwarz inequality and Hölder's inequality - Mathematics Stack Exchange

january 2017 by nhaliday

- Cauchy-Schwarz (special case of Holder's inequality where p=q=1/2) implies Holder's inequality

- pith: define potential F(t) = int f^{pt} g^{q(1-t)}, show log F is midpoint-convex hence convex, then apply convexity between F(0) and F(1) for F(1/p) = ||fg||_1

q-n-a
overflow
math
estimate
proofs
ground-up
math.FA
inner-product
tidbits
norms
duality
nibble
integral
- pith: define potential F(t) = int f^{pt} g^{q(1-t)}, show log F is midpoint-convex hence convex, then apply convexity between F(0) and F(1) for F(1/p) = ||fg||_1

january 2017 by nhaliday

5/8 bound in group theory - MathOverflow

january 2017 by nhaliday

very elegant proof (remember sum d_i^2 = |G| and # irreducible rep.s = # conjugacy classes)

q-n-a
overflow
math
tidbits
proofs
math.RT
math.GR
oly
commutativity
pigeonhole-markov
nibble
shift
january 2017 by nhaliday

pr.probability - "Entropy" proof of Brunn-Minkowski Inequality? - MathOverflow

q-n-a overflow math information-theory wormholes proofs geometry math.MG estimate gowers mathtariat dimensionality limits intuition insight stat-mech concentration-of-measure 👳 cartoons math.FA additive-combo measure entropy-like nibble tensors coarse-fine brunn-minkowski boltzmann high-dimension curvature convexity-curvature

january 2017 by nhaliday

q-n-a overflow math information-theory wormholes proofs geometry math.MG estimate gowers mathtariat dimensionality limits intuition insight stat-mech concentration-of-measure 👳 cartoons math.FA additive-combo measure entropy-like nibble tensors coarse-fine brunn-minkowski boltzmann high-dimension curvature convexity-curvature

january 2017 by nhaliday

Dvoretzky's theorem - Wikipedia

january 2017 by nhaliday

In mathematics, Dvoretzky's theorem is an important structural theorem about normed vector spaces proved by Aryeh Dvoretzky in the early 1960s, answering a question of Alexander Grothendieck. In essence, it says that every sufficiently high-dimensional normed vector space will have low-dimensional subspaces that are approximately Euclidean. Equivalently, every high-dimensional bounded symmetric convex set has low-dimensional sections that are approximately ellipsoids.

http://mathoverflow.net/questions/143527/intuitive-explanation-of-dvoretzkys-theorem

http://mathoverflow.net/questions/46278/unexpected-applications-of-dvoretzkys-theorem

math
math.FA
inner-product
levers
characterization
geometry
math.MG
concentration-of-measure
multi
q-n-a
overflow
intuition
examples
proofs
dimensionality
gowers
mathtariat
tcstariat
quantum
quantum-info
norms
nibble
high-dimension
wiki
reference
curvature
convexity-curvature
tcs
http://mathoverflow.net/questions/143527/intuitive-explanation-of-dvoretzkys-theorem

http://mathoverflow.net/questions/46278/unexpected-applications-of-dvoretzkys-theorem

january 2017 by nhaliday

soft question - What notions are used but not clearly defined in modern mathematics? - MathOverflow

q-n-a overflow math list big-list discussion mathtariat tcstariat conceptual-vocab vague rigor nibble thinking definition clarity physics quantum iteration-recursion algebra fields math.CA math.NT structure logic proofs math.DS grokkability-clarity

january 2017 by nhaliday

q-n-a overflow math list big-list discussion mathtariat tcstariat conceptual-vocab vague rigor nibble thinking definition clarity physics quantum iteration-recursion algebra fields math.CA math.NT structure logic proofs math.DS grokkability-clarity

january 2017 by nhaliday

probability - How to prove Bonferroni inequalities? - Mathematics Stack Exchange

january 2017 by nhaliday

- integrated version of inequalities for alternating sums of (N choose j), where r.v. N = # of events occuring

- inequalities for alternating binomial coefficients follow from general property of unimodal (increasing then decreasing) sequences, which can be gotten w/ two cases for increasing and decreasing resp.

- the final alternating zero sum property follows for binomial coefficients from expanding (1 - 1)^N = 0

- The idea of proving inequality by integrating simpler inequality of r.v.s is nice. Proof from CS 150 was more brute force from what I remember.

q-n-a
overflow
math
probability
tcs
probabilistic-method
estimate
proofs
levers
yoga
multi
tidbits
metabuch
monotonicity
calculation
nibble
bonferroni
tricki
binomial
s:null
elegance
- inequalities for alternating binomial coefficients follow from general property of unimodal (increasing then decreasing) sequences, which can be gotten w/ two cases for increasing and decreasing resp.

- the final alternating zero sum property follows for binomial coefficients from expanding (1 - 1)^N = 0

- The idea of proving inequality by integrating simpler inequality of r.v.s is nice. Proof from CS 150 was more brute force from what I remember.

january 2017 by nhaliday

Compressed Sensing: Basic results and self contained proofs

january 2017 by nhaliday

- Shai Shalev-Shwartz

Johnson-Lindenstrauss and compressed sensing

pdf
lecture-notes
exposition
yoga
levers
tcs
acm
linear-algebra
embeddings
sparsity
proofs
concentration-of-measure
norms
nibble
compressed-sensing
PAC
features
Johnson-Lindenstrauss and compressed sensing

january 2017 by nhaliday

In Computers We Trust? | Quanta Magazine

january 2017 by nhaliday

As math grows ever more complex, will computers reign?

Shalosh B. Ekhad is a computer. Or, rather, it is any of a rotating cast of computers used by the mathematician Doron Zeilberger, from the Dell in his New Jersey office to a supercomputer whose services he occasionally enlists in Austria. The name — Hebrew for “three B one” — refers to the AT&T 3B1, Ekhad’s earliest incarnation.

“The soul is the software,” said Zeilberger, who writes his own code using a popular math programming tool called Maple.

news
org:mag
org:sci
popsci
math
culture
academia
automation
formal-methods
ai
debate
interdisciplinary
rigor
proofs
nibble
org:inst
calculation
bare-hands
heavyweights
contrarianism
computation
correctness
oss
replication
logic
frontier
state-of-art
technical-writing
trust
Shalosh B. Ekhad is a computer. Or, rather, it is any of a rotating cast of computers used by the mathematician Doron Zeilberger, from the Dell in his New Jersey office to a supercomputer whose services he occasionally enlists in Austria. The name — Hebrew for “three B one” — refers to the AT&T 3B1, Ekhad’s earliest incarnation.

“The soul is the software,” said Zeilberger, who writes his own code using a popular math programming tool called Maple.

january 2017 by nhaliday

ho.history overview - Proofs that require fundamentally new ways of thinking - MathOverflow

january 2017 by nhaliday

my favorite:

Although this has already been said elsewhere on MathOverflow, I think it's worth repeating that Gromov is someone who has arguably introduced more radical thoughts into mathematics than anyone else. Examples involving groups with polynomial growth and holomorphic curves have already been cited in other answers to this question. I have two other obvious ones but there are many more.

I don't remember where I first learned about convergence of Riemannian manifolds, but I had to laugh because there's no way I would have ever conceived of a notion. To be fair, all of the groundwork for this was laid out in Cheeger's thesis, but it was Gromov who reformulated everything as a convergence theorem and recognized its power.

Another time Gromov made me laugh was when I was reading what little I could understand of his book Partial Differential Relations. This book is probably full of radical ideas that I don't understand. The one I did was his approach to solving the linearized isometric embedding equation. His radical, absurd, but elementary idea was that if the system is sufficiently underdetermined, then the linear partial differential operator could be inverted by another linear partial differential operator. Both the statement and proof are for me the funniest in mathematics. Most of us view solving PDE's as something that requires hard work, involving analysis and estimates, and Gromov manages to do it using only elementary linear algebra. This then allows him to establish the existence of isometric embedding of Riemannian manifolds in a wide variety of settings.

q-n-a
overflow
soft-question
big-list
math
meta:math
history
insight
synthesis
gowers
mathtariat
hi-order-bits
frontier
proofs
magnitude
giants
differential
geometry
limits
flexibility
nibble
degrees-of-freedom
big-picture
novelty
zooming
big-surf
wild-ideas
metameta
courage
convergence
ideas
innovation
the-trenches
discovery
creative
elegance
Although this has already been said elsewhere on MathOverflow, I think it's worth repeating that Gromov is someone who has arguably introduced more radical thoughts into mathematics than anyone else. Examples involving groups with polynomial growth and holomorphic curves have already been cited in other answers to this question. I have two other obvious ones but there are many more.

I don't remember where I first learned about convergence of Riemannian manifolds, but I had to laugh because there's no way I would have ever conceived of a notion. To be fair, all of the groundwork for this was laid out in Cheeger's thesis, but it was Gromov who reformulated everything as a convergence theorem and recognized its power.

Another time Gromov made me laugh was when I was reading what little I could understand of his book Partial Differential Relations. This book is probably full of radical ideas that I don't understand. The one I did was his approach to solving the linearized isometric embedding equation. His radical, absurd, but elementary idea was that if the system is sufficiently underdetermined, then the linear partial differential operator could be inverted by another linear partial differential operator. Both the statement and proof are for me the funniest in mathematics. Most of us view solving PDE's as something that requires hard work, involving analysis and estimates, and Gromov manages to do it using only elementary linear algebra. This then allows him to establish the existence of isometric embedding of Riemannian manifolds in a wide variety of settings.

january 2017 by nhaliday

pr.probability - If you break a stick at two points chosen uniformly, the probability the three resulting sticks form a triangle is 1/4. Is there a nice proof of this? - MathOverflow

q-n-a overflow tidbits math probability trivia puzzles oly proofs nibble calculation symmetry visual-understanding caltech

january 2017 by nhaliday

q-n-a overflow tidbits math probability trivia puzzles oly proofs nibble calculation symmetry visual-understanding caltech

january 2017 by nhaliday

Copy this bookmark: