Glossary: R

Definitions in this project whose names start with R. 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

R def

Let $R(N)$ be the size of the largest $A\subseteq\{1, ..., N\}$ such that all sums $\sum_{n\in S} \frac{1}{n}$ are distinct for $S\subseteq A$. · Erdos321.R

r abbrev

abbrev r · Erdos139.r

r abbrev

abbrev r · Erdos142.r

r abbrev

$r_k(N)$ is the largest size of a subset of $\{1, \dots, N\}$ that does not contain a non-trivial $k$-term arithmetic progression. · Erdos3.r

r def

Let `r(x)` be the smallest even integer `t` such that `primeGap = t` has no solutions for `n ≤ x`. · Erdos853.r

r def

The quantity $r_k(N)$, defined as the size of the largest subset of $\{1, \dots, N\}$ without non-trivial $k$-term arithmetic progressions. · Green9.r

r def

def r (α : ℝ) : ℝ · MovingSofa.GerversSofa.r

r def

r w is the word obtained by reversing w and adding 1 to every term. · OeisA108081.r

rademacherMeasure def

The law of an infinite sequence of independent fair coins (ε_k)_{k ≥ 0}, each uniform on {-1, +1}. · Erdos521.rademacherMeasure

radical def

The radical of n denoted is the product of the distinct prime factors of n. · ABC.radical

RadoCondition def

The coefficients $a_1, \dots, a_k$ satisfy Rado's condition if $\sum_{i \in I} a_i = 0$ for some non-empty $I \subseteq [k]$. · Green21.RadoCondition

rank abbrev

The rank of an elliptic curve over ℚ. · EllipticCurveRank.RatEllipticCurve.rank

ranksunbounded30 def

The elliptic curve over ℚ of rank at least 30 found by user ranksunbounded in 2026. User profile: https://elliptic-rank.icarm.cloud/user/18 It has rank exactly 30 assuming the generalized Riemann hypothesis and Birch and Swinnerton-Dyer … · EllipticCurveRank.WeierstrassCurve.ranksunbounded30

ratDiagonal def

The subgroup Γ = G(ℚ) of G(𝔸_f) × G(ℝ): the range of the diagonal embedding of GL n ℚ. Condition (a) for an automorphic form is left invariance under this subgroup. · Matrix.GeneralLinearGroup.ratDiagonal

RatEllipticCurve structure

A data structure representing isomoprhism classes of elliptic curves over ℚ. Every elliptic curve over ℚ is isomorphic to one with Weierstrass equation y² = x³ + Ax + B, and the pair (A,B) is unique if it satisfy the reduced … · EllipticCurveRank.RatEllipticCurve

ratExpression def

The rational number inside the numerator function in the conjecture. $$ -\frac{2}{n} + \sum_{k=1}^n \frac{2^k}{k} $$ · OeisA108866.ratExpression

ratio def

def ratio (r : ℝ) (f : ℂ → ℂ) : ℝ · Erdos513.ratio

ratio def

def ratio (r : ℝ) (f : ℂ → ℂ) : ℝ · Erdos516.ratio

ratioSeq def

The sequence of ratios $P(N)/Neg(N)$ as a sequence of real numbers. · OeisA117027.ratioSeq

ratRed def

We need to reduce a rational modulo p, in practice we won't be dividing by zero since the conductor of the elliptic curve saves us. · ModularityConjecture.ratRed

rConst def

The constant $r = (2 + \sqrt{5})/2$. · OeisA341254.rConst

Reachable inductive

The reachable configurations of a branching vector addition system. · BranchingVAS.Bvas.Reachable

Reachable inductive

The inductively defined predicate that m is reachable in n steps. · Mathoverflow75792.Reachable

reachableFinset def

The finset of vertices reachable from u, computed by breadth-first search. · SimpleGraph.reachableFinset

Reaches def

The statement Reaches M s₁ s₂ means that s₂ is obtained starting from s₁ after a finite number of steps from s₂. · Turing.BusyBeaver.Machine.Reaches

ReachesPrime def

A starting value reaches a prime after finitely many prime-factor splicing steps. · OeisA37274.ReachesPrime

RealCardinalRamsey3 def

RealCardinalRamsey3 β c asserts the 3-uniform partition relation $\mathfrak{c} \to (\beta, c)^3_2$, where $\mathfrak{c}$ is the order type of the real numbers with their usual order. · Erdos70.RealCardinalRamsey3

realPeriod def

The real period as an integral: the integral of $|\omega|$ over the real locus $E(\mathbb{R})$, that is $2 \int_{\mathbb{R}} dx / \sqrt{F(x)}$ with the integrand taken to be $0$ where $F \leq 0$. This is the real period of the Birch … · WeierstrassCurve.realPeriod

realPeriodIntegrand def

The density $|\omega| / dx = 1 / \sqrt{4x^3 + b_2 x^2 + 2 b_4 x + b_6}$ of the invariant differential on either branch of the real locus, as a function on $\mathbb{R}$, with the junk value $0$ where the cubic is not positive. · WeierstrassCurve.realPeriodIntegrand

realRootCount def

R_n: the number of distinct real roots of f_n. · Erdos521.realRootCount

RealSchanuelConjecture def

The real version of Schanuel's conjecture: if $x_1, \ldots, x_n$ are real numbers that are linearly independent over $\mathbb{Q}$, then the field $\mathbb{Q}(x_1, \ldots, x_n, e^{x_1}, \ldots, e^{x_n})$ has transcendence degree at least … · TarskiExponentialFunctionProblem.RealSchanuelConjecture

reciprocalMass def

The reciprocal sum ∑_{n ∈ A} 1/n of the problem. · Erdos538.reciprocalMass

reciprocalSum def

The reciprocal sum of a finite set of natural numbers. · Finset.reciprocalSum

recipSum def

The reciprocal sum of a finite set of natural numbers, as a rational number. · Erdos296.recipSum

Rectangle structure

A rectangle is specified by its width, height, starting point, and rotation. The rectangle is assumed to start in the lower left corner. For example, the unit square $\{ (x, y) \mid 0 \le x \le 1, 0 \le y \le 1 \}$ is specified as `⟨1, 1, … · Mathoverflow34145.Rectangle

recurrenceSet def

The set $\{ n\geq 1: \| \alpha n^2\| < \epsilon(n)\}$. · Erdos1147.recurrenceSet

reducedDensityFirst def

The reduced density matrix obtained by tracing out the last $n-m$ parties. · OpenQuantumProblem35.reducedDensityFirst

regularExtension def

Given an integral Diophantine 3-tuple, there is a standard way to extend it to a 4-tuple by adjoining the value of this function. This is $d_+$ in [Du]. · DiophantineTuple.regularExtension

RegularFunction abbrev

The type of regular functions from $k^σ$ to $k^τ$. · MvPolynomial.RegularFunction

regularNGon def

The regular $n$-gon inscribed in the unit circle. · Erdos94.regularNGon

RegularPrimeConjecture def

Conjecture: The set of regular primes is infinite. · RegularPrimes.RegularPrimeConjecture

regularPrimes def

The set of regular primes. · RegularPrimes.regularPrimes

regulator def

The absolute determinant of the height pairing on a finite basis of E(K) modulo torsion. For number fields with their standard height instance, this is the non-normalised regulator. · WeierstrassCurve.Affine.Point.regulator

Rel inductive

The relations defining K^M_*(F)/ℓ as a quotient of the tensor algebra of Fˣ: the Steinberg relation {a}{b} = 0 when a + b = 1, and the relation ℓ = 0. · MilnorK.Rel

relativeUnitary def

The relative unitary between two bases. · OpenQuantumProblem13.relativeUnitary

RelatorTuple abbrev

An n-tuple of relators in the free group on n generators. · AndrewsCurtis.RelatorTuple

Rep def

Rep A m h means m is a sum of exactly h elements of A, which is m ∈ h • A. · Erdos330.Rep

repCount def

$F_A(g) = \#\{ S\subseteq A : g = \sum_{x\in S}x\}$. · Erdos1179.repCount

repCount def

The number of unordered representations m = a₁ * a₂ by two distinct elements a₁ < a₂ of A. · Erdos796.repCount

Representable def

$n$ is representable with respect to $p$ and $q$ if it is the sum of a finite divisibility antichain of terms of the form $p^kq^l$. · Erdos1110.Representable

representable def

The set of positive integers representable as a sum of distinct unit fractions with denominators from {1, …, N}. · Erdos308.representable

representationCount def

For k ≥ 3, the number of ordered representations of n as a sum of k many kth powers of positive integers. The bases can be restricted to the interval from 1 to n, since x ≤ x ^ k for positive x. · Erdos322.representationCount

representations def

The representations m = p * a with p prime and a ∈ A. · Erdos538.representations

Represents def

Represents ε p a s says that the multiset s of denominators n with 1 ≤ n ≤ p^ε and n coprime to p has ∑ n⁻¹ = a in ZMod p. · Erdos1180.Represents

RepresentsAPs def

The predicate that a : ℕ → ℕ is a strictly monotone sequence such that every infinite arithmetic progression contains infinitely many integers that are the sum of distinct $a_i$s. · Erdos253.RepresentsAPs

repunit def

The repunit with digits digits in the given base, expressed without division. · Goormaghtigh.repunit

repunit10 def

The decimal repunit of length $n$, defined as $1 + 10 + \cdots + 10^{n-1}$. · RepunitPrime.repunit10

RequiredCondition def

Condition on the sets $A$ appearing in Erdős 888. Namely, let $A$ be a subset of ${1,...,n}$ such that if $a ≤ b ≤ c ≤ d ∈ A$ and $abcd$ square then $ad=bc$. · Erdos888.RequiredCondition

residue def

Computes the residue of a graph G, i.e. the number of zeros remaining after iteratively applying the Havel-Hakimi algorithm to the degree sequence until all remaining degrees are zero. Starts with the descending degree sequence and … · SimpleGraph.residue

residueAux def

Auxiliary function to calculate the residue recursively. Applies Havel-Hakimi steps until the sequence consists only of zeros or is empty. Defined by well-founded recursion on the list length (via havelHakimiStep_length_cons), so that it … · SimpleGraph.residueAux

ResidueChoice def

Choices of congruence classes $a_i \pmod{n_i}$. · Erdos281.ResidueChoice

residueEqTwoIndicator def

The characteristic function for the predicate $\mathrm{residue}\, G = 2$: returns $1$ when $G.\mathrm{residue} = 2$ and $0$ otherwise. This is the WOWII $\chi_{\mathrm{residue}=2}(G)$ indicator appearing in Conjecture 217. · WrittenOnTheWallII.GraphConjecture217.residueEqTwoIndicator

residuePrimesUpTo def

The primes $\ell \leq m^{1/4+\varepsilon}$ with $\chi(\ell) = 1$. · Erdos1141.residuePrimesUpTo

residuePrimeUpperBound def

The cutoff $m^{1/4 + \varepsilon}$ of Theorem 1.3 of [Po17]. · Erdos1141.residuePrimeUpperBound

restrictedSumset def

The restricted sumset of a set $S$, denoted $S \hat{+} S$, is the set $\lbrace s_1 + s_2 : s_1, s_2 \in S, s_1 \neq s_2 \rbrace$. · Finset.restrictedSumset

rev10 def

The digit-reversal map $\operatorname{rev}_{10}(n)$. · LychrelNumbers.rev10

revBase def

The number whose base-$b$ digits are the reversal of $n$'s base-$b$ digits. · OeisA77408.revBase

reverseDigits def

Reverses the base 10 digits of a natural number. · OeisA100475.reverseDigits

reverseNat def

The number whose digits in base 10 are $n$'s digits reversed. · OeisA62567.reverseNat

richDistances def

The distances determined by A which occur for at least k many pairs of points of A. · Erdos756.richDistances

richLineCount def

The number of lines that contain more than three points of P. · Erdos102.richLineCount

RightIdeal abbrev

A right ideal in a semiring R is an additive submonoid closed under multiplication on the right. It is implemented as a submodule of the right regular module. · RightIdeal

rightIndex def

The embedding of the last $n-m$ indices into $\mathrm{Fin}\, n$. · OpenQuantumProblem35.rightIndex

rightTranslateSpan def

The k-span of the right translates of f by the subgroup K. · AutomorphicForm.rightTranslateSpan

rightTranslation def

The right translation representation of G(𝔸_f) on the automorphic forms: g acts by f ↦ fun (x, y) => f (x * g, y). · Matrix.GeneralLinearGroup.rightTranslation

RigidMotion abbrev

A rigid motion of $\mathbb{R}^{N+1}$: an affine isometry of Euclidean space onto itself (a composition of translations and rotations/reflections). · PompeiuProblem.RigidMotion

rigidMotion def

A combination of a rotation and a translation to map the standard rectangle to the desired rectangle. · Mathoverflow34145.rigidMotion

rootArgCount def

The number of roots of f, counted with multiplicity, whose argument lies in I. The argument is normalised to [0, 2π). · Erdos990.rootArgCount

roots def

The random multiset of roots associated to a Kac polynomial · Erdos522.KacCoefficients.roots

rotateTranslate def

The rigid motion that translates by $p$ and then rotates counterclockwise by $\alpha$. Note that [Ge92] used this definition while [Ro18] used rotation first and then translation. · MovingSofa.rotateTranslate

routeAExponent def

The Route A exponent $A(\alpha) = \log 2 / \log \alpha + \log 2 / \log(1 / \rho)$ of [Ste26], where $\rho$ is the largest modulus of a conjugate of $\alpha$ other than $\alpha$ itself. It is the sum of the box dimensions of $C(\alpha)$ and … · Bugeaud61.routeAExponent

rsConstant def

The constant of Corollary 29, $\frac{2\Gamma(1+1/q)^2}{\Gamma(1+2/q)} + 2$. · Arxiv.«2607.03582».rsConstant

rSq def

The constant $r^2$. · OeisA341254.rSq

runMetaMInCommandElabM def

A copy of ContextInfo.runMetaM that keeps the messages and passes in the same filename. · Lean.Elab.ContextInfo.runMetaMInCommandElabM

runnerUpFrequency def

For a fixed distance $d$, the largest multiplicity among all other represented distances (Finset.sup returns $0$ when there is no other value). · Erdos959.runnerUpFrequency

runTermLinter def

A linter that applies to terms. · Lean.Elab.Command.Linter.runTermLinter