Glossary: F

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

F def

F n is the maximal size of a family of subsets of $\{1,\ldots,n\}$ such that no set in this family is the union of other members of the family. · Erdos1023.F

F def

If $\omega(n)$ counts the number of distinct prime divisors of $n$ then let $F(n)=\max_k \omega(n+k)\frac{\log\log k}{\log k}.$ · Erdos1203.F

F def

$F_k(N)$ is the size of the largest $A\subseteq \{1,\ldots,N\}$ such that the product of no $k$ many distinct elements of $A$ is a square. · Erdos121.F

F def

$F(N)$ is the maximal size of a non-dividing subset of $\{1, \dots, N\}$. · Erdos131.F

F def

F k is the number of solutions to $1 = \frac{1}{n_1} + \cdots + \frac{1}{n_k}$ with $1 \leq n_1 < \cdots < n_k$, that is, the number of $k$-element sets of positive integers whose reciprocals sum to $1$. · Erdos148.F

F abbrev

Let $F(N)$ be the size of the largest Sidon subset of $\{1, \dots, N\}$. · Erdos155.F

F def

$F(n, \alpha)$: the smallest k such that some 2-colouring of $K_n$ satisfies IsBalancedAbove n α c k. · Erdos162.F

F abbrev

F N is the size of the largest non ternary subset of {1,...,N}. · Erdos168.F

F def

We define a function F N as the minimum cardinality of an N-perfect ruler of length N. · Erdos170.F

F def

The number of integers which can be written as the sum of distinct unit fractions with denominators from $\{1,\ldots,N\}$. · Erdos309.F

F def

The largest prime factor of $n(n+1)$. · Erdos368.F

F def

Let $F(n) := \max\{m + p(m) \mid \textrm{$m < n$ composite}\}\}$ where $p(m)$ is the least prime divisor of $m$. · Erdos385.F

F def

$F(n,\alpha)$ is the smallest $m$ such that there exists a 2-coloring of the edges of $K_n$ so that every $X\subseteq [n]$ with $|X|\geq m$ contains more than $\alpha\binom{|X|}{2}$ edges of each color. · Erdos563.F

F def

F n is the maximal size of a strongly 2-primitive subset of {1, …, n}. · Erdos793.F

F def

$F(n)$ is the maximal integer such that every graph on $n$ vertices contains a regular induced subgraph on at least $F(n)$ vertices. · Erdos82.F

F abbrev

Let $a$ be some sequence of natural numbers. We set $F(A,X,k)$ to be the count of the number of $i$ such that $[a_i,a_{i+1}, \dots ,a_{i+k−1}] < X$, where the left-hand side is the least common multiple. · Erdos873.F

F def

Let $F(x)$ be the maximal $k$ such that there exist $n+1, \dots, n+k \le x$ with $τ(n+1), \dots, τ(n+k)$ all distinct, where $τ(m)$ counts the divisors of $m$. · Erdos945.F

F def

Let $F(N)$ be the largest Sidon subset of $[N]$. · Green31.F

F abbrev

Alpöge/Fable's counterexample: a polynomial self-map of k³ with Jacobian determinant -2 which is not injective. · JacobianConjecture.F

F def

The generalized sum $F(n, L) = \sum_{k=0}^{\lfloor n/2 \rfloor} \binom{n-k}{k}^L$. · OeisA181546.F

F def

F n is the smallest number of vertices of a triangle-free graph with chromatic number n and f = 3. · SimpleGraph.F

f def

f n is the largest integer such that any two Farey fractions of order n whose indices differ by at most f n are similarly ordered: it is the minimum, over all pairs x < y of Farey fractions of order n with `(x.num - y.num) * … · Erdos1005.f

f def

The maximum number of edges in an r-uniform hypergraph on n vertices containing no matching of size k (i.e. no k pairwise vertex-disjoint edges). · Erdos1020.f

f def

Let $f(n)$ be the minimal integer $m$ such that $n$ is the sum of the $k$ smallest divisors of $m$ for some $k\geq 1$. · Erdos1054.f

f def

The extremal function from Erdős problem 1062: the largest size of a fork-free subset of {1,...,n}. · Erdos1062.f

f def

The function $f(n)$ specified in erdos_107. · Erdos107.f

f def

For any prime $p$, let $f(p)$ be the least integer such that $f(p)! + 1 \equiv 0 \mod p$. · Erdos1072.f

f def

The maximal number of pairs of points which are distance 1 apart that a set of n 1-separated points in ℝ^d make. · Erdos1084.f

f def

The maximal number of pairs of points which are distance 1 apart that a set of n points in ℝ^d make. · Erdos1085.f

f def

The least m such that every m-point subset of ℝ^d contains an n-point subset with all pairwise distances distinct. · Erdos1088.f

f def

f N is the largest size of a subset A ⊆ {1, ..., N} such that every element of A + A is squarefree. · Erdos1109.f

f def

f m is the largest k such that every graph with m edges contains a bipartite subgraph with at least $\frac{m}{2}+\frac{\sqrt{8m+1}-1}{8}+k$ edges. · Erdos127.f

f def

f n is the least possible maximum degree of a triangle-free graph on n vertices with diameter 2, i.e. the largest f such that every such graph has a vertex of degree ≥ f. · Erdos133.f

f def

f n is the least number of colours in a (4, 5)-colouring of K_n. · Erdos136.f

f def

Define f n to be the minimum of |{s | s - 1 ∉ A + A, s ∈ A + A, s + 1 ∉ A + A}| as A ranges over all Sidon sets of size n. · Erdos152.f

f def

Define $f(n)$ to be the minimum of $\frac{1}{t}\sum_{1\leq i<t}(s_{i+1}-s_i)^2$ as $A$ ranges over all Sidon sets of size $n$, where $A+A=\{s_1<\cdots<s_t\}$. · Erdos153.f

f def

Let $f(n,k)$ be minimal such that every $F$ family of $n$-uniform sets with $|F| \ge f(n,k)$ contains a $k$-sunflower. · Erdos20.f

f def

f N is the maximum possible r such that there are moduli $n_1<\cdots<n_r\leq N$ with associated residues $a_i\pmod{n_i}$ whose congruence classes are disjoint. · Erdos202.f

f def

f n is the minimal size of an Erdős–Lovász family of order n. · Erdos21.f

f def

$f(n)$ counts the number of solutions to $n=p+2^k$ for prime $p$ and $k\geq 0$. · Erdos236.f

f def

Let $f(N)$ be the maximum size of $A\subseteq \{1,\ldots,N\}$ such that the sums $a+b+c$ with $a,b,c\in A$ are all distinct (aside from the trivial coincidences). · Erdos241.f

f def

f N is the smallest positive integer which is not representable as a sum of distinct unit fractions with denominators from {1, …, N}. · Erdos308.f

f def

Let $1\leq m\leq k$ and $f_{k,m}(x)$ denote the number of integers $\leq x$ which are the sum of $m$ many nonnegative $k$th powers. · Erdos323.f

f def

We define a sequence f by the formula f n = n.fib - (- 1) ^ n. · Erdos346.f

f def

Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. · Erdos357.f

f def

Let $a$ be an infinite sequence of integers. Let $f(n)$ count the number of solutions to $$n=\sum_{u\leq i\leq v}a_i.$$ · Erdos358.f

f def

Let f n be the smallest integer for which n! can be represented as the product of distinct integers greater than n, the largest of which is f n. · Erdos390.f

f abbrev

Let $f(N)$ be the maximum possible size of a Sidon set in $\{1,\ldots,N\}$. · Erdos43.f

f def

Define f n to be the minimum of (n + i).nth Prime + (n - i).nth Prime over 0 < i < n. · Erdos454.f

f def

The function from the problem, in its equivalent form: f u is the smallest v > u all of whose prime factors divide u. (Equivalently, f u is the largest v such that no m ∈ (u, v) is composed entirely of primes dividing u * v.) · Erdos459.f

f def

The minimum number of terms of the square of a rational polynomial with exactly k nonzero terms, where the number of terms of P is P.support.card. · Erdos485.f

f def

The largest size of a set $A\subseteq\{1,\ldots,N\}$ on which Euler's totient function is strictly increasing. · Erdos49.f

f def

f r N is the maximum size of a subset A ⊆ {1,…,N} such that no r-element subset of A has constant pairwise GCD. · Erdos535.f

f def

f m is the maximal k such that every triangle-free graph on m edges contains a bipartite subgraph with k edges. · Erdos581.f

f def

$f(n)$ is the minimal $m$ such that if the edges of $K_{2^n+1}$ are coloured with $n$ colours then there must be a monochromatic odd cycle of length at most $m$. · Erdos609.f

f def

f m is the largest r such that whenever A ⊆ {1, …, N} has m elements, every interval in [1, ∞) of length 2 * N contains r distinct integers b 0, …, b (r - 1), each b i being divisible by some a i ∈ A, where `a 0, …, a … · Erdos650.f

f def

f n = min_{1 < k ≤ n/2} gcd(n, C(n,k)). (The infimum is 0 when the range is empty, i.e. n < 4.) · Erdos700.f

f def

f n counts the number of sum-free $A\subseteq \{1,\ldots,n\}$, i.e. $A$ contains no solutions to $a=b+c$ with $a,b,c\in A$. · Erdos748.f

f def

f k is the minimal n such that any $2$-colouring of $\{1,\ldots,n\}$ (identified with Fin n) contains a monochromatic $k$-term descending wave. · Erdos781.f

f def

$f_c(n)$, the largest book size forced on every admissible graph, which is the least book number among them. · Erdos80.f

f def

f m n is maximal such that any graph on n vertices in which every induced subgraph on m vertices has an independent set of size at least $\log n$ must contain an independent set of size at least f m n. · Erdos804.f

f def

Let $f(n)$ be the smallest integer for which every graph on $n$ vertices with minimal degree $\geq f(n)$ contains a $C_4$. · Erdos85.f

f def

def f (N k : ℕ) : ℕ · Erdos865.f

f def

Definition of function $f(n) := \sum_{1\leq k\leq n}\tau(2^k-1)$. Here $\tau$ is the divisor counting function, which is σ 0 in mathlib. · Erdos893.f

f def

Let $f(n)$ be maximal such that there exists a set $A$ of $n$ points in $\mathbb^2$ in which every $x \in A$ has at least $f(n)$ points in $A$ equidistant from $x$. · Erdos92.f

f def

$f_k(n)$ is the maximum possible chromatic number of a graph with $n$ vertices which contains no $K_k$. · Erdos920.f

f def

Let $f(n) = \sum_{p<n}\frac{1}{n-p}$. · Erdos950.f

f def

For $k$, let $f(k)$ be the minimal $n$ such that every set of $n$ consecutive integers $>k$ contains an integer divisible by a prime $>k$, i.e. not $(k+1)$-smooth. · Erdos961.f

f def

The maximum size of a solution-free subset of $[N]$. · Green16.f

f def

Let $f(r)$ be the smallest constant such that there exists an infinite sequence of $n$'s together with subspaces $V_n \leq \mathbb{F}_2^n$ with $V_n + H(r) = \mathbb{F}_2^n$ and $|V_n| = \left(f(r) + o(1)\right) \frac{2^n}{|H(r)|}$. · Green40.f

f def

The statement is false in general if we restrict to polynomials. The polynomial (by Motzkin) $f(x, y) = x^4 y^2 + x^2 y^4 - 3 x^2 y^2 + 1$ takes only nonnegative values but cannot be written as a sum of squares of polynomials. · Hilbert17.f

f def

$f(2n) = f(2n+1) = d(2n+1)/2$ · OeisA100434.f

f def

The function $f(n) = n + \text{sum of the digits of } n$. · OeisA100800.f

f def

Halve even numbers, leave odd numbers unchanged. · OeisA120424.f

f def

The rational sequence whose Dirichlet convolution square is A046644, written using the defining recurrence from the OEIS entry. · OeisA317940.f

f3 def

$f_3(n)$ is the maximal size of a subset of $\{0,1,2\}^n$ which contains no three points on a line (in $\mathbb{R}^n$). · Erdos185.f3

f_all def

def f_all (r : ℕ) : ℝ≥0∞ · Green40.f_all

f_r def

For $A\subset \mathbb{N}$ let $f_r(n)$ count the number of solutions to $n=a_1+\cdots+a_r$ with $a_i\in A$. · Erdos1192.f_r

f_tilde def

def f_tilde (r : ℕ) : ℝ≥0∞ · Green40.f_tilde

factorDifferenceSet def

For integer $n \geq 1$ we define the factor difference set of $n$ by $D(n) = \{|a-b| : n=ab\}$. · Erdos885.factorDifferenceSet

factorialDivisorRatio def

The ratio $\sigma_0((n+1)!)/\sigma_0(n!)$, where $\sigma_0$ is the divisor-counting function. · Erdos419.factorialDivisorRatio

factorialsLessThanN def

def factorialsLessThanN (n : ℕ) : Set ℕ · Erdos1059.factorialsLessThanN

FactorialSums def

The set $A = \left\{ \sum_{n\in S}n! : S\subset \mathbb{N}_{\geq 1}\text{ finite}\right\}$ of all finite sums of distinct factorials. The indices are positive because $0! = 1!$, so allowing $0$ would count the value $1$ twice. · Erdos1108.FactorialSums

fairCoin def

One fair coin: the uniform probability measure on Bool. · Erdos521.fairCoin

familyExtremal def

$\mathrm{ex}(n;\mathcal{F})$, the greatest number of edges of a graph on n vertices containing no member of family. · Erdos180.familyExtremal

FamilyFree def

A host graph is family-free when it contains no member of family as a subgraph. · Erdos180.FamilyFree

fano_plane def

Sanity check: the Fano plane is an $S(2, 3, 7)$-Steiner system. · SteinerSystems.fano_plane

fEntry def

Characteristic function $f(j, k)$ for matrix entries in $\mathbb{Z}/p^2\mathbb{Z}$. · OeisA1818.fEntry

fermatCatalanConjecture def

The proposition that the Fermat-Catalan Conjecture is true. · FermatCatalanConjecture.fermatCatalanConjecture

FermatCatalanSet def

def FermatCatalanSet : Set (ℕ × ℕ × ℕ) · FermatCatalanConjecture.FermatCatalanSet

FermatCatalanSet' def

The set of solutions to the Fermat-Catalan Conjecture, i.e. the set of solutions $(a,b,c,m,n,k)$ to the equation $a^m + b^n = c^k$ where $\frac 1 m + \frac 1 n + \frac 1 k < 1$. · FermatCatalanConjecture.FermatCatalanSet'

fermatFactors def

OEIS A46052 The number of distinct prime factors of nth Fermat number. Known terms: 1, 1, 1, 1, 1, 2, 2, 2, 2, 3, 4, 5 · Selfridge.fermatFactors

fHat def

The real-valued Fourier transform used in the Cohn--Elkies conditions. For real radial admissible functions, the complex Fourier transform is expected to be real-valued; we take .re to expose the real scalar used in the inequality. · Green42.fHat

findAnswerExpr def

Find the first subexpression carrying the answer annotation, returning the inner (unwrapped) expression if found. · Google.findAnswerExpr

findAnswerExprs def

Collect all subexpressions carrying the answer annotation, returning the inner (unwrapped) expressions. · Google.findAnswerExprs

finiteAdditiveConvolution def

Define $p \boxplus_n q(x)$ to be the polynomial $$ (p \boxplus_n q)(x) = \sum_{k=0}^n c_k x^{n-k} $$ where the coefficients $c_k$ are given by the formula: $$ c_k = \sum_{i+j=k} \frac{(n-i)! (n-j)!}{n! (n-k)!} a_i b_j $$ for $k = 0, 1, … · Arxiv.«2602.05192».finiteAdditiveConvolution

FiniteGraph structure

A finite graph, bundled with its vertex count, so that a family may mix orders. · Erdos180.FiniteGraph

FiniteRankVectorBundleData structure

structure FiniteRankVectorBundleData (M : SheafOfModules R) extends VectorBundleData M · SheafOfModules.FiniteRankVectorBundleData

finiteWord def

The n-th iterate of the morphism applied to [a]. · OeisA6697.finiteWord

firoozbakhtSeq def

The sequence of $\sqrt[n]{p_n}$ where $p_n$ is the n:th prime number. · Firoozbakht.firoozbakhtSeq

FirstHardyLittlewoodConjectureFor def

The first Hardy–Littlewood conjecture for the tuple $(m_0, m_1, \dots, m_k)$: if $m_0 = 0$ and the $m_i$ are pairwise distinct, then $$ \pi_P(n)\sim C_P\int_2^n\frac{dt}{\log^{k+1}t}. $$ · HardyLittlewood.FirstHardyLittlewoodConjectureFor

firstKindTerm def

The nth term generated from p by the first-kind recurrence q ↦ 2q + 1. · CunninghamChain.firstKindTerm

FirstPrimesMultiples def

FirstPrimesMultiples N k is the set of numbers in {1,..., N} that are a multiple of one of the first k primes. · Erdos56.FirstPrimesMultiples

fixedSizeFamilies def

All r-uniform hypergraphs on n vertices with exactly m edges. · Hypergraph.fixedSizeFamilies

flip def

Flip operator, flip x B returns input x with bits in block B inverted. · StrongSensitivityConjecture.flip

FloorMultiples def

The sequence ⌊a⌋, ⌊γ * a⌋, ⌊γ ^ 2 * a⌋, ..., ⌊γ ^ i * a⌋, .... · Erdos354.FloorMultiples

fm def

fm n counts the number of maximal sum-free subsets $A\subseteq\{1,\ldots,n\}$. · Erdos877.fm

foo def

def foo : Nat · AMSLinter.foo

foo def

def foo : Nat · CategoryLinter.foo

forallToAnd def

Changes and expression of the form ∀ (h1 : Prop1) (h2 : Prop2) ..., Propn to Prop1 ∧ Prop2 ∧ ... ∧ Propn. · ExistsImplicationLinter.forallToAnd

ForceCondition structure

The basic smoothness condition on the external forcing term. · NavierStokes.ForceCondition

ForceConditionDecay structure

Force conditions for the Navier-Stokes problem on all of $\mathbb{R}^n$. · NavierStokes.ForceConditionDecay

ForceConditionPeriodic structure

Force conditions for the periodic Navier-Stokes problem on $\mathbb{R}^n/\mathbb{Z}^n$. · NavierStokes.ForceConditionPeriodic

ForcesMonochromaticTriangle def

n forces a monochromatic triangle on k colours when every k-colouring of the edges of K_n has a colour class containing a triangle. · Erdos183.ForcesMonochromaticTriangle

ForkFree def

A set A of positive integers is fork-free if no element divides two distinct other elements of A. · Erdos1062.ForkFree

FormalProofKind inductive

The type of formal proof that exists for a problem. · ProblemAttributes.FormalProofKind

formalProofLinter def

Checks the assumptions named by a conditional formal_proof and ensures formal_proof statements are sorry. · FormalProofLinter.formalProofLinter

FormalProofTag structure

A tag recording the existence and location of a formal proof for a declaration. · ProblemAttributes.FormalProofTag

format def

Print an answer · Google.AnswerInfo.format

FormsEquilateralTriangle def

Three points form an equilateral triangle of side length 1. · Erdos99.FormsEquilateralTriangle

Formula inductive

Formula is the inductive type of propositional modal formulas: · Arxiv.«1308.0994».Formula

fortunateNumber def

The $n$-th Fortunate number (0-indexed): the smallest integer $m > 1$ such that $p_{n+1}\\# + m$ is prime. · FortuneConjecture.fortunateNumber

fourierPartial def

def fourierPartial {T : ℝ} [hT : Fact (0 < T)] (f : Lp ℂ 2 (@haarAddCircle T hT)) (k : ℕ) : AddCircle T → ℂ · Erdos996.fourierPartial

FourProp def

A predicate that holds if $p(x)$ and $q(x)$ are monic real-rooted polynomials of degree $n$, then $$\frac{1}{\Phi_n(p\boxplus_n q)} \ge \frac{1}{\Phi_n(p)}+\frac{1}{\Phi_n(q)}?$$ · Arxiv.«2602.05192».FourProp

frac def

The rational number defined by $\binom{6n-2}{2n} / \left(2 \binom{4n-1}{2n}\right)$, whose numerator is A109074. · OeisA109074.frac

fracPart def

The fractional part of a rational number. · OeisA108.fracPart

fractionalAlpha def

Fractional alpha. This is defined as $$ \max_x \sum_{v \in V} x_v $$ subject to $0 \le x_v \le 1$ for all $v \in V$ and $x_u + x_v \le 1$ whenever $(u, v)$ are connected by an edge. · SimpleGraph.fractionalAlpha

fractScalarInv def

The function $\rho_{\theta} := \left\{\frac{\theta}{x}\right\}$ appearing in the Beurling-Nyman criterion. · RiemannHypothesis.fractScalarInv

fractScalarInvSumL2 def

The linear combination $\sum_{\nu = 1}^n c_{\nu}\rho_{\theta_\nu}$ expressed explicitly as an element of $L^2(0, 1)$. · RiemannHypothesis.fractScalarInvSumL2

freqMinTriangles def

The number of vertices achieving the minimum triangle count. · WrittenOnTheWallII.GraphConjecture291.freqMinTriangles

frequency def

$f(d)$: the number of unordered pairs in $P$ determining distance $d$. · Erdos959.frequency

Friendly def

Two positive integers $m$ and $n$ are friendly if they have the same abundancy index, that is $\sigma(m) / m = \sigma(n) / n$, expressed via cross-multiplication to avoid rationals. · SolitaryNumber.Friendly

friendshipF4 def

The friendship graph $F_4$: a hub vertex $0$ joined to four triangles, whose rims are the pairs $\{1,2\}, \{3,4\}, \{5,6\}, \{7,8\}$. It has $12$ edges on $9$ vertices ($8$ spokes and $4$ rim edges). · Arxiv.«2507.17780».friendshipF4

frobeniusNumber def

The Frobenius number of a finite set $A$: the greatest natural number outside the additive submonoid generated by $A$. · Erdos433.frobeniusNumber

fromSperner def

Backward map: Sperner family → monotone Boolean function. · DedekindNumber.fromSperner

fSet def

The set whose infimum defines f. · Erdos700.fSet

FugledeConjectureFor def

Fuglede's conjecture in dimension n: A bounded subset of ℝ^n with positive Lebesgue measure is spectral iff it tiles ℝ^n by translation. · Fuglede.FugledeConjectureFor

Full def

A natural number $n$ is said to be $k$-full (or $k$-powerful) if for every prime factor $p$ of $n$, the $k$-th power $p^k$ also divides $n$. · Nat.Full

functional def

The linear functional on G → ℂ given by φ ↦ Re ∑ g, a g * φ g. · Green57.functional