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 · X · Y · Z · Other

A

a def

A309132: a(n) is the denominator of F(n) = A027641(n-1)/n + A027642(n-1)/n^2. · a

a def

A091669: $a(n) = \frac{2^{n-1}}{n!} \prod_{k=1}^{n-1} (2^k-1)$. The sequence $a(n)$ is composed of natural numbers, thus we define it as a function $\mathbb{N} \to \mathbb{N}$. · a

a def

A325046: G.f.: $\sum_{n \ge 0} x^n \cdot \frac{(1 + x^n)^n}{(1 - x^{n+1})^{n+1}}$. · a

a def

A103311: A transform of the Fibonacci numbers. The sequence $a(n)$ satisfies the linear recurrence relation: $$a(n) = 3a(n-1) - 4a(n-2) + 2a(n-3) - a(n-4)$$ with initial terms $a(0)=0, a(1)=1, a(2)=1, a(3)=0$. The sequence takes values in … · a

a def

A000108 Catalan numbers: C(n) = binomial(2n,n)/(n+1). · a

a def

A113254: Corresponds to $m = 8$ in a family of 4th-order linear recurrence sequences. · a

a def

A175386: $a(n)$ is the denominator of the sum $$\sum_{i=1}^n \frac{1}{i} \binom{2n-i-1}{i-1}$$ · a

a def

A194806: Size of the smallest subset $S$ of $T = \{1,2,3,\dots,n\}$ such that $S \cdot S$ contains $T$, where $S \cdot S$ is the set of all products of elements of $S$. · a

a def

A227582: Expansion of $(2+3*x+2*x^2+2*x^3+3*x^4+x^5-x^6)/(1-2x+x^2-x^5+2*x^6-x^7)$. The sequence is 1-indexed in OEIS, so $a(n)$ is the $(n-1)$-th term of the 0-indexed solution. · a

a def

A228143: Determinant of the $(n+1) \times (n+1)$ Hankel-type matrix with $(i,j)$-entry equal to A005259$(i+j)$ for all $i,j = 0,\dots,n$. The entry function A005259 is taken to be $\sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k}^2$. · a

a def

A243106: The sequence $$a(n) = \sum_{k=1}^n (-1)^{\operatorname{isprime}(k)} 10^k$$ where the sign is $-1$ if $k$ is prime, and $1$ if $k$ is not prime. · a

a def

A248802: Smallest prime factor of $2^{(2^n+2)} + 3$. · a

a def

A267581: Decimal representation of the middle column of the "Rule 167" elementary cellular automaton starting with a single ON (black) cell. The term $a(n)$ is the decimal value of the binary number $C_{0, 0} C_{1, 0} \dots C_{n, 0}$, … · a

a def

A271591: Second most significant bit of the tribonacci number A000073(n). This is formalized by extracting the bit at position $\lfloor \log_2 T_n \rfloor - 1$. · a

a def

The sequence $a(n)$ is defined by $a(n) = \binom{2n}{n}^3$. We use Nat.choose (2 * n) n for the central binomial coefficient. · a

a def

The sequence A306424: Numbers $k$ such that the base $b$ expansion of $k$ for each $b = 3..k-1$ never contains more than two distinct digits. · a

a def

A307865: $a(n)$ is the number of natural bases $b < 2n+1$ such that $b^n \equiv -1 \pmod{2n+1}$. The bases $b$ are interpreted as $b \in \{1, 2, \dots, 2n\}$. We check the condition in the ring $\mathbb{Z}/(2n+1)\mathbb{Z}$. · a

a def

A323557: G.f.: $\sum_{n\ge 0} x^n \cdot \frac{(1 + x^n)^n}{(1 + x^{n+1})^{n+1}}$. The $m$-th term $a(m)$ is the coefficient of $x^m$, which is explicitly given by the sum: $$ a(m) = \sum_{n=0}^m \sum_{k=0}^n \binom{n}{k} (-1)^j … · a

a def

A341254: $a(n) = \lfloor r \cdot \lfloor r \cdot n \rfloor \rfloor$, where $r = (2 + \sqrt{5})/2$. Note: The original OEIS definition has $n$ starting at 1. We define $a(n)$ for all $\mathbb{N}$. · a

a def

A372761: Denominator of the continued fraction $$ \frac{1}{2 - \frac{3}{3 - \frac{4}{4 - \frac{5}{\dots - \frac{n-1}{(n-1) - \frac{n}{n+4}}}}}} $$ · a

a def

A062567: First multiple of $n$ whose reverse is also divisible by $n$, or 0 if no such multiple exists. · a

a def

A028859 (OEIS): $a(n+2) = 2 \cdot a(n+1) + 2 \cdot a(n)$; $a(0) = 1$, $a(1) = 3$. · a

a def

Integral factorial ratio sequence: $$a(n) = \frac{(30n)! n!}{(15n)! (10n)! (6n)!}$$ · a

a def

A237271: Number of parts in the symmetric representation of $\sigma(n)$. a(n) is $1$ plus the number of pairs $(d_k, d_{k+1})$ of consecutive divisors of $n$ such that $d_{k+1}$ is odd and $d_{k+1} \ge 2 d_k$. · a

a def

A300997: $a(n)$ is the number of steps needed to reach a stable configuration in the 1D cellular automaton initialized with one cell with mass $n$ and based on the rule "each cell gives half of its mass, rounded down, to its right … · a

a def

A363102: Denominator of the continued fraction $1/(2-3/(3-4/(4-5/(...(n-1)-n/(-2)))))$. The sequence is defined by the formula: $$a(n) = \frac{n^2 - 2}{\gcd(n^2 - 2, 2 \cdot A051403(n-3) + n \cdot A051403(n-4))}$$ The formula is valid for … · a

a def

A368692: $$a(n) = \frac{(12n + 6)! \cdot (6n + 9)!}{108 \cdot (4n + 2)! \cdot (2n + 3)! \cdot ((6n + 5)!)^2}$$ It is conjectured that $a(n)$ are integers. · a

A005259' def

A005259: The auxiliary sequence used for the Hankel matrix, defined as $$\sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k}^2$$ · A005259'

A005259_comp def

def A005259_comp (n : ℕ) : ℕ · A005259_comp

A051293 def

A051293: Number of nonempty subsets of $\{1, 2, 3, \dots, n\}$ whose elements have an integer average. · A051293

a051403 def

Auxiliary sequence A051403, defined as $$\frac{(n+2) \sum_{k=0}^n k!}{2}$$ · a051403

A224515 def

A224515: $a(n) = \text{least } k \text{ such that } \sqrt{k^2 \operatorname{XOR} (k+1)^2} = 2n+1, \text{ } a(n) = -1 \text{ if there is no such } k$. This is equivalent to finding the smallest $k \in \mathbb{N}$ such that $k^2 \oplus … · A224515

A227582_base def

The sequence $b_n$ such that $A227582(n) = b_{n-1}$ for $n \ge 1$. This is the 0-indexed solution to the linear recurrence in $\mathbb{Z}$. · A227582_base

A256012 def

A256012: Number of partitions of $n$ into distinct parts that are not squarefree. This is the number of finite subsets of positive integers $P$ such that $\sum_{k \in P} k = n$ and every element $k \in P$ is not squarefree. · A256012

A258667 def

A258667: A total of $n$ married couples, including a mathematician M and his wife, are to be seated at the $2n$ chairs around a circular table, with no man seated next to his wife. After the ladies are seated at every other chair, M is the … · A258667

A258667_asymptotic_sum_part def

The infinite series part of the asymptotic expansion: $\sum_{k \ge 1} \frac{(-1)^k}{k!(n-1)_k}$. · A258667_asymptotic_sum_part

A258667_asymptotic_term def

The proposed asymptotic expression for A258667(n). · A258667_asymptotic_term

A258667_inner_sum def

The inner sum of the formula used in A258667: $$\sum_{\max(k-n+5, 0) \le j \le \min(k,4)} \binom{8-j}{j}\binom{2n-k+j-10}{k-j}$$ · A258667_inner_sum

A278070 def

A278070: $a(n) = \text{hypergeometric}([n, -n], [], -1)$. This is equivalent to the combinatorial sum: $$a(n) = \sum_{k=0}^n \binom{n}{k} \binom{n+k-1}{k} k!$$ The expression uses $\mathbb{N}$ arithmetic throughout, safely handling the … · A278070

A282779 def

A282779: Period of cubes mod $n$. The $n$-th term $a(n)$ is the smallest positive integer $T$ such that $\forall k \in \mathbb{N}$, $(k+T)^3 \equiv k^3 \pmod n$. · A282779

A289411 def

A289411: $\mathrm{a}(n) = \sum_{k=0}^n \mathrm{sign}(\mathrm{A007953}(5k) - \mathrm{A007953}(k))$. $\mathrm{A007953}(n)$ is the digital sum of $n$ in base 10. The sequence is non-negative, so the sum over $\mathbb{Z}$ is converted to … · A289411

A306424_condition def

A306424: Numbers $k$ such that the base $b$ expansion of $k$ for each $b = 3..k-1$ never contains more than two distinct digits. · A306424_condition

A340737 def

A340737: Numerators of a sequence of fractions converging to $e$. $$a(1) = 3, a(2) = 5$$ For $n > 2$: $$a(n) = \begin{cases} \left(\frac{n+2}{2}\right) a(n-1) - a(n-2) - \left(\frac{n-2}{2}\right) a(n-3) & \text{if } n \text{ is even} \ 2 … · A340737

A340738 def

A340738: Denominators of a sequence of fractions converging to $e$. This sequence is defined by the same recurrence relation as A340737 but with initial values $b(1)=1, b(2)=2$. $$b(1) = 1, b(2) = 2$$ For $n > 2$: $$b(n) = \begin{cases} … · A340738

A363347 def

A363347: Denominator of the continued fraction $$\frac{1}{2 - \frac{3}{3 - \frac{4}{4 - \frac{5}{\dots - \frac{n-1}{(n-1) - \frac{n}{-4}}}}}} $$ The value of the continued fraction is $C_n = 1/R_2(n)$. If $R_2(n) = N/D$ in reduced form, … · A363347

A382590 def

A382590: $a(n)$ is the sequence defined by the mutual recurrence relations: $a(n) = a(n-1)b(n-2) + a(n-2)b(n-1)$ and $b(n) = a(n-1)b(n-2) - a(n-2)b(n-1)$ starting with $a(0) = b(0) = b(1) = 1$ and a(1) = 2. The terms are in $\mathbb{Z}$ … · A382590

A382590_pair def

Helper function for A382590, computing the pair $(a(n), b(n))$ such that: $a(n) = a(n-1)b(n-2) + a(n-2)b(n-1)$ $b(n) = a(n-1)b(n-2) - a(n-2)b(n-1)$ · A382590_pair

a_comp def

def a_comp (n : ℕ) : ℕ · a_comp

A_int def

def A_int (n k : ℕ) : ℤ · A_int

A_j def

def A_j (j : ℕ) : Finset ℕ · Erdos26.A_j

a_rat def

def a_rat (n : ℕ) : ℚ · a_rat

a_real def

def a_real (n : ℕ) : ℝ · a_real

A_seq def

def A_seq (n : ℕ) : ℝ · A_seq

A_seq def

def A_seq (n k : ℕ) : ℚ · A_seq

A_set def

def A_set (q : ℕ × ℕ → ℝ²) : Set ℝ² · Erdos846.A_set

a_vec def

def a_vec : ZMod 3 → ℂ · Green57.a_vec

abs_diff def

def abs_diff (a b : ℕ) : ℕ · abs_diff

add def

def Eisen.add (x y : Eisen) : Eisen · Green57.Eisen.add

AddEdge def

def AddEdge (T : SimpleGraph α) (a b : α) (h_neq : a ≠ b) : SimpleGraph α · WrittenOnTheWallII.GraphConjecture2.AddEdge

alg_dir_lim def

def alg_dir_lim (k : Type u) [Field k] (ι : Type w) [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι] (G : ι → Type (max u v)) [∀ i, CommRing (G i)] [∀ i, Algebra k (G i)] (f : ∀ i j, i ≤ j → G i … · alg_dir_lim

all_fail def

def all_fail (k max : ℕ) : Bool · all_fail

allEqual def

All indices equal on Fin N (using the canonical ordered vertex list). · MonochromaticQuantumGraph.allEqual

allEqualList def

Chain-equality along a list of vertices. · MonochromaticQuantumGraph.allEqualList

ap_equiv def

For `d>0`, the map `m ↦ a+m*d` is an equivalence from the `k` indices to the set of the first `k` terms of the arithmetic progression. · Erdos138.ap_equiv

B

B def

def B : Set ℕ · Erdos741.B

B1 def

`B1` is the range of `split1`. Its elements use only 0-or-1 base-four digits, making `B1+B1` digitwise sparse even though `B1+B2` will cover every natural number. · Erdos741.B1

B2 def

`B2` is the range of `split2`. It is the digitwise complement to `B1`: together the two sets represent every natural, while `B2+B2` has the same sparse-count phenomenon as `B1+B1`. · Erdos741.B2

B_orbit def

def B_orbit (d : ℕ) : List ℕ · B_orbit

B_seq def

def B_seq (n : ℕ) : ℝ · B_seq

B_seq def

def B_seq (n : ℕ) : ℤ · B_seq

B_seq def

def B_seq (d : ℕ) : ℕ → ℕ · B_seq

B_series def

def B_series : PowerSeries ℤ · B_series

bad_for_even_k def

def bad_for_even_k (p : ℕ) : Bool · bad_for_even_k

bad_for_k def

def bad_for_k (p : ℕ) (k : ℕ) : Bool · bad_for_k

base2_to_base4 def

def base2_to_base4 (n : ℕ) : ℕ · Erdos741.base2_to_base4

base3_to_base4 def

def base3_to_base4 (n : ℕ) : ℕ · Erdos741.base3_to_base4

base_change_map def

def base_change_map (k k' A L : Type*) [Field k] [Field k'] [CommRing A] [Field L] [Algebra k k'] [Algebra k' A] [Algebra k A] [IsScalarTower k k' A] [Algebra k L] [Algebra k' L] [IsScalarTower k k' … · base_change_map

baseΦ def

The generating family of functions for Φ(G). The functions fᵢ : G × G → ℂ are bounded by 1 in sup norm. · Green57.baseΦ

baseΦ' def

The generating family of functions for Φ′(G), where the third kernel depends only on x₁ + x₂. · Green57.baseΦ'

bellState abbrev

The standard $d$-dimensional Bell state. · OpenQuantumProblem35.bellState

bipartiteDeck def

Deck of a bipartite graph. Deck is the multiset of all vertex-deleted subgraphs viewed unlabeled up to bipartite isomorphism. · bipartiteDeck

BipartiteIso structure

Strict bipartite isomorphism that explicitly preserves the left and right partitions. · BipartiteIso

BipartiteIso_refl def

def BipartiteIso_refl (G : SimpleGraph V) (leftU rightV : Finset V) : BipartiteIso G G leftU rightV · BipartiteIso_refl

BipartiteIso_symm def

def BipartiteIso_symm {G H : SimpleGraph V} {leftU rightV : Finset V} (iso : BipartiteIso G H leftU rightV) : BipartiteIso H G leftU rightV · BipartiteIso_symm

block_multiples_A def

def block_multiples_A (j k : ℕ) : Set ℕ · Erdos26.block_multiples_A

BlockSeq def

def BlockSeq · Erdos741.BlockSeq

bound_seq def

def bound_seq (k : ℕ) : ℝ · bound_seq

branch_A def

def branch_A (k0 k1 k2 : ZMod 3) : ℂ · Green57.branch_A

branch_A_eisen def

def branch_A_eisen (k0 k1 k2 : ZMod 3) : Eisen · Green57.branch_A_eisen

branch_B def

def branch_B (k0 k1 k2 : ZMod 3) : ℂ · Green57.branch_B

branch_B_eisen def

def branch_B_eisen (k0 k1 k2 : ZMod 3) : Eisen · Green57.branch_B_eisen

branch_C def

def branch_C (k0 k1 k2 : ZMod 3) : ℂ · Green57.branch_C

branch_C_eisen def

def branch_C_eisen (k0 k1 k2 : ZMod 3) : Eisen · Green57.branch_C_eisen

C

C1 def

def C1 (X : Set ℤ) · Erdos152.C1

C2 def

def C2 (X : Set ℤ) · Erdos152.C2

C3 def

def C3 (X : Set ℤ) · Erdos152.C3

C4 def

def C4 (X : Set ℤ) · Erdos152.C4

c_seq def

def c_seq (A B : ℕ) (d : ℤ) : ℤ · c_seq

C_set_Z def

def C_set_Z (X : Set ℤ) · Erdos152.C_set_Z

c_val def

def c_val (k : ZMod 3) : ℂ · Green57.c_val

c_val_eisen def

def c_val_eisen (k : ZMod 3) : Eisen · Green57.c_val_eisen

ca_rule_167 def

The rule function for Rule 167. Inputs must be 0 or 1. · ca_rule_167

ca_state def

The state of the Rule 167 elementary cellular automaton at time $t$ and position $x$. The initial condition is a single ON cell at $x=0$. $C(t, x)$ is structurally recursive on $t$. · ca_state

ca_step_fun def

def ca_step_fun (f : ℕ → ℕ) : ℕ → ℕ · ca_step_fun

ca_step_list def

def ca_step_list (config : List ℕ) : List ℕ · ca_step_list

cassels_set def

def cassels_set : Set ℕ · Erdos741.cassels_set

catalan_reciprocal_sum def

The sum $\sum_{i=j}^k \frac{1}{a(i)}$ of reciprocals of Catalan numbers. · catalan_reciprocal_sum

check_271_all def

def check_271_all : Bool · check_271_all

check_523_all def

def check_523_all : Bool · check_523_all

check_all_subsets_complement def

def check_all_subsets_complement : Bool · OpenQuantumProblem35.check_all_subsets_complement

check_all_subsets_det def

def check_all_subsets_det : Bool · OpenQuantumProblem35.check_all_subsets_det

check_chunk def

def check_chunk (a b : ℕ) : Bool · check_chunk

check_cond def

def check_cond (k : ℕ) : Bool · check_cond

check_p_fast def

def check_p_fast (p : ℕ) : Bool · check_p_fast

check_p_fast_loop def

def check_p_fast_loop (p y fuel : ℕ) : Bool · check_p_fast_loop

check_p_fast_with_P def

def check_p_fast_with_P (p P : ℕ) : Bool · check_p_fast_with_P

classEdgeCount def

def classEdgeCount (S : Set (SimpleGraph V)) : ℕ · classEdgeCount

coefficients_schedule def

def coefficients_schedule (gamma K : ℝ) (t : ℕ) : ℝ × ℝ · Arxiv.«1905.10899».coefficients_schedule

combineFirst def

Merge a configuration on the first $m$ parties and a configuration on the remaining $n-m$ parties into a configuration on all $n$ parties. · OpenQuantumProblem35.combineFirst

comm_K_alg def

def comm_K_alg {k K S : Type*} [Field k] [Field K] [CommRing S] [Algebra k K] [Algebra k S] : letI : Algebra K (S ⊗[k] K) · comm_K_alg

Config abbrev

A computational-basis configuration of $n$ parties with local dimension $d$. · OpenQuantumProblem35.Config

constantCompletion def

The completion function for constant-support states reduced to one party. · OpenQuantumProblem35.constantCompletion

constantConfig def

The constant configuration with value $a$. · OpenQuantumProblem35.constantConfig

construct_k def

def construct_k (S M : ℕ) : ℕ → ℕ · construct_k

construct_Q def

def construct_Q {k K A : Type*} [Field k] [Field K] [Field A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] [IsAlgClosed A] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (e : ℕ) (S : … · construct_Q

ContiguousGT1 def

def ContiguousGT1 (f : ℕ → ℕ) : Prop · ContiguousGT1

continued_fraction_denominator def

Helper function for A363347, which computes the denominator $R_k(n)$ of the continued fraction expression. For $2 \le k \le n-1$, $R_k(n)$ is defined recursively: $$R_k(n) = k - \frac{k+1}{R_{k+1}(n)}$$ The base case is $R_{n-1}(n) = (n-1) … · continued_fraction_denominator

continued_fraction_tail def

Recursive function to compute $A_k(n)$, the denominator tail $k - \frac{k+1}{A_{k+1}(n)}$. The base case is at $k = n - 1$, where $A_{n-1} = (n-1) - \frac{n}{n+4}$. · continued_fraction_tail

continued_fraction_val def

The total value of the continued fraction $C_n$. · continued_fraction_val

coprime_indices def

def coprime_indices (r : ℕ) : Finset ℕ · coprime_indices

count_distinct def

def count_distinct (l : List ℕ) : ℕ · count_distinct

covered_by_C1 def

An index k is covered by Conjecture 1 if k = 10m + 2 for some m >= 0, predicting a(k)=67. · covered_by_C1

covered_by_C2 def

An index k is covered by Conjecture 2 if k = 36m + 16 for some m >= 0, and m is not 1 mod 5, predicting a(k)=271. · covered_by_C2

covered_by_C3 def

An index k is covered by Conjecture 3 if k = 84m + 22 for some m >= 0, and m is not 0 mod 5, predicting a(k)=523. · covered_by_C3

D

D_mat def

def D_mat (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℤ · D_mat

D_mat4 def

def D_mat4 (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℤ · D_mat4

D_set def

def D_set (A : Set ℕ) : Set ℤ · Erdos152.D_set

dc_seq def

def dc_seq (A B : ℕ) (x : ℤ) : ℤ · dc_seq

ddu def

def ddu (k : ℕ) (x : ℝ) : ℝ · ddu

deg3t_minus_1_fat def

def deg3t_minus_1_fat (t : ℕ) : Finset (Monomial 3) · deg3t_minus_1_fat

deg3t_minus_1_long def

def deg3t_minus_1_long (t : ℕ) : Finset (Monomial 3) · deg3t_minus_1_long

deg3t_minus_2_fat def

def deg3t_minus_2_fat (t : ℕ) : Finset (Monomial 3) · deg3t_minus_2_fat

deg3t_minus_2_long def

def deg3t_minus_2_long (t : ℕ) : Finset (Monomial 3) · deg3t_minus_2_long

degreeMultiset def

`degreeMultiset G` lists the degree of every vertex of `G` while forgetting which vertex has which degree. This is the intermediate invariant reconstructed from the edge counts of the deck's cards. · degreeMultiset

degreeProfile def

The neighbor-degree profile of x ∈ U ⊔ V is the multiset P(x) = {deg_G(y) : y ∈ Neighbors(x)} · degreeProfile

degXY def

def degXY (m : Monomial 3) : ℕ · degXY

degZ def

def degZ (m : Monomial 3) : ℕ · degZ

det2 def

def det2 (m00 m01 m10 m11 : Nat) : Nat · OpenQuantumProblem35.det2

det3 def

def det3 (m00 m01 m02 m10 m11 m12 m20 m21 m22 : Nat) : Nat · OpenQuantumProblem35.det3

det4 def

def det4 (m00 m01 m02 m03 m10 m11 m12 m13 m20 m21 m22 m23 m30 m31 m32 m33 : Nat) : Nat · OpenQuantumProblem35.det4

det5 def

def det5 (m00 m01 m02 m03 m04 m10 m11 m12 m13 m14 m20 m21 m22 m23 m24 m30 m31 m32 m33 m34 m40 m41 m42 m43 m44 : Nat) : Nat · OpenQuantumProblem35.det5

diagonalState def

The diagonal $n$-party state: the uniform superposition over constant computational-basis strings. · OpenQuantumProblem35.diagonalState

diff def

At a positive index, `diff(h,d)` (Lean: `diff h d`) is `h(d)-h(d-1)`, the change from the preceding value. At index zero the definition uses `h(0)`, giving the difference operator a total boundary value on natural-number indices. · diff

diff2 def

At a positive index, `diff2(h,d)` (Lean: `diff2 h d`) measures how the first difference changes: `Δh(d)-Δh(d-1)`. This discrete curvature is the quantity bounded by `1` for each principal sequence and by `2` for their sum. · diff2

DiffByOneF def

def DiffByOneF (f1 f2 : ℕ → ℕ) (p : ℕ) : Prop · DiffByOneF

dipMonomialFat def

def dipMonomialFat (t : ℕ) : Monomial 3 · dipMonomialFat

dipMonomialLong def

def dipMonomialLong (i t : ℕ) : Monomial 3 · dipMonomialLong

dipMonomials3 def

def dipMonomials3 (t : ℕ) : Finset (Monomial 3) · dipMonomials3

dipOrderIdeal3 def

def dipOrderIdeal3 (t : ℕ) : OrderIdeal 3 · dipOrderIdeal3

dipPureOrderIdeal3 def

def dipPureOrderIdeal3 (t : ℕ) (ht : 5 ≤ t) : PureOrderIdeal 3 · dipPureOrderIdeal3

divisor_product def

The product term in the denominator of the general conjecture: $$\prod_{i = 1..r, i \text{ coprime to } 30} (30n - i)$$ We define this in ℤ to handle the $n=0$ case where $30n-i$ in the product might be negative. · divisor_product

divisorsFinset def

The finite set of divisors of a monomial, i.e. the principal lower set {m | m ≤ g}. · divisorsFinset

doubleDeck def

The double deck is D_2(G) = {G - x - y := x ≠ y ∈ U ⊔ V} viewed unlabeled up t bipartite isomorphism. · doubleDeck

DoubleStar def

def DoubleStar (G : SimpleGraph α) (x y : α) (hxy : G.Adj x y) : SimpleGraph α · WrittenOnTheWallII.GraphConjecture2.DoubleStar

drop_col def

def drop_col (k : Fin 6) (i : Fin 5) : Fin 6 · OpenQuantumProblem35.drop_col

du def

def du (k : ℕ) (x : ℝ) : ℝ · du

E

E_n abbrev

abbrev E_n · Arxiv.«1905.10899».E_n

E_poly def

def E_poly (n : ℝ) : ℝ · E_poly

E_seq def

def E_seq (n : ℕ) : ℝ · E_seq

edgeCount abbrev

abbrev edgeCount (G : SimpleGraph V) : ℕ · edgeCount

EdgeN structure

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

Eisen structure

structure Eisen · Green57.Eisen

embedFin3 def

def embedFin3 {r : ℕ} (hr : 3 ≤ r) : Fin 3 ↪ Fin r · embedFin3

embedFinset def

def embedFinset {r : ℕ} (S : Finset (Monomial r)) : Finset (Monomial (r + 1)) · embedFinset

embedMonomial def

def embedMonomial {r : ℕ} (hr : 3 ≤ r) (m : Monomial 3) : Monomial r · embedMonomial

embedMonomial def

def embedMonomial {r : ℕ} (m : Monomial r) : Monomial (r + 1) · embedMonomial

embedOrderIdeal def

def embedOrderIdeal {r : ℕ} (hr : 3 ≤ r) (I : OrderIdeal 3) : OrderIdeal r · embedOrderIdeal

embedPureOrderIdeal def

def embedPureOrderIdeal {r : ℕ} (hr : 3 ≤ r) (P : PureOrderIdeal 3) : PureOrderIdeal r · embedPureOrderIdeal

eps def

def eps (n : ℕ) : ℝ · eps

EqSystemN def

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

eval_hom def

def eval_hom {k A : Type*} [Field k] [CommRing A] [Algebra k A] (m : Ideal A) [m.IsMaximal] (psi : (A ⧸ m) ≃ₐ[k] k) : A →ₐ[k] k · eval_hom

eval_tensor_hom def

def eval_tensor_hom {k A L : Type*} [Field k] [CommRing A] [Field L] [Algebra k A] [Algebra k L] (pi : A →ₐ[k] k) : A ⊗[k] L →ₐ[k] L · eval_tensor_hom

evalMap def

def evalMap (k S : Type*) [CommRing k] [CommRing S] [Algebra k S] : S →ₗ[k] ProdResidueFields S · evalMap

ExistsAME def

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

ExistsNonLogConcavePureOSeq def

Helper predicate for open problems about non-log-concavity at fixed codimension/type. · ExistsNonLogConcavePureOSeq

expected_state def

def expected_state (t : ℕ) (x : ℤ) : ℕ · expected_state

explicit_A def

def explicit_A : Matrix (Fin 11) (Fin 11) (ZMod 5) · OpenQuantumProblem35.explicit_A

explicit_A_nat def

def explicit_A_nat (i j : Nat) : Nat · OpenQuantumProblem35.explicit_A_nat

extend_coloring def

`extend_coloring N c` agrees with the subtype-valued colouring `c` on `{1,...,N}` and assigns colour `0` everywhere outside that interval. · Erdos138.extend_coloring

extract_binary def

def extract_binary (m : ℕ) : ℕ · Erdos741.extract_binary

F

F def

def F (n t : ℕ) : ℕ → ℕ · 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

def f (n : ℕ) : ℤ · f

f def

def f (j : ℕ) : ℤ · f

F_list def

def F_list (n : ℕ) : List (Fin (n + 1) → ℕ) · F_list

F_m abbrev

abbrev F_m · Arxiv.«1905.10899».F_m

f_nat def

def f_nat (x d : ℕ) : ℤ · f_nat

F_operator def

Operator G(z) = (∇_x L(z), -∇_y L(z)) · Arxiv.«1905.10899».F_operator

f_seq def

def f_seq (n : ℕ) : Set ℕ · Erdos741.f_seq

F_set def

def F_set (n : ℕ) : Finset (Fin (n + 1) → ℕ) · F_set

f_val def

`f_val m i = M m + x_val m + i*P m` is the `i`th candidate in block `m`. · Erdos12.f_val

fA_alg def

def fA_alg (k k' A L : Type*) [Field k] [Field k'] [CommRing A] [Field L] [Algebra k k'] [Algebra k' A] [Algebra k A] [IsScalarTower k k' A] [Algebra k L] [Algebra k' L] [IsScalarTower k k' L] : A … · fA_alg

fA_hom def

def fA_hom (k k' A L : Type*) [Field k] [Field k'] [CommRing A] [Field L] [Algebra k k'] [Algebra k' A] [Algebra k A] [IsScalarTower k k' A] [Algebra k L] [Algebra k' L] [IsScalarTower k k' L] : A … · fA_hom

fib def

def fib : ℕ → ℤ · fib

fiberMap def

def fiberMap {k : Type u} {R S : Type v} [Field k] [CommRing R] [CommRing S] [Algebra k R] [Algebra k S] (P : Ideal R) [P.IsPrime] : (R ⊗[k] S) →ₐ[k] (S ⊗[k] FiberRing k R P) · fiberMap

fiberMap_alt def

def fiberMap_alt {k : Type u} {R S : Type v} [Field k] [CommRing R] [CommRing S] [Algebra k R] [Algebra k S] (P : Ideal R) [P.IsPrime] : (R ⊗[k] S) →ₐ[k] (FiberRing k R P ⊗[k] S) · fiberMap_alt

FiberRing def

def FiberRing (k : Type u) (R : Type v) [Field k] [CommRing R] [Algebra k R] (P : Ideal R) : Type (max u v) · FiberRing

FinSepSubext abbrev

abbrev FinSepSubext (k k' : Type*) [Field k] [Field k'] [Algebra k k'] · FinSepSubext

FirstDiffZ def

def FirstDiffZ (P : PureOrderIdeal 3) (j : ℕ) : ℤ · FirstDiffZ

fL_alg def

def fL_alg (k k' A L : Type*) [Field k] [Field k'] [CommRing A] [Field L] [Algebra k k'] [Algebra k' A] [Algebra k A] [IsScalarTower k k' A] [Algebra k L] [Algebra k' L] [IsScalarTower k k' L] : L … · fL_alg

fL_hom def

def fL_hom (k k' A L : Type*) [Field k] [Field k'] [CommRing A] [Field L] [Algebra k k'] [Algebra k' A] [Algebra k A] [IsScalarTower k k' A] [Algebra k L] [Algebra k' L] [IsScalarTower k k' L] : L … · fL_hom

FormsTriangle def

def FormsTriangle (e₁ e₂ e₃ : ℕ × ℕ) : Prop · Erdos846.FormsTriangle

frac_part def

The fractional part of a rational number, viewed as a real number. Must be noncomputable due to dependence on the real floor function. · frac_part

functional def

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

G

g_block def

`g_block n` is the least `k` with `M k≤n<M (k+1)`, when such a block exists; otherwise it is zero. · Erdos12.g_block

G_D def

def G_D (t : ℕ) : Finset (Monomial 3) · G_D

G_D_minus_1 def

def G_D_minus_1 (t : ℕ) : Finset (Monomial 3) · G_D_minus_1

G_D_minus_2 def

def G_D_minus_2 (t : ℕ) : Finset (Monomial 3) · G_D_minus_2

g_p def

def g_p (p : ℕ) : ℕ · g_p

g_val def

`g_val n` pairs the block index containing `n` with the quotient `(n-M k)/P k` inside that block. · Erdos12.g_val

GammaP1 def

The order ideal generated by the two monomials from P1. · GammaP1

gap_seq def

def gap_seq (n : ℕ) : ℕ · Erdos741.gap_seq

gen_G def

def gen_G (n : ℕ) : List (List ℕ) · gen_G

gen_states def

def gen_states : ℕ → List (List ℕ) × List (List ℕ) · gen_states

generatedOrderIdeal def

The finite order ideal generated by a finite set of monomials. · generatedOrderIdeal

GeometricallyIrreducibleAlgebra class

class GeometricallyIrreducibleAlgebra (k : Type u) (S : Type v) [Field k] [CommRing S] [Algebra k S] : Prop · GeometricallyIrreducibleAlgebra

get_cols def

def get_cols (f0 f1 f2 f3 f4 : Nat) : Nat × Nat × Nat × Nat × Nat × Nat · OpenQuantumProblem35.get_cols

get_cols_complement_bool def

def get_cols_complement_bool (f0 f1 f2 f3 f4 : Nat) : Bool · OpenQuantumProblem35.get_cols_complement_bool

get_period def

def get_period (p : ℕ) : ℕ · get_period

get_period_loop def

def get_period_loop (mod target fuel r curr : ℕ) : ℕ · get_period_loop

get_y_fun def

def get_y_fun (k k' A L : Type*) [Field k] [Field k'] [CommRing A] [Field L] [Algebra k k'] [Algebra k' A] [Algebra k A] [IsScalarTower k k' A] [Algebra k L] [Algebra k' L] [IsScalarTower k k' L] … · get_y_fun

ghzState abbrev

The standard $d$-dimensional GHZ state on $3$ parties. · OpenQuantumProblem35.ghzState

ghzState4 abbrev

The standard $d$-dimensional GHZ state on $4$ parties. · OpenQuantumProblem35.ghzState4

GoodCasselsProperty def

def GoodCasselsProperty (A : Set ℕ) : Prop · Erdos741.GoodCasselsProperty

GoodDigit def

def GoodDigit (b d : ℕ) : Prop · GoodDigit

graphState def

def graphState {n : ℕ} (A : Matrix (Fin n) (Fin n) (ZMod 5)) : StateVector n 5 · OpenQuantumProblem35.graphState

graphStateAmp def

def graphStateAmp {n : ℕ} (A : Matrix (Fin n) (Fin n) (ZMod 5)) (x : Config n 5) : ℂ · OpenQuantumProblem35.graphStateAmp

GreedyGaps def

def GreedyGaps (f : ℕ → Set ℕ) (gap_end : ℕ → ℕ) : Prop · Erdos741.GreedyGaps

GreedySpaced def

def GreedySpaced (f : ℕ → Set ℕ) (gap_end : ℕ → ℕ) : Prop · Erdos741.GreedySpaced

H

H_calc def

`H_calc(A,B,C,d)` sums the two-coordinate count `L_seq(A,B,k)` over possible partial degrees `k`, retaining only those for which the remaining exponent `d-k` fits below `C`. Lean writes these applications with spaces. · H_calc

H_seq def

`H_seq` adds the principal degree counts below `m₁` to a shifted residual degree count derived from `m₂`. The second term is zero below the threshold `m₁(x)+1`, exactly encoding the piecewise decomposition of the manuscript's equation (2). · H_seq

h_seq def

`h_seq(m,d)` (Lean: `h_seq m d`) counts the divisors of `m` having total degree `d`. Geometrically this is a slice of the exponent box below `m`; it is the principal sequence denoted `h_m(d)` in the companion proof. · h_seq

H_sum def

def H_sum (n : ℕ) : ℝ · H_sum

H_Z def

def H_Z (m2 m1_star : Monomial 3) (shift : ℕ) (d : ℤ) : ℤ · H_Z

half_ceil def

def half_ceil (m : ℕ) : ℕ · half_ceil

half_floor def

def half_floor (m : ℕ) : ℕ · half_floor

HasLargeGaps def

def HasLargeGaps (S : Set ℕ) : Prop · Erdos741.HasLargeGaps

HasMaximallyMixedFirstReduction def

A state has maximally mixed reduction on the first $m$ parties. · OpenQuantumProblem35.HasMaximallyMixedFirstReduction

HasMonoAP def

`HasMonoAP c N k` supplies a first term `a` and positive step `d` such that all `k` terms `a+m*d` have colour `c a`, start at or above 1, and end at or before `N`. · Erdos138.HasMonoAP

I

I_map def

def I_map (N : ℕ) (p : ℕ × ℕ) : ℕ × ℕ · I_map

I_N def

def I_N (X : Set ℕ) : ℕ · Erdos152.I_N

I_rel def

def I_rel (k k' A L : Type*) [Field k] [Field k'] [CommRing A] [Field L] [Algebra k k'] [Algebra k' A] [Algebra k A] [IsScalarTower k k' A] [Algebra k L] [Algebra k' L] [IsScalarTower k k' L] : Ideal … · I_rel

I_sum def

def I_sum (n : ℕ) : ℝ · I_sum

I_val def

def I_val (n : ℕ) : ℤ · I_val

I_Z def

def I_Z (X : Set ℤ) : ℕ · Erdos152.I_Z

ind def

def ind (X : Set ℤ) (x : ℤ) : ℤ · Erdos152.ind

initial_config_list def

def initial_config_list (n : ℕ) : List ℕ · initial_config_list

InSubalgebra def

def InSubalgebra {K F L : Type*} [Field K] [CommRing F] [Algebra K F] [CommRing L] [Algebra K L] (A : Subalgebra K F) (x : F ⊗[K] L) : Prop · InSubalgebra

int_choose def

def int_choose (n : ℕ) (k : ℤ) : ℕ · int_choose

integralClosure_to_IntermediateField def

def integralClosure_to_IntermediateField (k k' : Type*) [Field k] [Field k'] [Algebra k k'] : IntermediateField k k' · integralClosure_to_IntermediateField

IntQ2 def

def IntQ2 (n : ℕ) : ℤ · IntQ2

is_carmichael_number def

Definition of a Carmichael number $n$: a composite number s.t. $b^{n-1} \equiv 1 \pmod n$ for all $b$ coprime to $n$. · is_carmichael_number

is_composite def

Helper definition for "composite number" · is_composite

is_full_rank_M def

def is_full_rank_M (f0 f1 f2 f3 f4 c0 c1 c2 c3 c4 c5 : Nat) : Bool · OpenQuantumProblem35.is_full_rank_M

is_maximal_run def

def is_maximal_run (v : ℕ) (n L : ℕ) : Prop · is_maximal_run

is_prime def

def is_prime (p : ℕ) : Bool · is_prime

is_prime_fast def

def is_prime_fast (p : ℕ) : Bool · is_prime_fast

is_prime_loop def

def is_prime_loop (p i fuel : ℕ) : Bool · is_prime_loop

is_ratio_decreasing_Z def

def is_ratio_decreasing_Z (f : ℤ → ℤ) : Prop · is_ratio_decreasing_Z

is_valid_Y def

def is_valid_Y (l : List ℕ) : Prop · is_valid_Y

IsAbsoluteEulerPseudoprime def

A natural number $m > 1$ is an absolute Euler pseudoprime if it is composite and for all $b$ coprime to $m$, $b^{(m-1)/2} \equiv \pm 1 \pmod m$. · IsAbsoluteEulerPseudoprime

IsAME def

A state $\psi$ is absolutely maximally entangled. · OpenQuantumProblem35.IsAME

IsBehrend def

A sequence of naturals $(a_i)$ is Behrend if almost all integers are a multiple of some $a_i$. In other words, if the set of multiples has natural density $1$. · Erdos26.IsBehrend

IsConstantConfig def

A configuration is constant if all coordinates agree. · OpenQuantumProblem35.IsConstantConfig

IsGood abbrev

A set A is "good" if it is infinite and there are no distinct a,b,c in A such that a ∣ (b+c) and b > a, c > a. · Erdos12.IsGood

IsGood def

def IsGood (b : ℕ) (X : ℤ) : Prop · IsGood

IsGoodMap def

def IsGoodMap (q : ℕ × ℕ → ℝ²) : Prop · Erdos846.IsGoodMap

IsGoodSarkozySeq def

def IsGoodSarkozySeq (B : ℕ → Set ℕ) (p : ℕ → ℕ) (c : ℝ) : Prop · Erdos12.IsGoodSarkozySeq

IsGreedyBasis def

def IsGreedyBasis (f : ℕ → Set ℕ) : Prop · Erdos741.IsGreedyBasis

IsLogConcaveUpTo def

Log-concavity up to degree e: h_i² ≥ h_{i-1} h_{i+1} for i ∈ (0, e). · IsLogConcaveUpTo

IsMaximalIn def

Maximality with respect to divisibility inside an order ideal. · IsMaximalIn

IsNormalized def

A state vector is normalized if it has $L^2$ norm $1$. · OpenQuantumProblem35.IsNormalized

IsPure def

Purity: all maximal monomials have the same total degree. · IsPure

IsSaddlePoint def

def IsSaddlePoint (L : Z_space n m → ℝ) (z_star : Z_space n m) : Prop · Arxiv.«1905.10899».IsSaddlePoint

IsSeparableExtensionSP class

class IsSeparableExtensionSP (k K : Type*) [Field k] [Field K] [Algebra k K] : Prop · IsSeparableExtensionSP

IsSeparablyFinitelyGenerated class

class IsSeparablyFinitelyGenerated (k K : Type*) [Field k] [Field K] [Algebra k K] : Prop · IsSeparablyFinitelyGenerated

IsSeparablyGenerated class

class IsSeparablyGenerated (k K : Type*) [Field k] [Field K] [Algebra k K] : Prop · IsSeparablyGenerated

IsThick def

A sequence of naturals $(a_i)$ is thick if their sum of reciprocals diverges: $$ \sum_i \frac{1}{a_i} = \infty $$ · Erdos26.IsThick

IsUnimodal def

Unimodality of a finite sequence h up to index e: there exists a peak j ≤ e such that h is weakly increasing on [0, j] and weakly decreasing on [j, e]. · IsUnimodal

isValidBranch def

def isValidBranch (k0 k1 k2 : ZMod 3) : Bool · Green57.isValidBranch

IsWeaklyBehrend def

A sequence of naturals $(a_i)$ is weakly Behrend with respect to $\varepsilon \in \mathbb{R}$ if at least $1 - \varepsilon$ density of all numbers are a multiple of $A$. · Erdos26.IsWeaklyBehrend

J

J def

def J (k : ℕ) : ℝ · J

K

K def

`K 0 = 729 = 3^6`, and `K (m+1) = K m * q m`. · Erdos12.K

K def

def K (n : ℕ) : ℕ · K

K_equiv_polynomial def

def K_equiv_polynomial {E K : Type*} [Field E] [Field K] [Algebra E K] [FiniteDimensional E K] (x : K) (hx : IntermediateField.adjoin E ({x} : Set K) = ⊤) : (E[X] ⧸ Ideal.span {minpoly E x}) ≃ₐ[E] K · K_equiv_polynomial

K_j def

def K_j (j : ℕ) : ℕ · Erdos26.K_j

kth_prime_factor def

The k-th prime factor of an integer n (where k>=1), counted with multiplicity. This is defined as the k-th element (0-indexed k-1) of Nat.primeFactorsList n.natAbs. Returns 1 if n has fewer than k prime factors or if n is 0, 1, or -1, … · kth_prime_factor

L

L5 def

def L5 : List ℕ · L5

L_def def

def L_def (n : ℕ) : ℕ · L_def

L_seq def

`L_seq(A,B,d)` (Lean: `L_seq A B d`) counts pairs of nonnegative exponents with first coordinate below `A`, second coordinate below `B`, and total degree `d`. Lean stores only the first coordinate because the second is forced to be `d-x`. · L_seq

L_seq def

def L_seq : ℕ → List ℕ · L_seq

LCFailureThreshold def

Helper: t0 is a threshold after which all types admit a non-log-concave example. · LCFailureThreshold

leftIndex def

The embedding of the first $m$ indices into $\mathrm{Fin}\, n$. · OpenQuantumProblem35.leftIndex

lift_to_S def

def lift_to_S (k k' A L : Type*) [Field k] [Field k'] [CommRing A] [Field L] [Algebra k k'] [Algebra k' A] [Algebra k A] [IsScalarTower k k' A] [Algebra k L] [Algebra k' L] [IsScalarTower k k' L] : … · lift_to_S

list_max def

def list_max (l : List ℕ) : ℕ · list_max

list_to_fun def

def list_to_fun (l : List ℕ) : ℕ → ℕ · list_to_fun

loc_equiv_of_eq def

def loc_equiv_of_eq.{v} {R : Type v} [CommRing R] (M P : Ideal R) [M.IsPrime] [P.IsPrime] (h : P = M) : Localization.AtPrime P ≃+* Localization.AtPrime M · loc_equiv_of_eq

loop_comp_f0 def

def loop_comp_f0 (f0 : Nat) : Bool · OpenQuantumProblem35.loop_comp_f0

loop_comp_f1 def

def loop_comp_f1 (m0 f1 : Nat) : Bool · OpenQuantumProblem35.loop_comp_f1

loop_comp_f2 def

def loop_comp_f2 (m0 m1 f2 : Nat) : Bool · OpenQuantumProblem35.loop_comp_f2

loop_comp_f3 def

def loop_comp_f3 (m0 m1 m2 f3 : Nat) : Bool · OpenQuantumProblem35.loop_comp_f3

loop_comp_f4 def

def loop_comp_f4 (m0 m1 m2 m3 f4 : Nat) : Bool · OpenQuantumProblem35.loop_comp_f4

loop_det_f0 def

def loop_det_f0 (f0 : Nat) : Bool · OpenQuantumProblem35.loop_det_f0

loop_det_f1 def

def loop_det_f1 (m0 f1 : Nat) : Bool · OpenQuantumProblem35.loop_det_f1

loop_det_f2 def

def loop_det_f2 (m0 m1 f2 : Nat) : Bool · OpenQuantumProblem35.loop_det_f2

loop_det_f3 def

def loop_det_f3 (m0 m1 m2 f3 : Nat) : Bool · OpenQuantumProblem35.loop_det_f3

loop_det_f4 def

def loop_det_f4 (m0 m1 m2 m3 f4 : Nat) : Bool · OpenQuantumProblem35.loop_det_f4

lucas def

def lucas : ℕ → ℤ · lucas

M

M def

`M m` is the eighth power of `P m`. · Erdos12.M

M def

def M (n : ℕ) : ℕ · M

M0 def

def M0 : ℝ · M0

m002 def

def m002 : Monomial 3 · m002

m011 def

def m011 : Monomial 3 · m011

M1 def

def M1 : ℝ · M1

m101 def

def m101 : Monomial 3 · m101

m110 def

def m110 : Monomial 3 · m110

M2 def

def M2 : ℝ · M2

M3 def

def M3 : ℝ · M3

M4 def

def M4 : ℝ · M4

M5 def

def M5 : ℝ · M5

M_prime def

def M_prime (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℤ · M_prime

M_prime4 def

def M_prime4 (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℤ · M_prime4

m_star def

def m_star (t : ℕ) : Monomial 3 · m_star

m_star_divs_1 def

def m_star_divs_1 (t : ℕ) : Finset (Monomial 3) · m_star_divs_1

m_star_divs_2 def

def m_star_divs_2 (t : ℕ) : Finset (Monomial 3) · m_star_divs_2

M_val def

def M_val (a : ℕ) : Set ℕ · Erdos26.M_val

m_val def

def m_val (n : ℕ) : ℤ · m_val

map_frac def

def map_frac {R S : Type*} [CommRing R] [IsDomain R] [CommRing S] [IsDomain S] (f : R →+* S) (hf : Function.Injective f) : FractionRing R →+* FractionRing S · map_frac

map_powerSeries_frac def

def map_powerSeries_frac {A : Type*} [CommRing A] [IsDomain A] : FractionRing A⟦X⟧ →+* FractionRing (FractionRing A)⟦X⟧ · map_powerSeries_frac

mapToS def

def mapToS {k K S : Type*} [Field k] [CommRing K] [Algebra k K] [CommRing S] [Algebra k S] (g : K →ₗ[k] k) : K ⊗[k] S →ₗ[k] S · mapToS

max_A_j def

def max_A_j (j : ℕ) : ℕ · Erdos26.max_A_j

maximallyMixed def

The maximally mixed state on $m$ parties. · OpenQuantumProblem35.maximallyMixed

maximalMonomials def

The finite set of maximal monomials of an order ideal. · maximalMonomials

maxIndepSet def

def maxIndepSet (G : SimpleGraph α) (v : α) : Finset α · WrittenOnTheWallII.GraphConjecture2.maxIndepSet

menage_denom_term def

The denominator term $k! (n-1)_k$ represented as a Real number. · menage_denom_term

middle_column_bit def

The sequence of bits forming the middle column of the CA pattern, $C_{t, 0}$. · middle_column_bit

minor_matrix def

def minor_matrix (f0 f1 f2 f3 f4 d0 d1 d2 d3 d4 : Fin 11) : Matrix (Fin 5) (Fin 5) (ZMod 5) · OpenQuantumProblem35.minor_matrix

mkEdge def

Helper: build an EdgeN from endpoints and endpoint indices. · MonochromaticQuantumGraph.mkEdge

mkStateVector abbrev

Build a state vector from its computational-basis amplitudes. · OpenQuantumProblem35.mkStateVector

monoAP_guarantee_set def

The set of natural numbers that guarantee a monochromatic arithmetic progression. · Erdos138.monoAP_guarantee_set

monoAPNumber def

The van der Waerden number, is the smallest integer N such that any r-coloring of {1, ..., N} is guaranteed to contain a monochromatic arithmetic progression of length k. It is defined as the infimum of the (non-empty) set of … · Erdos138.monoAPNumber

Monomial abbrev

Monomials in r variables as finitely supported exponent vectors on Fin r. · Monomial

monomialInf def

def monomialInf {r : ℕ} (m1 m2 : Monomial r) : Monomial r · monomialInf

mul def

def Eisen.mul (x y : Eisen) : Eisen · Green57.Eisen.mul

MultiplesOf def

The set of multiples of a sequence $(a_i)$ is $\{na_i | n \in \mathbb{N}, i\}$. · Erdos26.MultiplesOf

mvPolynomial_tensor_equiv_inv def

def mvPolynomial_tensor_equiv_inv {k S : Type*} [CommRing k] [CommRing S] [Algebra k S] (s : Type*) : MvPolynomial s S →ₐ[k] (MvPolynomial s k ⊗[k] S) · mvPolynomial_tensor_equiv_inv

mvPolynomial_tensor_equiv_lift def

def mvPolynomial_tensor_equiv_lift {k S : Type*} [CommRing k] [CommRing S] [Algebra k S] (s : Type*) : (MvPolynomial s k ⊗[k] S) →ₐ[k] MvPolynomial s S · mvPolynomial_tensor_equiv_lift

mXYZ def

The monomial xyz encoded as an exponent vector in 3 variables. · mXYZ

mXZ2 def

The monomial xz^2 encoded as an exponent vector in 3 variables. · mXZ2

my_digits def

def my_digits (fuel b k : ℕ) : List ℕ · my_digits

MyGoodSet def

`MyGoodSet` contains a natural number `n` when some block index `m` places it near `M m`, below a controlled progression cutoff, with `n ≡ 1 (mod K m)` and `n ≡ 0 (mod q m)`. · Erdos12.MyGoodSet

N

N_k_N def

def N_k_N (X : Set ℕ) (k : ℕ) : ℕ · Erdos152.N_k_N

N_k_Z def

def N_k_Z (X : Set ℤ) (k : ℤ) : ℕ · Erdos152.N_k_Z

n_p def

def n_p (p : ℕ) : ℕ · n_p

nat_fac_to_real def

def nat_fac_to_real (n : ℕ) : ℝ · nat_fac_to_real

next_state def

def next_state (s : (ℤ × ℤ) × (ℤ × ℤ)) : (ℤ × ℤ) × (ℤ × ℤ) · next_state

next_state def

def next_state (state : List (List ℕ) × List (List ℕ)) : List (List ℕ) × List (List ℕ) · next_state

next_y def

def next_y (p y : ℕ) : ℕ · next_y

NonTrilinearFor def

We say a subset A of points in the plane is ε-non-trilinear if any subset B of A, contains a non-trilinear subset C of size at least ε|B|. · Erdos846.NonTrilinearFor

NormalDomain class

class NormalDomain (R : Type*) [CommRing R] : Prop extends IsDomain R, IsIntegrallyClosed R · NormalDomain

NormalRing class

class NormalRing (R : Type*) [CommRing R] : Prop · NormalRing

normSq def

def Eisen.normSq (x : Eisen) : ℤ · Green57.Eisen.normSq

num_2_dense_sublists def

Number of maximal contiguous sublists of divisors of n where each adjacent pair (d_k, d_{k+1}) satisfies d_{k+1} <= 2 * d_k. This is 1 + the number of "jumps" where d_{k+1} > 2 * d_k. · num_2_dense_sublists

num_isolated def

def num_isolated (A : Set ℕ) : ℕ · Erdos152.num_isolated

O

oeis_108_index_cond def

The index condition on $(j, k)$ from the conjecture: $0 < \min\{2,k\} \le j \le k$. Since j and k are natural numbers, $0 < \min\{2,k\}$ is equivalent to $1 \le k$. · oeis_108_index_cond

oeis_floor_term def

The floor term in the conjectured recurrence relation for A267581. This term, $\lfloor (1/2)^{(2^{n+1} \bmod n)} \rfloor$, simplifies to 1 if $(2^{n+1} \bmod n) = 0$ (i.e., $n \mid 2^{n+1}$), and 0 otherwise. Since the recurrence is only … · oeis_floor_term

OGF_A_scaled def

The power series $A(x/3) = \sum_{n=0}^\infty \frac{a(n)}{3^n} x^n$ over ℚ. · OGF_A_scaled

omega5 def

def omega5 : ℂ · OpenQuantumProblem35.omega5

op1_dup def

def op1_dup (l : List ℕ) : List ℕ · op1_dup

op1_uniq def

def op1_uniq (l : List ℕ) : List ℕ · op1_uniq

op2 def

def op2 (l : List ℕ) : List ℕ · op2

orbit_safe_ok def

def orbit_safe_ok (d : ℕ) : Bool · orbit_safe_ok

orbit_step_ok def

def orbit_step_ok (d : ℕ) : Bool · orbit_step_ok

OrderIdeal structure

A finite order ideal of monomials, closed downward under divisibility. Divisibility of monomials uses the standard pointwise ≤ on Finsupp. · OrderIdeal

OSeq def

def OSeq (m : Monomial 3) (d : ℕ) : ℕ · OSeq

OSeq_diff def

def OSeq_diff (m1 m2 : Monomial 3) (d : ℕ) : ℕ · OSeq_diff

OSeqZ def

def OSeqZ (m : Monomial 3) (d : ℤ) : ℤ · OSeqZ

P

P def

`P m = K m * q m`, combining the accumulated earlier-prime modulus with the block's new prime. · Erdos12.P

P def

def P (k : ℕ) : Prop · P

P def

def P (n t : ℕ) : ℕ · P

P0 def

def P0 (n : ℝ) : ℝ · P0

P1 def

def P1 (n : ℝ) : ℝ · P1

P2 def

def P2 (n : ℝ) : ℝ · P2

P3 def

def P3 (n : ℝ) : ℝ · P3

P4 def

def P4 (n : ℝ) : ℝ · P4

P5 def

def P5 (n : ℝ) : ℝ · P5

P_lower def

def P_lower (n : ℝ) : ℝ · P_lower

P_mat def

def P_mat (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℤ · P_mat

P_mat4 def

def P_mat4 (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℤ · P_mat4

P_n def

The polynomial $P_n(X, Y, Z) = (1 + X + Y + Z)^{2n} (1 + X + Y - Z)^n (1 + X - Y + Z)^n$. We identify $X_0, X_1, X_2$ with $X, Y, Z$. We mark it noncomputable due to dependencies in the polynomial ring structure. · P_n

P_n_def def

def P_n_def (p : ℕ → ℕ) (n : ℕ) : ℕ · Erdos12.P_n_def

P_poly def

def P_poly (X : PowerSeries ℤ) : PowerSeries ℤ · P_poly

P_poly def

S_real n k is the number of $k$-element subsets of $\{1, 2, \dots, n\}$ whose sum is divisible by $k$. By the roots of unity filter, this exact count can be written as: $S_{n,k} = \frac{1}{k} \sum_{j=0}^{k-1} \sum_{A \in \binom{n}{k}} … · P_poly

P_prod def

def P_prod (n : ℕ) : ℕ · P_prod

P_upper def

def P_upper (n : ℝ) : ℝ · P_upper

period_of_power_mod def

The length of the minimal positive period of the sequence $k^p \pmod n$. $a_p(n) = \min \{ T \in \mathbb{N}^+ \mid \forall k \in \mathbb{N}, (k+T)^p \equiv k^p \pmod n \}$. · period_of_power_mod

permuteConfig def

Permute the parties of a configuration. · OpenQuantumProblem35.permuteConfig

permuteState def

Permute the parties of a state vector. · OpenQuantumProblem35.permuteState

pmSumList def

Perfect-matching sum on a list: run pmSumListAux with fuel = L.length. · MonochromaticQuantumGraph.pmSumList

pmSumListAux def

Auxiliary perfect-matching sum on a vertex list, using a fuel parameter n for termination. · MonochromaticQuantumGraph.pmSumListAux

pmSumN def

The perfect-matching sum for $K_N$: use the canonical ordered vertex list vertices N. · MonochromaticQuantumGraph.pmSumN

pow_mod def

def pow_mod (a b m : ℕ) : ℕ · pow_mod

pow_mod_loop def

def pow_mod_loop (base exp m acc : ℕ) : ℕ · pow_mod_loop

pow_mod_rec def

def pow_mod_rec (base exp m : ℕ) : ℕ · pow_mod_rec

ProblemP1 def

P1 statement: the degree-counting values for the generated order ideal are (1, 3, 4, 2). · ProblemP1

ProblemP2 def

P2 statement, split into a coefficient-level formula plus two sequence consequences. · ProblemP2

ProblemP2CoeffFormula def

P2 (coefficient-level): one-generator degree counts match the product-formula coefficients. · ProblemP2CoeffFormula

ProblemP2Type1LogConcave def

P2 consequence: every type-1 pure O-sequence is log-concave. · ProblemP2Type1LogConcave

ProblemP2Type1Unimodal def

P2 consequence: every type-1 pure O-sequence is unimodal. · ProblemP2Type1Unimodal

ProblemP3 def

P3 statement: in codimension 3, first-half log-concavity up to e / 2. Here e is the socle degree of the pure order ideal. · ProblemP3

ProblemP4 def

P4 statement: codimension 3 and type 2 imply unimodality. · ProblemP4

ProblemP5 def

P5: in codimension 3, every type-2 pure O-sequence is log-concave. · ProblemP5

ProblemP6 def

P6: for fixed r ≥ 5, every type-2 pure O-sequence in codimension r is unimodal. · ProblemP6

ProblemP7 def

P7: threshold existence for eventual log-concavity failure in codimension r. · ProblemP7

ProblemP8 def

P8: least threshold for eventual log-concavity failure in codimension r. · ProblemP8

ProdResidueFields abbrev

abbrev ProdResidueFields (S : Type*) [CommRing S] · ProdResidueFields

pureIdeal_S_t def

def pureIdeal_S_t (t : ℕ) (ht : 5 ≤ t) : PureOrderIdeal 3 · pureIdeal_S_t

PureOrderIdeal structure

A pure order ideal packages an order ideal with purity and a nonempty maximal set. · PureOrderIdeal

pureOrderIdealOfSet def

def pureOrderIdealOfSet {r : ℕ} (S : Finset (Monomial r)) (d : ℕ) (hS : ∀ m ∈ S, totalDeg m = d) (h_nonempty : S.Nonempty) : PureOrderIdeal r · pureOrderIdealOfSet

pureOSequence def

The pure O-sequence: number of monomials of total degree d in an order ideal. · pureOSequence

Q

q def

`q 0 = 5`; each `q (m+1)` is a prime chosen strictly above `q m` but no larger than `2*q m+2`. · Erdos12.q

Q_explicit def

def Q_explicit (n k : ℕ) : ℚ · Q_explicit

quad_fiber def

def quad_fiber (A : Set ℕ) (s k : ℕ) : Set (ℕ × ℕ × ℕ × ℕ) · Erdos152.quad_fiber

quad_k_N def

def quad_k_N (A : Set ℕ) (k : ℕ) : Set (ℕ × ℕ × ℕ × ℕ) · Erdos152.quad_k_N

R

R def

The typecount R(u, t) is the number of neighbors of u in rightV whose type τ equals t. Symmetrically, R'(v, s) is the number of neighbors of v in leftU whose type τ equals s. · R

R' def

def R' (v : V) (s : ℕ × Multiset ℕ) : ℕ · R'

r_const def

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

R_def def

def R_def (n : ℕ) : ℕ · R_def

r_sq def

The constant $r^2$. · r_sq

R_val def

def R_val (n k : ℕ) : ℚ · R_val

r_val def

`r_val m` selects the natural-number representative produced by the Chinese remainder theorem for residue `1` modulo `K m` and residue `0` modulo `q m`. · Erdos12.r_val

rankCondition def

def rankCondition {n : ℕ} (m : ℕ) (hm : m ≤ n) (M : Matrix (Fin n) (Fin n) (ZMod 5)) : Prop · OpenQuantumProblem35.rankCondition

re_double def

def Eisen.re_double (x : Eisen) : ℤ · Green57.Eisen.re_double

real_point def

def real_point (x y : ℝ) : ℝ² · Erdos846.real_point

reduced_monomial def

Given oriented maxima `m₁,m₂` and the exceptional coordinate `x`, `reduced_monomial` lowers the `x` exponent of `m₂` by `m₁(x)+1` and leaves its other exponents unchanged. Its degree is correspondingly reduced by the same shift. · reduced_monomial

reducedDensityFirst def

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

reverse_nat def

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

rightIndex def

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

rightV_types def

def rightV_types {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (rightV : Finset V) : Multiset (ℕ × Multiset ℕ) · rightV_types

root_set def

def root_set (K A : Type*) [Field K] [Field A] [Algebra K A] (S : Set K) (q : ℕ) : Set A · root_set

S

S def

The sum which A175386 $a(n)$ is the denominator of. · S

S def

def S (n : ℕ) : ℕ · S

S_algebra_A def

def S_algebra_A (k k' A L : Type*) [Field k] [Field k'] [CommRing A] [Field L] [Algebra k k'] [Algebra k' A] [Algebra k A] [IsScalarTower k k' A] [Algebra k L] [Algebra k' L] [IsScalarTower k k' L] : … · S_algebra_A

S_algebra_k' def

def S_algebra_k' (k k' A L : Type*) [Field k] [Field k'] [CommRing A] [Field L] [Algebra k k'] [Algebra k' A] [Algebra k A] [IsScalarTower k k' A] [Algebra k L] [Algebra k' L] [IsScalarTower k k' L] … · S_algebra_k'

S_algebra_L def

def S_algebra_L (k k' A L : Type*) [Field k] [Field k'] [CommRing A] [Field L] [Algebra k k'] [Algebra k' A] [Algebra k A] [IsScalarTower k k' A] [Algebra k L] [Algebra k' L] [IsScalarTower k k' L] : … · S_algebra_L

S_C def

`S_C` is the union of every half-open interval `[S_x(k),S_y(k))`. Each interval is locally large, but the starting scales grow so quickly that earlier intervals become negligible at the next lower checkpoint. · Erdos741.S_C

S_good def

def S_good (A : Set ℕ) (k : ℕ) · Erdos152.S_good

S_heavy def

def S_heavy (G : SimpleGraph α) [DecidableRel G.Adj] : Finset α · WrittenOnTheWallII.GraphConjecture2.S_heavy

S_j def

def S_j (j : ℕ) : ℕ · Erdos26.S_j

S_list def

def S_list (n t : ℕ) : List ℕ · S_list

S_mat def

def S_mat (rs : List (Fin 11)) (cs : List (Fin 11)) (i : Fin 5) (j : Fin 6) : ZMod 5 · OpenQuantumProblem35.S_mat

S_multiset def

def S_multiset (G : SimpleGraph V) (rightV : Finset V) (u : V) : Multiset (ℕ × Multiset ℕ) · S_multiset

S_pred_list def

def S_pred_list (l : List ℕ) : Prop · S_pred_list

S_pred_seq def

def S_pred_seq (n : ℕ) (σ : Fin (n + 1) → ℕ) : Prop · S_pred_seq

S_real def

def S_real (n k : ℕ) : ℝ · S_real

S_ring def

def S_ring (k k' A L : Type*) [Field k] [Field k'] [CommRing A] [Field L] [Algebra k k'] [Algebra k' A] [Algebra k A] [IsScalarTower k k' A] [Algebra k L] [Algebra k' L] [IsScalarTower k k' L] : Type … · S_ring

S_set def

def S_set (n : ℕ) : Finset ℕ · S_set

S_sum def

def S_sum (n : ℕ) : ℝ · S_sum

S_t def

def S_t (t : ℕ) : Finset (Monomial 3) · S_t

S_t_minus_1 def

def S_t_minus_1 (t : ℕ) : Finset (Monomial 3) · S_t_minus_1

S_t_minus_2 def

def S_t_minus_2 (t : ℕ) : Finset (Monomial 3) · S_t_minus_2

S_to_base_change def

def S_to_base_change (k k' A L : Type*) [Field k] [Field k'] [CommRing A] [Field L] [Algebra k k'] [Algebra k' A] [Algebra k A] [IsScalarTower k k' A] [Algebra k L] [Algebra k' L] [IsScalarTower k k' … · S_to_base_change

S_val def

def S_val (n : ℕ) : ℤ · S_val

S_x def

`S_x(k)=4^(3^k)` is the rapidly growing left endpoint of the `k`th scale. Base four makes the digit split carry-free, while the double-exponential spacing prevents earlier added intervals from controlling the next density measurement. · Erdos741.S_x

S_y def

`S_y(k)=10*S_x(k)` gives each added interval a fixed nine-scale-unit width. Those fat intervals later force many same-colour sums before the next enormous base-four scale arrives. · Erdos741.S_y

SandorA def

`SandorA` joins the carry-free covering set `B1∪B2` to the sparse union of fat intervals `S_C`. Coverage makes `SandorA+SandorA` all naturals; the intervals make every two-colouring oscillate too much for both monochromatic self-sumsets to … · Erdos741.SandorA

seq_of_g def

def seq_of_g {r : ℕ} (g : Monomial r) : ℕ → ℕ · seq_of_g

seq_of_g_Z def

def seq_of_g_Z {r : ℕ} (g : Monomial r) : ℤ → ℤ · seq_of_g_Z

seq_step def

def seq_step : ℕ → State · Erdos741.seq_step

seq_sum def

def seq_sum (n : ℕ) : ℤ · seq_sum

seq_sum_ratio def

def seq_sum_ratio (n : ℕ) : ℝ · seq_sum_ratio

seq_sum_ratio_term def

def seq_sum_ratio_term (n k : ℕ) : ℝ · seq_sum_ratio_term

seqA def

def seqA (n : ℕ) : ℕ · Erdos26.seqA

seqA_equiv def

def seqA_equiv : ℕ ≃ {y // y ∈ seqA_set} · Erdos26.seqA_equiv

seqA_set def

def seqA_set : Set ℕ · Erdos26.seqA_set

seqA_sigma_equiv def

def seqA_sigma_equiv : (Σ (j : {k // 1 ≤ k}), {x : ℕ // x ∈ A_j j.val}) ≃ {y // y ∈ seqA_set} · Erdos26.seqA_sigma_equiv

seqD def

def seqD (k : ℕ) : ℝ · seqD

seqE def

def seqE (k : ℕ) : ℝ · seqE

seqState def

def seqState (j : ℕ) : Finset ℕ × ℕ × ℕ × ℕ · Erdos26.seqState

seqU def

def seqU : ℕ → ℝ · seqU

seqV def

def seqV : ℕ → ℝ · seqV

set_prod def

The set of all products of elements from a Finset S. · set_prod

setD def

def setD (P : PureOrderIdeal 3) (j : ℕ) : Finset (Monomial 3) · setD

setD_X def

def setD_X (P : PureOrderIdeal 3) (j : ℕ) : Finset ℕ · setD_X

setE def

def setE (P : PureOrderIdeal 3) (j : ℕ) : Finset (Monomial 3) · setE

shifted_h_seq def

`shifted_h_seq(m,c,d)` (Lean: `shifted_h_seq m c d`) is zero below `c` and otherwise reads the divisor-count sequence of `m` at degree `d-c`. · shifted_h_seq

shiftEquiv def

def shiftEquiv {k : ℕ} (j : Fin k) : Equiv (Fin k → Fin 5) (Fin k → Fin 5) · OpenQuantumProblem35.shiftEquiv

sigma def

def sigma (t : ℕ × ℕ × ℕ) : ℕ × ℕ × ℕ · sigma

sign_f def

def sign_f (j : ℕ) : ℤ · sign_f

slice_size def

def slice_size (P : PureOrderIdeal 3) (k : ℕ) (d : ℕ) : ℕ · slice_size

slice_X def

def slice_X (P : PureOrderIdeal 3) (k d : ℕ) : Finset ℕ · slice_X

SmallFieldLift def

def SmallFieldLift (F : Type u_1) · SmallFieldLift

smul def

def Eisen.smul (c : ℤ) (x : Eisen) : Eisen · Green57.Eisen.smul

socleDegree def

Socle degree of a pure order ideal (the common degree of maximal monomials). · socleDegree

sorted_divisors_list def

def sorted_divisors_list (n : ℕ) : List ℕ · sorted_divisors_list

split1 def

`split1(n)` recursively keeps the parity bit of each base-four digit. Its base-four digits are therefore only 0 or 1, which prevents carries when two `B1` elements are added. · Erdos741.split1

split2 def

`split2(n)` keeps `n % 4 - n % 2` at each digit, so its base-four digits are 0 or 2. Digit by digit, `split1(n)+split2(n)=n` without a carry. · Erdos741.split2

sq_mod def

def sq_mod (p x : ℕ) : ℕ → ℕ · sq_mod

sq_mod_iter def

def sq_mod_iter (p y : ℕ) : ℕ → ℕ · sq_mod_iter

star def

def Eisen.star (x : Eisen) : Eisen · Green57.Eisen.star

State structure

structure State · Arxiv.«1905.10899».State

State def

def State · Erdos741.State

state_seq def

def state_seq : ℕ → (ℤ × ℤ) × (ℤ × ℤ) · state_seq

StateVector abbrev

A state vector in the computational basis, viewed as a finite-dimensional Hilbert space. · OpenQuantumProblem35.StateVector

step def

Anchored Simultaneous Gradient Descent z_{t+1} = z_t - α_t * G(z_t) + β_t * (z_0 - z_t) · Arxiv.«1905.10899».step

step_prop def

def step_prop (prev : State) (C : ℕ) (next : State) : Prop · Erdos741.step_prop

sub def

def Eisen.sub (x y : Eisen) : Eisen · Green57.Eisen.sub

submatrix def

def submatrix {n : ℕ} (m : ℕ) (hm : m ≤ n) (M : Matrix (Fin n) (Fin n) (ZMod 5)) (p : Equiv.Perm (Fin n)) : Matrix (Fin m) (Fin (n - m)) (ZMod 5) · OpenQuantumProblem35.submatrix

subset_rank_cond_det_bool def

def subset_rank_cond_det_bool (f0 f1 f2 f3 f4 : Fin 11) : Bool · OpenQuantumProblem35.subset_rank_cond_det_bool

subset_rank_cond_fn def

def subset_rank_cond_fn (M : Matrix (Fin 11) (Fin 11) (ZMod 5)) (f0 f1 f2 f3 f4 : Fin 11) : Prop · OpenQuantumProblem35.subset_rank_cond_fn

sum_abs_coeff def

def sum_abs_coeff (P : Polynomial ℂ) : ℝ · sum_abs_coeff

sum_ap def

def sum_ap (x P L : ℕ) : ℝ · Erdos26.sum_ap

sum_digits def

def sum_digits : List ℕ → ℕ · sum_digits

sum_fact def

def sum_fact : ℕ → ℕ · sum_fact

supportFn def

The support function of a set S with respect to a linear functional a: sup_{φ ∈ S} Re ⟨a, φ⟩. · Green57.supportFn

swap02 def

def swap02 (m : Monomial 3) : Monomial 3 · swap02

swap12 def

def swap12 (m : Monomial 3) : Monomial 3 · swap12

T

T def

def T (N : ℕ) (p : ℕ × ℕ) : ℕ · T

T_multiset def

def T_multiset (G : SimpleGraph V) (rightV : Finset V) (u : V) : Multiset (ℕ × Multiset ℕ) · T_multiset

t_seq def

def t_seq : ℕ → ℝ · Erdos846.t_seq

target_config_list def

def target_config_list (n : ℕ) : List ℕ · target_config_list

target_set def

`target_set m` contains pairs `(k,i)` with `k<m` and `0≤i≤P (k+1)^4/2`. · Erdos12.target_set

TargetF def

def TargetF (n : ℕ) : ℕ → ℕ · TargetF

tensor_baseChange_map def

def tensor_baseChange_map (k R K L : Type*) [Field k] [CommRing R] [Algebra k R] [Field K] [Algebra k K] [Field L] [Algebra k L] [Algebra K L] [IsScalarTower k K L] [Algebra K (R ⊗[k] K)] … · tensor_baseChange_map

tensor_basis def

def tensor_basis {k R S : Type*} [Field k] [CommRing R] [CommRing S] [Algebra k R] [Algebra k S] : Module.Basis (Module.Free.ChooseBasisIndex k S) R (R ⊗[k] S) · tensor_basis

tensor_basis_equiv def

def tensor_basis_equiv {k M k' : Type _} [Field k] [AddCommGroup M] [Module k M] [Field k'] [Algebra k k'] : M ⊗[k] k' ≃ₗ[k] (Module.Basis.ofVectorSpaceIndex k k') →₀ M · tensor_basis_equiv

tensor_basis_K def

def tensor_basis_K {k : Type u} {R S : Type v} [Field k] [CommRing R] [CommRing S] [Algebra k R] [Algebra k S] (P : Ideal R) [P.IsPrime] : Module.Basis (Module.Free.ChooseBasisIndex k S) (FiberRing k … · tensor_basis_K

tensor_equiv_base_change_f def

def tensor_equiv_base_change_f (k_ E_ K_ S_ : Type*) [Field k_] [Field E_] [Field K_] [CommRing S_] [Algebra k_ E_] [Algebra k_ K_] [Algebra k_ S_] [Algebra E_ K_] [IsScalarTower k_ E_ K_] : K_ ⊗[k_] … · tensor_equiv_base_change_f

tensor_equiv_base_change_g def

def tensor_equiv_base_change_g (k_ E_ K_ S_ : Type*) [Field k_] [Field E_] [Field K_] [CommRing S_] [Algebra k_ E_] [Algebra k_ K_] [Algebra k_ S_] [Algebra E_ K_] [IsScalarTower k_ E_ K_] : K_ ⊗[E_] … · tensor_equiv_base_change_g

tensor_eval def

def tensor_eval {k A L : Type*} [Field k] [CommRing A] [Field L] [Algebra k A] [Algebra k L] (f : L →ₗ[k] k) : A ⊗[k] L →ₗ[k] A · tensor_eval

tensor_finsupp_equiv def

def tensor_finsupp_equiv {k ι M : Type _} [Field k] [AddCommGroup M] [Module k M] [DecidableEq ι] : M ⊗[k] (ι →₀ k) ≃ₗ[k] ι →₀ M · tensor_finsupp_equiv

tensorFinsuppEquiv def

def tensorFinsuppEquiv {k K S : Type*} [Field k] [CommRing K] [Algebra k K] [CommRing S] [Algebra k S] : K ⊗[k] S ≃ₗ[k] (Module.Free.ChooseBasisIndex k K →₀ S) · tensorFinsuppEquiv

tensorProduct_isReduced_of_finite_separable_inv def

def tensorProduct_isReduced_of_finite_separable_inv {E K R : Type*} [Field E] [Field K] [CommRing R] [Algebra E K] [Algebra E R] [IsReduced R] [FiniteDimensional E K] (x : K) (hx : … · tensorProduct_isReduced_of_finite_separable_inv

tensorProduct_isReduced_of_finite_separable_inv_K def

def tensorProduct_isReduced_of_finite_separable_inv_K {E K R : Type*} [Field E] [Field K] [CommRing R] [Algebra E K] [Algebra E R] [IsReduced R] [FiniteDimensional E K] (x : K) (hx : … · tensorProduct_isReduced_of_finite_separable_inv_K

tensorProduct_isReduced_of_finite_separable_map def

def tensorProduct_isReduced_of_finite_separable_map {E K R : Type*} [Field E] [Field K] [CommRing R] [Algebra E K] [Algebra E R] [IsReduced R] (x : K) : R[X] ⧸ Ideal.span {Polynomial.map (algebraMap … · tensorProduct_isReduced_of_finite_separable_map

TensorProduct_isReduced_of_primitive_element_aux_equiv_to def

def TensorProduct_isReduced_of_primitive_element_aux_equiv_to {E K R : Type*} [Field E] [Field K] [CommRing R] [Algebra E K] [Algebra E R] (x : K) : R[X] →ₐ[E] K ⊗[E] R · TensorProduct_isReduced_of_primitive_element_aux_equiv_to

term def

def term (t : ℕ × ℕ × ℕ) : ℕ · term

tfae_2_to_3_A_i abbrev

abbrev tfae_2_to_3_A_i (k k' : Type*) [Field k] [Field k'] [Algebra k k'] (R : Type*) [CommRing R] [Algebra k R] (E : FinSepSubext k k') · tfae_2_to_3_A_i

tfae_2_to_3_f abbrev

abbrev tfae_2_to_3_f (k k' : Type*) [Field k] [Field k'] [Algebra k k'] (R : Type*) [CommRing R] [Algebra k R] (E : FinSepSubext k k') : tfae_2_to_3_A_i k k' R E →+* R ⊗[k] k' · tfae_2_to_3_f

to_seq def

def to_seq {n : ℕ} (l : List ℕ) : Fin (n + 1) → ℕ · to_seq

toComplex def

def Eisen.toComplex (e : Eisen) : ℂ · Green57.Eisen.toComplex

toProd def

def toProd : Z_space n m ≃L[ℝ] (E_n n × F_m m) · Arxiv.«1905.10899».toProd

totalDeg def

Total degree of a monomial (sum of all exponents). · totalDeg

tribonacci def

The Tribonacci numbers $T_n$ (A000073). $T_0=0, T_1=0, T_2=1$, and $T_n = T_{n-1} + T_{n-2} + T_{n-3}$ for $n \ge 3$. · tribonacci

trim_trailing_zeros def

def trim_trailing_zeros (l : List ℕ) : List ℕ · trim_trailing_zeros

tripleKernel def

Uniform average over pairs (x₁, x₂) in G × G, with the third variable determined by the relation x₁ + x₂ + x₃ = g. The functions fᵢ are complex-valued. · Green57.tripleKernel

trips def

def trips (m : ℕ) : Finset (ℕ × ℕ × ℕ) · trips

trunc_ps def

def trunc_ps (n : ℕ) (S : PowerSeries ℤ) : PowerSeries ℤ · trunc_ps

typeDrop def

`typeDrop t d` lowers the type's degree coordinate by one using natural-number subtraction and erases one occurrence of `d` from its degree-profile multiset. It models deleting the edge to a vertex of degree `d`. · typeDrop

typePO def

Type of a pure order ideal: the number of maximal monomials. · typePO

typeProfile def

`typeProfile G x` maps the vertex-type invariant `τ G` over every neighbor of `x`. Compared with `degreeProfile`, it remembers both each neighbor's degree and that neighbor's own surrounding degree multiset. · typeProfile

U

u def

def u (k : ℕ) (x : ℝ) : ℝ · u

u_elem def

def u_elem (k k' A L : Type*) [Field k] [Field k'] [CommRing A] [Field L] [Algebra k k'] [Algebra k' A] [Algebra k A] [IsScalarTower k k' A] [Algebra k L] [Algebra k' L] [IsScalarTower k k' L] (y : … · u_elem

U_limit_color def

Given a sequence of two-colourings `C n`, `U_limit_color C U x` chooses colour `0` when the indices assigning `0` to `x` are large in `U`, and otherwise chooses colour `1`. · Erdos138.U_limit_color

u_seq def

def u_seq : ℕ → ℕ · u_seq

U_val def

def U_val (k : ℕ) : ℚ · U_val

Uhat def

def Uhat (f1 : ZMod 3 × ZMod 3 → ℂ) (z k : ZMod 3) : ℂ · Green57.Uhat

uliftRingEquiv def

def uliftRingEquiv {R : Type u} [CommRing R] : R ≃+* ULift.{v, u} R · uliftRingEquiv

uniformCoeff def

The common amplitude of the Bell and GHZ witnesses. · OpenQuantumProblem35.uniformCoeff

UnionBlocks def

def UnionBlocks (B : BlockSeq) : Set ℕ · Erdos741.UnionBlocks

V

V abbrev

Vertices of $K_N$. · MonochromaticQuantumGraph.V

V def

def V (N : ℕ) : Finset (ℕ × ℕ) · V

V def

def V (k : ℕ) : ℕ · V

V_2_N def

def V_2_N (X : Set ℕ) : ℕ · Erdos152.V_2_N

V_2_Z def

def V_2_Z (X : Set ℤ) : ℕ · Erdos152.V_2_Z

valid_bounds def

def valid_bounds (n : ℕ) : Prop · valid_bounds

valid_states def

def valid_states : List ((ℤ × ℤ) × (ℤ × ℤ)) · valid_states

ValidMSeq def

def ValidMSeq (c : ℝ) (p : ℕ → ℕ) (M : ℕ → ℕ) : Prop · Erdos12.ValidMSeq

ValidStep def

def ValidStep (j : ℕ) (K_prev max_prev S_prev : ℕ) (A_curr : Finset ℕ) (K_curr max_curr S_curr : ℕ) : Prop · Erdos26.ValidStep

ValuationGe def

def ValuationGe (m : ℕ) (S : PowerSeries ℤ) : Prop · ValuationGe

Vars abbrev

abbrev Vars · Vars

vertices def

Ordered vertex list $[0, 1, \ldots, N-1]$. · MonochromaticQuantumGraph.vertices

Vhat def

def Vhat (f2 : ZMod 3 × ZMod 3 → ℂ) (z k : ZMod 3) : ℂ · Green57.Vhat

W

W abbrev

An abbreviation for the van der Waerden number for 2 colors, commonly written as W(k). This represents the smallest integer N such that any 2-coloring of {1, ..., N} must contain a monochromatic arithmetic progression of length k. · Erdos138.W

w_root def

def w_root : ℂ · Green57.w_root

WeaklyNonTrilinear def

We say a subset A of points in the plane is weakly non-trilinear if it is a finite union of non-trilinear sets. · Erdos846.WeaklyNonTrilinear

weight_digits def

def weight_digits : List ℕ → ℕ · weight_digits

WeightsN abbrev

Weights on edges. · MonochromaticQuantumGraph.WeightsN

What def

def What (h_circ : ZMod 3 → ℂ) (z k : ZMod 3) : ℂ · Green57.What

What_max def

def What_max (h_circ : ZMod 3 → ℂ) (z : ZMod 3) : ℝ · Green57.What_max

Witness4_d2 def

def Witness4_d2 : WeightsN 4 2 α · MonochromaticQuantumGraph.Witness4_d2

Witness4_d3 def

def Witness4_d3 : WeightsN 4 3 α · MonochromaticQuantumGraph.Witness4_d3

Witness6_d2 def

def Witness6_d2 : WeightsN 6 2 α · MonochromaticQuantumGraph.Witness6_d2

witness_f1 def

def witness_f1 (y z : ZMod 3) : ℂ · Green57.witness_f1

witness_f2 def

def witness_f2 (x z : ZMod 3) : ℂ · Green57.witness_f2

witness_f3 def

def witness_f3 (x y : ZMod 3) : ℂ · Green57.witness_f3

witness_phi def

def witness_phi : ZMod 3 → ℂ · Green57.witness_phi

X

X_int def

def X_int (n k : ℕ) : ℤ · X_int

X_seq def

def X_seq (m : ℕ) : ℕ · Erdos26.X_seq

X_seq def

def X_seq (Y : ℕ → ℤ) : ℕ → ℤ · X_seq

x_seq def

def x_seq (A₁ : Set ℕ) (k : ℕ) : ℝ · Erdos741.x_seq

x_seq def

def x_seq (n : ℕ) : ℝ · x_seq

X_series def

def X_series (Y : PowerSeries ℤ) : PowerSeries ℤ · X_series

x_val def

`x_val m` reduces `r_val m` modulo `P m = K m*q m`. · Erdos12.x_val

xyz_pow_n def

The finsupp corresponding to the monomial $x^n y^n z^n$. This is the map $\lambda i. n$. Since Fin 3 is finite, this function is finitely supported. We mark it noncomputable as it builds a mathematical object defined in terms of finite … · xyz_pow_n

Y

Y def

def Y : ℕ → ℤ · Y

Y_int def

def Y_int (n k : ℕ) : ℤ · Y_int

Y_seq def

def Y_seq (n : ℕ) : ℤ · Y_seq

y_seq def

def y_seq (A₁ : Set ℕ) (k : ℕ) : ℝ · Erdos741.y_seq

Y_series def

def Y_series : PowerSeries ℤ · Y_series

Y_val def

def Y_val (n k : ℕ) : ℚ · Y_val

yz_pow_n def

def yz_pow_n (n : ℕ) : Finsupp Vars ℕ · yz_pow_n

Z

Z_calc def

`Z_calc(A,B,C,d)` (Lean: `Z_calc A B C d`) combines three single-side, three pair-sum, and one triple-sum indicators. Its value is the exact second difference of a three-dimensional monomial box count. · Z_calc

Z_S def

def Z_S (X : Set ℕ) : Set ℤ · Erdos152.Z_S

Z_seq def

def Z_seq : ℕ → ℤ · Z_seq

Z_space abbrev

abbrev Z_space · Arxiv.«1905.10899».Z_space

Other

τ def

The type of x is τ(x) = (deg_G(x), P(x)) · τ

Φ def

The space Φ(G) of "convex combinations" of kernels from baseΦ. · Green57.Φ

Φ' def

The restricted space Φ′(G) of "convex combinations" of kernels from baseΦ'. · Green57.Φ'

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.