Writing the blueprint

Stream: Brownian motion

[Rémy Degenne]

The project has been quiet recently, but there has been some work happening: Lorenzo Luccioli, Kexing Ying and I have written parts of the blueprint, and in the next few days I will write Lean statements with sorry proofs and create tasks for those. It will be possible to claim those tasks on github, thanks to workflows that Pietro Monticone added to the repository.

Since I am no longer writing the blueprint alone, I think it's a good time to share a few tips on how to effectively do it. This is also useful information when you contribute a Lean proof: it's better to update the blueprint at the same time to indicate that the work is done.

General principles

The blueprint will be read by people who want to implement a new lemma from the blueprint in Lean, without having read everything that comes before, and who will be able to use only tools in Mathlib and introduced before in the blueprint.

• Extract many small lemmas. A theorem in a book will correspond to many statements in the blueprint.
• In proofs, refer explicitly to all other lemmas you use, with \ref{}. The reader should not be expected to know well what has been proved so far, nor where to find it. Don't write "since X has property P, [...]", but "since X has property P by Lemma~\ref{lem:px}`, [...]".
• Go from Mathlib (+ the current project state) to your goal. The proof you find in a book will use prerequisites that are not in Mathlib yet: you should describe those. Sometimes the book spends time explaining a lemma that is already proved in Mathlib: simply add a node for it with a \mathlibok tag and don't repeat the proof.
• Write in a "Mathlib-like" way: don't write "there is a set of measure zero $N$ such that on $N^c$,...", instead write "almost surely, ...". It corresponds better to the code, and our goal is to produce code. This is particularly important for definitions.
• Make sure the dependency graph is right: use correctly \uses{}, \leanok and \mathlibok. This is very important.

How to write definitions and lemmas

Here is an example of definition as it is written in the blueprint when not yet implemented in Lean:

\begin{definition}[Localizing sequence]\label{def:localizingSequence}
  \uses{def:preLocalizingSequence}
A localizing sequence is a sequence of stopping times $(\tau_n)_{n \in \mathbb{N}}$ such that $\tau_n$ is non-decreasing and $\tau_n \to \infty$ as $n \to \infty$ (a.s.).
That is, it is a pre-localizing sequence that is also almost surely non-decreasing.
\end{definition}

Important points:

• \label{def:DefNameHere}: the label of the definition, which will be used in \ref{} and in \uses{} later.
• \uses{def:AnotherDef, def:AThirdDef}: list here all the definitions (and possibly theorems) used in the new definition.

Once the definition is implemented in Lean it becomes this:

\begin{definition}[Localizing sequence]\label{def:localizingSequence}
  \uses{def:preLocalizingSequence}
  \leanok
  \lean{ProbabilityTheory.IsLocalizingSequence}
A localizing sequence is a sequence of stopping times $(\tau_n)_{n \in \mathbb{N}}$ such that $\tau_n$ is non-decreasing and $\tau_n \to \infty$ as $n \to \infty$ (a.s.).
That is, it is a pre-localizing sequence that is also almost surely non-decreasing.
\end{definition}

We added \leanok to mark it as done, and \lean{Full.Declaration.Name} to link to the Lean definition. It's possible to list several Lean declarations in \lean{...}, but most often there is only one.
If the definition (or lemma) is in Mathlib, use \mathlibok instead of \leanok.

An example of lemma which is not yet implemented:

\begin{lemma}\label{lem:localizingSequence_min}
  \uses{def:localizingSequence}
Let $(\sigma_n), (\tau_n)$ be localizing sequences.
Then $(\sigma_n \wedge \tau_n)$ is a localizing sequence.
\end{lemma}

\begin{proof}
  \uses{lem:some_other_lemma, def:someDef}
Describe the proof here. In this proof we use Lemma~\ref{lem:some_other_lemma} and introduce an object which is a someDef (Definition~\ref{def:someDef}).
\end{proof}

• In the first \uses{...}, in the lemma statement, list all the definitions used to state the lemma (not those used only in the proof).
• In the secont \uses{...} in the proof, list all the definitions and theorems used in the proof.

Once the lemma is stated in Lean, add a \leanok to the statement and a \lean{} to indicate the lemma name. Once the lemma is also proved, add a second \leanok to the proof.
For example, a lemma that is stated and proved in Mathlib will look like this:

\begin{lemma}[Doob's maximal inequality for $\mathbb{N}$]\label{lem:maximal_ineq}
  \uses{def:Submartingale}
  \mathlibok
  \lean{MeasureTheory.maximal_ineq}
Let $X : \mathbb{N} \rightarrow \Omega \rightarrow \mathbb{R}$ be [...]
\end{lemma}

\begin{proof}\leanok

\end{proof}

We omitted the proof here, and that proof does not have a \uses{} to refer to previous lemmas, because it's from Mathlib. Note that the proof environment with a \leanok tag is important (even if the proof is empty) because if we don't have it, the dependency graph will show the lemma as not proved yet.

How to check your work

Rather that waiting for CI, it's handy to check the blueprint in local. First, you should have leanblueprint installed. Then:

• Write your modifications to the blueprint
• run leanblueprint all in the project folder. If you get an error when compiling or in the lake build step, fix it. Then, look at the end of the log for an error like this:

MeasureTheory.maximal_ineqd is missing.
Command 'lake exe checkdecls blueprint/lean_decls' returned non-zero exit status 1.

This means that you have a \lean{MeasureTheory.maximal_ineqd} somewhere in your latex, but MeasureTheory.maximal_ineqd is not a Lean declaration imported by your project. Fix the lemma name or add an import.

• run leanblueprint serve and follow the link to look at the blueprint in local. Go to the dependency graph. Check that the dependency links between your new definitions and lemmas are right. Check that the colors of the nodes are right (see the graph legend for the color meanings).

[Etienne Marion]

Just to be sure: if we use a result that is in Mathlib, we should add the statement to the blueprint? I feel like this would require to add a lot of lemmas.

[Rémy Degenne]

I've been adding definitions only.

[Rémy Degenne]

You could add a link to the lemma in the Mathlib docs in the proof if you want.

[Rémy Degenne]

In PR https://github.com/RemyDegenne/brownian-motion/pull/264, I want to introduce a new type of nodes in the blueprint: lemmas that gather immediate properties of definitions.
The explanation, copied from the PR:

Some lemmas are about immediate consequences of definitions, and we don't want to have to track their uses in every downstream theorem when connecting the dependency graph. Currently they form a cloud of nodes in the graph that is seemingly not used by anything else (although they are).

The tentative solution is, for a definition def:definition with many small such lemmas that are immediate consequences of the def, to create a fake lemma called lem:definition_basic which imports all of them. Then whenever we want to use the definition in the blueprint we instead import that lemma.
The main benefit is a more legible, less cluttered dependency graph.

This is an approach I used previously on my TestingLowerBounds project to get a clearer graph:
https://remydegenne.github.io/testing-lower-bounds/blueprint/dep_graph_document.html

[Rémy Degenne]

In the PR I do that for the right continuation of a filtration (for which we currently have a several lemmas that are not connected to anything downstream and are immediate from the def) and for right-continuous filtrations.

[Rémy Degenne]

The downside is of course that we lose the information of which lemma is or is not used exactly in further developments. But for lemmas that are trivial consequences of the definition we currently don't even think about mentioning their use downstream so we don't have that information anyway.