For all n,k∈N, Ω∈Type, w:Ω→R, g:N→Ω→ListR→Finn, out:Ω→ListR→R, hist:(Finn→R)→Ω→N→ListR, τ:(Finn→R)→Ω→N, E∈R and R,V∈R, if ∀ω, 0≤w(ω), ∑ωw(ω)=1, ∀y,ω, hist(y,ω,0)=[], ∀y,ω,t, hist(y,ω,t+1)=hist(y,ω,t)++([y(g(t,ω,hist(y,ω,t)))]), ∀y,y′,ω, (∀t, t≤τ(y,ω)⟹hist(y′,ω,t)=hist(y,ω,t))⟹τ(y′,ω)=τ(y,ω), E=∑ωw(ω)⋅τ(⋅↦0,ω), ∑ωw(ω)⋅out(ω,hist(⋅↦0,ω,τ(⋅↦0,ω)))=0, ∑ωw(ω)⋅(out(ω,hist(⋅↦0,ω,τ(⋅↦0,ω)))−0)2≤V, ∀S∈powersetCard(k+1,univ), ∑ωw(ω)⋅out(ω,hist(j↦{R0if j∈Sotherwise,ω,τ(j↦{R0if j∈Sotherwise,ω)))=k+1⋅eR+(n−(k+1))k+1⋅eR, ∀S∈powersetCard(k+1,univ), ∑ωw(ω)⋅(out(ω,hist(j↦{R0if j∈Sotherwise,ω,τ(j↦{R0if j∈Sotherwise,ω)))−k+1⋅eR+(n−(k+1))k+1⋅eR)2≤V, k+1≤n, 0<V, 0≤R, n−(k+1)≤k+1⋅eR and k+1⋅(1+eR)≤2n (given FintypeΩ), then
min(21,64V1)⋅(21+eR)≤EWhat the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - x ∈ TVariables
- n, k range over natural numbers: the statement must hold for every choice. (
(n k : ℕ)) - Type
- Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Type) - Fintype
- Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fintype) - f(x)Function application
- Fintype applied to Ω. Lean writes f x; papers write f(x). (
Fintype Ω) - ⟹Implies
- If Ω, then ℝ. (Between types, A → B is the type of functions from A to B.) (
Ω → ℝ) - ∀For all
- The statement after the comma holds for every ω. (
∀ ω, 0 ≤ w ω) - ∑Summation
- Add up w(ω) for every ω. (
∑ ω, w ω) - =Equality
- ∑ ω, w(ω) and 1 are the same. (
∑ ω, w ω = 1) - <Less than
- 0 is strictly smaller than V. (
0 < V) - minMinimum
- The smaller of 1/2 and 1/(64 · V). (
min (1 / 2) (1 / (64 * V))) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - ≤At most
- 0 is less than or equal to w(ω). (
0 ≤ w ω) - powersetCard
- Finset.powersetCard: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Finset.powersetCard) - List
- List: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
List) - ·Multiplication
- w(ω) times τ(_ ↦ 0, ω). (
w ω * (τ (fun _ => 0) ω : ℝ)) - aᵇPower
- out(ω, hist(_ ↦ 0, ω, τ(_ ↦ 0, ω))) − 0 raised to the power 2. (
(out ω (hist (fun _ => 0) ω (τ (fun _ =…) - -Subtraction
- out(ω, hist(_ ↦ 0, ω, τ(_ ↦ 0, ω))) minus 0. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
out ω (hist (fun _ => 0) ω (τ (fun _ =>…) - (x : T)As real numbers
- τ(_ ↦ 0, ω) read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(τ (fun _ => 0) ω : ℝ)) - Fin
- Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fin) - +Addition
- t plus 1. (
t + 1) - x ↦ f(x)Function (λ-abstraction)
- The function sending _ to 0. Lean writes fun x => …; papers write x ↦ …. (
fun _ => 0) - [a, b]List
- The list of , in order. (
[]) - (x : T)Type ascription
- univ read as a Finset(Fin(n)). Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(Finset.univ : Finset (Fin n))) - univ
- Finset.univ: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Finset.univ) - { a if c; b otherwiseCases (if … then … else)
- R when j ∈ S, and 0 otherwise. (
if j ∈ S then R else 0) - ∈Element of
- j is a member of S. (
j ∈ S) - a/bDivision
- (k + 1) · exp(R) divided by (k + 1) · exp(R) + (n − (k + 1)). In Lean, dividing by 0 gives 0. (
((k + 1 : ℝ) * Real.exp R) / ((k + 1 : …) - eˣExponential function
- e raised to the power R, where e ≈ 2.718. (
Real.exp R)