1in = 2.54cm

Limit + Limit

Cheaply, using an Iverson bracket expression:

\[ \begin{aligned} \lim_{a \to \infty} \lim_{b \to \infty} [a > b] &= 0 \\ \lim_{b \to \infty} \lim_{a \to \infty} [a > b] &= 1 \end{aligned} \]

For more continuity, use \(\frac{a}{a + b}\) instead (Rudin Example 7.2).

Uniform convergence on one limit suffices to allow this exchange, almost by definition.

Limit + Continuity

Let

\[ f_\epsilon(x) = \begin{cases} 0 & \text{if } |x| \geq \epsilon \\ 1 - \left|\frac{x}{\epsilon}\right| &\text{if } |x| < \epsilon \end{cases}. \]

(Ported from betaveros.stash. Wow, I get syntax highlighting and footnotes! Probably years out of date though. I probably wrote this somewhere in 2012–2014, but am editing this parenthetical in 2021.)

A quick brief guide. At least, that’s how I planned it.

A lot of stuff is in the package java.awt.datatransfer. Class Toolkit is in java.awt.

Some basic classes. The class Clipboard is a clipboard, obviously. Its content is/will be an instance of the class Transferable. Some content can be read as different types of objects depending on what you want; to choose which type you use an instance of DataFlavor. It provides three basic ones: DataFlavor.imageFlavor, DataFlavor.javaFileListFlavor, and DataFlavor.stringFlavor.

Okay, now step by step. This is the low-level method.

1. Get the default clipboard with Clipboard clipboard = Toolkit.getDefaultToolkit().getSystemClipboard();
2. Get a transferable with Transferable content = clipboard.getContents(null); ¹
3. Check if content can be read as the kind of object you want with (content != null) && content.isDataFlavorSupported(someFlavor)
4. If it does, get the object with content.getTransferData(someFlavor) ².

If you just want a quick-and-dirty function:

static String getClipboard()
        throws java.awt.datatransfer.UnsupportedFlavorException, IOException {
    return (String) java.awt.Toolkit.getDefaultToolkit()
        .getSystemClipboard()
        .getData(java.awt.datatransfer.DataFlavor.stringFlavor);
}

1

• Firefox
  • LeechBlock, Xmarks, HTTPS Everywhere, uBlock Origin
  • Formerly: Pentadactyl (nightlies), LastPass, Disconnect, All-in-One Sidebar
• Dropbox (db.tt)
• (g)Vim / MacVim
  • NeoBundle; jellybeans, syntastic, airline, fugitive, unite.vim, nerdtree, …
  • Make sure you change your home folder and other paths in your .vimrc if necessary.
• LaTeX
• VLC
• Anki
• Geogebra, CaRMetal
• osu!
• Gargoyle
• MuseScore
• μTorrent
• VeraCrypt
• Gyazo

Editor’s note: This is almost certainly years out of date. cabal has v2 commands and stuff now? Sorry.

diagrams is a nifty Haskell library for making vector diagrams. I keep coming back to it to generate graphics for puzzles:

• the very old A Signature Puzzle from this blog
• A Fork in the Road (DP Puzzle Hunt)
• Symbols (Galactic Puzzle Hunt 2020)
• A Lot of Research into Things That Have Very Little Meaning (Silph Puzzle Hunt)

I got sick of relearning it every time, and I think there’s some small chance other people will find it useful too, so I wrote something up. This post is a sort of reference that tries to compromise between the quick start tutorial and manual on one hand, and the API reference on the other, to try to be deeper and more comprehensive than the former, but also flow better and be easier to navigate than the latter. Some types are just really intimidating when fully written out…

circle :: (TrailLike t, V t ~ V2, N t ~ n, Transformable t) => n -> t

To avoid unhelpfully generic types, I will deal concretely with two-dimensional diagrams that measure everything in Double, and will frequently abbreviate complex types with an asterisk, like I will write V2* for V2 Double. I will introduce these aliases along the way for easy greppability. They’re not legal Haskell, of course.

This reference assumes basic-to-intermediate Haskell knowledge. Some of the more intermediate stuff includes:

• Monoids, and that the Haskell Monoid operator is <>
• Typeclasses. I will sometimes write fake type signatures as abbreviations for typeclass restrictions: for example, TrailLike is a typeclass, and I might say or write that a function returns TrailLike when I really mean TrailLike t => t, any type t that is in that typeclass.

van Laarhoven lenses may help, but mostly I’ll try to black-box them.

It seems like a rite of passage to create one of these because there are so many Coq tactic cheat sheets out there and there’s just so much to learn. Here’s mine.

This is mostly about tactics but I realized not really.

Links:

• Coq Tactics. Authoritative but dense.
• Logical Foundations (Software Foundations Volume 1). I think the order of ideas makes pedagogical sense but also makes it hard for me to look up particular tactics or concepts.

• Other Coq cheat sheets found by Googling “Coq cheat sheets”:

  • Coq Tactics Index (Joseph Redmon)
  • Coq Tactics Cheatsheet (Cornell CS3110)
  • Coq Tactics Quick Reference (Adam Chlipala) / the Formal Reasoning About Programs book also has a nice appendix
  • Coq Tactics (UPenn ???)

Meta-notes: I cover a lot of weak tactics because I like knowing exactly what my tools are doing. I try to use the variants of tactics that explicitly name things produced when possible. I am sure there is nomenclature I don’t understand precisely and use sloppily in this list; I am also sloppy with metavariables. Even things that are correct might be horrible style. There are likely other errors and omissions. They might be fixed one day. I’m putting this up nevertheless because it’s personally useful.

Things I wish I knew but didn’t learn from Software Foundations or Coq tactic cheat sheets

• The first two sections are not about tactics per se but how to find theorems to use and how to use them. Knowing how to use all of these query commands is super useful.
• To clean up repeating subexpressions with “local variables”, I find remember expr as X eqn:Hname. easier to work with than set (X := expr).
• pose proof expr as Hname. adds expr to the context, with name Hname. Modus ponens where you know H1 and H2, which is “H1 implies H3”, is just pose proof (H2 H1) as H3.
• Software Foundations covers bullets and curly braces early, but I like subgoal specification with 1:, 2: etc., which can really help limit nesting depth. 2: (tactic that solves subgoal 2). If you want more bullets, there are infinitely many, not just three. After - + * you can use -- ++ ** --- etc.

Bruce Lindbloom has a ton of equations, but I just want the big ones on one page. We’ll assume sRGB, which implies using D65 as white (if you’re using Bruce Lindbloom’s calculator to check your implementation, make sure to set these).

RGB ↔ Linear RGB

Let \(\Xi\) (one of \(R\), \(G\), and \(B\)) be an RGB component in the range \([0, 1]\). (This is an obnoxious variable choice, but I’m trying to not overload any variable names in this entire post.) If you have RGB values in \([0, 255]\), divide them by 255. It can be converted to/from the linearized component \(\xi\) (one of \(r\), \(g\), and \(b\)) as:

\[\xi = \begin{cases} \Xi/12.92 & \text{if }\Xi \leq 0.04045 \\ ((\Xi + 0.055)/1.055)^{2.4} & \text{if }\Xi > 0.04045 \end{cases}\]

\[\Xi = \begin{cases} 12.92\xi & \text{if }\xi \leq 0.0031308 \\ 1.055v^{1/2.4} - 0.055 & \text{if }\xi > 0.0031308 \end{cases}\]

This is called “companding”.

However, you can use \(\xi = \Xi^{2.4}\) and \(\Xi = \xi^{1/2.4}\) in a pinch.

Linear RGB ↔ XYZ

Convert between XYZ and linearized RGB. Again, this assumes sRGB and D65.

\[\begin{align*} X &= 0.4124564r + 0.3575761g + 0.1804375b \\ Y &= 0.2126729r + 0.7151522g + 0.0721750b \\ Z &= 0.0193339r + 0.1191920g + 0.9503041b \end{align*}\]