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 · B · C · D · E · F · G · H · I · J · K · L · M · N · O · P · Q · R · S · T · U · V · W · Y · Other

A

A def

def A (hX : GeneralCase f (α' a α)) : Set X · A

adjointBoundaryOperator def

The operator S_{2,𝔲} f(x), given above Lemma 7.4.3. · TileStructure.Forest.adjointBoundaryOperator

adjointCarleson def

The definition of Tₚ*g(x), defined above Lemma 7.4.1 · adjointCarleson

adjointCarlesonRowSum def

The definition of T_{ℜ_j}*f(x), defined above Lemma 7.7.2. · TileStructure.Forest.adjointCarlesonRowSum

adjointCarlesonSum def

The definition of T_ℭ*g(x), defined at the bottom of Section 7.4 · adjointCarlesonSum

AESubadditiveOn def

The operator is subadditive on functions satisfying P with constant A (this is almost vacuous if A = ⊤). · MeasureTheory.AESubadditiveOn

AESublinearOn def

The operator is almost everywhere sublinear on functions satisfying P with constant A. · MeasureTheory.AESublinearOn

AllBallsCoverBalls def

For all r, balls of radius r in X are covered by n balls of radius a * r · AllBallsCoverBalls

approxHilbertTransform def

The approximate Hilbert transform L_N g, defined in (11.3.2). defined slightly differently. · approxHilbertTransform

approxOnCube def

The projection operator P_𝓒 f(x), given above Lemma 7.1.3. In lemmas the c will be pairwise disjoint on C. · TileStructure.Forest.approxOnCube

As def

The blow-up factor of repeatedly increasing the size of balls. · As

auxℭ def

def auxℭ (k n : ℕ) : Set (𝔓 X) · auxℭ

aux𝓒 def

def aux𝓒 (k : ℕ) : Set (Grid X) · aux𝓒

aux𝔐 def

def aux𝔐 (k n : ℕ) : Set (𝔓 X) · aux𝔐

B

BallsCoverBalls def

Balls of radius r in X are covered by n balls of radius r' · BallsCoverBalls

big_ball def

Ball that covers the image of `𝒬`. Radius chosen for convenience with `BallsCoverBalls.pow_mul` · big_ball

boundaryOperator def

The operator S_{1,𝔲} f(x), given in (7.1.4). · TileStructure.Forest.boundaryOperator

BoundedCompactSupport structure

Bounded compactly supported measurable functions · MeasureTheory.BoundedCompactSupport

BoundedFiniteSupport structure

Bounded measurable function $g$ on $X$ supported on a set of finite measure · BoundedFiniteSupport

C

c def

def c : Grid X → X · c

C10_0_1 def

The constant used in two_sided_metric_carleson. Has value 2 ^ (474 * a ^ 3) / (q - 1) ^ 6 in the blueprint. · C10_0_1

C1_0_2 def

The constant used in MetricSpaceCarleson and LinearizedMetricCarleson. Has value 2 ^ (443 * a ^ 3) / (q - 1) ^ 6 in the blueprint. · C1_0_2

C2_0_1 def

The constant used in Proposition 2.0.1. Has value 2 ^ (442 * a ^ 3) / (q - 1) ^ 5 in the blueprint. · C2_0_1

C2_0_2 def

The constant used in Proposition 2.0.2. Has value 2 ^ (442 * a ^ 3) / (q - 1) ^ 5 in the blueprint. · C2_0_2

C2_0_3 def

The constant appearing in Proposition 2.0.3. Has value 2 ^ (117 * a ^ 3) in the blueprint. · C2_0_3

C2_0_4_aux def

The constant in the f side of Proposition 2.0.4. Has value 2 ^ (283 * a ^ 3) in the blueprint. · TileStructure.Forest.C2_0_4_aux

C2_0_5 def

The constant occurring in Proposition 2.0.5. Has value 2 ^ (7 * a) in the blueprint. · C2_0_5

C2_1_1 def

def C2_1_1 (k : ℕ) (a : ℕ) : ℕ · C2_1_1

C2_1_2 def

The constant appearing in Lemma 2.1.2, 2 ^ {-95a}. · Grid._root_.C2_1_2

C2_1_3 def

The constant appearing in part 2 of Lemma 2.1.3. Equal to 2 ^ (102 * a ^ 3) in the blueprint. · C2_1_3

C3_0_4 def

The constant used in linearized_truncation and S_truncation. Has value 2 ^ (442 * a ^ 3 + 2) in the blueprint. · C3_0_4

C4_1_1 def

def C4_1_1 · C4_1_1

C4_1_7 def

TODO: fix overlapping instance warning; this will also fix the linter · C4_1_7

C4_2_1 def

7 / 10 · C4_2_1

C5_1_2 def

The constant used in Lemma 5.1.2. Has value 2 ^ (441 * a ^ 3) / (q - 1) ^ 4 in the blueprint. · C5_1_2

C5_1_2_optimized def

An optimized constant for the forest union theorem. The constant from the blueprint, defined as C5_1_2 below, is slightly worse. · C5_1_2_optimized

C5_1_3 def

The constant used in Lemma 5.1.3. Has value 2 ^ (120 * a ^ 3) / (q - 1) ^ 5 in the blueprint. · C5_1_3

C5_1_3_optimized def

An optimized constant for Lemma 5.1.3. · C5_1_3_optimized

C5_2_9 def

The constant in Lemma 5.2.9, with value D ^ (1 - κ * Z * (n + 1)) · C5_2_9

C5_3_2 def

def C5_3_2 (a : ℕ) : ℝ · C5_3_2

C5_3_3 def

The constraint on λ in the first part of Lemma 5.3.3. · C5_3_3

C5_4_8 def

The multiplicity appearing in Lemma 5.4.8. · C5_4_8

C6_1_2 def

Constant appearing in Lemma 6.1.2. Has value 2 ^ (102 * a ^ 3) in the blueprint. · C6_1_2

C6_1_3 def

Constant appearing in Lemma 6.1.3. Has value 2 ^ (103 * a ^ 3) in the blueprint. · C6_1_3

C6_1_5 def

The constant from lemma 6.1.5. Has value 2 ^ (232 * a ^ 3) in the blueprint. · Tile.C6_1_5

C6_1_6 def

The constant appearing in Lemma 6.1.6. · Antichain.C6_1_6

C6_2_1 def

The constant from lemma 6.2.1. Has value 2 ^ (231 * a ^ 3) in the blueprint. · Tile.C6_2_1

C6_2_3 def

The constant from lemma 6.2.3. · Tile.C6_2_3

C6_3_4 def

The constant appearing in Lemma 6.3.4. · Antichain.C6_3_4

C6_3_4' def

Auxiliary constant for Lemma 6.3.4. · Antichain.C6_3_4'

C8_0_1 def

The constant occurring in Lemma 8.0.1. · C8_0_1

C_carleson_hasStrongType def

The constant used in two_sided_metric_carleson_hasStrongType. · C_carleson_hasStrongType

C_control_approximation_effect def

The constant used in C_control_approximation_effect. · C_control_approximation_effect

C_control_approximation_effect' def

The constant used in C_control_approximation_effect'. · C_control_approximation_effect'

C_distribution_carlesonOperatorReal_le def

The constant used in C_distribution_carlesonOperatorReal_le. · C_distribution_carlesonOperatorReal_le

C_distribution_carlesonOperatorReal_le' def

The constant used in C_distribution_carlesonOperatorReal_le'. · C_distribution_carlesonOperatorReal_le'

C_distribution_le_of_eLpNorm_le def

The constant used in C_distribution_le_of_eLpNorm_le. · MeasureTheory.C_distribution_le_of_eLpNorm_le

C_K def

The constant used twice in the definition of the Calderon-Zygmund kernel. · C_K

C_LorentzInterpolation def

The constant occurring in the general real interpolation theorem (for Lorentz spaces) · C_LorentzInterpolation

C_realInterpolation def

The constant occurring in the real interpolation theorem · MeasureTheory.C_realInterpolation

C_realInterpolation_ENNReal def

The definition of the constant in the real interpolation theorem, when viewed as an element of ℝ≥0∞. · MeasureTheory.C_realInterpolation_ENNReal

C_Ts def

A constant used on the boundedness of T_Q^θ and T_*. We generally assume HasBoundedStrongType (linearizedNontangentialOperator Q θ K · ·) 2 2 volume volume (C_Ts a) throughout this formalization. · C_Ts

cancelPt def

The point o in the blueprint · cancelPt

carlesonOn def

The operator T_𝔭 defined in Proposition 2.0.2. · carlesonOn

carlesonOperator def

The generalized Carleson operator T, taking values in ℝ≥0∞. Use ENNReal.toReal to get the corresponding real number. · carlesonOperator

carlesonOperatorIntegrand def

The integrand in the (linearized) Carleson operator. This is G in Lemma 3.0.1. · carlesonOperatorIntegrand

carlesonOperatorReal def

TODO: avoid this extra definition? · carlesonOperatorReal

carlesonRowSum def

The definition of T_{ℜ_j}f(x), defined above Lemma 7.7.2. · TileStructure.Forest.carlesonRowSum

carlesonSum def

The operator T_ℭ f defined at the bottom of Section 7.4. We will use this in other places of the formalization as well. · carlesonSum

cc def

def cc (x : X) (r R : ℝ) · Set.Annulus.cc

cc def

def cc (x : X) (r R : ℝ≥0∞) · Set.EAnnulus.cc

ci def

def ci (x : X) (r : ℝ) · Set.Annulus.ci

ci def

def ci (x : X) (r : ℝ≥0∞) · Set.EAnnulus.ci

ClassicalCarleson def

Theorem 1.0.1: Carleson's theorem asserting a.e. convergence of the partial Fourier sums for continous functions. For the proof, see classical_carleson in the file Carleson.Classical.ClassicalCarleson. · ClassicalCarleson

ClosenessProperty structure

structure ClosenessProperty {k1 k2 : ℤ} (hk1 : -S ≤ k1) (hk2 : -S ≤ k2) (y1 : Yk X k1) (y2 : Yk X k2) : Prop · ClosenessProperty

co def

def co (x : X) (r R : ℝ) · Set.Annulus.co

co def

def co (x : X) (r R : ℝ≥0∞) · Set.EAnnulus.co

coe def

def 𝓓.coe (z : 𝓓 X) : Set X · 𝓓.coe

CompatibleFunctions class

A set Θ of (continuous) functions is compatible. A will usually be 2 ^ a. · CompatibleFunctions

component def

TODO: check whether this is the right approach · RCLike.component

Components def

TODO: check whether this is the right approach · RCLike.Components

const_K def

def const_K : ℕ · const_K

const_n def

TODO: linter false positive · const_n

correlation def

Def 6.2.1 (from Lemma 6.2.1), denoted by φ(y) in the blueprint. · Tile.correlation

CoveredByBalls class inductive

s can be covered by at most N balls with radius r. · CoveredByBalls

CP304 structure

Convenience structure for the parameters that stay constant throughout the recursive calls to finitary Carleson in the proof of Lemma 3.0.4. · CP304

cS_bound def

def cS_bound (x' : X) · TileStructure.Forest.cS_bound

cubeOf def

The definition I_i(x), given above Lemma 7.1.3. The cube of scale s that contains x. There is at most 1 such cube, if it exists. · TileStructure.Forest.cubeOf

cutoff def

cutoff R t x y is L(x, y) in the proof of Lemma 8.0.1. · cutoff

czApproximation def

The function g in Lemma 10.2.5. (both cases) · czApproximation

czBall abbrev

The ball B_j in the proof of Lemma 10.2.5 (general case). · czBall

czBall3 abbrev

The ball B_j* in Lemma 10.2.5 (general case). · czBall3

czBall6 abbrev

The ball B_j' introduced below Lemma 10.2.5 (general case). · czBall6

czBall7 abbrev

The ball B_j** in the proof of Lemma 10.2.5 (general case). · czBall7

czCenter def

The center of B_j in the proof of Lemma 10.2.5 (general case). · czCenter

czOperator def

The Calderon Zygmund operator T_r in chapter Two-sided Metric Space Carleson · czOperator

czOperatorBound def

The function F defined in Lemma 10.2.7. · czOperatorBound

czOperatorBoundSummand abbrev

abbrev czOperatorBoundSummand (hX : GeneralCase f (α' a α)) (i : ℕ) (x : X) : ℝ≥0∞ · czOperatorBoundSummand

czPartition def

Q_i in the proof of Lemma 10.2.5 (general case). · czPartition

czRadius def

The radius of B_j in the proof of Lemma 10.2.5 (general case). · czRadius

czRemainder def

The function b = ∑ⱼ bⱼ introduced below Lemma 10.2.5. In the finite case, we also use this as the function b = b₁ in Lemma 10.2.5. We choose a more convenient definition, but prove in tsum_czRemainder' that this is the same. · czRemainder

czRemainder' def

The function b_i in Lemma 10.2.5 (general case). · czRemainder'

CΩ def

1 / 5 · Construction.CΩ

c𝓑 def

The center function for the collection of balls 𝓑. · TileStructure.Forest.c𝓑

C𝓩 def

The constant appearing in 4.2.2 (3 / 10). · C𝓩

D

d def

def d · ChoiceScale.d

d def

def d (hX : GeneralCase f (α' a α)) (j : ℕ) · d

D2_1_3 def

The constant appearing in part 3 of Lemma 2.1.3. Equal to 2 ^ (127 * a ^ 3) in the blueprint. · D2_1_3

dach def

h(p) in the proof of Lemma 6.1.4 (dens₁ antichain h). · dach

defaultA abbrev

This is usually the value of the argument A in DoublingMeasure and CompatibleFunctions · defaultA

defaultD def

The constant D from (2.0.1). · defaultD

defaultS def

def defaultS : ℕ · defaultS

defaultZ def

The constant Z from (2.0.3). · defaultZ

defaultκ def

The constant κ from (2.0.2). · defaultκ

defaultτ def

defaultτ is the inverse of a. · defaultτ

dens' def

The definition dens'_k(𝔓') given in (5.1.6). · dens'

dens₁ def

This density is defined to live in ℝ≥0∞. Use ENNReal.toReal to get a real number. · dens₁

dens₂ def

This density is defined to live in ℝ≥0∞. Use ENNReal.toReal to get a real number. · dens₂

depth def

δ(x) in the blueprint. The depth of a point x in a set O is the supremum of radii of balls centred on x that are subsets of O. · depth

dirichletApprox def

The function L', defined in the Proof of Lemma 11.3.5. · dirichletApprox

dirichletApproxAux def

The function L'', defined in the Proof of Lemma 11.3.5. · dirichletApproxAux

dirichletKernel def

def dirichletKernel (N : ℕ) : ℝ → ℂ · dirichletKernel

dirichletKernel' def

def dirichletKernel' (N : ℕ) : ℝ → ℂ · dirichletKernel'

distribution def

The distribution function of a function f. Todo: rename to something more Mathlib-appropriate. · MeasureTheory.distribution

DoublingMeasure class

A metric space with a measure with some nice properties, including a doubling condition. This is called a "doubling metric measure space" in the blueprint. A will usually be 2 ^ a. · MeasureTheory.DoublingMeasure

doublingMeasure_real_two def

The volume measure on the real line is doubling. · doublingMeasure_real_two

E

E def

The set E defined in Proposition 2.0.2. · E

edgeScales def

The fringes of the scale interval in Lemma 3.0.2's proof that require separate handling. · edgeScales

eI𝒬u_mul def

Auxiliary function used in the proof of Lemma 7.2.1 · TileStructure.Forest.eI𝒬u_mul

eLorentzNorm def

The Lorentz seminorm of a function · MeasureTheory.eLorentzNorm

eLorentzNorm' def

The Lorentz seminorm of a function, for 0 < p < ∞ · MeasureTheory.eLorentzNorm'

ENormedAddCommSubMonoid class

An enormed monoid is an additive monoid endowed with a continuous enorm. Note: not sure if this is the "right" class to add to Mathlib. · ENormedAddCommSubMonoid

enumΘ' def

An enumeration of Θ' X, assuming it is nonempty. It may contain duplicates. · enumΘ'

enumΘ'ArgMax def

The argmax of g (enumΘ' nΘ' i) x over i ≤ n with lower indices winning ties. · enumΘ'ArgMax

EquivalenceOn structure

An equivalence relation on the set s. · EquivalenceOn

essProjFst def

For a (s : Set (α × β)) and (ν : Measure β), we define essProjFst such that x ∈ essProjFst s ν iff 0 < ν {y | ⟨x, y⟩ ∈ s}. · MeasureTheory.essProjFst

essProjSnd def

For a (s : Set (α × β)) and (μ : Measure α), we define essProjSnd such that y ∈ essProjSnd s μ iff 0 < μ {x | ⟨x, y⟩ ∈ s}. · MeasureTheory.essProjSnd

E₁ def

def E₁ (p : 𝔓 X) : Set X · E₁

E₂ def

def E₂ (l : ℝ) (p : 𝔓 X) : Set X · E₂

F

finite_spanning_sets_from_lintegrable def

def finite_spanning_sets_from_lintegrable {g : α → ℝ≥0∞} (hg : AEMeasurable g μ) (hg_int : ∫⁻ x, g x ∂μ < ⊤) : Measure.FiniteSpanningSetsIn (μ.restrict g.support) Set.univ · MeasureTheory.finite_spanning_sets_from_lintegrable

Forest structure

An n-forest · TileStructure.Forest

forest def

The forest based on 𝔘₄ k n j l. · forest

forget_map def

def forget_map (x : 𝓓 X) : (k : Set.Icc (-S : ℤ) S) × (Yk X k) · forget_map

fst def

def TileLike.fst (x : TileLike X) : Grid X · TileLike.fst

FunctionDistances class

A class stating that continuous functions have distances associated to every ball. We use a separate type to conveniently index these functions. · FunctionDistances

G

g abbrev

abbrev g (hX : GeneralCase f (α' a α)) (j : ℕ) (y : X) · g

G' def

The set G', defined below (5.1.28). · G'

G2_0_4 def

The constant on the g side of Proposition 2.0.4. Has value 2 ^ (440 * a ^ 3) in the blueprint. · TileStructure.Forest.G2_0_4

GeneralCase def

The property specifying whether we are in the "general case". · GeneralCase

Grid abbrev

The indexing type of the grid structure. Elements are called (dyadic) cubes. Note that this type has instances for both ≤ and ⊆, but they do not coincide. · Grid

grid_existence def

Proof that there exists a grid structure. · grid_existence

GridStructure class

A grid structure on X. We prefer coeGrid : Grid → Set X over Grid : Set (Set X) Note: the s in this paper is -s of Christ's paper. · GridStructure

g₀ abbrev

abbrev g₀ (hX : GeneralCase f (α' a α)) (j : ℕ) (y : X) · g₀

G₁ def

The exceptional set G₁, defined in (5.1.25). · G₁

G₂ def

The set G₂, defined in (5.1.27). · G₂

G₃ def

The set G₃, defined in (5.1.28). · G₃

H

HasBoundedStrongType def

A weaker version of HasStrongType. This is the same as HasStrongType if T is continuous w.r.t. the L^2 norm, but weaker in general. · MeasureTheory.HasBoundedStrongType

HasBoundedWeakType def

A weaker version of HasWeakType. · MeasureTheory.HasBoundedWeakType

HasLorentzType def

An operator has Lorentz type (p, r, q, s) if it is bounded as a map from L^{q, s} to L^{p, r}. HasLorentzType T p r q s μ ν c means that T has Lorentz type (p, r, q, s) w.r.t. measures μ, ν and constant c. · MeasureTheory.HasLorentzType

HasRestrictedWeakType def

Defines when an operator "has restricted weak type". This is an even weaker version of HasBoundedWeakType. · MeasureTheory.HasRestrictedWeakType

HasRestrictedWeakType' def

An enhanced version of HasRestrictedWeakType · MeasureTheory.HasRestrictedWeakType'

HasStrongType def

An operator has strong type (p, q) if it is bounded as an operator on L^p → L^q. HasStrongType T p p' μ ν c means that T has strong type (p, p') w.r.t. measures μ, ν and constant c. · MeasureTheory.HasStrongType

HasWeakType def

An operator has weak type (p, q) if it is bounded as a map from L^p to weak L^q. HasWeakType T p p' μ ν c means that T has weak type (p, p') w.r.t. measures μ, ν and constant c. · MeasureTheory.HasWeakType

highDensityTiles def

The set $\mathcal{P}_{F,G}$, defined in (5.1.24). · highDensityTiles

holderApprox def

φ ↦ \tilde{φ} in the proof of Lemma 8.0.1. · holderApprox

holderFunction def

The definition of h_J, defined in the proof of Section 7.5.2 · TileStructure.Forest.holderFunction

I

I12 def

Definition (6.2.27). · Tile.I12

I7_5_4 def

An intermediate constant in Lemma 7.5.4. · TileStructure.Forest.I7_5_4

iHolENorm def

the L^∞-normalized t-Hölder norm. Defined in ℝ≥0∞ to avoid sup-related issues. · iHolENorm

iHolNNNorm def

The NNReal version of the L^∞-normalized t-Hölder norm, iHolENorm. · iHolNNNorm

ijIntegral def

Scaled integral appearing in the definition of boundaryOperator. · TileStructure.Forest.ijIntegral

iLipENorm def

The inhomogeneous Lipschitz norm on a ball. · iLipENorm

iLipNNNorm def

The NNReal version of the inhomogeneous Lipschitz norm on a ball, iLipENorm. · iLipNNNorm

insert def

Gives the partial function sending a to b and agreeing with f otherwise. · MeasureTheory.NoAtoms'.PFun.insert

int def

The set I ↦ Iᵒ in the blueprint. · Grid.int

integer_linear def

def integer_linear (n : ℤ) : C(ℝ, ℝ) · integer_linear

interpolation_param def

The parameter where linear interpolation between t₀ and t₁ results in t. · interpolation_param

IsAtom def

An atom of a measure μ is a set s of positive measure for which all measurable subsets either have measure 0 or μ s. · MeasureTheory.IsAtom

IsCancellative class

Θ is τ-cancellative. τ will usually be 1 / a · IsCancellative

IsDoubling class

A doubling measure is a measure on a metric space with the condition that doubling the radius of a ball only increases the volume by a constant factor, independent of the ball. · MeasureTheory.Measure.IsDoubling

IsOneSidedKernel class

K is a one-sided Calderon-Zygmund kernel. In the formalization K x y is defined everywhere, even for x = y. The assumptions on K show that K x x = 0. · IsOneSidedKernel

IsTwoSidedKernel class

K is a two-sided Calderon-Zygmund kernel. In the formalization K x y is defined everywhere, even for x = y. The assumptions on K show that K x x = 0. · IsTwoSidedKernel

iteratedMaximalSubfamily def

Iterating maximalSubfamily to obtain disjoint subfamilies of A. · iteratedMaximalSubfamily

J

J102 def

A countable dense subset of the range of R₁ and R₂. · J102

K

K def

def K : ℝ → ℝ → ℂ · K

k def

def k (x : ℝ) : ℂ · k

K' def

Truncated version of `K` used in proof of `nontangential_pointwise_bound` · K'

KernelProofData class

Data common through most of chapters 2 through 7. These contain the minimal axioms for kernel-summand's proof. This is used in Chapter 3 when we don't have all other fields from ProofData. · KernelProofData

kissing def

The set of cubes in Lemma 7.2.4. · TileStructure.Forest.kissing

Ks def

K_s in the blueprint · Ks

L

L' def

The L' introduced in the proof of Lemma 6.3.4. · Antichain.L'

L302 def

The largest integer s₁ satisfying D ^ (-(s₁ - 2)) * R₁ > 1 / 2. · L302

layersAbove def

The elements above A's n minimal layers. · Set.layersAbove

layersBelow def

The elements below A's n maximal layers. · Set.layersBelow

layervol def

The volume of a "layer" in the key function of Lemma 5.2.7. · layervol

lcoConvergent def

A monotone sequence of functions converging to linearizedCarlesonOperator. · lcoConvergent

linearizedCarlesonOperator def

The linearized generalized Carleson operator T_Q, taking values in ℝ≥0∞. Use ENNReal.toReal to get the corresponding real number. · linearizedCarlesonOperator

LinearizedMetricCarleson def

Theorem 1.1.2. For the proof, see linearized_metric_carleson in the file Carleson.MetricCarleson.Linearized. · LinearizedMetricCarleson

linearizedNontangentialOperator def

The linearized maximally truncated nontangential Calderon–Zygmund operator T_Q^θ. · linearizedNontangentialOperator

linearOrder def

def Encodable.linearOrder {α : Type*} (i : Encodable α) : LinearOrder α · Encodable.linearOrder

localOscillation def

The local oscillation of two functions w.r.t. a set E. This is d_E in the blueprint. · localOscillation

Lorentz def

TODO: basic results · MeasureTheory.Lorentz

lorentz_helper def

The function k in the proof of Theorem 6.7 in https://doi.org/10.1007/978-3-319-30034-4 · MeasureTheory.lorentz_helper

LorentzAddConst def

A constant for the inequality ‖f + g‖_{L^{p,q}} ≤ C * (‖f‖_{L^{p,q}} + ‖g‖_{L^{p,q}}). It is equal to 1 if p = 0 or 1 ≤ r ≤ p and 2^(1/p) * LpAddConst r else. · MeasureTheory.LorentzAddConst

lowerCubes def

𝔓(𝔓') in the blueprint. The set of all tiles whose cubes are less than the cube of some tile in the given set. · lowerCubes

M

M14 def

The maximalFunction instance that appears in Lemma 6.1.4's proof. · M14

max_𝓓 def

def max_𝓓 : 𝓓 X · max_𝓓

maxCubes def

def maxCubes (s : Finset (Grid X)) : Finset (Grid X) · Grid.maxCubes

maximalSubfamily def

A disjoint subfamily of A covering everything. · maximalSubfamily

maxLayer def

The nth maximal layer of A. · Set.maxLayer

maxℭ def

def maxℭ : ℕ · maxℭ

measurableEquivIco' def

Replacement for existing proof of `measurableEquivIco` now that the proof of `measurable_toFun` is extracted as a separate lemma. The name is primed here only to avoid a collision. · AddCircle.measurableEquivIco'

measurableEquivIoc' def

Replacement for existing proof of `measurableEquivIoc` now that the proof of `measurable_toFun` is extracted as a separate lemma. The name is primed here only to avoid a collision. · AddCircle.measurableEquivIoc'

MemLorentz def

A function is in the Lorentz space L^{p,q} if it is (strongly a.e.)-measurable and has finite Lorentz seminorm. · MeasureTheory.MemLorentz

MemWLp def

A function is in weak-L^p if it is (strongly a.e.)-measurable and has finite weak L^p norm. · MeasureTheory.MemWLp

MetricSpaceCarleson def

Theorem 1.1.1. For the proof, see metric_carleson in the file Carleson.MetricCarleson.Main. · MetricSpaceCarleson

mf def

The good choice of an element to get a contradiction in the proof of Lemma 5.4.8. · mf

minLayer def

The nth minimal layer of A. · Set.minLayer

MKD abbrev

MKD is short for "modulated kernel times dilated bump". · MKD

modulationOperator def

The modulation operator M_n g, defined in (11.3.1) · modulationOperator

mono def

Monotonicity of doubling measure metric spaces in A. · MeasureTheory.DoublingMeasure.mono

Monotone def

The property of a partial function f to be monotone, i.e. f a ≤ f b whenever a ≤ b and both a and b are in the domain of f. · MeasureTheory.NoAtoms'.PFun.Monotone

MsetA def

Finset of cubes in setA. Appears in the proof of Lemma 5.2.5. · MsetA

N

niceKernel def

The kernel k_r(x) defined in (11.3.11). When used, we may assume that r ∈ Ioo 0 1. Todo: find better name? · niceKernel

nnapprox def

Approximate a function α → ℝ≥0 by a sequence of simple functions. · MeasureTheory.SimpleFunc.nnapprox

nnD def

D as an element of ℝ≥0. · nnD

nnq def

q as an element of ℝ≥0. · nnq

nnrealRatEmbed def

A sequence of ℝ≥0s such that its range is the set of non-negative rational numbers. · MeasureTheory.SimpleFunc.nnrealRatEmbed

nnτ def

τ as an element of ℝ≥0. · nnτ

NoAtoms' class

Measure μ has no atoms if for any measurable set s with positive μ-measure, there exists a measurable t ⊆ s such that 0 < μ t < μ s. While this implies μ {x} = 0, the converse is not true. · MeasureTheory.NoAtoms'

nontangentialMaximalFunction def

The definition T_𝓝^θ f(x), given in (7.1.3). For convenience, the suprema are written a bit differently than in the blueprint (avoiding cubeOf), but this should be equivalent. This is 0 if x doesn't lie in a cube. · TileStructure.Forest.nontangentialMaximalFunction

nontangentialOperator def

The maximally truncated nontangential Calderon–Zygmund operator T_*. · nontangentialOperator

nonzeroS def

the one or two numbers s where ψ (D ^ (-s) * x) is possibly nonzero · nonzeroS

O

oc def

`Set.Annulus.oo` has moved to `Defs.lean` · Set.Annulus.oc

oc def

`Set.EAnnulus.oo` has moved to `Defs.lean` · Set.EAnnulus.oc

ofGraph' def

Constructs a partial function α →. β from its graph of type SetRel α β. · MeasureTheory.NoAtoms'.PFun.ofGraph'

oi def

def oi (x : X) (r : ℝ) · Set.Annulus.oi

oi def

def oi (x : X) (r : ℝ≥0∞) · Set.EAnnulus.oi

oo def

def Set.Annulus.oo [PseudoMetricSpace X] (x : X) (r R : ℝ) · Set.Annulus.oo

oo def

def Set.EAnnulus.oo [PseudoMetricSpace X] (x : X) (r R : ℝ≥0∞) · Set.EAnnulus.oo

operatorBound def

The function used to bound the partial Fourier sum in partialFourierSum_bound · operatorBound

opSize def

An auxiliary measure used in the well-foundedness of Ω in Lemma tile_structure. · Grid.opSize

out def

An arbitrary representative of x w.r.t. the equivalence relation r. · EquivalenceOn.out

P

p def

Exponent used for the application of Hölder's inequality in the proof of Lemma 6.1.3. · Lemma6_1_3.p

p' def

p' in the blueprint. · Antichain.p'

p'' def

p'' in the blueprint · Antichain.p''

P304 structure

All the parameters needed to apply the recursion of Lemma 3.0.4. · P304

P7_5_4 def

The product on the right-hand side of Lemma 7.5.4. · TileStructure.Forest.P7_5_4

partialFourierSum def

The Nᵗʰ partial Fourier sum of f : ℝ → ℂ for N : ℕ. · partialFourierSum

partialFourierSum' def

def partialFourierSum' {T : ℝ} [hT : Fact (0 < T)] (N : ℕ) (f : AddCircle T → ℂ) : C(AddCircle T, ℂ) · partialFourierSum'

partialFourierSumLp def

def partialFourierSumLp {T : ℝ} [hT : Fact (0 < T)] (p : ℝ≥0∞) [Fact (1 ≤ p)] (N : ℕ) (f : AddCircle T → ℂ) : Lp ℂ p (@haarAddCircle T hT) · partialFourierSumLp

PreservesAEStrongMeasurability def

Proposition that expresses that the map T map between function spaces preserves AE strong measurability on L^p. · MeasureTheory.PreservesAEStrongMeasurability

PreTileStructure class

The data in a tile structure, and some basic properties. This is mostly separated out so that we can nicely define the notation `d_𝔭`. Note: compose `𝓘` with `Grid` to get the `𝓘` of the paper. · PreTileStructure

preℭ₁ def

def preℭ₁ (k n j : ℕ) : Set (𝔓 X) · preℭ₁

ProofData class

Data common through most of chapters 2-7 (except 3). · ProofData

property_set def

def property_set (k : ℤ) : Set (Set X) · property_set

pΘ def

p_Θ in the blueprint · Antichain.pΘ

p₆ def

p in Lemma 6.1.6. We append a subscript ₆ to keep p available for tiles. · Antichain.p₆

Q

qt def

$\tilde{q}$ from definition 6.1.10, as a real number. · Lemma6_1_3.qt

QΘ' def

The simple function corresponding to the blueprint's Q_n. · QΘ'

Qᵣ def

Rationals as a set of real numbers. · Qᵣ

q₆ def

p' in the proof of Lemma 6.1.4, the Hölder conjugate exponent of p₆. · Antichain.q₆

R

rearrangement def

The decreasing rearrangement function f^#. It equals μ univ for t = 0. Note that unlike the notes, we also define this for t = ∞. · MeasureTheory.rearrangement

reprs def

The set of representatives of an equivalence relation on a set. · EquivalenceOn.reprs

res def

def res (j : Bool) (β : ℝ≥0∞) : Set ℝ · MeasureTheory.res

res' def

def res' (j : Bool) (β : ℝ≥0∞) : Set ℝ · MeasureTheory.res'

Row structure

An n-row · TileStructure.Row

rowDecomp def

The row-decomposition of a tree, defined in the proof of Lemma 7.7.1. The indexing is off-by-one compared to the blueprint. · TileStructure.Forest.rowDecomp

rowDecomp_zornset def

def rowDecomp_zornset (s : Set (𝔓 X)) · TileStructure.Forest.rowDecomp_zornset

rowDecomp_𝔘 def

def rowDecomp_𝔘 (t : Forest X n) (j : ℕ) : Set (𝔓 X) · TileStructure.Forest.rowDecomp_𝔘

rowSupport def

The definition of Eⱼ defined above Lemma 7.7.4. · TileStructure.Forest.rowSupport

r𝓑 def

The radius function for the collection of balls 𝓑. · TileStructure.Forest.r𝓑

S

s def

def s : Grid X → ℤ · s

ScaledPowerFunction structure

A ScaledPowerFunction is meant to represent a function of the form t ↦ (t / d)^σ, where d is strictly positive and either σ > 0 or σ < 0. · ScaledPowerFunction

sel def

TODO: add a doc-string, explaining the purpose of this definition · MeasureTheory.sel

setA def

The set A(λ, k, n), defined in (5.1.26). · setA

setoid def

The setoid defined from an equivalence relation on a set. · EquivalenceOn.setoid

simpleNontangentialOperator def

The operator T_*^r g(x), defined in (10.1.31), above Lemma 10.1.6. · simpleNontangentialOperator

slice def

slice CP bG mG n contains G_n and its associated data. · slice

smul def

This is not defined as such in the blueprint, but λp ≲ λ'p' can be written using smul l p ≤ smul l' p'. Beware: smul 1 p is very different from toTileLike p. · smul

snd def

def TileLike.snd (x : TileLike X) : Set (Θ X) · TileLike.snd

spf_ch def

The particular choice of scaled power function that works in the proof of the real interpolation theorem. · ChoiceScale.spf_ch

spf_to_tc def

A scaled power function gives rise to a ToneCouple. · spf_to_tc

stackSize def

The number of tiles p in s whose underlying cube 𝓘 p contains x. · stackSize

StrictRangeToneCouple structure

A StrictRangeToneCouple is a ToneCouple for which the functions in the couple, when restricted to Ioo 0 ∞, map to Ioo 0 ∞. · StrictRangeToneCouple

SubadditiveOn def

The operator is subadditive on functions satisfying P with constant A. · MeasureTheory.SubadditiveOn

SubadditiveTrunc def

def SubadditiveTrunc [ENorm ε] (T : (α → ε₁) → α' → ε) (A : ℝ≥0∞) (f : α → ε₁) (ν : Measure α') : Prop · MeasureTheory.SubadditiveTrunc

SublinearOn def

The operator is sublinear on functions satisfying P with constant A. · MeasureTheory.SublinearOn

succ def

If i is not a maximal element, this is the (unique) minimal element greater than i. This is not a SuccOrder since an element can be the successor of multiple other elements. · Grid.succ

succ def

Construct G_{n+1} given G_n. · P304.succ

superlevelSet def

The superlevel set of a function f. · MeasureTheory.superlevelSet

T

T def

def T (i : ι) (u : X → ε) · T

T_lin def

The operator T_{2, σ₁, σ₂} introduced in Lemma 3.0.4. · T_lin

T_R def

The operator T_{R₁, R₂, R} introduced in Lemma 3.0.2. · T_R

T_S def

The operator T_{s₁, s₂} introduced in Lemma 3.0.3. · T_S

tile_existence def

def tile_existence : TileStructure Q D κ S o · tile_existence

TileLike def

def TileLike : Type _ · TileLike

TilesAt def

The definition 𝔓(k) given in (5.1.3). · TilesAt

TileStructure class

A tile structure. · TileStructure

ToneCouple structure

A ToneCouple is a couple of two monotone functions that are practically inverses of each other. It is used in the proof of the real interpolation theorem. · ToneCouple

toSet def

From a TileLike, we can construct a set. This is used in the definitions E₁ and E₂. · TileLike.toSet

toTile def

def TileLike.toTile (t : TileLike X) : Set (X × Θ X) · TileLike.toTile

toTileLike def

def toTileLike (p : 𝔓 X) : TileLike X · toTileLike

toWithFunctionDistance def

def toWithFunctionDistance {x : X} {r : ℝ} [FunctionDistances 𝕜 X] : Θ X ≃ WithFunctionDistance x r · toWithFunctionDistance

tr def

def tr (k : ℕ) : Set ι · tr

trnc def

A function to deal with truncations and complement of truncations in one go. · MeasureTheory.trnc

trunc def

The t-truncation of a function f. · MeasureTheory.trunc

truncCompl def

The complement of a t-truncation of a function f. · MeasureTheory.truncCompl

truncCut def

def truncCut (f : α → ℝ≥0∞) (μ : Measure α) [SigmaFinite μ] · MeasureTheory.truncCut

U

U302 def

The smallest integer s₂ satisfying D ^ (-(s₂ + 2)) * R₂ < 1 / (4 * D). · U302

upperRadius def

R_Q(θ, x) defined in (1.1.17). · upperRadius

URel def

The relation ∼ defined below (5.4.2). It is an equivalence relation on 𝔘₂ k n j. · URel

V

vol def

The "volume function" V. Preferably use vol instead. · Real.vol

vol def

The "volume function" V. We will need to assume IsFiniteMeasureOnCompacts and ProperSpace to actually know that this volume is finite. · vol

W

WeaklyContinuous def

The weak continuity assumption needed for HasRestrictedWeakType.hasLorentzType_helper. · MeasureTheory.WeaklyContinuous

WithFunctionDistance def

Class used to endow Θ X with a pseudometric space structure. · WithFunctionDistance

wnorm def

The weak L^p norm of a function. · MeasureTheory.wnorm

wnorm' def

The weak L^p norm of a function, for p < ∞ · MeasureTheory.wnorm'

Y

Yk def

def Yk (k : ℤ) : Set X · Yk

Yk_encodable def

def Yk_encodable (k : ℤ) : Encodable (Yk X k) · Yk_encodable

Other

α' def

Auxiliary constant used in the proofs of estimate_good, estimate_bad and distribution_czOperatorBound. · α'

ζ def

def ζ (p₀ q₀ p₁ q₁ : ℝ≥0∞) (t : ℝ) : ℝ · ComputationsChoiceExponent.ζ

Θ' def

A countable dense subset of Θ X. · Θ'

σ def

The definition σ(u, x) given in Section 7.1. We may assume u ∈ t whenever proving things about this definition. · TileStructure.Forest.σ

σMax def

def σMax (u : 𝔓 X) (x : X) (hσ : (t.σ u x).Nonempty) : ℤ · TileStructure.Forest.σMax

σMin def

def σMin (u : 𝔓 X) (x : X) (hσ : (t.σ u x).Nonempty) : ℤ · TileStructure.Forest.σMin

χ def

The definition of χ, defined in the proof of Lemma 7.5.2 · TileStructure.Forest.χ

χtilde def

The definition of χ-tilde, defined in the proof of Lemma 7.5.2 · TileStructure.Forest.χtilde

ψ def

The function ψ used as a basis for a dyadic partition of unity. · ψ

Ω def

def Ω (p : 𝔓 X) : Set (Θ X) · Construction.Ω

Ω def

The set Ω introduced below Lemma 10.2.5. · Ω

Ω₁ def

def Ω₁ (p : 𝔓 X) : Set (Θ X) · Construction.Ω₁

Ω₁_aux def

def Ω₁_aux (I : Grid X) (k : ℕ) : Set (Θ X) · Construction.Ω₁_aux

ℜ₀ def

The union occurring in the statement of Lemma 5.5.1 containing 𝔏₀ · ℜ₀

ℜ₁ def

The union occurring in the statement of Lemma 5.5.1 containing 𝔏₁ · ℜ₁

ℜ₂ def

The union occurring in the statement of Lemma 5.5.1 containing 𝔏₂ · ℜ₂

ℜ₃ def

The union occurring in the statement of Lemma 5.5.1 containing 𝔏₃ · ℜ₃

ℭ def

The partition ℭ(k, n) of 𝔓(k) by density, given in (5.1.7). · ℭ

ℭ₁ def

The subset ℭ₁(k, n, j) of ℭ(k, n), given in (5.1.9). Together with 𝔏₀(k, n) this forms a partition. · ℭ₁

ℭ₁' def

Type synonym of ℭ₁ to apply the Preorder of the proof of Lemma 5.5.3 on. · ℭ₁'

ℭ₂ def

The subset ℭ₂(k, n, j) of ℭ₁(k, n, j), given in (5.1.13). · ℭ₂

ℭ₃ def

The subset ℭ₃(k, n, j) of ℭ₂(k, n, j), given in (5.1.16). · ℭ₃

ℭ₄ def

The subset ℭ₄(k, n, j) of ℭ₃(k, n, j), given in (5.1.19). · ℭ₄

ℭ₅ def

The subset ℭ₅(k, n, j) of ℭ₄(k, n, j), given in (5.1.23). · ℭ₅

ℭ₆ def

The subset ℭ₆(k, n, j) of ℭ₅(k, n, j), given above (5.4.1). · ℭ₆

𝒥₁ def

def 𝒥₁ (r : ℝ) (x : X) (hX : GeneralCase f (α' a α)) : Set ℕ · 𝒥₁

𝒥₂ def

def 𝒥₂ (r : ℝ) (x : X) (hX : GeneralCase f (α' a α)) : Set ℕ · 𝒥₂

𝒥₃ def

def 𝒥₃ (r : ℝ) (x : X) (hX : GeneralCase f (α' a α)) : Set ℕ · 𝒥₃

𝓑 def

The indexing set for the collection of balls 𝓑, defined above Lemma 7.1.3. · TileStructure.Forest.𝓑

𝓒 def

The partition 𝓒(G, k) of Grid X by volume, given in (5.1.1) and (5.1.2). Note: the G is fixed with properties in ProofData. · 𝓒

𝓓 structure

structure 𝓓 · 𝓓

𝓘 def

def 𝓘 : 𝔓 X → Grid X · 𝓘

𝓙 def

The definition of `𝓙(𝔖), defined above Lemma 7.1.2 · TileStructure.Forest.𝓙

𝓙₀ def

The definition of `𝓙₀(𝔖), defined above Lemma 7.1.2 · TileStructure.Forest.𝓙₀

𝓙₅ def

The definition 𝓙' at the start of Section 7.5.1. We use a different notation to distinguish it from the 𝓙' used in Section 7.6 · TileStructure.Forest.𝓙₅

𝓙₆ def

The definition 𝓙' at the start of Section 7.6. We use a different notation to distinguish it from the 𝓙' used in Section 7.5 · TileStructure.Forest.𝓙₆

𝓛 def

The set 𝓛 defined in Lemma 6.3.4. · Antichain.𝓛

𝓛 def

The definition of `𝓛(𝔖), defined above Lemma 7.1.2 · TileStructure.Forest.𝓛

𝓛 def

The subset 𝓛(u) of Grid X, given near (5.1.20). Note: It seems to also depend on n. · 𝓛

𝓛' def

The set 𝓛* defined in Lemma 6.3.4. · Antichain.𝓛'

𝓛_min def

The set 𝓛_{-S} defined in Lemma 6.3.4. · Antichain.𝓛_min

𝓛₀ def

The definition of `𝓛₀(𝔖), defined above Lemma 7.1.2 · TileStructure.Forest.𝓛₀

𝓜 def

The maximal function used in the proof of Lemma 6.1.3 · Lemma6_1_3.𝓜

𝓜p def

The p maximal function used in the proof. · Lemma6_1_3.𝓜p

𝓩 def

A finset of maximal cardinality satisfying (4.2.1) and (4.2.2). · 𝓩

𝓩_cands def

def 𝓩_cands : Finset (Finset (Θ X)) · 𝓩_cands

𝔄' def

The set 𝔄' defined in Lemma 6.3.4. · Antichain.𝔄'

𝔄_aux def

Def 6.3.15. · Antichain.𝔄_aux

𝔄_min def

The set 𝔄_-S defined in Lemma 6.3.4. · Antichain.𝔄_min

𝔅 def

The subset 𝔅(p) of 𝔐(k, n), given in (5.1.8). · 𝔅

𝔏₀ def

The subset 𝔏₀(k, n) of ℭ(k, n), given in (5.1.10). Not to be confused with 𝔏₀(k, n, j) which is called 𝔏₀' in Lean. · 𝔏₀

𝔏₀' def

The subset 𝔏₀(k, n, l) of 𝔏₀(k, n), given in Lemma 5.5.3. We use the name 𝔏₀' in Lean. · 𝔏₀'

𝔏₁ def

𝔏₁(k, n, j, l) consists of the minimal elements in ℭ₁(k, n, j) not in 𝔏₁(k, n, j, l') for some l' < l. Defined near (5.1.11). · 𝔏₁

𝔏₂ def

The subset 𝔏₂(k, n, j) of ℭ₂(k, n, j), given in (5.1.15). · 𝔏₂

𝔏₃ def

𝔏₃(k, n, j, l) consists of the maximal elements in ℭ₃(k, n, j) not in 𝔏₃(k, n, j, l') for some l' < l. Defined near (5.1.17). · 𝔏₃

𝔏₄ def

The subset 𝔏₄(k, n, j) of ℭ₄(k, n, j), given near (5.1.22). Todo: we may need to change the definition to say that p is at most the least upper bound of 𝓛 n u in Grid X. · 𝔏₄

𝔐 def

The definition 𝔐(k, n) given in (5.1.4) and (5.1.5). · 𝔐

𝔐' def

def 𝔐' (u : 𝔓 X) · 𝔐'

𝔒 def

The set 𝔒 in the proof of Lemma 5.5.2. · 𝔒

𝔓 def

def 𝔓 · 𝔓

𝔓pos def

The set 𝔓_{G\G'} in the blueprint · 𝔓pos

𝔓X_s def

Used to simplify notation in the proof of `tile_sum_operator` · 𝔓X_s

𝔓₁ def

The set 𝔓₁, defined in (5.1.30). · 𝔓₁

𝔖₀ def

The set 𝔖 defined in the proof of Lemma 7.4.4. We append a subscript 0 to distinguish it from the section variable. · TileStructure.Forest.𝔖₀

𝔗₁ def

The subset 𝔗₁(u) of ℭ₁(k, n, j), given in (5.4.1). In lemmas, we will assume u ∈ 𝔘₁ k n l · 𝔗₁

𝔗₂ def

The subset 𝔗₂(u) of ℭ₆(k, n, j), given in (5.4.5). In lemmas, we will assume u ∈ 𝔘₃ k n l · 𝔗₂

𝔘 def

The function 𝔘(m) used in the proof of Lemma 5.2.8 · 𝔘

𝔘₁ def

The subset 𝔘₁(k, n, j) of ℭ₁(k, n, j), given in (5.1.14). · 𝔘₁

𝔘₂ def

The subset 𝔘₂(k, n, j) of 𝔘₁(k, n, j), given in (5.4.2). · 𝔘₂

𝔘₃ def

𝔘₃(k, n, j) ⊆ 𝔘₂ k n j is an arbitary set of representatives of URel on 𝔘₂ k n j, given above (5.4.5). · 𝔘₃

𝔘₄ def

Define 𝔘₄ k n j l as the union of 2 ^ n disjoint subfamilies in 𝔘₃ k n j, to make sure the multiplicity is at most 2 ^ n to get a forest. · 𝔘₄

𝔠 def

def 𝔠 (p : 𝔓 X) : X · 𝔠

𝔰 def

def 𝔰 (p : 𝔓 X) : ℤ · 𝔰

Terms from the explanations

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

a.e.

almost everywhere: outside a set of Lebesgue measure zero · ClassicalCarleson

doubling measure

a measure on a metric space for which the measure of a ball of radius 2r is bounded by a fixed constant times the measure of the ball of radius r · KernelProofData

phase space

the space Theta X of functions used as oscillation phases in the Carleson operator; it carries a compatible family of metrics on balls · carlesonOperator

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.