Activity for Derek Elkins
| Type | On... | Excerpt | Status | Date |
|---|---|---|---|---|
| Answer | — |
A: Picture proof for expansion of $x^n−y^n$ Here's a semi-visual, semi-algebraic approach. A useful alternative perspective on (univariate) polynomials is to think of them as being represented by their sequence of coefficients – filling in zeroes for any missing monomials. With this perspective, multiplying by $z$ simply shifts the se... (more) |
— | about 1 year ago |
| Edit | Post #289084 | Initial revision | — | over 1 year ago |
| Answer | — |
A: Intuitively, why doesn't picking unpopular integers ($> 31$) lower your probability of winning lotteries? Let's say every lottery you buy exactly one ticket and always use the same numbers. Does that lower your odds of winning versus a strategy where you always pick a random set of numbers? No. Assuming the winning numbers are uniformly distributed, your odds of winning are always directly proportiona... (more) |
— | over 1 year ago |
| Edit | Post #288782 | Initial revision | — | over 1 year ago |
| Answer | — |
A: Should posting on Meta affect reputation? Just to put out the other option, which is the one I prefer: No, votes on meta posts should not affect main site reputation. (more) |
— | over 1 year ago |
| Edit | Post #288411 | Initial revision | — | over 1 year ago |
| Answer | — |
A: Average distance from circle's center to a point The problem is indeed that you aren't computing the average distance. What you're computing is a median distance. Essentially, you are equally weighting points that are just slightly outside $C2$ and points that are near the boundary of $C1$, but those contribute different amounts to the average dist... (more) |
— | over 1 year ago |
| Edit | Post #288285 |
Post edited: Mention Skolem functions |
— | over 1 year ago |
| Edit | Post #288285 | Initial revision | — | over 1 year ago |
| Answer | — |
A: how to mathematically express a relationship in which a vector can be any 3D unit vector What makes the most sense to do somewhat depends on the context of this expression. What it seems you are really trying to do is defined $\mathbf e$ as a function of $\mathbf s$. What's making it awkward is that $\mathbf e$ isn't a function of $\mathbf s$ but merely a total (multi-valued) relation... (more) |
— | over 1 year ago |
| Edit | Post #288172 | Initial revision | — | over 1 year ago |
| Answer | — |
A: Finding a single row of Matrix after exponentiation While there are no doubt even more clever things you can do, the most straightforward approach, which will likely make a significant improvement, is to move from matrix-matrix multiplication to matrix-vector multiplication. Let $ek$ be a (column) vector with all $0$s except the $k$-th entry is $1$... (more) |
— | over 1 year ago |
| Comment | Post #288003 |
Sorry, that was just a typo because these examples are using dependent products in a degenerate way that makes them into function types. (I should have just defined $A \to B :\equiv \Pi(A,[x:A]B)$.) It should be $$\lambda(A,[x:A]\Pi(B,[y:B]A),[x:A]\lambda(B,[y:B]A,[y:B]x))$$ And, yes, as mentioned in... (more) |
— | over 1 year ago |
| Comment | Post #288007 |
Yes, this is basically correct. The only caveat is you need to factor in how later defined constants can depend on earlier defined constants. One approach (which I dislike but is technically fine) is to have later constants declared with respect to a context containing all earlier constants, so the c... (more) |
— | over 1 year ago |
| Comment | Post #288005 |
If you treat $\square$ as a term (which is probably not the case), then it is a term that is not classified by a type. If you don't treat it as a term (and in the [original description](https://hal.inria.fr/file/index/docid/76024/filename/RR-0530.pdf) there was no $\square$), then $\*$ is a term that... (more) |
— | over 1 year ago |
| Comment | Post #288007 |
You are correct with that being how you would axiomatize two Tarski-style universes. You do need $T_0$ much as LF needs $El$. Because it gets cluttered, invocations of $El$ are suppresed, but they should actually be all over the place. For example, the type of the identity function would be written l... (more) |
— | over 1 year ago |
| Comment | Post #288007 |
More generally, *by design* the type structure of LF is *not* reflected in the object language. We want to use LF to describe any language we desire which may or may not have pi types or universes or may have pi types/universes that work in a different way than in LF. The reason LF has pi types and a... (more) |
— | over 1 year ago |
| Comment | Post #288007 |
As I explicitly state in the answer you reference, if we're modeling a language with a cumulative hierarchy *within* LF, then the $El$ of LF has no particular relation to the $T_0$ in the object language. As I state there, they aren't even the same *kind* of thing in that context. (more) |
— | over 1 year ago |
| Comment | Post #288005 |
Sure it can be finite. It is for LF. The top-level universe is simply not a term of any other universe. The universe being Tarki-style or Russell-style doesn't change that. (This is why LF doesn't have a code for $\mathsf{Type}$ and a corresponding $El(\mathsf{type})=\mathsf{Type}$ equation. If we di... (more) |
— | over 1 year ago |
| Comment | Post #288003 |
In the informal meta-logic of LF, i.e. the meta-meta-logic relative to our object language, asserting these constants and equations adds them to the signature. From there, you can almost immediately derive those informal rules in the informal meta-meta-logic. But what we care about are the rules of o... (more) |
— | over 1 year ago |
| Edit | Post #288005 | Initial revision | — | over 1 year ago |
| Answer | — |
A: On Tarski-style universes in type theory I'm a bit confused about what you're confused about for the first part. In a Russell-style universe system, we'd have a hierarchy of universes with $\mathcal Ui : \mathcal U{i+1}$, i.e. the $i$th universe is a type in the $(i+1)$th universe. As you state, for a Tarski-style universe system, $\mathcal... (more) |
— | over 1 year ago |
| Edit | Post #288003 | Initial revision | — | over 1 year ago |
| Answer | — |
A: The purpose of logical frameworks in specifying type theories András Kovács answer and comments to your question on Math.SE hit some of the main points. I'll give a bit more detail and context. First, the point of logical frameworks like LF is to be a formal meta-language, and, in particular, a formal specification language. The definitions in the HoTT book ... (more) |
— | over 1 year ago |
| Edit | Post #287980 | Initial revision | — | over 1 year ago |
| Answer | — |
A: The meaning of $\pm$ I think I can explain what's going on by interpreting things more formally, though it could be gotten at informally as well; it's just clearer to see formally. One way to interpret "$y = \pm x$" (and other informal notations like $y = 1,2,3$) is as $y \in \{x, -x\}$ ($y \in \{1,2,3\}$). This is lo... (more) |
— | over 1 year ago |
| Edit | Post #287887 | Initial revision | — | almost 2 years ago |
| Answer | — |
A: Unification and generalization of limit and colimit Let $\mathcal I$ be the category with two objects and two parallel arrows between them: $1 \rightrightarrows 2$ and $\mathcal P$ be the cone over $\mathcal I$ with apex labelled $0$. Write $\mathsf f$ and $\mathsf g$ for the two arrows $1 \to 2$. Let $\iota : \mathcal I \hookrightarrow \mathcal P$ be... (more) |
— | almost 2 years ago |
| Edit | Post #287879 |
Post edited: |
— | almost 2 years ago |
| Edit | Post #287879 | Initial revision | — | almost 2 years ago |
| Answer | — |
A: Generalization of categorical product The $F(\pii) = id$ doesn't really fit the form of a universal property. If we drop that constraint, we can present your universal property in terms of representability $$\mathcal C(Y, X1 \timesF X2) \cong \{(f1,f2)\in\mathcal C(Y, X1)\times\mathcal C(Y, X2)\mid F(f1) = F(f2) \}$$ natural in $Y$. No... (more) |
— | almost 2 years ago |
| Edit | Post #287849 |
Post edited: Improve kerning of quotient set notation. |
— | almost 2 years ago |
| Comment | Post #287849 |
Both here and in your answer you are not explicitly using the fact that $f$ is constant on equivalences classes nor the definition of the quotient topology. You implicitly use the former when saying $g([x]):=f(x)$ is well-defined in the vague sketch of the proof at the beginning, but not in the separ... (more) |
— | almost 2 years ago |
| Suggested Edit | Post #287849 |
Suggested edit: Improve kerning of quotient set notation. (more) |
helpful | almost 2 years ago |
| Edit | Post #287721 | Initial revision | — | almost 2 years ago |
| Answer | — |
A: Proving $|{\bf R}^{\bf R}|=|2^{\bf R}|$ using the Schroeder-Bernstein Theorem By definition $\mathbb R^\mathbb R \subset \mathbf 2^{\mathbb R\times\mathbb R}$. So all we need is a surjection $\mathbb R \twoheadrightarrow \mathbb R \times \mathbb R$ of which there are plenty such as space filling curves. If you have a bijection between $\mathbf 2^\mathbb N$ and $\mathbb R$, the... (more) |
— | almost 2 years ago |
| Edit | Post #287644 | Initial revision | — | almost 2 years ago |
| Answer | — |
A: What is the Name of Function for Probability of a Certain Sum on Random Die Rolls? I don't know some special name for exactly that sum, but it is closely related to what are known as polynomial coefficients or extended binomial coefficients. These are often written as ${n \choose j}{k+1}$ and are defined indirectly via: $$\left(\sum{i=0}^k x^i\right)^n = \sum{j=0}^{nk} {n \choose j... (more) |
— | almost 2 years ago |
| Comment | Post #287625 |
The equation you give in the title doesn't seem to appear in the image (which you should reproduce the relevant part as MathJax and also crop it much more aggressively). The equation you reference is $\int_C f(x,y)ds = \int_a^b f(x, 0)dx$ There is no $f(x)$. The domain of integration is critical here... (more) |
— | almost 2 years ago |
| Edit | Post #287003 | Initial revision | — | about 2 years ago |
| Answer | — |
A: Proving that $p\mid (p+1776)$ if $p$ is a prime and $p(p+1776)$ is a perfect square You basically have it. I'll give an overly detailed rendition of an informal proof below. As you state, the assumption is that $p(p+1776) = k^2$ for some natural number $k$ with $p$ a prime. We want to show that $p\mid p + 1776$, or, equivalently, $p + 1776 = pm$ for some natural $m$. Proof:... (more) |
— | about 2 years ago |
| Edit | Post #286957 |
Post edited: cases environment accomplishes the same output in a simpler way |
— | about 2 years ago |
| Suggested Edit | Post #286957 |
Suggested edit: cases environment accomplishes the same output in a simpler way (more) |
helpful | about 2 years ago |
| Comment | Post #286908 |
@#8056 That's also a common definition according to Wikipedia, though [Wikipedia seems to agree with my experience](https://en.wikipedia.org/wiki/Exponentiation#Real_exponents) that the logarithm-based definition is more common. The logarithm-based definition seems more convenient and easier to work ... (more) |
— | over 2 years ago |
| Comment | Post #286908 |
For $e^x$, given *some other* definition of $e^x$, you can certainly prove that the power series definition I gave is the Taylor series. However, if you take the power series I gave as the definition, then there's no need to talk about the theory of Taylor series. You just have a power series; the fa... (more) |
— | over 2 years ago |
| Comment | Post #286908 |
$\lim_{a\to 0}a$ is just $0$. The limit of an (real) expression is either undefined or it's a real number. It's not some infinitesimal thing. So $\forall x.P(x)\implies P(x\pm\lim_{\epsilon\to 0}\epsilon)$ is just $\forall x.P(x)\implies P(x)$. You could try to do something like $\forall x.\exists\ep... (more) |
— | over 2 years ago |
| Edit | Post #286907 |
Post edited: Format implications so it not an unreadable blob of text. Correct minor typo/thinko. |
— | over 2 years ago |
| Edit | Post #286908 | Initial revision | — | over 2 years ago |
| Answer | — |
A: Prove $e^x \ge x+1 \\\; \forall x \in \mathbb{R}$ using induction You can't do induction on the real numbers because the real numbers aren't inductively defined. That said, it's not clear what you intend "induction on reals" to mean. Before continuing, I'd like to make an aside on proof writing. First, as a matter of presentation, it's useful to make it clear wh... (more) |
— | over 2 years ago |
| Suggested Edit | Post #286907 |
Suggested edit: Format implications so it not an unreadable blob of text. Correct minor typo/thinko. (more) |
helpful | over 2 years ago |