Other results
Results named in the rest of Tau Ceti's TauCeti.Combinatorics modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremThe Frobenius determinant formula#
The Frobenius determinant formula for the number f^μ of standard Young tableaux of shape
μ: for any bound r on the number of rows, f^μ times the product of the factorials of the
beta-numbers is μ.card ! times the product of their differences over the ordered pairs of rows.
The differences are differences of natural numbers, and are truncated at no ordered pair: the
beta-numbers strictly decrease across k < l < r.
This is the multiplicative form of f^μ = n ! * ∏_{k < l} (β_k - β_l) / ∏_k β_k !, and carries no
division obligation.
TauCeti.standardCount_mul_prod_factorial_betaNumber (μ : YoungDiagram) {r : ℕ}
(hr : μ.colLen 0 ≤ r) :
TauCeti.standardCount μ * ∏ i ∈ Finset.range r, (μ.betaNumber r i).factorial =
μ.card.factorial *
∏ k ∈ Finset.range r, ∏ l ∈ Finset.Ico (k + 1) r, (μ.betaNumber r k - μ.betaNumber r l)
Lean
Formalized in Tau Ceti as TauCeti.standardCount_mul_prod_factorial_betaNumber.
Sources
Uses 1
TheoremHall's theorem for expanding sets#
If a finite set D acting on β satisfies
k · |F| ≤ |D • F| for every finite F ⊆ β, then there is an injective map
j : β × Fin k → β moving each point by an element of D: j (x, i) = d • x for some d ∈ D.
This applies Hall's marriage theorem to the neighbour sets D • {x} indexed by β × Fin k.
Finset.exists_injective_of_mul_card_le_card_smul.{u_1, u_2} {α : Type u_1} {β : Type u_2} [SMul α β]
[DecidableEq β] {D : Finset α} {k : ℕ} (h : ∀ (F : Finset β), k * F.card ≤ (D • F).card) :
∃ j, Function.Injective j ∧ ∀ (p : β × Fin k), ∃ d ∈ D, d • p.1 = j p
Lean
Formalized in Tau Ceti as Finset.exists_injective_of_mul_card_le_card_smul.
Sources
Used by 1
TheoremHoeffding's inequality for a color count#
Color the points of a finite type ι
independently according to a PMF q on κ. The number of points of T with color c
deviates from its mean q c * #T by at least a ≥ 0 with probability at most
2 * exp (-2 a² / #T).
TauCeti.measureReal_le_abs_card_filter_sub_le.{u_1, u_2} {ι : Type u_1} {κ : Type u_2}
[DecidableEq κ] [Fintype ι] [MeasurableSpace κ] [MeasurableSingletonClass κ] (q : PMF κ)
(T : Finset ι) (c : κ) {a : ℝ} (ha : 0 ≤ a) :
(MeasureTheory.Measure.pi fun x => q.toMeasure).real
{x | a ≤ |↑{e ∈ T | x e = c}.card - (q c).toReal * ↑T.card|} ≤
2 * Real.exp (-2 * a ^ 2 / ↑T.card)
TheoremHoeffding's lemma on the grid {0, 1 / r, …, 1}#
For r ≠ 0 and every real t, the
exponential moment of the uniformly distributed centred point k / r - 1 / 2 satisfies
∑ k ∈ range (r + 1), exp (t (k / r - 1 / 2)) ≤ (r + 1) exp (t² / 8).
TauCeti.sum_range_exp_mul_div_sub_half_le {r : ℕ} (hr : r ≠ 0) (t : ℝ) :
∑ k ∈ Finset.range (r + 1), Real.exp (t * (↑k / ↑r - 1 / 2)) ≤ (↑r + 1) * Real.exp (t ^ 2 / 8)
Used by 1
TheoremMenger's theorem for vertex deletion in a digraph, predicate form#
Distinct nonadjacent
vertices remain joined after deleting any fewer than k other vertices exactly when there are
k pairwise internally vertex-disjoint directed paths between them.
Digraph.forall_reachableAvoiding_iff_exists_paths.{u} {V : Type u} {D : Digraph V} {s t : V}
[Finite V] (hst : s ≠ t) (hadj : ¬D.Adj s t) (k : ℕ) :
(∀ (X : Finset V), s ∉ X → t ∉ X → X.card < k → TauCeti.ReachableAvoiding D.AdjHom (↑X) s t) ↔
∃ P, (∀ (i : Fin k), (P i).IsPath) ∧ Pairwise fun i j => (P i).InternallyDisjoint (P j)
Lean
Formalized in Tau Ceti as Digraph.forall_reachableAvoiding_iff_exists_paths.
Other forms
Menger's theorem for internally vertex-disjoint paths in a digraph. Formalized in Tau Ceti as Digraph.exists_paths_vertexSeparator_card_eq.
Digraph.exists_paths_vertexSeparator_card_eq.{u} {V : Type u} {D : Digraph V} {s t : V} [Finite V]
(hst : s ≠ t) (hadj : ¬D.Adj s t) :
∃ k P X,
Function.Injective P ∧
(∀ (i : Fin k), (P i).IsPath) ∧
(Pairwise fun i j => (P i).InternallyDisjoint (P j)) ∧
s ∉ X ∧ t ∉ X ∧ ¬TauCeti.ReachableAvoiding D.AdjHom (↑X) s t ∧ X.card = k
Sources
Uses 1
TheoremThe Riemann–Hurwitz inequality for a block quotient#
The Euler characteristic of a triple
with transitive monodromy is at most |B| times that of its quotient by a nonempty block B.
TauCeti.PermutationTriple.eulerChar_le_ncard_mul_eulerChar_blockQuotient {n m : ℕ}
{t : TauCeti.PermutationTriple n} {B : Set (Fin n)}
(e : ↑(MulAction.orbit (↥t.monodromyGroup) B) ≃ Fin m)
(ht : MulAction.IsPretransitive (↥t.monodromyGroup) (Fin n))
(hB : MulAction.IsBlock (↥t.monodromyGroup) B) (hBne : B.Nonempty) :
t.eulerChar ≤ ↑B.ncard * (t.blockQuotient B e).eulerChar
Lean
Formalized in Tau Ceti as TauCeti.PermutationTriple.eulerChar_le_ncard_mul_eulerChar_blockQuotient.
Sources
TheoremSchützenberger's symmetry theorem#
The Robinson--Schensted correspondence of the inverse permutation exchanges the insertion and recording tableaux.
Equiv.Perm.rsk_inv {n : ℕ} (σ : Equiv.Perm (Fin n)) :
(TauCeti.rsk n) σ⁻¹ =
⟨((TauCeti.rsk n) σ).fst, (((TauCeti.rsk n) σ).snd.2, ((TauCeti.rsk n) σ).snd.1)⟩
TheoremVertex-capacitated Menger's theorem for a digraph#
Let s and t be distinct vertices
with no arrow from s to t, and let c v be the capacity of vertex v. Some family of k
directed s-to-t paths respects every nonterminal vertex capacity, and some terminal-excluding
vertex separator has total capacity k.
Digraph.exists_paths_vertexSeparator_sum_eq.{u} {V : Type u} {D : Digraph V} {s t : V} [Finite V]
[DecidableEq V] (c : V → ℕ) (hst : s ≠ t) (hadj : ¬D.Adj s t) :
∃ k P X,
(∀ (i : Fin k), (P i).IsPath) ∧
(∀ (v : V), v ≠ s → v ≠ t → {i | v ∈ (P i).vertices}.card ≤ c v) ∧
s ∉ X ∧ t ∉ X ∧ ¬TauCeti.ReachableAvoiding D.AdjHom (↑X) s t ∧ ∑ v ∈ X, c v = k
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.