CoClassdef
The complement class co(C) of a complexity class C on languages over alphabet α consists of all languages L whose complement is in C.
def CoClass {α : Type*} (C : Language α → Prop) : Language α → Prop
Verified in Lean 4
Knowledgebase
115 declarations — 82 theorems and 33 definitions in 18 topics — each elaborated by Lean 4 against Mathlib, with nothing outside the trusted axioms. Open one for its proof, what it builds on and what builds on it.
115 declarations
Theoretical Computer Science
83The mathematics of computation: what can be computed, at what cost, and with what guarantees. Machine models, complexity classes, algorithm analysis, and the lower-bound techniques that go with them.
Complexity Classes & Machine Models
17 of 30 targetedco_class_involutivetheorem
The complement operation on complexity classes is an involution: a language L is in co(co(C)) if and only if L is in C.
theorem co_class_involutive {α : Type*} (C : Language α → Prop) (L : Language α) : CoClass (CoClass C) L ↔ C L
A complexity class C is closed under complement if and only if C equals its complement class co(C).
theorem class_closed_under_compl_iff_eq_co {α : Type*} (C : Language α → Prop) : (∀ L, C L → C Lᶜ) ↔ (∀ L, C L ↔ CoClass C L)
co_class_monotonetheoremoriginal
If a complexity class C₁ is contained in a complexity class C₂, then co(C₁) is contained in co(C₂).
theorem co_class_monotone {α : Type*} (C₁ C₂ : Language α → Prop) (h : ∀ L, C₁ L → C₂ L) (L : Language α) (hL : CoClass C₁ L) : CoClass C₂ L
decider_class_eq_cotheorem
Any complexity class defined by a family of deciders that is closed under negation equals its complement class.
theorem decider_class_eq_co {α : Type*} (D : (List α → Bool) → Prop) (hD : ∀ f, D f → D (fun w => !f w)) : ∀ L : Language α, (∃ f, D f ∧ ∀ w, w ∈ L ↔ f w = true) ↔ CoClass (fun L' : Language α => ∃ f, D f ∧ ∀ w, w ∈ L' ↔ f w = true) L
class_eq_co_iff_subset_cotheorem
A complexity class equals its complement class if and only if it is contained in its complement class.
theorem class_eq_co_iff_subset_co {α : Type*} (C : Language α → Prop) : (∀ L, C L ↔ CoClass C L) ↔ (∀ L, C L → CoClass C L)
If a complexity class equals its complement class and is contained in a second class, then it is contained in the intersection of that second class with the second class's complement class.
theorem class_subset_inter_co_of_eq_co {α : Type*} (C₁ C₂ : Language α → Prop) (h₁ : ∀ L, C₁ L ↔ CoClass C₁ L) (h₂ : ∀ L, C₁ L → C₂ L) : ∀ L, C₁ L → C₂ L ∧ CoClass C₂ L
class_eq_co_of_class_eqtheorem
If two complexity classes are equal and the first equals its complement class, then the second equals its complement class too.
theorem class_eq_co_of_class_eq {α : Type*} (C₁ C₂ : Language α → Prop) (h₁ : ∀ L, C₁ L ↔ CoClass C₁ L) (h₂ : ∀ L, C₁ L ↔ C₂ L) : ∀ L, C₂ L ↔ CoClass C₂ L
TimeBoundeddef
A language L over an alphabet Γ is decidable in time T (T : ℕ → ℕ) if there is a total decider f : List Γ → Bool together with a Turing machine M computing f, such that M runs for at most T n steps on every input of length n, and f agrees with the characteristic function of L: for every word w, w ∈ L iff f w = true.
def TimeBounded (Γ : Type) (T : ℕ → ℕ) (L : Language Γ) : Prop
The class P over alphabet Γ consists of all languages L for which there is a polynomial p : Polynomial ℕ such that L is decidable in time n ↦ p.eval n, i.e. by a Turing machine whose running time on inputs of length n is bounded by p(n).
def PolyTimeBounded (Γ : Type) (L : Language Γ) : Prop
The class EXP over alphabet Γ consists of all languages L for which there is a polynomial p such that L is decidable in time n ↦ 2 ^ (p.eval n), i.e. by a Turing machine whose running time on inputs of length n is bounded by 2^(p(n)).
def ExpTimeBounded (Γ : Type) (L : Language Γ) : Prop
pairEncodedeforiginal
For words w and c over an alphabet Γ, pairEncode w c is the word over Γ ⊕ Unit obtained by writing w, then the single separator symbol Sum.inr (), then c, each of the three parts written with Sum.inl.
def pairEncode {Γ : Type} (w c : List Γ) : List (Γ ⊕ Unit)
A language L over Γ is in NP in verifier form if there are a polynomial p and a language V of words over Γ ⊕ Unit such that V is decidable in time n ↦ p.eval n and, for every word w, w ∈ L holds if and only if there exists a certificate word c over Γ with c.length ≤ p (w.length) and pairEncode w c ∈ V.
def NondeterministicPolyTimeBounded (Γ : Type) (L : Language Γ) : Prop
time_bounded_eq_co_of_decider_negation_closedtheoremoriginal
Let T be a time bound and suppose the family of deciders computable within T steps is closed under Boolean negation, i.e. for every f : List Γ → Bool computed in time T there is g computed in time T with g w = !f w. Then the time-bounded class C = TimeBounded Γ T equals its complement class CoClass C: for every language L, L is decidable in time T if and only if its complement is.
theorem time_bounded_eq_co_of_decider_negation_closed {Γ : Type} {T : ℕ → ℕ} (hD : ∀ f : List Γ → Bool, (∃ M : Turing.TM2ComputableInTime (id : List Γ → List Γ) Computability.encodeBool f, ∀ n, M.time n ≤ T n) → ∃ M : Turing.TM2ComputableInTime (id : List Γ → List Γ) Computability.encodeBool (fun w => !f w), ∀ n, M.time n ≤ T n) : ∀ L : Language Γ, TimeBounded Γ T L ↔ CoClass (TimeBounded Γ T) L
time_bounded_monotheorem
If T and T' are time bounds with T n ≤ T' n for every n, then every language decidable in time T is decidable in time T'.
theorem time_bounded_mono {Γ : Type} {T T' : ℕ → ℕ} (h : ∀ n, T n ≤ T' n) {L : Language Γ} (hL : TimeBounded Γ T L) : TimeBounded Γ T' L
poly_time_subset_exp_timetheorem
Every language in P is in EXP: if L is decidable in time p(n) for a polynomial p, then L is decidable in time 2^(p(n)).
theorem poly_time_subset_exp_time {Γ : Type} {L : Language Γ} (h : PolyTimeBounded Γ L) : ExpTimeBounded Γ L
pair_encode_injectivetheorem
The pair encoding is injective: if pairEncode w₁ c₁ = pairEncode w₂ c₂ then w₁ = w₂ and c₁ = c₂.
theorem pair_encode_injective {Γ : Type} {w₁ c₁ w₂ c₂ : List Γ} (h : pairEncode w₁ c₁ = pairEncode w₂ c₂) : w₁ = w₂ ∧ c₁ = c₂
Computability & Recursion Theory
12 of 30 targetedRECompletedef
A predicate `p` is RE-complete if it is recursively enumerable and every recursively enumerable predicate many-one reduces to `p`.
def REComplete {α : Type*} [Primcodable α] (p : α → Prop) : Prop
If a predicate is recursively enumerable but undecidable, then its complement is not recursively enumerable (Post's theorem).
theorem not_re_compl_of_re_and_not_computable {α : Type*} [Primcodable α] {p : α → Prop} (hre : REPred p) (hnc : ¬ComputablePred p) : ¬REPred (fun a => ¬p a)
self_halting_problem_retheorem
The diagonal halting problem, consisting of codes c such that c halts on its own code, is recursively enumerable.
theorem self_halting_problem_re : REPred (fun c : Nat.Partrec.Code => (Nat.Partrec.Code.eval c (Encodable.encode c)).Dom)
The diagonal halting problem is not computable.
theorem self_halting_problem_undecidable : ¬ComputablePred (fun c : Nat.Partrec.Code => (Nat.Partrec.Code.eval c (Encodable.encode c)).Dom)
re_pred_ortheorem
If p and q are recursively enumerable predicates, then their disjunction fun a => p a ∨ q a is recursively enumerable.
theorem re_pred_or {α : Type*} [Primcodable α] {p q : α → Prop} (hp : REPred p) (hq : REPred q) : REPred (fun a => p a ∨ q a)
self_halting_compl_not_retheorem
The complement of the diagonal halting problem is not recursively enumerable.
theorem self_halting_compl_not_re : ¬REPred (fun c : Nat.Partrec.Code => ¬(Nat.Partrec.Code.eval c (Encodable.encode c)).Dom)
re_complete_of_letheorem
If p is RE-complete, q is recursively enumerable, and p many-one reduces to q, then q is RE-complete.
universe u in theorem re_complete_of_le {α β : Type*} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} (hp : REComplete.{_, u} p) (hq : REPred q) (h : p ≤₀ q) : REComplete.{_, u} q
If `p` is many-one reducible to `q` and `p` is undecidable (not computable), then `q` is undecidable.
theorem not_computable_of_manyOneReducible {α β : Type*} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} (h₁ : p ≤₀ q) (h₂ : ¬ComputablePred p) : ¬ComputablePred q
re_of_manyOneReducibletheorem
If `p` is many-one reducible to `q` and `q` is recursively enumerable, then `p` is recursively enumerable.
theorem re_of_manyOneReducible {α β : Type*} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} (h₁ : p ≤₀ q) (h₂ : REPred q) : REPred p
re_pred_andtheorem
If p and q are recursively enumerable predicates, then their conjunction fun a => p a ∧ q a is recursively enumerable.
theorem re_pred_and {α : Type*} [Primcodable α] {p q : α → Prop} (hp : REPred p) (hq : REPred q) : REPred (fun a => p a ∧ q a)
manyOneReducible_compltheorem
If a predicate p many-one reduces to q, then the complement of p many-one reduces to the complement of q.
theorem manyOneReducible_compl {α β : Type*} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} (h : p ≤₀ q) : (fun a => ¬p a) ≤₀ (fun b => ¬q b)
If p is many-one reducible to q and p is not recursively enumerable, then q is not recursively enumerable.
theorem not_re_of_manyOneReducible_and_not_re {α β : Type*} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} (h : p ≤₀ q) (hp : ¬REPred p) : ¬REPred q
Algorithm Design & Analysis
10 of 30 targetedThe number of leaves of any binary tree is at most 2 raised to its height.
theorem binary_tree_num_leaves_le_pow_height {α : Type*} (t : BinaryTree α) : t.numLeaves ≤ 2 ^ t.height
If a binary decision tree has at least n! leaves, then 2^(height) >= n!, establishing the comparison sorting lower bound.
theorem comparison_sort_decision_tree_height_ge {α : Type*} (t : BinaryTree α) (n : ℕ) (h : n.factorial ≤ t.numLeaves) : n.factorial ≤ 2 ^ t.height
For any real branching factor a, base value d and step cost c, the recurrence T(k+1) = a*T(k) + c*a^(k+1) has exact solution T(k) = d*a^k + c*k*a^k.
theorem divide_and_conquer_equal_roots_recurrence
(T : ℕ → ℝ) (a c d : ℝ)
(h0 : T 0 = d)
(hrec : ∀ k : ℕ, T (k + 1) = a * T k + c * a ^ (k + 1)) :
∀ k : ℕ, T k = d * a ^ k + c * (k : ℝ) * a ^ kThe mergesort recurrence T(k+1) = 2*T(k) + c*2^(k+1) with base cost T(0) = d has exact solution T(k) = d*2^k + c*k*2^k.
theorem divide_and_conquer_mergesort_recurrence
(T : ℕ → ℝ) (c d : ℝ)
(h0 : T 0 = d)
(hrec : ∀ k : ℕ, T (k + 1) = 2 * T k + c * 2 ^ (k + 1)) :
∀ k : ℕ, T k = d * 2 ^ k + c * (k : ℝ) * 2 ^ kFor any branching factor a and cost function g, the divide-and-conquer recurrence T(k+1) = a*T(k) + g(k+1) has exact solution T(k) = a^k * T(0) + sum_{j=1}^k a^(k-j) * g(j).
theorem divide_and_conquer_recursion_tree (T : ℕ → ℝ) (g : ℕ → ℝ) (a : ℝ) (hrec : ∀ k : ℕ, T (k + 1) = a * T k + g (k + 1)) : ∀ k : ℕ, T k = a ^ k * T 0 + Finset.sum (Finset.Icc 1 k) (fun j => a ^ (k - j) * g j)
For real branching factor a and cost ratio r with a != r, base value d and cost scale c, the recurrence T(k+1) = a*T(k) + c*r^(k+1) with T(0) = d has exact solution T(k) = d*a^k + c*r*(a^k - r^k)/(a - r).
theorem divide_and_conquer_unequal_roots_recurrence
(T : ℕ → ℝ) (a r c d : ℝ) (har : a ≠ r)
(h0 : T 0 = d)
(hrec : ∀ k : ℕ, T (k + 1) = a * T k + c * r ^ (k + 1)) :
∀ k : ℕ, T k = d * a ^ k + c * r * ((a ^ k - r ^ k) / (a - r))Let a ≥ 0, b > 1 and c ≥ 0 be real numbers, d a natural number, and T : ℕ → ℝ a sequence with T(0) ≥ 0 satisfying the master recurrence at problem size n = b^k, namely T(k+1) = a·T(k) + c·b^{d(k+1)}. If a < b^d (the driving term c·n^d dominates), then for every k ≥ 1 the value T(k) is Θ(n^d) with n = b^k, in the explicit two-sided form c·(b^d)^k ≤ T(k) ≤ (T(0) + c·b^d/(b^d − a))·(b^d)^k.
theorem master_theorem_polynomial_case_one (T : ℕ → ℝ) (a b c : ℝ) (d : ℕ)
(hrec : ∀ k : ℕ, T (k + 1) = a * T k + c * b ^ (d * (k + 1)))
(hT0 : 0 ≤ T 0) (ha : 0 ≤ a) (hb : 1 < b) (hc : 0 ≤ c) (hlt : a < b ^ d) :
∀ k : ℕ, 1 ≤ k →
c * (b ^ d) ^ k ≤ T k ∧ T k ≤ (T 0 + c * b ^ d / (b ^ d - a)) * (b ^ d) ^ kLet a ≥ 0, b > 1 and c ≥ 0 be real numbers, d a natural number, and T : ℕ → ℝ a sequence with T(0) ≥ 0 satisfying the master recurrence at problem size n = b^k, namely T(k+1) = a·T(k) + c·b^{d(k+1)}. If b^d < a (the branching term dominates), then for every k ≥ 1 the value T(k) is Θ(n^{log_b a}) with n = b^k, in the explicit two-sided form (c·b^d/a)·a^k ≤ T(k) ≤ (T(0) + c·b^d/(a − b^d))·a^k.
theorem master_theorem_polynomial_case_three (T : ℕ → ℝ) (a b c : ℝ) (d : ℕ)
(hrec : ∀ k : ℕ, T (k + 1) = a * T k + c * b ^ (d * (k + 1)))
(hT0 : 0 ≤ T 0) (ha : 0 ≤ a) (hb : 1 < b) (hc : 0 ≤ c) (hgt : b ^ d < a) :
∀ k : ℕ, 1 ≤ k →
c * b ^ d / a * a ^ k ≤ T k ∧ T k ≤ (T 0 + c * b ^ d / (a - b ^ d)) * a ^ kfactorial_ge_half_pow_halftheorem
For every natural number n, (n/2)^{⌊n/2⌋} ≤ n!, where the base n/2 is the real number n/2 and the exponent ⌊n/2⌋ is the natural number n/2. Equivalently n! ≥ (n/2)^{n/2}.
theorem factorial_ge_half_pow_half (n : ℕ) :
((n : ℝ) / 2) ^ (n / 2) ≤ (n.factorial : ℝ)For every type α, every binary tree t over α, and every natural number n, if n! ≤ t.numLeaves and 2 ≤ n, then (n/2)·log₂(n/2) ≤ t.height. The label type is arbitrary and the statement is purely combinatorial; the comparison-sort lower bound follows as a corollary but is not itself part of the Lean declaration.
theorem comparison_sort_height_ge_half_n_logb_half_n {α : Type*} (t : BinaryTree α) (n : ℕ) (h : n.factorial ≤ t.numLeaves) (hn : 2 ≤ n) : (n : ℝ) / 2 * Real.logb 2 ((n : ℝ) / 2) ≤ (t.height : ℝ)
NP-Completeness & Reductions
10 of 30 targetedCnfLitinductive
A CNF literal over a variable type V is either a positive variable or a negated variable.
inductive CnfLit (V : Type*)
A CNF formula (a list of clauses, each a list of literals) is satisfiable if there is a truth assignment such that every clause contains at least one true literal.
def CnfSatisfiable {V : Type*} (f : List (List (CnfLit V))) : Prop
cnf_empty_satisfiabletheorem
The empty CNF formula has no clauses to satisfy, hence is satisfiable under any truth assignment.
theorem cnf_empty_satisfiable (V : Type*) : CnfSatisfiable (V := V) []
cnf_satisfiable_subsettheorem
If every clause of a CNF formula `f1` is contained in a CNF formula `f2` (that is, `f1 ⊆ f2`), and `f2` is satisfiable (`CnfSatisfiable f2`), then `f1` is also satisfiable (`CnfSatisfiable f1`).
theorem cnf_satisfiable_subset {V : Type*} {f1 f2 : List (List (CnfLit V))} (hsub : f1 ⊆ f2) (hsat : CnfSatisfiable f2) : CnfSatisfiable f1
A CNF formula consisting of a single clause `c`, namely `[c]`, is satisfiable (`CnfSatisfiable [c]`) if and only if the clause `c` is non-empty (`c ≠ []`).
theorem cnf_single_clause_satisfiable_iff {V : Type*} (c : List (CnfLit V)) : CnfSatisfiable [c] ↔ c ≠ []
cnf_resolution_soundnesstheorem
Soundness of the resolution rule: for any truth assignment `τ : V → Bool`, variable `v : V`, and clauses `C, D : List (CnfLit V)`, if there exists a literal in `C ++ [CnfLit.pos v]` satisfied by `τ` (that is, `match l with | CnfLit.pos u => τ u = true | CnfLit.neg u => τ u = false`) and a literal in `D ++ [CnfLit.neg v]` satisfied by `τ`, then there exists a literal in `C ++ D` satisfied by `τ`.
theorem cnf_resolution_soundness {V : Type*} (τ : V → Bool) (v : V) (C D : List (CnfLit V)) (hC : ∃ l ∈ C ++ [CnfLit.pos v], match l with | CnfLit.pos u => τ u = true | CnfLit.neg u => τ u = false) (hD : ∃ l ∈ D ++ [CnfLit.neg v], match l with | CnfLit.pos u => τ u = true | CnfLit.neg u => τ u = false) : ∃ l ∈ C ++ D, match l with | CnfLit.pos u => τ u = true | CnfLit.neg u => τ u = false
cnf_satisfiable_of_appendtheorem
If the concatenation `f1 ++ f2` of two CNF formulas is satisfiable (`CnfSatisfiable (f1 ++ f2)`), then both `f1` and `f2` are satisfiable (`CnfSatisfiable f1 ∧ CnfSatisfiable f2`).
theorem cnf_satisfiable_of_append {V : Type*} {f1 f2 : List (List (CnfLit V))} (h : CnfSatisfiable (f1 ++ f2)) : CnfSatisfiable f1 ∧ CnfSatisfiable f2
A language L over an alphabet Γ Karp-reduces (polynomial-time many-one reduces) to a language L' over an alphabet Γ' if there is a function f from words over Γ to words over Γ' that is computed by a multi-tape Turing machine in polynomial time in the length of the input word, and such that for every word w over Γ, w ∈ L if and only if f w ∈ L'.
def KarpReducible (Γ Γ' : Type) (L : Language Γ) (L' : Language Γ') : Prop
NPHarddef
A language L over an alphabet Γ is NP-hard if every language L' that is in NP Karp-reduces to L, the languages L' ranging over all alphabets Γ'.
def NPHard {Γ : Type} (L : Language Γ) : Prop
Let f be a CNF formula over a variable type V and g a CNF formula over a variable type W. Replace every literal of f by the literal of the same sign whose variable is Sum.inl of the old variable, and every literal of g by the literal of the same sign whose variable is Sum.inr of the old variable, and concatenate the clause lists. The resulting formula over the disjoint union V ⊕ W is satisfiable if and only if f is satisfiable over V and g is satisfiable over W.
theorem cnf_satisfiable_append_sum_iff {V W : Type*} (f : List (List (CnfLit V))) (g : List (List (CnfLit W))) : CnfSatisfiable (f.map (List.map (fun l : CnfLit V => match l with | CnfLit.pos v => CnfLit.pos (Sum.inl v) | CnfLit.neg v => CnfLit.neg (Sum.inl v))) ++ g.map (List.map (fun l : CnfLit W => match l with | CnfLit.pos v => CnfLit.pos (Sum.inr v) | CnfLit.neg v => CnfLit.neg (Sum.inr v)))) ↔ CnfSatisfiable f ∧ CnfSatisfiable g
Combinatorics for TCS
10 of 25 targetedIsSunflowerdef
A finite family F of finite sets is a sunflower (a delta-system) with kernel C if every member of F contains C and any two distinct members of F have intersection exactly C.
def IsSunflower {α : Type*} [DecidableEq α] (F : Finset (Finset α)) (C : Finset α) : Prop
Sauer-Shelah lemma: let α be a finite set with n elements and let A be a finite family of subsets of α. If the VC-dimension of A, that is the largest size of a set s such that every subset of s occurs as s ∩ u for some u ∈ A, is at most d, then A has at most ∑_{k=0}^{d} binom(n,k) members.
theorem sauer_shelah_card_le_sum_choose {α : Type*} [Fintype α] [DecidableEq α] (𝒜 : Finset (Finset α)) (d : ℕ) (h : 𝒜.vcDim ≤ d) : 𝒜.card ≤ ∑ k ∈ Finset.Iic d, (Fintype.card α).choose k
exists_notMem_of_sum_card_lttheorem
First moment method (counting form of the union bound): let S be a finite set and let B be a finite family of finite sets. If the sum of the cardinalities of the members of B is strictly less than the cardinality of S, then there is an element of S that belongs to no member of B.
theorem exists_notMem_of_sum_card_lt {α : Type*} [DecidableEq α] (S : Finset α) (B : Finset (Finset α)) (h : ∑ b ∈ B, b.card < S.card) : ∃ ω ∈ S, ∀ b ∈ B, ω ∉ b
A finite family F of finite sets is a sunflower with empty kernel if and only if its members are pairwise disjoint.
theorem isSunflower_empty_core_iff_pairwise_disjoint {α : Type*} [DecidableEq α] (F : Finset (Finset α)) : IsSunflower F ∅ ↔ ∀ A ∈ F, ∀ B ∈ F, A ≠ B → Disjoint A B
Property B (Erdős). Let α be a finite set, let k ≥ 1, and let F be a finite family of subsets of α, each of cardinality at least k. If 2·|F| < 2^k, then there is a Boolean colouring c : α → Bool under which no member of F is monochromatic, that is, for every A ∈ F it is not the case that every element of A has c = true, nor that every element of A has c = false.
theorem exists_two_coloring_of_card_mul_two_lt_two_pow {α : Type*} [Fintype α] [DecidableEq α] {k : ℕ} (hk : 1 ≤ k) (F : Finset (Finset α)) (hsize : ∀ A ∈ F, k ≤ A.card) (hcard : F.card * 2 < 2 ^ k) : ∃ c : α → Bool, ∀ A ∈ F, ¬ (∀ a ∈ A, c a = true) ∧ ¬ (∀ a ∈ A, c a = false)
There is a finite family F of six 2-element subsets of a 6-element ground set (namely the six edges of two disjoint triangles) such that no 3-element subfamily of F is a sunflower with any kernel: for every G ⊆ F with |G| = 3 and every set C, G is not a sunflower with kernel C. Since |F| = 6 > 2!·2 = 4, this shows that the folklore threshold k!·s is not a valid bound in the sunflower lemma; the threshold must grow as k!·s^k.
theorem exists_family_card_six_no_three_petal_sunflower :
∃ F : Finset (Finset (Fin 6)), (∀ A ∈ F, A.card = 2) ∧ F.card = 6 ∧
(∀ G ⊆ F, G.card = 3 → ∀ C, ¬ IsSunflower G C)card_simpleGraphtheorem
The number of simple graphs on a finite vertex set V is 2^{C(|V|,2)}, where C(|V|,2) = |V|(|V|-1)/2 is the number of unordered pairs of distinct vertices.
theorem card_simpleGraph {V : Type*} [Fintype V] [DecidableEq V] : Fintype.card (SimpleGraph V) = 2 ^ (Fintype.card V).choose 2
sauer_shelah_card_le_mul_powtheoremoriginal
Polynomial form of the Sauer–Shelah lemma. Let 𝒜 be a finite family of subsets of a finite set α with n = |α| ≥ 1. If the VC-dimension of 𝒜 is at most d, then |𝒜| ≤ (d + 1)·n^d.
theorem sauer_shelah_card_le_mul_pow {α : Type*} [Fintype α] [DecidableEq α] (𝒜 : Finset (Finset α)) (d : ℕ) (hn : 1 ≤ Fintype.card α) (h : 𝒜.vcDim ≤ d) : 𝒜.card ≤ (d + 1) * (Fintype.card α) ^ d
isSunflower_core_uniquetheorem
If a finite family F of finite sets has at least two members and is a sunflower with kernel C and also a sunflower with kernel C', then C = C'.
theorem isSunflower_core_unique {α : Type*} [DecidableEq α] {F : Finset (Finset α)} {C C' : Finset α} (h : IsSunflower F C) (h' : IsSunflower F C') (hF : 2 ≤ F.card) : C = C'
isSunflower_monotheorem
A subfamily of a sunflower is again a sunflower with the same kernel: if G ⊆ F and F is a sunflower with kernel C, then every member of G contains C and any two distinct members of G intersect in exactly C, so G is a sunflower with kernel C.
theorem isSunflower_mono {α : Type*} [DecidableEq α] {F G : Finset (Finset α)} {C : Finset α} (hGF : G ⊆ F) (h : IsSunflower F C) : IsSunflower G C
Automata & Formal Languages
9 of 30 targetedis_regular_zerotheorem
The empty language is regular.
theorem is_regular_zero {α : Type*} : (0 : Language α).IsRegular
is_regular_difftheorem
The difference L1 \\ L2 of two regular languages is regular.
theorem is_regular_diff {α : Type*} {L1 L2 : Language α} (h1 : L1.IsRegular) (h2 : L2.IsRegular) : (L1 \ L2).IsRegular
is_regular_left_quotienttheorem
For any word w and regular language L, the left quotient L / w = { u | w ++ u ∈ L } is regular.
theorem is_regular_left_quotient {α : Type*} {L : Language α} (h : L.IsRegular) (w : List α) : (L.leftQuotient w).IsRegular
is_regular_iff_nfatheorem
A language is regular if and only if it is accepted by a nondeterministic finite automaton with finitely many states.
theorem is_regular_iff_nfa {α : Type*} {L : Language α} : L.IsRegular ↔ ∃ (σ : Type) (_ : Fintype σ) (M : NFA α σ), M.accepts = L
is_regular_iff_enfatheorem
A language is regular if and only if it is accepted by an epsilon-nondeterministic finite automaton with finitely many states.
theorem is_regular_iff_enfa {α : Type*} {L : Language α} : L.IsRegular ↔ ∃ (σ : Type) (_ : Fintype σ) (M : εNFA α σ), M.accepts = L
is_regular_symm_difftheorem
The symmetric difference of two regular languages is regular.
theorem is_regular_symm_diff {α : Type*} {L1 L2 : Language α} (h1 : L1.IsRegular) (h2 : L2.IsRegular) : (symmDiff L1 L2).IsRegular
nfa_accepts_is_regulartheorem
The language accepted by any finite-state nondeterministic finite automaton is regular.
theorem nfa_accepts_is_regular {α : Type*} {σ : Type*} [Fintype σ] (M : NFA α σ) : M.accepts.IsRegular
is_regular_kstartheorem
The Kleene star of any regular language is regular.
theorem is_regular_kstar {α : Type*} {L : Language α} (h : L.IsRegular) : (KStar.kstar L).IsRegular
is_regular_multheorem
The concatenation of two regular languages is regular.
theorem is_regular_mul {α : Type*} {L1 L2 : Language α} (h1 : L1.IsRegular) (h2 : L2.IsRegular) : (L1 * L2).IsRegular
Graph Theory & Graph Algorithms
7 of 30 targetedThe matching number of a graph G is the supremum of the cardinalities of the edge sets of all matchings in G.
noncomputable def graph_matching_num {V : Type*} (G : SimpleGraph V) : ℕ∞
For any matching M and any vertex cover c of a simple graph G, the number of edges in M is at most the number of vertices in c.
theorem graph_matching_encard_le_vertex_cover_encard {V : Type*} (G : SimpleGraph V) (M : SimpleGraph.Subgraph G) (c : Set V) (hM : M.IsMatching) (hc : G.IsVertexCover c) : M.edgeSet.encard ≤ c.encard
In any simple graph G, the matching number is at most the vertex cover number.
theorem graph_matching_num_le_vertex_cover_num {V : Type*} (G : SimpleGraph V) : graph_matching_num G ≤ G.vertexCoverNum
graph_matching_num_bottheorem
The matching number of the empty graph (bot) is 0.
theorem graph_matching_num_bot {V : Type*} : graph_matching_num (⊥ : SimpleGraph V) = 0
graph_matching_num_monotheorem
If G and G' are simple graphs on the same vertex set with G ≤ G', then the matching number of G is at most the matching number of G'.
theorem graph_matching_num_mono {V : Type*} {G G' : SimpleGraph V} (h : G ≤ G') : graph_matching_num G ≤ graph_matching_num G'
In any finite simple graph G, the sum of the vertex cover number and the independence number is equal to the number of vertices.
theorem vertex_cover_num_add_indep_num {V : Type*} [Fintype V] (G : SimpleGraph V) : G.vertexCoverNum + G.indepNum = Fintype.card V
In any simple graph G, the matching number is at most the cardinality of the edge set.
theorem graph_matching_num_le_encard_edgeSet {V : Type*} (G : SimpleGraph V) : graph_matching_num G ≤ G.edgeSet.encard
Circuit Complexity & Lower Bounds
6 of 20 targetedGateTypeinductive
The standard Boolean gate types in circuit complexity: conjunction (AND), disjunction (OR), and negation (NOT).
inductive GateTypeBooleanCircuitinductive
A Boolean circuit with n inputs over the standard De Morgan basis, with constructors for input variables indexed by Fin n, Boolean constants, negation (NOT), conjunction (AND), and disjunction (OR).
inductive BooleanCircuit (n : Nat)CircuitGateinductive
A gate in a straight-line program representation of a Boolean circuit on n inputs, which can be an input variable indexed by Fin n, a Boolean constant, a NOT gate referencing a previous gate index, or an AND or OR gate referencing two previous gate indices.
inductive CircuitGate (n : Nat)Evaluates a Boolean circuit c with n inputs on a variable truth assignment x : Fin n → Bool, by structural recursion: variables look up their value in x, constants return their Boolean value, and NOT, AND, OR gates apply the corresponding Boolean operations to the evaluations of their subcircuits.
def boolean_circuit_eval {n : Nat} (c : BooleanCircuit n) (x : Fin n → Bool) : Boolboolean_circuit_eval_not_nottheorem
For any Boolean circuit c on n variables and any input assignment x : Fin n → Bool, evaluating the double negation BooleanCircuit.not (BooleanCircuit.not c) on x equals evaluating c on x.
theorem boolean_circuit_eval_not_not {n : Nat} (c : BooleanCircuit n) (x : Fin n → Bool) : boolean_circuit_eval (BooleanCircuit.not (BooleanCircuit.not c)) x = boolean_circuit_eval c xFor any Boolean circuits c₁ and c₂ on n variables and any input assignment x : Fin n → Bool, evaluating the negation of their conjunction BooleanCircuit.not (BooleanCircuit.and c₁ c₂) on x equals evaluating the disjunction of their negations BooleanCircuit.or (BooleanCircuit.not c₁) (BooleanCircuit.not c₂) on x.
theorem boolean_circuit_eval_demorgan_and {n : Nat} (c₁ c₂ : BooleanCircuit n) (x : Fin n → Bool) : boolean_circuit_eval (BooleanCircuit.not (BooleanCircuit.and c₁ c₂)) x = boolean_circuit_eval (BooleanCircuit.or (BooleanCircuit.not c₁) (BooleanCircuit.not c₂)) xRandomised Computation
2 of 25 targetedLet F be an integral domain, p a nonzero polynomial in n variables over F, and S a nonempty finite subset of F. If the total degree of p is less than the cardinality of S, then there is a point x in S^n at which p does not vanish. Equivalently, a nonzero polynomial of total degree d is not the zero function on S^n, so random evaluation from S^n detects nonzeroness.
theorem schwartz_zippel_exists_nonzero_eval {F : Type*} [CommRing F] [IsDomain F] [DecidableEq F] {n : ℕ} {p : MvPolynomial (Fin n) F} (hp : p ≠ 0) {S : Finset F} (hS : 0 < S.card) (hd : p.totalDegree < S.card) : ∃ x ∈ Fintype.piFinset (fun _ : Fin n => S), MvPolynomial.eval x p ≠ 0
Let F be an integral domain, S a nonempty finite subset of F, n a positive integer, and p a nonzero polynomial in n variables over F of total degree d. Then the number of points x of S^n at which p vanishes is at most d·|S|^(n−1); equivalently, the fraction of the points of S^n at which p vanishes is at most d/|S|.
open scoped Finset in theorem schwartz_zippel_zero_count_le {F : Type*} [CommRing F] [IsDomain F] [DecidableEq F] {n : ℕ} (hn : 0 < n) {p : MvPolynomial (Fin n) F} (hp : p ≠ 0) {S : Finset F} (hS : 0 < S.card) : #{x ∈ Fintype.piFinset (fun _ : Fin n => S) | MvPolynomial.eval x p = 0} ≤ p.totalDegree * S.card ^ (n - 1)
Game Theory & Mathematical Economics
16Strategic interaction and the theory of collective decisions: when equilibria exist, what aggregation rules are possible, and what mechanisms can be made incentive-compatible.
Matching & Market Design
8 of 20 targetedMarriageMarketstructure
A marriage market with types M and W consists of a relation pref_m : M → W → W → Prop representing men's preferences over women, and a relation pref_w : W → M → M → Prop representing women's preferences over men.
structure MarriageMarket (M W : Type*)
In a marriage market market with agent types M and W, if a matching equivalence μ : M ≃ W has no blocking pairs (that is, for all m : M and w : W, ¬ (market.pref_m m w (μ m) ∧ market.pref_w w m (μ.symm w))), and a man m : M strictly prefers woman w : W to his assigned partner μ m under market.pref_m, then woman w does not strictly prefer m to her assigned partner μ.symm w under market.pref_w.
theorem stable_matching_not_pref_of_pref {M W : Type*} (market : MarriageMarket M W) (μ : M ≃ W) (h_stable : ∀ (m : M) (w : W), ¬ (market.pref_m m w (μ m) ∧ market.pref_w w m (μ.symm w))) (m : M) (w : W) (h : market.pref_m m w (μ m)) : ¬ market.pref_w w m (μ.symm w)
In a marriage market market with agent types M and W, if every man m : M is matched under equivalence μ : M ≃ W to a woman μ m such that for all women w : W he does not strictly prefer w to μ m (that is, ∀ (m : M) (w : W), ¬ market.pref_m m w (μ m)), then the matching has no blocking pairs, meaning that for all m : M and w : W, ¬ (market.pref_m m w (μ m) ∧ market.pref_w w m (μ.symm w)).
theorem stable_matching_of_all_men_top_choice {M W : Type*} (market : MarriageMarket M W) (μ : M ≃ W) (h_top : ∀ (m : M) (w : W), ¬ market.pref_m m w (μ m)) : ∀ (m : M) (w : W), ¬ (market.pref_m m w (μ m) ∧ market.pref_w w m (μ.symm w))
In a marriage market market with agent types M and W, if every woman w : W is matched under equivalence μ : M ≃ W to a man μ.symm w such that for all men m : M she does not strictly prefer m to μ.symm w (that is, ∀ (w : W) (m : M), ¬ market.pref_w w m (μ.symm w)), then the matching has no blocking pairs, meaning that for all m : M and w : W, ¬ (market.pref_m m w (μ m) ∧ market.pref_w w m (μ.symm w)).
theorem stable_matching_of_all_women_top_choice {M W : Type*} (market : MarriageMarket M W) (μ : M ≃ W) (h_top : ∀ (w : W) (m : M), ¬ market.pref_w w m (μ.symm w)) : ∀ (m : M) (w : W), ¬ (market.pref_m m w (μ m) ∧ market.pref_w w m (μ.symm w))
In a marriage market with agent types M and W and a matching μ : M ≃ W, a man m and a woman w form a blocking pair when m strictly prefers w to his assigned partner μ m, and w strictly prefers m to her assigned partner μ.symm w.
def is_blocking_pair {M W : Type*} (market : MarriageMarket M W) (μ : M ≃ W) (m : M) (w : W) : Prop
In a marriage market with agent types M and W, a matching μ : M ≃ W is stable when no man m and woman w form a blocking pair, that is, when for every m and every w it is not the case that m prefers w to μ m and w prefers m to μ.symm w.
def is_stable_matching {M W : Type*} (market : MarriageMarket M W) (μ : M ≃ W) : Prop
is_stable_matching_of_no_strict_preferencetheoremoriginal
In the marriage market on M and W whose two preference relations are identically false, so that no agent strictly prefers anyone to anyone, every matching μ : M ≃ W is stable.
theorem is_stable_matching_of_no_strict_preference {M W : Type*} (μ : M ≃ W) : is_stable_matching (MarriageMarket.mk (fun _ _ _ => False) (fun _ _ _ => False)) μ
not_is_stable_matching_of_universal_preferencetheoremoriginal
In the marriage market on M and W whose two preference relations are identically true, so that every agent strictly prefers everyone to everyone, no matching μ : M ≃ W is stable, provided M is inhabited.
theorem not_is_stable_matching_of_universal_preference {M W : Type*} (m : M) (μ : M ≃ W) : ¬ is_stable_matching (MarriageMarket.mk (fun _ _ _ => True) (fun _ _ _ => True)) μ
Equilibria in Games
4 of 20 targetedStrategicGamestructure
A strategic-form game with player type Player consists of a family of strategy types Strategy i for each player i : Player, and a real-valued payoff function payoff i : (∀ j : Player, Strategy j) → ℝ for each player i : Player.
structure StrategicGame (Player : Type*)
In a strategic-form game G with player type Player, a strategy profile s : ∀ i, G.Strategy i is a pure Nash equilibrium if for every player i : Player and every alternative strategy s_i' : G.Strategy i, player i's payoff from unilaterally deviating to s_i' satisfies G.payoff i (Function.update s i s_i') ≤ G.payoff i s.
def is_pure_nash_equilibrium {Player : Type*} [DecidableEq Player] (G : StrategicGame Player) (s : ∀ i, G.Strategy i) : Prop
In a strategic-form game G where all players have the same payoff function u (that is, G.payoff i s = u s for every player i and strategy profile s), any strategy profile s that globally maximizes u (that is, u s' ≤ u s for all strategy profiles s') is a pure Nash equilibrium.
theorem pure_nash_of_common_payoff_maximizer {Player : Type*} [DecidableEq Player] (G : StrategicGame Player) (u : (∀ j, G.Strategy j) → ℝ) (h_common : ∀ (i : Player) (s : ∀ j, G.Strategy j), G.payoff i s = u s) (s : ∀ i, G.Strategy i) (h_max : ∀ s' : ∀ j, G.Strategy j, u s' ≤ u s) : is_pure_nash_equilibrium G s
In a strategic-form game G, if some player i has an alternative strategy s_i' yielding a strictly higher payoff than at strategy profile s (that is, G.payoff i s < G.payoff i (Function.update s i s_i')), then s is not a pure Nash equilibrium.
theorem not_pure_nash_of_exists_better_response {Player : Type*} [DecidableEq Player] (G : StrategicGame Player) (s : ∀ i, G.Strategy i) (i : Player) (s_i' : G.Strategy i) (h : G.payoff i s < G.payoff i (Function.update s i s_i')) : ¬ is_pure_nash_equilibrium G s
Mechanism Design & Auctions
2 of 20 targetedDirectMechanismstructure
A direct mechanism with player type Player, type spaces Theta i for each player i : Player, and outcome type Outcome, consists of an allocation rule allocation : (∀ i : Player, Theta i) → Outcome and a payment rule payment : Player → (∀ i : Player, Theta i) → ℝ.
structure DirectMechanism (Player : Type*) (Theta : Player → Type*) (Outcome : Type*)
For a direct mechanism (M : DirectMechanism Player Theta Outcome) with {Player : Type*} [DecidableEq Player], {Theta : Player → Type*}, {Outcome : Type*}, and valuation profile (v : (i : Player) → Theta i → Outcome → ℝ), is_dominant_strategy_incentive_compatible M v is defined with body := ∀ (i : Player) (θ : ∀ j, Theta j) (θ_i' : Theta i), v i (θ i) (M.allocation (Function.update θ i θ_i')) - M.payment i (Function.update θ i θ_i') ≤ v i (θ i) (M.allocation θ) - M.payment i θ.
def is_dominant_strategy_incentive_compatible {Player : Type*} [DecidableEq Player] {Theta : Player → Type*} {Outcome : Type*} (M : DirectMechanism Player Theta Outcome) (v : (i : Player) → Theta i → Outcome → ℝ) : Prop
Social Choice Theory
2 of 20 targetedIn a profile of preferences P where a finite set of voters V have pairwise preferences over alternatives A, an alternative x : A is a Condorcet winner if for every alternative y ≠ x, the number of voters who strictly prefer x to y is strictly greater than the number of voters who strictly prefer y to x.
def condorcet_winner {V A : Type*} [Fintype V] (P : V → A → A → Prop) [∀ v, DecidableRel (P v)] (x : A) : Prop
condorcet_winner_uniquetheorem
If x and y are both Condorcet winners under a preference profile P with a finite voter set V, then x = y.
theorem condorcet_winner_unique {V A : Type*} [Fintype V] (P : V → A → A → Prop) [∀ v, DecidableRel (P v)] (x y : A) (hx : condorcet_winner P x) (hy : condorcet_winner P y) : x = y
Theoretical Physics
16The mathematical structure of physical theory: the variational principles that generate the equations of motion, the symmetries that constrain them, the conserved quantities that follow, and the operator and ensemble formalisms of quantum and statistical mechanics.
Lagrangian & Hamiltonian Mechanics
4 of 25 targetedThe Poisson bracket {f, g} of two scalar functions f, g on the phase space E × E evaluated at (q, p) is defined as the difference of inner products ⟪∇_q f, ∇_p g⟫ - ⟪∇_p f, ∇_q g⟫.
noncomputable def poisson_bracket {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f g : E × E → ℝ) (qp : E × E) : ℝ
A path γ : ℝ → E × E is a Hamiltonian trajectory for the Hamiltonian H : E × E → ℝ if for all times t, the time derivative of the position component equals the momentum gradient of H at γ(t) and the time derivative of the momentum component equals the negative position gradient of H at γ(t).
def IsHamiltonianTrajectory {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (H : E × E → ℝ) (γ : ℝ → E × E) : Prop
poisson_bracket_anticommtheorem
For any two scalar functions f and g on the phase space E × E and any phase-space point qp, the Poisson bracket satisfies {f, g}(qp) = -{g, f}(qp).
theorem poisson_bracket_anticomm {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f g : E × E → ℝ) (qp : E × E) : poisson_bracket f g qp = - poisson_bracket g f qp
The constant zero trajectory is a Hamiltonian trajectory for the zero Hamiltonian.
theorem is_hamiltonian_trajectory_zero {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : IsHamiltonianTrajectory (E := E) (fun _ => 0) (fun _ => (0, 0))
Special Relativity & Minkowski Geometry
4 of 20 targetedThe Minkowski metric matrix on ℝ⁴ with mostly-plus signature (-, +, +, +) is the 4x4 diagonal matrix with diagonal entries -1, 1, 1, 1.
def minkowski_matrix : Matrix (Fin 4) (Fin 4) ℝA 4x4 real matrix Λ is a Lorentz matrix if it preserves the Minkowski metric matrix, satisfying Λᵀ * minkowski_matrix * Λ = minkowski_matrix.
def is_lorentz_matrix (Λ : Matrix (Fin 4) (Fin 4) ℝ) : Prop
is_lorentz_matrix_multheorem
If A and B are 4x4 Lorentz matrices, then their matrix product A * B is also a Lorentz matrix.
theorem is_lorentz_matrix_mul {A B : Matrix (Fin 4) (Fin 4) ℝ} (hA : is_lorentz_matrix A) (hB : is_lorentz_matrix B) : is_lorentz_matrix (A * B)is_lorentz_matrix_onetheorem
The 4x4 identity matrix is a Lorentz matrix.
theorem is_lorentz_matrix_one : is_lorentz_matrix 1Quantum Mechanics
3 of 25 targetedThe commutator [A, B] = A * B - B * A of two self-adjoint continuous linear operators A and B on a complex Hilbert space is skew-adjoint, that is, star ⁅A, B⁆ = -⁅A, B⁆.
theorem quantum_commutator_self_adjoint_skew {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A B : E →L[ℂ] E) (hA : IsSelfAdjoint A) (hB : IsSelfAdjoint B) : star ⁅A, B⁆ = -⁅A, B⁆
For any orthogonal projection operator P (a self-adjoint idempotent continuous linear map) on a complex Hilbert space E and any state vector ψ in E, the inner product ⟪ψ, P ψ⟫_ℂ equals the complex square of the norm ‖P ψ‖.
theorem quantum_projection_expectation_norm_sq {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (P : E →L[ℂ] E) (hP : IsStarProjection P) (ψ : E) : inner ℂ ψ (P ψ) = (‖P ψ‖ : ℂ) ^ 2
For any unitary continuous linear operator U on a complex Hilbert space E and any vectors ϕ and ψ in E, the inner product is preserved: ⟪U ϕ, U ψ⟫_ℂ = ⟪ϕ, ψ⟫_ℂ.
theorem quantum_unitary_preserves_inner {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (U : E →L[ℂ] E) (hU : U ∈ unitary (E →L[ℂ] E)) (ϕ ψ : E) : inner ℂ (U ϕ) (U ψ) = inner ℂ ϕ ψ
Classical Field Theory & Electromagnetism
3 of 20 targetedA scalar field u : ℝ × ℝ → ℝ satisfies the one-dimensional wave equation with wave speed c if for all (x, t), the second partial derivative of u with respect to time equals c^2 times the second partial derivative of u with respect to space.
def WaveEquation1D (c : ℝ) (u : ℝ × ℝ → ℝ) : Prop
A scalar field φ : ℝ × ℝ → ℝ satisfies the one-dimensional Klein-Gordon equation with mass parameter m and propagation speed c if for all (x, t), the second time derivative minus c^2 times the second spatial derivative plus m^2 * φ(x, t) equals zero.
def KleinGordonEquation1D (m c : ℝ) (φ : ℝ × ℝ → ℝ) : Prop
klein_gordon_zero_mass_iff_wave_equationtheoremoriginal
A scalar field φ : ℝ × ℝ → ℝ satisfies the one-dimensional Klein-Gordon equation with mass parameter 0 and speed c if and only if it satisfies the one-dimensional wave equation with speed c.
theorem klein_gordon_zero_mass_iff_wave_equation (c : ℝ) (φ : ℝ × ℝ → ℝ) :
KleinGordonEquation1D 0 c φ ↔ WaveEquation1D c φStatistical Mechanics & Thermodynamics
2 of 20 targetedThe canonical partition function Z(β) of a system with finite configuration space Ω and Hamiltonian H : Ω → ℝ at inverse temperature β is the sum over all configurations ω of exp(-β * H(ω)).
noncomputable def canonicalPartitionFunction {Ω : Type*} [Fintype Ω] (H : Ω → ℝ) (β : ℝ) : ℝ
The Boltzmann (Gibbs) distribution on a finite configuration space Ω with Hamiltonian H : Ω → ℝ at inverse temperature β assigns to each configuration ω the probability exp(-β * H(ω)) / Z(β), where Z(β) is the canonical partition function.
noncomputable def boltzmannDistribution {Ω : Type*} [Fintype Ω] (H : Ω → ℝ) (β : ℝ) (ω : Ω) : ℝ
Nothing matches. Try fewer words, or a name from the topic list.