Skip to main content

Basic probability in Mathlib

Tutorial

How do I define a probability space and two independent random variables in Lean? Should I use IsProbabilityMeasure or ProbabilityMeasure? How do I condition on an event?

This post answers these and other simple questions about how to express probability concepts using Mathlib.

Read more…

Modular forms

New in mathlib

In PR# 13250 we define modular forms and cusp forms, and prove that they form complex vector spaces. These are analytic functions of number theoretic interest with strong links to geometry, representation theory and analysis. Most famously they are a key ingredient in the proof of Fermat's Last Theorem. In this post we discuss the formalization process, motivate some design choices and map out some future work.

Read more…

This month in mathlib (Oct and Nov 2022)

month-in-mathlib

In October and November 2022 there were 512 and 453 PRs merged into mathlib. We list some of the highlights below.

  • Measure theory.

    • PR #16830 improves Vitali families and Lebesgue density theorem.
    • PR #16762 adds a version of Lebesgue's density theorem.
    • PR #16906 proves Lebesgue differentiation theorem.
    • PR #16836 relates integrals over add_circle with integrals upstairs in ℝ.

  • Algebra.

    • PR #14672 defines mixed/equal characteristic zero.
    • PR #17018, PR #16849 and PR #17011 show the Kähler differential module is functorial and that $S/R$ is formally unramified if and only if $\Omega^1_{S/R} = 0$. They also give the standard presentation of the Kähler differential module.
    • PR #16000 proves Artin-Rees lemma and Krull's intersection theorems.
    • PR #16317 adds the multinomial theorem.
    • PR #17295 proves the Jordan-Hölder theorem for modules.
    • PR #17311 proves that a group with finitely many commutators has finite commutator subgroup.
    • PR #17243 proves the Third Isomorphism theorem for rings.
    • PR #13749 introduces non-unital subsemirings.

  • Analysis

    • PR #16723 shows that two analytic functions that coincide locally coincide globally.
    • PR #16683 and PR #16680 introduce functions of bounded variation and prove that they are almost everywhere differentiable. As a corollary, PR #16549 shows that a monotone function is differentiable almost everywhere.
    • PR #17119 defines and gives basic properties of the complex unit disc.
    • PR #16780 proves the open mapping theorem for holomorphic functions.
    • PR #16487 constructs the volume form.
    • PR #16796 generalizes the Hahn-Banach separation theorem to (locally convex) topological vector spaces.
    • PR #16835 proves functoriality of the character space.
    • PR #16638 introduces the Dirac delta distribution.
    • PR #17110 proves smoothness of series of functions.
    • PR #16201 and PR #17598 define the additive circle and develop Fourier analysis on it.
    • PR #17543 computes $\Gamma(1/2)$.
    • PR #16053 introduces the strong operator topology.

  • Number theory.

    • PR #15405 introduces the Selmer group of a Dedekind domain.
    • PR #17677 defines slash-invariant forms, a step towards the definition of modular forms.
    • PR #17203 defines the absolute ideal norm.

  • Representation theory.

    • PR #17005 is about exactness properties of resolutions.
    • PR #16043 proves the orthogonality of characters.
    • PR #13794 proves Schur's lemma.
    • PR #17443 adds the construction of a projective resolution of a representation.

  • Topology.

    • PR #16677 constructs the Galois correspondence between closed ideals in $C(X, 𝕜)$ and open sets in $X$.
    • PR #16719 shows that maximal ideals of $C(X, 𝕜)$ correspond to (complements of) singletons.
    • PR #16087 defines covering spaces.
    • PR #16797 proves that the stalk functor preserves monomorphism.
    • PR #17015 proves that Noetherian spaces have finite irreducible components.

  • Probability theory.

  • Algebraic and differential geometry.

  • Linear algebra.

    • PR #11468 shows that the clifford algebra is isomorphic as a module to the exterior algebra.
    • PR #16150 proves that the inverse of a block triangular matrix is block triangular.

  • Category theory.

    • PR #16969 adds basic results about localization of categories.

  • Combinatorics

    • PR #16195 adds the definition and some basic results about semistandard Young tableaux.
    • PR #17445 adds an equivalence between Young diagrams and weakly decreasing lists of positive natural numbers.
    • PR #17306 and PR #17213 define bridge edges, acyclic graphs, and trees for simple graphs, and provide some characterizations.

  • Tactics

    • PR #16313 introduces the qify tactic, to move from $\mathbb{Z}$ to $\mathbb{Q}$.
    • PR #13483 adds a tactic for moving around summands.
    • PR #16911 adds a tactic to find declarations that use sorry. This tactic is intended for projects that depend on mathlib.

During these two months, we got two new versions of Lean. We also started to systematically port mathlib to Lean4, see the wiki.

Definitions in the liquid tensor experiment

Community projects

A few weeks ago, we announced the completion of the liquid tensor experiment (LTE for short). What this means is that we stated and (completely) proved the following result in Lean:

variables (p' p : ℝ≥0) [fact (0 < p')] [fact (p' < p)] [fact (p ≤ 1)]

theorem liquid_tensor_experiment 
  (S : Profinite) (V : pBanach p) :
  ∀ i > 0, Ext i (ℳ_{p'} S) V ≅ 0 :=
-- the proof ...

The code block above, which is taken directly from the file challenge.lean in the main LTE repository, uses some custom notation to make the statement appear as close as possible to the main theorem mentioned in Scholze's original challenge. Fortunately, it's relatively straightforward to unravel the notation to see the underlying definitions themselves. But there is a bigger issue: How can we convince ourselves (and others) that the definitions we introduced in LTE are actually correct?

For instance, we could have defined Ext to be $0$ (spoiler: we didn't). Or, we could have made some subtle innocent mistake in setting up the definitions that somehow implies that Ext is always $0$, or that all condensed abelian groups are trivial, or one of several other pitfalls that renders the statement above meaningless.

To answer this question, we built a new examples folder in the repository which contains several files corresponding to the main players in the statement above. These examples can be considered as centralized "sanity checks" that the definitions we wrote using Lean actually behave as expected.

We tried to write the files in this folder in a way which should be (approximately) readable by mathematicians who have minimal experience with Lean. The goal is to make it easy for non-experts to look through the examples folder, then look through the concise final statement in challenge.lean, and be reasonably confident that the challenge was accomplished.

This blog post gives a detailed overview of this folder and its contents, and how it relates to the definitions used in the main statement of the liquid tensor experiment. It is meant to be read alongside the actual files from the examples folder.

Read more…