Glossary: E

Definitions in this project whose names start with E. The whole glossary has the other sections.

A · B · C · D · E · F · G · H · I · J · K · L · M · N · O · P · Q · R · S · T · U · V · W · X · Y · Z · Other

E def

The error term $$E(x; q) = \max_{\gcd(a,q)=1} \left|\pi(x;q,a) - \frac{\pi(x)}{\varphi(q)}\right|,$$ measuring the deviation of the primes in the arithmetic progressions modulo $q$ from uniform distribution among the $\varphi(q)$ coprime … · ElliottHalberstamConjecture.E

E abbrev

Let $E(r)$ be the error term between the number of integral points inside the circle and the area of the circle; that is $N(r) = \pi r^2 + E(r)$. · GaussCircleProblem.E

e def

$e(2n) = d(2n)/2$, $e(2n+1) = - d(2n)/2$ · OeisA100434.e

ecc def

Auxiliary quantity ecc used in conjecture 34. · SimpleGraph.ecc

eccSet def

The eccentricity of a set S: the maximum, over all vertices v of G, of the minimum distance from v to any vertex in S. (This includes vertices in S itself, which contribute distance 0.) Returns 0 when S is empty. · SimpleGraph.eccSet

ecliqueNum def

def ecliqueNum {V : Type} (G : SimpleGraph V) : ℕ∞ · SimpleGraph.ecliqueNum

edegree def

def edegree {V : Type*} (G : SimpleGraph V) (v : V) : ℕ∞ · SimpleGraph.edegree

edgeBoundary def

The edge-boundary of $F$ is the expectation of $h(S)$ (according to $\mu_p$) over all subsets $S$ of $X$. It is denoted by $I^p(F)$. · Mathoverflow10799.edgeBoundary

edgeCoverNumber def

The minimum edge cover number of G. · SimpleGraph.edgeCoverNumber

edgeDensity def

Edge density normalized by the number of possible uniform edges. · Hypergraph.edgeDensity

edgeDistancesToBipartite def

For a given subgraph A, this is the set of all numbers k such that A can be made bipartite by deleting k edges. · Erdos74.SimpleGraph.edgeDistancesToBipartite

edgeDominationNumber def

def edgeDominationNumber (G : SimpleGraph α) : ℕ · SimpleGraph.edgeDominationNumber

EdgeN structure

Edge label for $K_N$ with endpoint indices in Fin D. · MonochromaticQuantumGraph.EdgeN

EdgeRamseyTriangle def

A graph G is edge-Ramsey for triangles (in arrow notation, $G \to (K_3, K_3)^e$) if any $2$-colouring of the edges of G produces a monochromatic $K_3$: three pairwise adjacent vertices whose three connecting edges all receive the … · Erdos582.EdgeRamseyTriangle

edges def

The edges a cycle traverses. · SimpleGraph.Cycle.edges

edgesAdjacent def

def edgesAdjacent (e e' : Sym2 α) : Prop · SimpleGraph.edgesAdjacent

EFLConfig structure

A configuration of n pairwise edge-disjoint copies of $K_n$ covering the vertex type V. · Erdos19.EFLConfig

eFunction def

def eFunction (n : ℕ) (r : ℕ) : ℕ · Erdos600.eFunction

egyptianSum def

The Egyptian fraction sum: ∑_{m ∈ S} 1/m for a finset of natural numbers. · Erdos206.egyptianSum

EHSNumbers abbrev

The EHS numbers (after Erdős, Hardy, and Subbarao) are those $m\geq 1$ such that there exists a prime $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$. · Erdos1074.EHSNumbers

elabTermAndAnnotate def

def elabTermAndAnnotate (stx : TSyntax `term) (expectedType? : Option Expr) (postpone : Bool · Google.elabTermAndAnnotate

elkies28 def

The elliptic curve over ℚ of rank at least 28 found by Elkies in 2006. It has rank exactly 28 assuming the generalized Riemann hypothesis. · EllipticCurveRank.WeierstrassCurve.elkies28

elkiesKlagsbrun29 def

The elliptic curve over ℚ of rank at least 29 found by Elkies and Klagsbrun in 2024. It has rank exactly 29 assuming the generalized Riemann hypothesis. · EllipticCurveRank.WeierstrassCurve.elkiesKlagsbrun29

emaxDegree def

def emaxDegree {V : Type*} (G : SimpleGraph V) : ℕ∞ · SimpleGraph.emaxDegree

energy def

The Hamiltonian of the energy-critical NLS in $ℝ^3$. The kinetic term is $\frac12\sum_{j=1}^3 |\partial_j u|^2$, as in (1.2) of the reference. · NLSCritical.energy

engelCommutator def

The iterated commutator $[x,\, {}_n y]$, defined by $[x,\, {}_0 y] = x$ and $[x,\, {}_{n+1} y] = [[x,\, {}_n y], y]$. · Kourovka.«1.40».engelCommutator

entanglementFactor def

Artin's conjecture on $S(a)$ when $a = b^m$ is a power, and the squarefree part of $b_0\equiv 1\pmod{4}$, requires a further correct factor to ArtinConstant * powCorrectionFactor m, which modifies primes which divide $\gcd(b_0, m)$ and … · ArtinPrimitiveRootsConjecture.entanglementFactor

entrySup def

The sup norm on the entries of a matrix: for n = 2 this is |(a b; c d)| = max {|a|, |b|, |c|, |d|}. · Matrix.GeneralLinearGroup.entrySup

envelopingAction def

The action of the universal enveloping algebra U(𝔤𝔩 n ℂ) on the C^∞ functions on GL n ℝ, obtained from lieDerivHom by the universal property. A monomial X₁ ⋯ Xₖ acts as the composite of the corresponding left invariant … · Matrix.GeneralLinearGroup.envelopingAction

eps def

$\epsilon_m$ is the supremum of $\sum \frac{1}{n_i}$ over all finite sequences $m<n_1<\cdots<n_k$ for which there exist congruences $a_i\pmod{n_i}$ such that no integer satisfies two such congruences. · Erdos1190.eps

epsilon def

$\epsilon(n) = \sum_{n\leq k\leq m}\frac{1}{k}-1$, the overshoot of the minimal block sum reaching $1$. · Erdos314.epsilon

epsilonFunction def

def epsilonFunction (n : ℕ) : ℝ · Erdos688.epsilonFunction

EqSystemN def

The monochromatic quantum graph equation system for $K_N$. · MonochromaticQuantumGraph.EqSystemN

Equation255 abbrev

abbrev Equation255 (G: Type) [Magma G] · EquationalTheories_677_255.Equation255

Equation677 abbrev

abbrev Equation677 (G: Type) [Magma G] · EquationalTheories_677_255.Equation677

equiTriangle def

Equilateral triangle with unit side length, resting on the x-axis with one vertex at the origin. · Erdos91.equiTriangle

Equivalent def

Andrews-Curtis equivalence is the equivalence relation generated by elementary moves. · AndrewsCurtis.Equivalent

equivMonotoneSperner def

The set of monotone Boolean functions on n variables is in bijection with the set of Sperner families of subsets of Fin n. · DedekindNumber.equivMonotoneSperner

Erdos1141Prop def

The property that $n-k^2$ is prime for all $k$ with $(n,k)=1$ and $k^2 < n$. · Erdos1141.Erdos1141Prop

Erdos1142Prop def

The property that $n > 2$ and $n - 2^k$ is prime for all $k \geq 1$ with $2^k < n$. · Erdos1142.Erdos1142Prop

Erdos1145Prop def

Let $A=\{1\leq a_1 < a_2 < \cdots\}$ and $B=\{1\leq b_1 < b_2 < \cdots\}$ be sets of integers with $a_n/b_n\to 1$. · Erdos1145.Erdos1145Prop

Erdos1148Prop def

A natural number $n$ which can be written as $n$ if $n = x^2 + y^2 - z^2$ with $\max(x^2, y^2, z^2) \leq n$. · Erdos1148.Erdos1148Prop

Erdos1201Set def

The set of $n$ for which $P(n(n+1)\cdots(n+k)) > n^{1-\epsilon}$, where $P(m)$ is the greatest prime divisor of $m$. · Erdos1201.Erdos1201Set

Erdos120For def

There exists a set $E \subseteq \mathbb{R}$, dependent on set $A \subseteq \mathbb{R}$, of positive measure which does not contain any set of the shape $a * A + b$ for some $a,b \in \mathbb{R}$ and $a \neq 0$? · Erdos120.Erdos120For

Erdos16Set def

The set of odd integers not of the form $2^k+p$. · Erdos16.Erdos16Set

Erdos189For def

Erdős problem 189 asked whether the below holds for all rectangles. · Erdos189.Erdos189For

Erdos213For def

The predicate (on $n$) that there exist $n$ points in $\mathbb{R}^2$, no three on a line and no four on a circle, such that all pairwise distances are integers. · Erdos213.Erdos213For

Erdos261InfiniteRepresentation def

A canonical infinite representation of a rational number $x$ by positive integers. The denominators are strictly increasing so that reorderings are not counted as different representations. · Erdos261.Erdos261InfiniteRepresentation

Erdos261Prop def

A natural number $n$ is said to have property Erdos261Prop if there exist $t \ge 2$ pairwise distinct positive integers $a_1, \ldots, a_t$ such that $n / 2^n = \sum_{1 \le k \le t} a_k / 2^{a_k}$. · Erdos261.Erdos261Prop

erdos313Solutions def

This set contains all solutions (m, P) to the Erdős problem 313. A solution is a pair where m is an integer ≥ 2 and P is a non-empty, finite set of distinct prime numbers, such that the sum of the reciprocals of the primes in P … · Erdos313.erdos313Solutions

Erdos375Prop def

This is a proposition saying that for any n ≥ 1 and any k, if n + 1, ..., n + k are all composite, then there are distinct primes p₁, ... pₖ such that pᵢ ∣ n + i for all 1 ≤ i ≤ k. · Erdos375.Erdos375Prop

Erdos40For def

The predicate for a function $g\colon\mathbb{N} → \mathbb{R})$ that $$\lvert A\cap \{1,\ldots,N\}\rvert \gg \frac{N^{1/2}}{g(N)}$$ implies $\limsup 1_A\ast 1_A(n)=\infty$. · Erdos40.Erdos40For

erdos427 def

The predicate that for every $n$ and $d$, there exists $k$ such that $$ d \mid p_{n + 1} + \cdots + p_{n + k}, $$ where $p_r$ denotes the $r$th prime? · Erdos427.erdos427

Erdos445Prop def

The property that there exist $a,b\in(n,n+p^c)$ such that $ab\equiv 1\pmod{p}$. · Erdos445.Erdos445Prop

Erdos494Unique def

def Erdos494Unique (k : ℕ) (card : ℕ) · Erdos494.Erdos494Unique

Erdos4For def

def Erdos4For (C : ℝ) : Prop · Erdos4.Erdos4For

Erdos600Prop def

Let $e(n,r)$ be minimal such that every graph on $n$ vertices with at least $e(n,r)$ edges, each edge contained in at least one triangle, must have an edge contained in at least $r$ triangles. · Erdos600.Erdos600Prop

Erdos672With def

Erdős problem 672 conjectures that the below holds for any $k ≥ 4$ and $l > 1$. · Erdos672.Erdos672With

Erdos688Prop def

Define $\epsilon_n$ to be maximal such that there exists some choice of congruence class $a_p$ for all primes $n^{\epsilon_n} < p \leq n$ such that every integer in $[1,n]$ satisfies at least one of the congruences $\equiv a_p \pmod p$. · Erdos688.Erdos688Prop

Erdos769LowerBound def

The highlighted conjecture c(n) ≫ n^n: there is an absolute positive constant A/B with c(n) ≥ (A/B) n^n for all sufficiently large n. · Erdos769.Erdos769LowerBound

Erdos848For def

The Erdős Problem 848 statement for a fixed $N$: any set $A ⊆ \{0, \dots, N-1\}$ with the non-squarefree product property has cardinality at most $|A₇(N)|$. · Erdos848.Erdos848For

Erdos884Prop def

For a natural number n, let $1 = d_1 < \dotsc < d_{\tau(n)} = n$ denote the divisors of $n$ in increasing order. Does it hold that $\sum_{1 \le i < j \le \tau(n)} \frac{1}{d_j - d_i} \ll 1 + \sum_{1 \le i < \tau(n)} \frac{1}{d_{i + 1} - … · Erdos884.Erdos884Prop

Erdos886Divisors def

The set of divisors of $n$ in the interval $(n^{1/2}, n^{1/2} + n^{1/2-\epsilon})$. · Erdos886.Erdos886Divisors

Erdos939Sums def

A set S belongs to Erdos939Sums r if it meets the following criteria: - The elements are positive. 0 has no prime factors, so it is vacuously r-powerful, and the source means positive integers. - The size of the set is `$|S| = r - … · Erdos939.Erdos939Sums

Erdos945Constant def

def Erdos945Constant : Prop · Erdos945.Erdos945Constant

Erdos945Prop def

Implementation note: we define a Prop here and below to be able to easily formulate the equivalence between the two variants. Because the theorems require `answer(sorry)` we can't handle this with `type_of%`. · Erdos945.Erdos945Prop

erdos946Count def

Number of $n \le x$ with $τ(n) = τ(n+1)$. · Erdos946.erdos946Count

Erdos951Prop def

A sequence a : ℕ → ℝ is said to have property Erdos951Prop if for any pair of distinct finitely supported sequences k l : ℕ →₀ ℕ their corresponding Beurling integers are of distance at least one apart. · Erdos951.Erdos951Prop

Erdos961Prop def

def Erdos961Prop (k n : ℕ) : Prop · Erdos961.Erdos961Prop

Erdos962Prop def

Erdos962Prop n k : there exists $m \le n$ such that each of $m+1, \ldots, m+k$ has a prime divisor strictly larger than $k$. · Erdos962.Erdos962Prop

Erdos975Sum def

Sum of $\tau(f(n))$ from 0 to ⌊x⌋ for a polynomial $f \in \mathbb{Z}[X]$. · Erdos975.Erdos975Sum

Erdos9A def

The set of odd numbers that cannot be expressed as a prime plus two powers of 2. · Erdos9.Erdos9A

erdos_1148_weaker_prop def

The weaker property: $n = x^2 + y^2 - z^2$ such that $\max(x^2, y^2, z^2) \leq n + 2\sqrt{n}$. · Erdos1148.erdos_1148_weaker_prop

erdos_252_sum def

The series ∑ σ k n / n!. · Erdos252.erdos_252_sum

erdosConstruction def

Erdős' construction: all integers in $[1,(N/2)^{1/2}]$ together with all even integers in $[(N/2)^{1/2},(2N)^{1/2}]$. · Erdos441.erdosConstruction

ErdosSeries def

The series $\sum_{n=0}^\infty \frac{1}{a_n \cdot a_{n+1}}$. · Erdos1051.ErdosSeries

erdosSzemerediConstant def

The Erdős–Szemerédi constant $c=\sum_{n\geq 1}\frac{1}{n^{1/2}(n+1)}\approx 1.86$ (summed here over $n = m + 1$, $m \geq 0$). · Erdos440.erdosSzemerediConstant

Euclid def

The n-th Euclid number is the product of the first n prime numbers plus one. · EuclidNumbers.Euclid

eval def

The degree-n polynomial $f(z)=\sum_{j\leq n}\epsilon_j z^j$ with coefficients ε : Fin (n + 1) → ℤˣ, i.e. $\epsilon_j\in\{-1,1\}$, evaluated at z. · Erdos525.eval

eval def

Evaluate a Turing machine on initial input to a final state, if it terminates. · Turing.BusyBeaver.Machine.eval

evalEdge def

Given a configuration x : V → UnitInterval and an edge e : Sym2 V, evaluate W on the endpoints as a real number. · LimitObjects.Graphon.evalEdge

evalSym2 def

Evaluate a graphon on an unordered pair of vertices in Sym2 UnitInterval as a real number. · LimitObjects.Graphon.evalSym2

evenDistancePairs def

The set of pairs of distinct vertices with even distance > 0. · SimpleGraph.evenDistancePairs

evenHorizontal def

The number of edges whose endpoints are at the same even distance from $v$. · WrittenOnTheWallII.GraphConjecture309.evenHorizontal

evenOrOddNonSquarefree def

Those $n \in \{1,\ldots,N\}$ which are even or not squarefree, that is, the set of even numbers together with the odd non-squarefree numbers. · Erdos844.evenOrOddNonSquarefree

EventuallyGreedy def

x has eventually greedy best Egyptian underapproximations: from some n₀ on, the best n-term underapproximations of x are the prefixes of a single strictly increasing sequence of denominators, so each is obtained from the previous … · Erdos206.EventuallyGreedy

EventuallyHasPrimeWitness def

The eventual prime inequality asked in Erdős Problem 453, using Mathlib's zero-based primes. · Erdos453.EventuallyHasPrimeWitness

EventuallyNotPowerful def

The predicate that a n is only powerful for finitely many n. · Erdos936.EventuallyNotPowerful

EveryEdgeInTriangle def

Every edge of G lies in at least one triangle. · Erdos80.EveryEdgeInTriangle

EverySevenHasTriangle def

Every set of $7$ vertices of G contains a triangle, that is, three pairwise adjacent vertices. For $n < 7$ there is no such set, so the condition is vacuous. · Erdos813.EverySevenHasTriangle

ExactCovering structure

An exact covering of a group G is a finite collection of subgroups {H_1, ..., H_k} and representative {g_1, ..., g_k} such that the cosets g_iH_i are pairwise disjoint and their union covers G. · Erdos274.Group.ExactCovering

exactlyOneDivisorIn def

The set of integers with exactly one divisor in the open interval $(n, m)$. · Erdos692.exactlyOneDivisorIn

exampleBvas def

A small BVAS of dimension 3 used for a test below. · BranchingVAS.exampleBvas

exampleBvas2 def

A small (indeed, degenerate, since it contains no binary rules) BVAS of dimension 2 used for a test below. · BranchingVAS.exampleBvas2

exceptional def

The exceptional set $E = \{n \geq 5 : |x_n| > n/2 + 1\}$. An index with $A_n = 0$ is a pole of the tangent rather than a large value, and is counted in, reading $|x_n|$ as infinite. · Arxiv.«2607.05739».exceptional

exceptional def

The degree-n polynomials with $\pm 1$ coefficients such that $|f(z)|\geq 1$ for all $|z|=1$. · Erdos525.exceptional

exceptionalSet def

The set of exceptional integers. · OeisA110475.exceptionalSet

ExistsAME def

Existence of an $\mathrm{AME}(n,d)$ state. · OpenQuantumProblem35.ExistsAME

ExistsEventuallySurjective def

The condition that an integer m ensures the existence of a function f covering Fin n for all large enough subsets Y. The property is invariant under bijection, so we use a representative Fin n for a finite set of size n. · Erdos624.ExistsEventuallySurjective

existsImplicationLinter def

The existsImplicationLinter detects expressions of the form ∃ a, P a → Q and flags them to the user since those are rarely correct. · ExistsImplicationLinter.existsImplicationLinter

ExistsPebblePath def

Indicates whether there exists a sequence of pebbling moves transforming one pebble distribution to another. · PebblingNumberConjecture.ExistsPebblePath

exp def

The language with a single unary function symbol exp and no relation symbols. · FirstOrder.Language.exp

expFunc inductive

The type of function symbols of Language.exp: a single unary symbol exp. · FirstOrder.expFunc

expGL def

The exponential of a matrix, as an element of GL n ℝ: exp X is invertible with inverse exp (-X). · Matrix.GeneralLinearGroup.expGL

explicitGraph def

The graph on Fin n described by an adjacency oracle adj. Two distinct vertices u and v are adjacent if adj (1ⁿ, u, v) or adj (1ⁿ, v, u) is true. · Erdos78.explicitGraph

exponentialCharacter def

The exponential character x ↦ exp(2π i ⟪ξ, x⟫). · exponentialCharacter

expProd def

expProd n is ∏ kᵢ when n = ∏ pᵢ ^ kᵢ, i.e. the product of the prime exponents of n. · Erdos413.expProd

extendGL def

A choice of C^∞ extension of φ to the invertible matrices, when one exists. Only its germ at each invertible matrix matters, by fderiv_extendGL_eq. · Matrix.GeneralLinearGroup.extendGL

extremalFamily def

Defines a family of subsets of $A_n$ where each permutation $\pi$ in a subset obeys $\pi(x)$ and $\forall v \in I$, $\pi(v)\notin I$ for a fixed $x$ and $I$. It is easy to demonstrate that such a subset is product-free, because for any … · Green4.extremalFamily

extremalGap def

The extremal quantity of the problem, $\max_{|A| = n} (f(d_1) - f(d_2))$. There are Nat.choose n 2 unordered pairs, so this is a valid finite search interval. · Erdos959.extremalGap

extremalNumber def

Maximum number of edges among r-uniform families satisfying P on n labeled vertices. The value is zero if no family is admissible. · Hypergraph.extremalNumber

extremalSize def

The largest size of a square-sum-free subset of {1, …, N}. · Erdos438.extremalSize