Tau Ceti: ten theorems from the first month
It's been a month since we launched, so I'd like to make a brief post highlighting some of the results that have landed in Tau Ceti.
We're ready for more contributors at this point. Please come to the #Tau Ceti channel to discuss contributing to the roadmaps, or if you have existing material you would like to migrate into Tau Ceti.
If you'd just like to point your AI at Tau Ceti, it can be as simple as
uv tool install git+https://github.com/kim-em/TauCetiWorker.git tauceti --loop
(if you would like to run this inside a Docker container, please read, or have your AI read, https://github.com/kim-em/TauCetiWorker/blob/main/docs/docker.md)
1. Planar Harnack inequality and strong maximum principle
A nonnegative harmonic function on a planar disk satisfies the sharp two-sided Harnack bounds relative to its value at the center; consequently, a harmonic function on a connected planar domain that attains an interior local extremum is constant.
theorem harnack_inequality_center
{f : ℂ → ℝ} {c w : ℂ} {R : ℝ} (hf : HarmonicOnNhd f (ball c R))
(hnonneg : ∀ z ∈ ball c R, 0 ≤ f z) (hw : w ∈ ball c R) :
(R - ‖w - c‖) / (R + ‖w - c‖) * f c ≤ f w ∧
f w ≤ (R + ‖w - c‖) / (R - ‖w - c‖) * f ctheorem eqOn_const_of_harmonicOnNhd_of_isLocalMax
{f : ℂ → ℝ} {Ω : Set ℂ} {a : ℂ}
(hΩa : Ω ∈ 𝓝 a) (hΩconn : IsPreconnected Ω) (hf : HarmonicOnNhd f Ω)
(hmax : IsLocalMax f a) : EqOn f (const ℂ (f a)) ΩHarnack inequality: source · documentation · PR #1299 Strong maximum principle: source · documentation · PR #1724
2. Peter–Weyl theorem
For a compact group, the normalized matrix coefficients of its irreducible unitary
representations form a Hilbert basis of L²(G), and the representative functions are uniformly
dense in C(G).
noncomputable def stdPeterWeylBasis
(𝕜 G : Type*) [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] :
HilbertBasis (Σ i : IrrepClass 𝕜 G,
Fin (IrrepClass.model i).dim × Fin (IrrepClass.model i).dim)
𝕜 (Lp 𝕜 2 (haarProb G))theorem representativeStarSubalgebra_dense
(𝕜 G : Type*) [RCLike 𝕜] [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] [CompactSpace G] :
(representativeStarSubalgebra 𝕜 G).topologicalClosure = ⊤Hilbert basis: source · documentation · PR #2677 Representative density: source · documentation · PR #2640
3. Krull–Schmidt theorem
Any two decompositions of a finite-length module into finitely many indecomposable summands have isomorphic summands after reindexing.
theorem exists_equiv_linearEquiv_of_iSupIndep
{A M : Type*} [Ring A] [AddCommGroup M] [Module A M]
[IsNoetherian A M] [IsArtinian A M]
{ι κ : Type*} [Finite ι] [Finite κ] {P : ι → Submodule A M}
{Q : κ → Submodule A M} (hP : iSupIndep P) (hPt : ⨆ i, P i = ⊤)
(hPind : ∀ i, IsIndecomposableModule A (P i)) (hQ : iSupIndep Q)
(hQt : ⨆ j, Q j = ⊤) (hQind : ∀ j, IsIndecomposableModule A (Q j)) :
∃ e : ι ≃ κ, ∀ i, Nonempty (P i ≃ₗ[A] Q (e i))
4. Hille–Yosida generation theorem
An operator on a real Banach space generates a strongly continuous semigroup with a prescribed growth bound exactly when its domain is dense and its resolvent satisfies the corresponding Hille–Yosida power bounds.
theorem hilleYosida_generation_iff
{X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
(A : X →ₗ.[ℝ] X) (M omega : ℝ) :
(∃ S : StronglyContinuousSemigroup X,
S.generator = A ∧ S.HasGrowthBound omega M) ↔
1 ≤ M ∧ Dense (A.domain : Set X) ∧
(∀ lambda : ℝ, omega < lambda → lambda ∈ LinearPMap.resolventSet A) ∧
∀ n : ℕ, 1 ≤ n → ∀ lambda : ℝ, omega < lambda →
‖LinearPMap.resolvent A lambda ^ n‖ ≤ M / (lambda - omega) ^ n
5. De Finetti–Ryll-Nardzewski theorem
For standard-Borel-valued sequences, contractability, exchangeability, and conditional independence with identical distributions coincide; every exchangeable law has a unique representation as a mixture of i.i.d. product laws.
theorem deFinetti_RyllNardzewski_equivalence
{Ω α : Type*} [MeasurableSpace Ω] [MeasurableSpace α]
[StandardBorelSpace α] [Nonempty α]
{μ : Measure Ω} [IsFiniteMeasure μ] {X : ℕ → Ω → α}
(hX_meas : ∀ n, AEMeasurable (X n) μ) :
Contractable μ X ↔ Exchangeable μ X ∧ ConditionallyIID μ Xtheorem deFinetti_mixture
{Ω α : Type*} [MeasurableSpace Ω] [MeasurableSpace α]
[StandardBorelSpace α] {μ : Measure Ω}
[IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hX : Exchangeable μ X)
(hX_meas : ∀ n, AEMeasurable (X n) μ) :
∃! π : ProbabilityMeasure (ProbabilityMeasure α),
pathLaw μ X = (π : Measure (ProbabilityMeasure α)).bind
fun P => Measure.infinitePi fun _ : ℕ => (P : Measure α)Equivalence: source · documentation · PR #891 Unique mixture: source · documentation · PR #1462
6. Frobenius isogeny
For a Weierstrass curve over a finite field with q elements, the q-power Frobenius defines an
isogeny of degree q.
@[simp]
theorem degree_frobeniusIsogeny
{F : Type*} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) :
(frobeniusIsogeny W).degree = Nat.card F
7. Artin induction theorem
For a finite group G, induction from cyclic subgroups spans the rationalized group of virtual
characters; explicitly, |G| times every virtual character lies in the induced integral span.
theorem natCard_nsmul_mem_indVirtualCharacters_isCyclic
{k G : Type*} [Field k] [Group G] [Finite G] {f : G → k}
(hf : f ∈ virtualCharacters k G) :
Nat.card G • f ∈ indVirtualCharacters k G (fun C ↦ IsCyclic C)
8. Cartan–Killing classification
Every irreducible reduced crystallographic finite root system has a unique valid Dynkin type:
Aₙ, Bₙ, Cₙ, Dₙ, E₆, E₇, E₈, F₄, or G₂.
theorem existsUnique_dynkinType
{ι R M N : Type*} [CommRing R] [AddCommGroup M] [Module R M]
[AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι]
[CharZero R] [IsDomain R] [P.IsRootSystem] [P.IsCrystallographic]
[P.IsReduced] [P.IsIrreducible] [Nonempty ι] (b : P.Base) :
∃! t : DynkinType, t.Valid ∧ HasCartanType P b t
9. Cartier duality over a general base
Over any commutative ring, Cartier duality is an involutive anti-equivalence on finite locally free commutative affine group schemes.
noncomputable def cartierDuality (R : Type*) [CommRing R] :
(FiniteLocallyFreeCommAffineGroupSchemeCat (CommRingCat.of R))ᵒᵖ ≌
FiniteLocallyFreeCommAffineGroupSchemeCat (CommRingCat.of R)
10. Bochner's theorem
A function on a finite-dimensional real inner-product space is continuous and positive definite exactly when it is the Fourier transform of a unique finite positive Borel measure.
theorem bochner
{V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
[FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) :
(Continuous F ∧ IsPositiveDefiniteSub F) ↔
∃! μ : Measure V,
IsFiniteMeasure μ ∧ ∀ v, F v = ∫ q, fourierAtom v q ∂μ