structure SteinerTripleSystem (α : Type u_1) [DecidableEq α] : Type u_1

A Steiner triple system on $\alpha$ (Definition 10.2.8): a collection of 3-element subsets ("triples") such that every pair of distinct elements is contained in exactly one triple.

• triples : Set (Finset α)
• triple_card (t : Finset α) : t ∈ self.triples → t.card = 3
• pair_in_unique_triple (a b : α) : a ≠ b → ∃! t : Finset α, t ∈ self.triples ∧ a ∈ t ∧ b ∈ t

instance instFiniteSteinerTripleSystemFin (n : ℕ) : Finite (SteinerTripleSystem (Fin n))

Finiteness of the type of Steiner triple systems on $\{0,\dots,n-1\}$.

noncomputable def numSTS (n : ℕ) : ℕ

The number of Steiner triple systems on $\{0,\dots,n-1\}$, denoted $\mathrm{STS}(n)$.

theorem integral_log_sq : ∫ (t : ℝ) in 0..1, Real.log (t ^ 2) = -2

The integral $\int_0^1 \log(t^2) \, dt = -2$.

theorem antitone_log_inv_add_sq (t : ℝ) : Antitone fun (n : ℕ) => Real.log (1 / (↑n + 4) + t ^ 2)

The sequence $n \mapsto \log\bigl(\tfrac{1}{n+4} + t^2\bigr)$ is antitone in $n$.

theorem tendsto_log_inv_add_sq {t : ℝ} (ht : t ≠ 0) : Filter.Tendsto (fun (n : ℕ) => Real.log (1 / (↑n + 4) + t ^ 2)) Filter.atTop (nhds (Real.log (t ^ 2)))

Pointwise convergence: $\log\bigl(\tfrac{1}{n+4} + t^2\bigr) \to \log(t^2)$ as $n \to \infty$, for any $t \neq 0$.

theorem integrableOn_log_sq : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.log (t ^ 2)) (Set.Ioc 0 1) MeasureTheory.volume

Integrability of $t \mapsto \log(t^2)$ on $(0,1]$.

theorem integrableOn_log_inv_add_sq (n : ℕ) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.log (1 / (↑n + 4) + t ^ 2)) (Set.Ioc 0 1) MeasureTheory.volume

Integrability of $t \mapsto \log\bigl(\tfrac{1}{n+4} + t^2\bigr)$ on $(0,1]$.

theorem tendsto_integral_log_inv_add_sq : Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ) in 0..1, Real.log (1 / (↑n + 4) + t ^ 2)) Filter.atTop (nhds (-2))

Convergence of integrals: $\int_0^1 \log\bigl(\tfrac{1}{n+4} + t^2\bigr) \, dt \to -2$ as $n \to \infty$, by the monotone convergence theorem.

theorem integral_log_one_add_mul_sq (c : ℝ) (hc : 0 < c) : ∫ (t : ℝ) in 0..1, Real.log (1 + c * t ^ 2) = Real.log c + ∫ (t : ℝ) in 0..1, Real.log (1 / c + t ^ 2)

Algebraic identity: $\int_0^1 \log(1 + c t^2) \, dt = \log c + \int_0^1 \log(1/c + t^2) \, dt$ for any $c > 0$.

theorem entropy_bound_sts (n : ℕ) (hn : 4 ≤ n) : Real.log ↑(numSTS n) ≤ ↑n * (↑n - 1) / 6 * ∫ (t : ℝ) in 0..1, Real.log (1 + (↑n - 3) * t ^ 2)

Entropy upper bound on Steiner triple systems: for $n \ge 4$, $\log |\mathrm{STS}(n)| \le \tfrac{n(n-1)}{6} \int_0^1 \log(1 + (n-3) t^2) \, dt$.

theorem sts_count_upper_bound (ε : ℝ) : ε > 0 → ∀ᶠ (n : ℕ) in Filter.atTop, Real.log ↑(numSTS n) ≤ ↑n * (↑n - 1) / 6 * (Real.log ↑n - 2 + ε)

The Linial-Luria upper bound (Theorem 10.2.10): for every $\varepsilon > 0$, eventually $\log |\mathrm{STS}(n)| \le \tfrac{n(n-1)}{6}(\log n - 2 + \varepsilon)$.