Data

Results named in Tau Ceti's TauCeti.Data modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremBirkhoff's contraction theorem#

A matrix K with strictly positive entries contracts Hilbert's projective metric between strictly positive vectors by the factor tanh (K.projectiveDiameter / 4), which is strictly less than 1.

Matrix.hilbertProjectiveDist_mulVec_le.{u_1, u_2} {ι : Type u_1} {κ : Type u_2} [Finite ι]
  [Fintype κ] {K : Matrix ι κ ℝ} (hK : ∀ (i : ι) (j : κ), 0 < K i j) {x y : κ → ℝ}
  (hx : ∀ (j : κ), 0 < x j) (hy : ∀ (j : κ), 0 < y j) :
  TauCeti.hilbertProjectiveDist (K.mulVec x) (K.mulVec y) ≤
    Real.tanh (K.projectiveDiameter / 4) * TauCeti.hilbertProjectiveDist x y
Lean

Formalized in Tau Ceti as Matrix.hilbertProjectiveDist_mulVec_le.

Sources
LeanMatrix.hilbertProjectiveDist_mulVec_le

DefinitionThe Chinese remainder theorem for units#

(ℤ/n)ˣ is the product of the unit groups modulo the prime powers exactly dividing n.

ZMod.unitsEquivPi {n : ℕ} (hn : n ≠ 0) :
  (ZMod n)ˣ ≃* ((p : ↥n.primeFactors) → (ZMod (↑p ^ n.factorization ↑p))ˣ)
Lean

Formalized in Tau Ceti as ZMod.unitsEquivPi.

Sources
LeanZMod.unitsEquivPi

TheoremFine's theorem#

The number of k ≤ n for which p ∤ n choose k is ∏ⱼ (nⱼ + 1), the product over the base-p digits nⱼ of n.

Nat.card_filter_not_dvd_choose {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) :
  {k ∈ Finset.range (n + 1) | ¬p ∣ n.choose k}.card = (List.map (fun x => x + 1) (p.digits n)).prod
Lean

Formalized in Tau Ceti as Nat.card_filter_not_dvd_choose.

Sources
LeanNat.card_filter_not_dvd_choose
Uses 1
Proof usesLucas' theorem for divisibility, one digit at a time

TheoremHensel's lemma for n-th roots, as a count#

For n coprime to the prime p, an integer a prime to p and k ≠ 0, reduction modulo p is a bijection from the n-th roots of a modulo p ^ k to those modulo p; so there are equally many.

ZMod.natCard_nthRoots_prime_pow_eq_natCard_nthRoots {p n k : ℕ} [Fact (Nat.Prime p)]
  (hn : n.Coprime p) (hk : k ≠ 0) {a : ℤ} (ha : ↑a ≠ 0) :
  Nat.card { x // x ^ n = ↑a } = Nat.card { x // x ^ n = ↑a }
Lean

Formalized in Tau Ceti as ZMod.natCard_nthRoots_prime_pow_eq_natCard_nthRoots.

Sources
LeanZMod.natCard_nthRoots_prime_pow_eq_natCard_nthRoots

TheoremLegendre's identity over a fixed range#

For a < b ^ f, (b - 1) ∑_{i < f} ⌊a / b ^ (i + 1)⌋ = a - s(a), where s(a) is the base-b digit sum of a. This is Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digits with the sum extended by zero terms from log b a + 1 to f.

Nat.sub_one_mul_sum_div_pow_succ_eq_sub_sum_digits {b f a : ℕ} (ha : a < b ^ f) :
  (b - 1) * ∑ i ∈ Finset.range f, a / b ^ (i + 1) = a - (b.digits a).sum
Lean

Formalized in Tau Ceti as Nat.sub_one_mul_sum_div_pow_succ_eq_sub_sum_digits.

Sources
LeanNat.sub_one_mul_sum_div_pow_succ_eq_sub_sum_digits

TheoremLucas' theorem for divisibility, one digit at a time#

For last digits r, a < p, the prime p divides (r + p q) choose (a + p b) exactly when r < a or p divides q choose b.

Nat.dvd_choose_add_mul_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {q r a b : ℕ} (hr : r < p)
  (ha : a < p) : p ∣ (r + p * q).choose (a + p * b) ↔ r < a ∨ p ∣ q.choose b
Lean

Formalized in Tau Ceti as Nat.dvd_choose_add_mul_iff.

Sources
LeanNat.dvd_choose_add_mul_iff
Used by 1
Used byFine's theorem

TheoremThe Sinkhorn–Knopp theorem for a strictly positive kernel#

a strictly positive matrix K and strictly positive row sums a and column sums b of equal total mass admit strictly positive row factors u and column factors v such that the diagonal scaling u i * K i j * v j has row sums a and column sums b.

The scaled matrix is the minimiser of the relative entropy against K with these marginals.

Matrix.exists_sinkhorn_scaling.{u_1, u_2} {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ]
  {K : Matrix ι κ ℝ} (hK : ∀ (i : ι) (j : κ), 0 < K i j) {a : ι → ℝ} {b : κ → ℝ}
  (ha : ∀ (i : ι), 0 < a i) (hb : ∀ (j : κ), 0 < b j) (hmass : ∑ i, a i = ∑ j, b j) :
  ∃ u v,
    (∀ (i : ι), 0 < u i) ∧
      (∀ (j : κ), 0 < v j) ∧
        (∀ (i : ι), ∑ j, u i * K i j * v j = a i) ∧ ∀ (j : κ), ∑ i, u i * K i j * v j = b j
Lean

Formalized in Tau Ceti as Matrix.exists_sinkhorn_scaling.

Sources
LeanMatrix.exists_sinkhorn_scaling

TheoremVandermonde's identity for finitely many groups#

the ways of choosing n objects from groups of sizes K i, i ∈ s, sorted by how many come from each group.

Finset.sum_piAntidiag_prod_choose.{u_1} {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (K : ι → ℕ)
  (n : ℕ) : ∑ k ∈ s.piAntidiag n, ∏ i ∈ s, (K i).choose (k i) = (∑ i ∈ s, K i).choose n
Lean

Formalized in Tau Ceti as Finset.sum_piAntidiag_prod_choose.

Other forms

Vandermonde's identity grouped along a map f : ι → κ. Formalized in Tau Ceti as Finset.sum_filter_piAntidiag_prod_choose_fiberwise.

Finset.sum_filter_piAntidiag_prod_choose_fiberwise.{u_1, u_2} {ι : Type u_1} [DecidableEq ι]
  {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq κ] (f : ι → κ) (K : ι → ℕ) (m : κ → ℕ) :
  ∑ k ∈ Finset.univ.piAntidiag (∑ j, m j) with ∀ (j : κ), ∑ i with f i = j, k i = m j,
      ∏ i, (K i).choose (k i) =
    ∏ j, (∑ i with f i = j, K i).choose (m j)
Sources
LeanFinset.sum_piAntidiag_prod_choose · Finset.sum_filter_piAntidiag_prod_choose_fiberwise

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.