Louis Wasserman
Louis Wasserman
Theorem 34 of the 100 Theorems, and should be provable with strictly elementary arguments.
I know we haven't even merged derivatives yet, but I think this is actually well within our reach. The hardest part, I think, is simply showing that the equivalence of...
With the geometric series under our belts, we should be able to define the ratio test, and from there start defining many useful power series. Their relationships to derivatives and...
This is a required lemma for many further operations. It's straightforward enough to get there from arithmetic location etc., it just has to get done, and this is a task...
As discussed in #1559, we should only link to Wikidata when we're defining the concept referred to by Wikidata, not just an instance of it. But that's a solvable problem...
``` warning: Potential incomplete link ┌─ elementary-number-theory.multiplication-closed-intervals-rational-numbers.md:882:41 │ 882 │ We can bound the width of the interval $[a,b] ∙ [c,d]$: │ ^^^^^ Did you forget to define a URL...
We have all the tools we need to define derivatives on functions from R to R at this point, and I'm working on a draft of that. But we might...
I haven't seen a proper homotopy type theory treatment of these. It might already exist in the library, or it might never have been heard of. No idea. https://en.wikipedia.org/wiki/Zipper_%28data_structure%29?wprov=sfla1 describes...
With the real numbers getting filled out, measure theory becomes plausible. https://arxiv.org/abs/2207.04000, for example, outlines a constructive, choice free foundation built atop the modulated Cauchy reals, which IIRC are equivalent...
I'm mostly filing an issue first to make sure this doesn't exist and that I'm not misunderstanding the goals of frames, locales, all that stuff I don't fully get yet....