Community problems

In a marriage market market with agent types M and W where M is a subsingleton (Subsingleton M), if men's preferences are irreflexive (∀ (m : M) (w : W), ¬ market.pref_m m w w), then any matching equivalence μ : M ≃ W 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_subsingleton {M W : Type*} [Subsingleton M] (market : MarriageMarket M W) (h_irrefl : ∀ (m : M) (w : W), ¬ market.pref_m m w w) (μ : M ≃ W) : ∀ (m : M) (w : W), ¬ (market.pref_m m w (μ m) ∧ market.pref_w w m (μ.symm w))

If an alternative y is strictly preferred to alternative x by more voters than prefer x to y, then x cannot be a Condorcet winner.

theorem condorcet_winner_not_of_majority_defeated {V A : Type*} [Fintype V]
    (P : V → A → A → Prop) [∀ v, DecidableRel (P v)] (x y : A)
    (h_defeat : (Finset.filter (fun v => P v y x) Finset.univ).card >
                (Finset.filter (fun v => P v x y) Finset.univ).card) :
    ¬ condorcet_winner P x

The zero function is a solution to the one-dimensional wave equation.

theorem wave_equation_zero (c : ℝ) : WaveEquation1D c (fun _ => 0)

For any scalar function f on the phase space E × E and any phase-space point qp, the Poisson bracket {f, f}(qp) vanishes.

theorem poisson_bracket_self {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    (f : E × E → ℝ) (qp : E × E) :
    poisson_bracket f f qp = 0

For any three continuous linear operators A, B, C on a complex inner product space E, their commutators satisfy the Jacobi identity: ⁅A, ⁅B, C⁆⁆ + ⁅B, ⁅C, A⁆⁆ + ⁅C, ⁅A, B⁆⁆ = 0.

theorem quantum_commutator_jacobi_identity {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
    (A B C : E →L[ℂ] E) :
    ⁅A, ⁅B, C⁆⁆ + ⁅B, ⁅C, A⁆⁆ + ⁅C, ⁅A, B⁆⁆ = 0

For any nonempty finite configuration space Ω, Hamiltonian H : Ω → ℝ, and inverse temperature β, the sum of the Boltzmann distribution over all configurations is equal to 1.

theorem boltzmann_distribution_sum_eq_one {Ω : Type*} [Fintype Ω] [Nonempty Ω] (H : Ω → ℝ) (β : ℝ) :
    ∑ ω : Ω, boltzmannDistribution H β ω = 1

For any nonempty finite configuration space Ω, Hamiltonian H : Ω → ℝ, and inverse temperature β, the canonical partition function is strictly positive.

theorem canonical_partition_function_pos {Ω : Type*} [Fintype Ω] [Nonempty Ω] (H : Ω → ℝ) (β : ℝ) :
    0 < canonicalPartitionFunction H β

The language {[]} containing only the empty word is regular.

theorem is_regular_one {α : Type*} : (1 : Language α).IsRegular

For any regular language L and natural number n, the n-th power L^n is regular.

theorem is_regular_pow {α : Type*} {L : Language α} (h : L.IsRegular) (n : ℕ) : (L ^ n).IsRegular

A CNF formula containing the empty clause cannot be satisfied by any assignment because the empty clause contains no literals to be made true.

theorem cnf_not_satisfiable_of_has_empty_clause {V : Type*} (f : List (List (CnfLit V))) (h : [] ∈ f) : ¬ CnfSatisfiable f

Every language L over a finite alphabet Γ Karp-reduces to itself: the reduction is the identity function on words, which is computed by the identity Turing machine in a constant number of steps, and w ∈ L if and only if w ∈ L.

theorem karp_reducible_refl {Γ : Type} [Fintype Γ] (L : Language Γ) : KarpReducible Γ Γ L L

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 of S^n at which p does not vanish is at least |S|^n − d·|S|^(n−1); equivalently, at least a fraction 1 − d/|S| of the points of S^n are nonzero for p. This is the guarantee of the random-evaluation identity test: a point where p is nonzero certifies p ≠ 0, so the test has one-sided error and rejects a nonzero p with probability at most d/|S|.

open scoped Finset in
theorem schwartz_zippel_nonzero_count_ge {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) :
    S.card ^ n - p.totalDegree * S.card ^ (n - 1)
      ≤ #{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 for every t the number of t-tuples (x_1, …, x_t) of points of S^n at which p vanishes at every one of the t coordinates is at most (d·|S|^(n−1))^t; equivalently, t independent random trials of the evaluation test all fail with probability at most (d/|S|)^t.

open scoped Finset in
theorem schwartz_zippel_repeated_trials_zero_count_le {F : Type*} [CommRing F] [IsDomain F]
    [DecidableEq F] {n t : ℕ} (hn : 0 < n) {p : MvPolynomial (Fin n) F} (hp : p ≠ 0)
    {S : Finset F} (hS : 0 < S.card) :
    #{X ∈ Fintype.piFinset (fun _ : Fin t => Fintype.piFinset (fun _ : Fin n => S)) |
        ∀ i, MvPolynomial.eval (X i) p = 0}
      ≤ (p.totalDegree * S.card ^ (n - 1)) ^ t

Let F be an integral domain, S a nonempty finite subset of F, n a positive integer, and let k ≥ 0, d ∈ ℕ and p_1, …, p_k be nonzero polynomials in n variables over F whose total degrees are all at most d. Then the number of points x of S^n at which at least one of p_1, …, p_k vanishes is at most k·d·|S|^(n−1). In particular, if k·d < |S| then some point of S^n is nonzero for all of p_1, …, p_k simultaneously.

open scoped Finset in
theorem schwartz_zippel_union_bound_zero_set {F : Type*} [CommRing F] [IsDomain F] [DecidableEq F]
    {n k d : ℕ} (hn : 0 < n) {S : Finset F} (hS : 0 < S.card)
    {p : Fin k → MvPolynomial (Fin n) F} (hp : ∀ i, p i ≠ 0)
    (hd : ∀ i, (p i).totalDegree ≤ d) :
    #{x ∈ Fintype.piFinset (fun _ : Fin n => S) | ∃ i, MvPolynomial.eval x (p i) = 0}
      ≤ k * (d * S.card ^ (n - 1))