Glossary

Defined in this project

Every definition in this project, under its own name: the first paragraph of its description, or how it is declared when it has none. Theorems are not listed here: they are results, not words.

A · C · D · E · F · I · K · M · N · O · P · R · S · T · W · Other

A

AEFiniteKernelSupport def

A kernel κ has almost everywhere finite support wrt a measure μ if, for almost every point t, then κ t has finite support. Note that we don't require any uniformity wrt t. · ProbabilityTheory.Kernel.AEFiniteKernelSupport

C

condEntropy def

def condEntropy (X : Ω → S) (Y : Ω → T) (μ : Measure Ω · ProbabilityTheory.condEntropy

CondIndepFun def

The assertion that f and g are conditionally independent relative to h. · ProbabilityTheory.CondIndepFun

condKLDiv def

If $X,Y,Z$ are random variables, with $X,Z$ defined on the same sample space, we define $$ D_{KL}(X|Z \Vert Y) := \sum_z \mathbf{P}(Z=z) D_{KL}( (X|Z=z) \Vert Y).$$ · condKLDiv

condMultiDist def

def condMultiDist {m : ℕ} {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i)) {S : Type*} [Fintype S] (X : ∀ i, Ω i → G) (Y : ∀ i, Ω i → S) : ℝ · condMultiDist

condMutualInfo def

def condMutualInfo (X : Ω → S) (Y : Ω → T) (Z : Ω → U) (μ : Measure Ω · ProbabilityTheory.condMutualInfo

condRho def

We define $\rho(X|Y) := \sum_y {\bf P}(Y=y) \rho(X|Y=y)$. · condRho

condRhoMinus def

Average of rhoMinus along the fibers. · condRhoMinus

condRhoPlus def

Average of rhoPlus along the fibers. · condRhoPlus

condRuzsaDist def

def condRuzsaDist (X : Ω → G) (Z : Ω → S) (Y : Ω' → G) (W : Ω' → T) (μ : Measure Ω · condRuzsaDist

condRuzsaDist' def

def condRuzsaDist' (X : Ω → G) (Y : Ω' → G) (W : Ω' → T) (μ : Measure Ω · condRuzsaDist'

Config structure

Configuration for ring_nf. · Mathlib.Tactic.RPowRing.Config

Context structure

The read-only state of the RPowRing monad. · Mathlib.Tactic.RPowRing.Context

D

delab_ofNat def

def delab_ofNat · Mathlib.Tactic.RPowRing.delab_ofNat

deleteMiddle def

def deleteMiddle (κ : Kernel α (β × γ × δ)) : Kernel α (β × δ) · ProbabilityTheory.Kernel.deleteMiddle

deleteRight def

def deleteRight (κ : Kernel α (β × γ × δ)) : Kernel α (β × γ) · ProbabilityTheory.Kernel.deleteRight

dual_iso def

Non canonical isomorphism between a finite 2-torsion group and its dual into ZMod 2. · dual_iso

E

elabRPowRingConv def

Elaborator for the rpow_ring tactic. · Mathlib.Tactic.RPowRing.elabRPowRingConv

entropy def

def entropy (X : Ω → S) (μ : Measure Ω · ProbabilityTheory.entropy

entropy def

def entropy (κ : Kernel T S) (μ : Measure T) · ProbabilityTheory.Kernel.entropy

eval def

def eval (e : Q(ℝ)) : AtomM (Result ExProd e) · Mathlib.Tactic.RPowRing.eval

evalAtom def

Evaluates an atom, an expression where ring can find no additional structure. · Mathlib.Tactic.RPowRing.evalAtom

evalMul def

Multiplies two monomials va, vb together to get a normalized result monomial. · Mathlib.Tactic.RPowRing.evalMul

evalPow def

def evalPow {a : Q(ℝ)} (va : ExProd a) (e : Q(ℝ)) : Option (Q(0 < $a) × Result ExProd q($a ^ $e)) · Mathlib.Tactic.RPowRing.evalPow

ExBase inductive

A monomial, which is a product of powers of ExBase expressions, terminated by a (nonzero) constant coefficient. · Mathlib.Tactic.RPowRing.ExBase

ExProd inductive

A monomial, which is a product of powers of ExBase expressions, terminated by a (nonzero) constant coefficient. · Mathlib.Tactic.RPowRing.ExProd

F

FiniteEntropy def

TODO: replace FiniteSupport hypotheses ∈ these files with FiniteEntropy hypotheses. · ProbabilityTheory.FiniteEntropy

FiniteKernelSupport def

The analogue of FiniteSupport for probability kernels. · ProbabilityTheory.Kernel.FiniteKernelSupport

FiniteRange class

The property of having a finite range. · FiniteRange

FiniteSupport class

A measure has finite support if there exists a finite set whose complement has zero measure. · ProbabilityTheory.FiniteSupport

finrank def

The dimension of the affine span over ℤ of a subset of an additive group. · AffineSpace.finrank

finrank abbrev

The dimension of a submodule · Submodule.finrank

fintype abbrev

fintype structure on the range of a finite range map. · FiniteRange.fintype

I

id def

def ExBase.id {e : Q(ℝ)} : ExBase e → ℕ · Mathlib.Tactic.RPowRing.ExBase.id

IsShift def

A set A is a shift of a set B if it can be written as x + B. · IsShift

IsUniform structure

The assertion that the law of $X$ is the uniform probability measure on a finite set $H$. While in applications $H$ will be non-empty finite set, $X$ measurable, and and $μ$ a probability measure, it could be technically convenient to have … · ProbabilityTheory.IsUniform

K

KLDiv def

If X, Y are two G-valued random variables, the Kullback--Leibler divergence is defined as KL(X ‖ Y) := ∑ₓ 𝐏(X = x) log (𝐏(X = x) / 𝐏(Y = x)). · KLDiv

M

M abbrev

The monad for RingNF contains, in addition to the AtomM state, a simp context for the main traversal and a simp function (which has another simp context) to simplify normalized polynomials. · Mathlib.Tactic.RPowRing.M

MeasurableFinGroup class

We will frequently be working with finite additive groups with the discrete sigma-algebra. · MeasurableFinGroup

measureEntropy def

def measureEntropy (μ : Measure S · ProbabilityTheory.measureEntropy

measureMutualInfo def

def measureMutualInfo (μ : Measure (S × T) · ProbabilityTheory.measureMutualInfo

mk def

def AEFiniteKernelSupport.mk {μ} {κ : Kernel T S} (_hκ : AEFiniteKernelSupport κ μ) : Kernel T S · ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk

multiDist def

Let X_[m] = (X₁, ..., Xₘ) be a non-empty finite tuple of G-valued random variables X_i. Then we define D[X_[m]] = H[∑ i, X_i'] - 1/m*∑ i, H[X_i'], where the X_i' are independent copies of the X_i. · multiDist

multiRefPackage structure

A structure that packages all the fixed information in the main argument. See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Problem.20when.20instances.20are.20inside.20a.20structure for more discussion of the design … · multiRefPackage

multiTau def

If $(X_i)_{1 \leq i \leq m}$ is a tuple, we define its $\tau$-functional $$ \tau[ (X_i)_{1 \leq i \leq m}] := D[(X_i)_{1 \leq i \leq m}] + \eta \sum_{i=1}^m d[X_i; X^0].$$ · multiTau

multiTauMinimizes def

A $\tau$-minimizer is a tuple $(X_i)_{1 \leq i \leq m}$ that minimizes the $\tau$-functional among all tuples of $G$-valued random variables. · multiTauMinimizes

mutualInfo def

def mutualInfo (κ : Kernel T (S × U)) (μ : Measure T) : ℝ · ProbabilityTheory.Kernel.mutualInfo

mutualInfo def

def mutualInfo (X : Ω → S) (Y : Ω → T) (μ : Measure Ω · ProbabilityTheory.mutualInfo

N

not_in_coset def

The property of two sets A,B of a group G not being contained in cosets of the same proper subgroup. · not_in_coset

NotInCoset def

The property of two sets A, B of a group G not being contained in cosets of the same proper subgroup · NotInCoset

O

offDiag_sum abbrev

The sum of f away from the diagonal. · offDiag_sum

P

phi def

Given $G$-valued random variables $X,Y$, define $$ \phi[X;Y] := d[X;Y] + \eta(\rho(X) + \rho(Y))$$. · phi

phiMinimizes def

Given $G$-valued random variables $X,Y$, define $$ \phi[X;Y] := d[X;Y] + \eta(\rho(X) + \rho(Y))$$ and define a \emph{$\phi$-minimizer} to be a pair of random variables $X,Y$ which minimizes $\phi[X;Y]$. · phiMinimizes

prod abbrev

The pair of two random variables · prod

R

rdist def

def rdist (κ : Kernel T G) (η : Kernel T' G) (μ : Measure T) (ν : Measure T') : ℝ · ProbabilityTheory.Kernel.rdist

rdist def

def rdist (X : Ω → G) (Y : Ω' → G) (μ : Measure Ω · rdist

rdistm def

def rdistm (μ ν : Measure G) : ℝ · ProbabilityTheory.Kernel.rdistm

refPackage structure

A structure that packages all the fixed information in the main argument. In this way, when defining the τ functional, we will only only need to refer to the package once in the notation instead of stating the reference spaces, the … · refPackage

Result abbrev

abbrev Result · Mathlib.Tactic.RPowRing.Result

reverse def

def reverse (κ : Kernel α (β × γ × δ)) : Kernel α (δ × γ × β) · ProbabilityTheory.Kernel.reverse

rewrite def

def rewrite (parent : Expr) (root · Mathlib.Tactic.RPowRing.rewrite

rho def

We define $\rho(X) := (\rho^+(X) + \rho^-(X))/2$. · rho

rhoMinus def

For any $G$-valued random variable $X$, we define $\rho^-(X)$ to be the infimum of $D_{KL}(X \Vert U_A + T)$, where $U_A$ is uniform on $A$ and $T$ ranges over $G$-valued random variables independent of $U_A$. · rhoMinus

rhoMinusSet def

The set of possible values of $D_{KL}(X \Vert U_A + T)$, where $U_A$ is uniform on $A$ and $T$ ranges over $G$-valued random variables independent of $U_A$. We also require an absolute continuity condition so that the KL divergence makes … · rhoMinusSet

rhoPlus def

For any $G$-valued random variable $X$, we define $\rho^+(X) := \rho^-(X) + \bbH(X) - \bbH(U_A)$. · rhoPlus

rpowRingLocalDecl def

Use rpow_ring to rewrite hypothesis h. · Mathlib.Tactic.RPowRing.rpowRingLocalDecl

rpowRingTarget def

Use rpow_ring to rewrite the main goal. · Mathlib.Tactic.RPowRing.rpowRingTarget

run def

Runs a tactic in the RingNF.M monad, given initial data: · Mathlib.Tactic.RPowRing.M.run

S

self_or_prod abbrev

abbrev self_or_prod : Fin 2 → Type _ · ProbabilityTheory.iIndepFun.self_or_prod

setRuzsaDist def

The Ruzsa distance between two subsets A, B of a group G is defined to be the Ruzsa distance between their uniform probability distributions. Is only intended for use when A, B are finite and non-empty. · ProbabilityTheory.setRuzsaDist

support def

def _root_.MeasureTheory.Measure.support (μ : Measure S) [hμ : FiniteSupport μ] : Finset S · ProbabilityTheory._root_.MeasureTheory.Measure.support

symmGroup def

The symmetry group Sym of $X$: the set of all $h ∈ G$ such that $X + h$ has an identical distribution to $X$. · symmGroup

T

tau def

If $X_1,X_2$ are two $G$-valued random variables, then $$ \tau[X_1; X_2] := d[X_1; X_2] + \eta d[X^0_1; X_1] + \eta d[X^0_2; X_2].$$ Here, $X^0_1$ and $X^0_2$ are two random variables fixed once and for all in most of the argument. To … · tau

TauMinimizes def

Property recording the fact that two random variables minimize the tau functional. Expressed in terms of measures on the group to avoid quantifying over all spaces, but this implies comparison with any pair of random variables, see Lemma … · TauMinimizes

toFinset def

The range of a finite range map, as a finset. · FiniteRange.toFinset

toProd def

Embed an exponent (an ExBase, ExProd pair) as an ExProd by multiplying by 1. · Mathlib.Tactic.RPowRing.ExBase.toProd

W

WeakPFRAsymmConclusion def

Separating out the conclusion of weak_PFR_asymm for convenience of induction arguments. · WeakPFRAsymmConclusion

Other

κ abbrev

abbrev κ : Fin 3 → Type · ProbabilityTheory.iIndepFun.κ

κ abbrev

abbrev κ : Fin 2 → Type · ProbabilityTheory.iIndepFun.κ

κ_equiv def

def κ_equiv : (Σ i, κ i) ≃ Fin 4 · ProbabilityTheory.iIndepFun.κ_equiv

κ_equiv def

def κ_equiv : (Σ i, κ i) ≃ Fin 3 · ProbabilityTheory.iIndepFun.κ_equiv

Terms from the explanations

Words defined in the explanations on this site (Lean4 Domain Explanation Language term lines). Where they appear, they link here.

affine dimension

the dimension of the smallest affine subspace over the integers containing a set, written AffineSpace.finrank over the integers in the source. · weak_PFR_int

doubling constant

the number K bounding |A + A| / |A| from above; small K means A is close to a subgroup. · PFR_conjecture

elementary abelian 2-group

an abelian group in which every element has order at most 2; the same thing as a vector space over the field with two elements, here a module over ZMod 2. · PFR_conjecture

Ruzsa distance

for random variables X and Y in an abelian group, d[X ; Y] = H[X' - Y'] - H[X']/2 - H[Y']/2, where X' and Y' are independent copies and H is Shannon entropy in nats. · rdist_le_of_isUniform_of_card_sub_le

tau functional

tau[X1 ; X2] = d[X1 ; X2] + eta d[X01 ; X1] + eta d[X02 ; X2], where X01 and X02 are the fixed reference variables of the package; minimizing it is the engine of the entropic proof. · entropic_PFR_conjecture

Types

What kind of object something is. The Reading says these in words wherever they appear.

Bool

true or false

Equiv.Perm

Equiv.Perm α — a permutation (reordering) of α

EReal

a real number or ±∞

EuclideanSpace

EuclideanSpace ℝ (Fin n) — a point in n-dimensional space

Fin

Fin n — a number from 0 up to n − 1

Finset

Finset α — a finite set of elements of α

Ideal

Ideal R — a ideal (Ideal R)

IntermediateField

IntermediateField K L — a intermediate field (IntermediateField K L)

List

List α — a list of elements of α

Matrix

Matrix m n R — a matrix with rows m, columns n and entries in R

Measure

Measure α — a measure on α (a way to give sets a size)

Multiset

Multiset α — a finite collection of elements of α, repeats allowed

Option

Option α — either nothing or an element of α

Polynomial, R[X]

Polynomial R — a polynomial with coefficients in R

Prop

a statement (something true or false)

Set

Set α — a set of elements of α

SimpleGraph

SimpleGraph V — a graph whose vertices are the elements of V

String

a piece of text

Subfield

Subfield K — a subfield (Subfield K)

Subgroup

Subgroup G — a subgroup (Subgroup G)

Submodule

Submodule R M — a submodule (Submodule R M)

Subring

Subring R — a subring (Subring R)

Type, Type*, Type _, Type u, Type v, Sort*

a type (a collection of objects)

ZMod

ZMod n — an integer modulo n

× (pair type)

α × β — a pair (α, β)

ℂ, Complex

a complex number

ℕ+

a positive whole number

ℕ, Nat

a natural number (0, 1, 2, …)

ℚ, Rat

a rational number (a fraction)

ℝ, Real

a real number

ℝ≥0, NNReal

a real number that is at least 0

ℝ≥0∞, ENNReal

a number from 0 to ∞, ∞ included

ℤ, Int

an integer

→ (function type)

α → β — a function that takes α and gives β

Structures a type can have

Written in square brackets, such as [Field K]. Lean finds them by itself (they are type classes).

AddCommGroup

[AddCommGroup G] — G is a commutative group under addition

AddGroup

[AddGroup G] — G is a group under addition

CharZero

[CharZero α] — in α, 1 + 1 + … + 1 is never 0

CommGroup

[CommGroup G] — G is a commutative group

CommRing

[CommRing R] — R is a commutative ring: you can add, subtract and multiply, and order of multiplication does not matter

CommSemiring

[CommSemiring R] — R has addition and commutative multiplication

Countable

[Countable α] — α is countable

DecidableEq

[DecidableEq α] — equality between elements of α can be checked

DecidablePred

[DecidablePred p] — whether p holds can be checked

Fact

[Fact (Nat.Prime p)] — it is known that Nat.Prime p

Field

[Field K] — K is a field: you can add, subtract, multiply and divide (except by 0)

Finite

[Finite α] — α has finitely many elements

Fintype

[Fintype α] — α has finitely many elements

Group

[Group G] — G is a group: you can multiply and undo multiplication

Inhabited

[Inhabited α] — α has a chosen default element

InnerProductSpace

[InnerProductSpace ℝ E] — E has angles and lengths (an inner product)

LinearOrder

[LinearOrder α] — any two elements of α can be compared

MeasurableSpace

[MeasurableSpace X] — X has measurable sets

MetricSpace

[MetricSpace X] — X has a distance between any two points

Module

[Module R M] — M is a module (a vector space when the scalars form a field)

Monoid

[Monoid M] — M has a multiplication with a 1

NeZero

[NeZero n] — n is not 0

Nonempty

[Nonempty α] — α has at least one element

Nontrivial

[Nontrivial α] — α has at least two different elements

NormedAddCommGroup

[NormedAddCommGroup E] — E has a length (norm) for its elements

NormedSpace

[NormedSpace ℝ E] — E is a vector space with lengths

PartialOrder

[PartialOrder α] — α has an order (some pairs may be incomparable)

Ring

[Ring R] — R is a ring: you can add, subtract and multiply

Semiring

[Semiring R] — R has addition and multiplication

TopologicalSpace

[TopologicalSpace X] — X has a notion of nearness (open sets)

Properties

Statements about functions, numbers and sets that the Reading puts in words, each shown on a sample use.

AEMeasurable

AEMeasurable f — f is measurable, apart from a set of measure zero

AEStronglyMeasurable

AEStronglyMeasurable f — f is (strongly) measurable, apart from a set of measure zero

Antitone

Antitone f — f never increases

BddAbove

BddAbove S — S is bounded above

BddBelow

BddBelow S — S is bounded below

Bijective

Bijective f — f is a bijection: a perfect one-to-one pairing

BijOn

BijOn f s t — f pairs s one-to-one with t

Collinear

Collinear ℝ S — the points S lie on one line

Colorable

Colorable G n — the graph can be colored with n colors so that neighbors get different colors

Commute

Commute a b — a and b commute: their product is the same in either order

Computable

Computable f — f is computable

ConcaveOn

ConcaveOn ℝ s f — f is concave on s: its graph bends downward

ContDiff

ContDiff ℝ n f — f is smooth: it can be differentiated n times, continuously

ContDiffAt

ContDiffAt ℝ n f x — f is smooth at x

Continuous

Continuous f — f is continuous: no jumps or breaks

ContinuousAt

ContinuousAt f x — f is continuous at x

ContinuousOn

ContinuousOn f s — f is continuous on s

ContinuousWithinAt

ContinuousWithinAt f s x — f is continuous at x within s

Convex

Convex ℝ s — s is convex: it contains the segment between any two of its points

ConvexOn

ConvexOn ℝ s f — f is convex on s: its graph bends upward

Coprime

Coprime a b — a and b are coprime: no common factor bigger than 1

Countable

Countable S — S is countable

Dense

Dense S — S is dense: it comes arbitrarily close to every point

Differentiable

Differentiable ℝ f — f is differentiable: it has a derivative everywhere

DifferentiableAt

DifferentiableAt ℝ f x — f has a derivative at x

DifferentiableOn

DifferentiableOn ℝ f s — f has a derivative at every point of s

Disjoint

Disjoint s t — s and t have nothing in common

Even

Even n — n is even

Finite

Finite S — S is finite

HasDerivAt

HasDerivAt f f' x — f has derivative f' at x

HasSum

HasSum a s — the terms a add up to s

IdentDistrib

IdentDistrib X Y — X and Y have the same distribution

iIndepFun

iIndepFun m X μ — the random variables X are independent

IndepFun

IndepFun X Y — the random variables X and Y are independent

Infinite

Infinite S — S is infinite

Injective

Injective f — f is injective: different inputs always give different outputs

InjOn

InjOn f s — f is injective on s: different inputs there give different outputs

Integrable

Integrable f — f is integrable (its integral is finite)

IntegrableOn

IntegrableOn f s — f is integrable on s

IntervalIntegrable

IntervalIntegrable f volume a b — f can be integrated from a to b

Involutive

Involutive f — applying f twice gives back the input

Irrational

Irrational x — x is irrational: not a fraction of two integers

Irreducible

Irreducible p — p is irreducible: it cannot be factored into smaller non-units

IsAlgebraic

IsAlgebraic ℤ x — x is algebraic: a root of a nonzero polynomial

IsBigO

IsBigO l f g — f is at most a constant times g (big O)

IsClosed

IsClosed F — F is a closed set

IsCompact

IsCompact K — K is compact (closed and bounded, in ℝⁿ)

IsConnected

IsConnected S — S is connected: it is all in one piece

IsCoprime

IsCoprime a b — a and b are coprime

IsGLB

IsGLB S m — m is the greatest lower bound of S

IsGreatest

IsGreatest S m — m is the greatest element of S

IsLeast

IsLeast S m — m is the least element of S

IsLittleO

IsLittleO l f g — f is negligible compared with g (little o)

IsLUB

IsLUB S m — m is the least upper bound of S

IsOpen

IsOpen U — U is an open set

IsProbabilityMeasure

IsProbabilityMeasure μ — μ is a probability measure: the whole space has size 1

IsSquare

IsSquare n — n is a perfect square

IsUnit

IsUnit a — a has a multiplicative inverse

LeftInverse

LeftInverse g f — g undoes f: applying f then g gives back the input

LinearIndependent

LinearIndependent K v — the vectors v are linearly independent

LipschitzWith

LipschitzWith K f — f never stretches distances by more than a factor K

MapsTo

MapsTo f s t — f sends every element of s into t

Measurable

Measurable f — f is measurable

MeasurableSet

MeasurableSet S — S is a measurable set (one that has a size)

MeasurePreserving

MeasurePreserving f — f preserves the measure: sets keep their size

MemLp

MemLp f p — f is in Lᵖ for p = p (the p-th power of |f| has a finite integral)

Monotone

Monotone f — f never decreases: a bigger input gives an output at least as big

MonotoneOn

MonotoneOn f s — f never decreases on s

Nonempty

Nonempty S — S is not empty

Odd

Odd n — n is odd

Pairwise

Pairwise r — every two different elements are related by r

Periodic

Periodic f c — f repeats every c

Perm

Perm l₁ l₂ — l₁ is a rearrangement of l₂

Prime

Prime p — p is a prime number

Primrec

Primrec f — f is primitive recursive (computable by a simple kind of program)

Reachable

Reachable u v — there is a path from u to v

RightInverse

RightInverse g f — g is a right inverse of f

Sbtw

Sbtw ℝ x y z — y lies strictly between x and z

Squarefree

Squarefree n — n is squarefree: no square bigger than 1 divides it

StrictAnti

StrictAnti f — f is strictly decreasing

StrictMono

StrictMono f — f is strictly increasing: a bigger input gives a bigger output

StronglyMeasurable

StronglyMeasurable f — f is strongly measurable

Summable

Summable a — the series of the terms a adds up to a finite value

Surjective

Surjective f — f is surjective: every possible output is reached

SurjOn

SurjOn f s t — f maps s onto all of t

Tendsto

Tendsto f atTop (𝓝 0) — f tends to 0 as the input grows without bound

Transcendental

Transcendental ℤ x — x is transcendental: not a root of any nonzero polynomial with integer coefficients

UniformContinuous

UniformContinuous f — f is uniformly continuous

Wbtw

Wbtw ℝ x y z — y lies between x and z

Symbols

Notation a newcomer may not know. A Reading lists the ones its statement uses.

#s, card

the number of elements

%

remainder after division

.Finite

the set has finitely many elements

.Infinite

the set has infinitely many elements

/

division; on ℕ and ℤ it rounds down

^

a power

A × B

pairs (a, b) with a from A and b from B

answer(…)

marks the answer the problem asks for; answer(sorry) means the answer is not filled in

atTop

“as the input goes to infinity”

choose

binomial coefficient: the number of ways to pick k things from n

deriv

the derivative

exp

the exponential function eˣ

f '' s

the image: all outputs f gives on s

f =O[l] g

big O: f is at most a constant times g, along l

f =o[l] g

little o: f is negligible compared with g, along l

f ⁻¹' s

the preimage: all inputs that f sends into s

f ∘ g

composition: first g, then f

f ≪ g

f is at most a constant times g (for large inputs)

Finset.range n

the numbers 0, 1, …, n − 1

fun x ↦ …

a function: send x to …

gcd

greatest common divisor

lcm

least common multiple

log

the natural logarithm

n !

factorial: 1 · 2 · … · n

Set.Icc a b

the closed interval [a, b]

Set.Ioo a b

the open interval (a, b)

sᶜ

the complement: everything not in s

x⁻¹

the inverse, 1 / x for numbers

{x | p x}

the set of all x with property p

|x|

absolute value

¬

“not”

π

pi

‖x‖

the norm (length) of x

ℂ

the complex numbers

ℕ

the natural numbers 0, 1, 2, … (in Lean ℕ starts at 0)

ℚ

the rational numbers (fractions)

ℝ

the real numbers

ℤ

the integers …, −2, −1, 0, 1, 2, …

↑x

x viewed in a bigger number system, such as a natural number as a real number

→

“implies”, or for functions “to”

↔

“if and only if”: both directions hold

∀

“for every”

∃

“there exists”

∃!

“there is exactly one”

∏

a product over a range or a finite set

∑

a sum over a range or a finite set

√

square root

∣

“divides”: a ∣ b means b is a multiple of a

∧

“and”

∨

“or”

∩

intersection: what both sets have in common

∪

union: everything in either set

∫

an integral

≡ [MOD n]

same remainder when divided by n

⌈x⌉

ceiling: the smallest integer at least x

⌊x⌋

floor: the largest integer at most x

𝓝 x

“near x”: used for limits

Tactics

Steps inside a proof that starts with by. Each says what the tactic does in general; the goal it leaves depends on the proof.

abel

Both sides are equal by rearranging sums (abel: algebra in commutative groups).

absurd

absurd h h' — Two facts contradict each other: h h'.

admit

Not proved yet: admit is a placeholder, so this proof is unfinished.

aesop

Search automatically for a proof using many small rules (aesop).

all_goals

all_goals simp — On every remaining goal: Simplify with Lean's standard simplification rules.

and_intros

Split the “and” goal into its parts.

any_goals

any_goals simp — On every goal where it works: Simplify with Lean's standard simplification rules.

apply

apply h — Work backwards with h: it gives the goal once its own conditions hold, so those conditions become the new goals.

apply_fun

apply_fun f at h — Apply f to both sides in h.

assumption

The goal is exactly one of the assumptions.

bound

Prove the bound by combining standard inequalities.

by_cases

by_cases h : x = 0 — Split into two cases: x = 0 is true, or it is false.

by_contra

Proof by contradiction: assume the opposite and reach something false.

by_contra!

Proof by contradiction, with the assumed opposite already simplified.

calc

A chain of steps, each one justified on its own line.

case

case zero => simp — The case zero.

cases

cases h — Split into cases on how h can be built.

cases'

cases' h with x hx — Split into cases on how h can be built.

change

change a + 0 = a — Restate the goal as a + 0 = a (the same thing, written differently).

choose

choose f hf using h — From “for every x there is a y”, pick a function giving such a y: f hf using h.

classical

Allow classical reasoning from here on (every statement is true or false, even if we cannot compute which).

clear

clear h — Forget the assumptions h; they are not needed any more.

congr

Reduce to showing the matching parts of both sides are equal.

constructor

constructor function Object() { [native code] } — Split the goal into its parts: for “A and B” prove A and B, for “A iff B” prove both directions.

constructorm

Split every “and”-like assumption or goal into its parts.

continuity

Built automatically from the rules for continuous functions.

contradiction

Two assumptions contradict each other, so this case is done.

contrapose

Prove the contrapositive: if the conclusion fails, then so does the assumption.

contrapose!

Prove the contrapositive, with the negations pushed inward.

conv

Rewrite inside one chosen part of the goal.

conv_lhs

Rewrite inside the left-hand side only.

conv_rhs

Rewrite inside the right-hand side only.

convert

convert h using 1 — Close the goal with h, which almost matches; any differences become new goals.

decide

Lean checks it by direct computation (decide).

delta

delta f — Expand the definition of f.

dsimp

Simplify by unfolding definitions.

erw

erw [h] — Rewrite using h, matching up to unfolding definitions.

exact

exact h — Finish: h is exactly what is needed.

exact_mod_cast

exact_mod_cast h — Finish with h, ignoring conversions between number systems.

exacts

exacts [h₁, h₂] — Finish each remaining goal with [h₁, h₂].

exfalso

Switch to proving False: this case is impossible.

exists

exists 2 — Give 2 as the example that exists.

existsi

existsi 2 — Give 2 as the example that exists.

ext

Two functions (or sets) are equal when they agree at every input.

ext1

Two functions (or sets) are equal when they agree at every input.

field

Both sides are equal by algebra with division (field).

field_simp

Clear the denominators.

filter_upwards

Reduce a statement about “eventually” or “almost everywhere” to one about each point.

fin_cases

fin_cases i — Try each of the finitely many values of i, one case each.

finiteness

The quantity is finite (not ∞), checked automatically (finiteness).

first

first | simp | ring — Try these in order until one works: simp, ring

focus

Work on the first goal only.

fun_prop

Built automatically from the rules for continuity, differentiability or measurability (fun_prop).

funext

Two functions are equal when they agree at every input.

gcongr

Compare the two sides piece by piece: if each part on the left is at most the matching part on the right, so is the whole (gcongr).

generalize

generalize e : f x = y — Replace a specific expression by a general variable: e : f x = y.

grind

Automated reasoning that combines equalities, cases and arithmetic (grind).

group

Both sides are equal by the rules of a group (group).

grw

grw [h] — Rewrite with an inequality (or another relation) instead of an equation: h.

have

have h : 0 < 2 := by norm_num — Establish an intermediate fact h: 0 is less than 2. Proved by: Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.

have'

have' h : 0 < 2 := by norm_num — Establish an intermediate fact h: 0 is less than 2. Proved by: Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.

haveI

haveI h : 0 < 2 := by norm_num — Establish an intermediate fact h: 0 is less than 2. Proved by: Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.

if

Split on a condition, if-then-else.

induction

induction n with — Prove it by induction on n: first a starting case, then a step from each case to the next.

induction'

induction' n with n ih — Prove it by induction on n: a starting case, then the step to the next case.

infer_instance

Lean finds this automatically from known structures.

interval_cases

interval_cases n — Try every possible value of n in its known range, one case each.

intro

Move the next variable or assumption of the goal into view.

intros

Introduce everything the goal starts with.

left

Prove the left side of the “or”.

let

let y := x + 1 — Give a name to a value: y := x + 1.

letI

letI inst := Classical.decEq α — Give a name to a structure for Lean to use: inst := Classical.decEq α.

lia

Whole-number arithmetic, decided automatically (lia: linear integer arithmetic).

lift

lift n to ℕ using hn — Treat n to ℕ using hn as a value of a smaller number system, since it is known to fit.

linarith

It follows by adding up the linear inequalities in the assumptions (linarith).

linear_combination

linear_combination h₁ - h₂ — The goal is exactly this combination of the assumptions: h₁ - h₂.

match

match n with — Split on the shape of n, one case per pattern.

measurability

Built automatically from the rules for measurable functions.

module

Both sides are equal by algebra with vectors and scalars (module).

native_decide

Checked by running compiled code (native_decide). This also trusts the compiler, an extra axiom.

next

The next case.

nlinarith

Like linarith, but also multiplies assumptions together, which handles squares and products.

nofun

No case can occur, so there is nothing to prove.

nomatch

nomatch h — No case of h can occur.

noncomm_ring

Both sides are equal by algebra where multiplication need not commute (noncomm_ring).

norm_cast

Move the statement between number systems (ℕ, ℤ, ℚ, ℝ) to where it is simplest.

norm_num

Do the arithmetic: norm_num proves number facts such as 2 + 2 = 4, 7 ≠ 0 or that 13 is prime.

norm_num1

Do the arithmetic.

nth_rewrite

nth_rewrite 2 [h] — Rewrite one chosen occurrence using h.

nth_rw

nth_rw 2 [h] — Rewrite one chosen occurrence using h.

obtain

obtain ⟨x, hx⟩ := h — Unpack h into its pieces ⟨x, hx⟩.

omega

Whole-number arithmetic with +, −, constants and comparisons, decided automatically (omega).

on_goal

on_goal 2 => simp — On one chosen goal: 2 => simp.

order

It follows from the order facts in the assumptions (order).

peel

peel h with x hx — Strip matching quantifiers from both sides: h with x hx.

polyrith

The goal is a combination of the equations in the assumptions (polyrith).

positivity

The expression is positive (or at least 0), checked term by term (positivity).

push

Push the operation inward.

push_cast

Push the number-system conversions (↑) inward.

push_neg

Push the “not” inward: not-for-every becomes there-is-a-counterexample, and so on.

qify

Move the statement to ℚ, where division behaves normally.

rcases

rcases h with ⟨x, hx⟩ — Unpack h into its pieces ⟨x, hx⟩, one case per alternative.

refine

refine ⟨?_, ?_⟩ — Fill in the goal with ⟨?_, ?_⟩; every ?_ hole becomes a new goal.

refine'

refine' ⟨_, _⟩ — Fill in the goal with ⟨_, _⟩; every _ hole becomes a new goal.

rename_i

rename_i x y — Name the unnamed variables x, y.

repeat

repeat rw [h] — Repeat as long as it works: Rewrite using h.

replace

replace h : 0 < x := by linarith — Replace an assumption with a stronger form: the fact h: 0 is less than x. Proved by: It follows by adding up the linear inequalities in the assumptions (linarith).

revert

revert x — Put x back into the goal, so the goal is about every possible value of it.

rewrite

rewrite [h] — Rewrite using h.

rfl

Both sides are the same by definition (rfl).

right

Prove the right side of the “or”.

ring

Both sides are equal by algebra: expand and collect like terms (ring).

ring_nf

Put the expressions into a standard algebraic form.

rintro

rintro ⟨x, hx⟩ — Introduce and unpack in one go: ⟨x, hx⟩.

rotate_left

Change the order of the goals.

rw

rw [h] — Rewrite using h.

rwa

rwa [h] at h₁ — Rewrite using h in h₁, and then the goal is one of the assumptions.

set

set y := x + 1 with hy — Give a name to an expression and use the name from now on: y := x + 1.

show

show a + 0 = a — Restate the goal as a + 0 = a.

simp

Simplify with Lean's standard simplification rules.

simp_all

Simplify the goal and all the assumptions together.

simp_arith

Simplify, including arithmetic on natural numbers.

simp_rw

simp_rw [h] — Rewrite using h, also inside “for every” and “there is”.

simpa

Simplify, and the goal closes.

sorry

Not proved yet: sorry is a placeholder, so this proof is unfinished.

specialize

specialize h 2 — Use the assumption h for the specific 2.

split

Split into one case for each branch of the if-then-else or match.

split_ifs

Split into a case for each branch of every if-then-else.

subst

subst h — Replace h by what it equals, everywhere.

suffices

suffices h : 0 < x by linarith — It is enough to prove 0 < x; that is shown next, then used to finish.

swap

Work on the second goal first.

symm

Swap the two sides.

tauto

Pure logic: it follows from the assumptions by the rules of and, or, not and implies (tauto).

trans

trans b — Go through a middle point b.

trivial

This goal is immediate.

try

try linarith — Try this, and carry on if it fails: It follows by adding up the linear inequalities in the assumptions (linarith).

unfold

unfold f — Expand the definition of f.

use

use 2 — Give 2 as the example that exists; what remains is to check it works.

wlog

wlog h : a ≤ b with H — Without loss of generality, h : a ≤ b; the other case follows the same way.

zify

Move the statement from ℕ to ℤ, where subtraction behaves normally.

Lean words

Words of the Lean language itself, and of how its projects are organized.

#check, #eval

#eval 2 + 2 — Commands that ask Lean a question while you write: the type of a term, or its value.

:=

def two : ℕ := 2 — “is defined as” or “is proved by”: what comes after it is the value or the proof.

@[simp] (attribute)

@[simp] theorem add_zero' (n : ℕ) : n + 0 = n := rfl — Attributes add information to a declaration: @[simp] tells the simp tactic to use it.

_ and ?_

refine ⟨?_, ?_⟩ — A hole: Lean fills in _ by itself, and ?_ becomes a new goal to prove.

abbrev

abbrev Point := ℝ × ℝ — A definition that Lean unfolds freely, like a shorthand.

anonymous constructor ⟨ ⟩

⟨2, by norm_num⟩ — Builds an object from its parts: a pair, a structure, or a proof of “and” or “there exists”.

axiom

axiom my_assumption : 1 = 1 — Something assumed without proof. Lean's three standard axioms (propext, Classical.choice, Quot.sound) are normal; anything beyond them is worth a closer look.

by

theorem t : 1 + 1 = 2 := by norm_num — Starts a proof made of tactics.

class

class Zero (α : Type) where zero : α — A structure that Lean finds by itself when it is needed (a type class), such as “this type has an addition”.

class inductive

class inductive Decidable (p : Prop) — A class given by the ways to build it, like inductive.

declaration

Any named thing in Lean: a theorem, a definition, and so on. Each one has a line on its file page.

def (definition)

def double (n : ℕ) : ℕ := 2 * n — A name for a precise idea or a computation, such as “continuous” or “double a number”.

dot notation

n.succ — x.foo means Foo.foo x, where Foo is the type of x: n.succ is Nat.succ n.

example

example : 2 + 2 = 4 := rfl — A statement proved without a name, to show that something works.

explicit argument ( )

(n : ℕ) — An argument you write when you use the result.

goal

What is left to prove at a point in a proof. Each tactic changes the goal.

h.1, h.2

h.1 — The first and second part of h, for example of an “and”.

hypothesis (assumption)

(h : 0 < n) — A named fact you may use in a proof, such as h : 0 < n.

implicit argument { }

{α : Type} — An argument Lean works out by itself from the others.

import

import Mathlib.Data.Real.Basic — Brings in the declarations of another file or library.

inductive

inductive Color | red | green — A new type given by the ways to build its elements. The natural numbers are 0, or one more than a natural number.

instance

instance : Zero ℕ := ⟨0⟩ — A proof or construction that a type belongs to a class. Lean then finds it by itself.

instance argument [ ]

[Field K] — An argument Lean finds by itself among the class instances it knows.

kernel

The small core of Lean that finally accepts or rejects a proof.

Lake

lake build — Lean's build tool. A project's lakefile says which libraries it has and which it needs.

lemma

lemma helper (n : ℕ) : n ≤ n + 1 := by omega — A theorem, usually a smaller helper for a bigger one.

Mathlib

import Mathlib — The big shared library of formalized mathematics that many Lean projects build on.

namespace

namespace Nat … end Nat — A family name for declarations: inside namespace Nat, succ_le means Nat.succ_le.

noncomputable

noncomputable def half : ℝ := 1 / 2 — Marks a definition Lean cannot run as a program, usually because it uses choice or real numbers.

opaque

opaque secret : ℕ — A definition whose value Lean keeps hidden: only its type is known.

open

open Real — Lets you use short names: after open Real, pi means Real.pi.

private, protected

private theorem helper : True := trivial — private: usable only in this file. protected: must always be written with its full name.

proof

The argument. In Lean, a proof is code, and Lean checks every step of it.

Prop

(p : Prop) — The type of statements. A statement is true or false; its proofs are its elements.

section

section … end — A part of a file whose variables and open commands end with it.

sorry

theorem later : 1 = 1 := sorry — Lean's “I have not proved this yet”. A result that uses it is not finished, and the site flags it.

structure

structure Point where x : ℝ y : ℝ — A new kind of object made of named parts (its fields).

tactic

by rw [h] ring — One command inside a proof that starts with by, such as “rewrite using this equation”. The Reading explains each one.

termination_by

termination_by n — Says why a recursive definition stops: something gets smaller each time.

theorem

theorem two_pos : 0 < 2 := by norm_num — A statement that has been proved. The proof follows :=.

universe

universe u — The size level of types (Type u). You can usually ignore it.

variable

variable (n : ℕ) (hn : 0 < n) — Names (and assumptions) used by every result below it, until its section ends.

· (focusing dot)

constructor · norm_num · simp — Starts the proof of one goal when there are several.