diff --git a/Clt.lean b/Clt.lean
index f36514b..1cee3e4 100644
--- a/Clt.lean
+++ b/Clt.lean
@@ -1,5 +1,6 @@
 -- This module serves as the root of the `Clt` library.
 -- Import modules here that should be built as part of the library.
 import Clt.Tight
+import Clt.Separating
 import Clt.CharFun
 import Clt.ExpPoly
diff --git a/Clt/Separating.lean b/Clt/Separating.lean
new file mode 100644
index 0000000..71d5392
--- /dev/null
+++ b/Clt/Separating.lean
@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2023 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+import Mathlib.Topology.ContinuousFunction.Compact
+import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
+
+/-!
+# Separating sets of functions
+
+-/
+
+open BoundedContinuousFunction
+
+open scoped ENNReal
+
+namespace MeasureTheory
+
+variable {α E : Type*} [MeasurableSpace α] [TopologicalSpace α] [NormedRing E] [NormedAlgebra ℝ E]
+
+/-- A subalgebra `A` of the bounded continuous function from `α` to `E` is separating in the
+probability measures if for all probability measures `μ ≠ ν`, there exists `f ∈ A` such that
+`∫ x, f x ∂μ ≠ ∫ x, f x ∂ν`. -/
+structure Separating (A : Subalgebra ℝ (α →ᵇ E)) : Prop :=
+(exists_ne : ∀ ⦃μ ν : ProbabilityMeasure α⦄, μ ≠ ν → ∃ f ∈ A, ∫ x, f x ∂μ ≠ ∫ x, f x ∂ν)
+
+lemma ProbabilityMeasure.ext_of_Separating {μ ν : ProbabilityMeasure α} {A : Subalgebra ℝ (α →ᵇ E)}
+    (hA : Separating A) (h : ∀ f ∈ A, ∫ x, f x ∂μ = ∫ x, f x ∂ν) :
+    μ = ν := by
+  by_contra h_ne
+  obtain ⟨f, hfA, hf_ne⟩ := hA.exists_ne h_ne
+  exact hf_ne (h f hfA)
+
+end MeasureTheory
diff --git a/Clt/Tight.lean b/Clt/Tight.lean
index e69de29..8cc8300 100644
--- a/Clt/Tight.lean
+++ b/Clt/Tight.lean
@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2023 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+import Mathlib.MeasureTheory.Measure.Regular
+
+/-!
+# Characteristic function of a measure
+
+## Main definitions
+
+* `Tight`: A set `S` of measures is tight if for all `0 < ε`, there exists `K` compact such that
+  for all `μ` in `S`, `μ Kᶜ ≤ ε`.
+
+## Main statements
+
+* `fooBar_unique`
+
+## Notation
+
+
+
+## Implementation details
+
+
+
+-/
+
+open scoped ENNReal
+
+namespace MeasureTheory
+
+variable {α : Type*} {mα : MeasurableSpace α} {μ : Measure α}
+  [TopologicalSpace α]
+
+/-- A set `S` of measures is tight if for all `0 < ε`, there exists `K` compact such that for all
+`μ` in `S`, `μ Kᶜ ≤ ε`. -/
+def Tight (S : Set (Measure α)) : Prop :=
+  ∀ ε : ℝ≥0∞, 0 < ε → ∃ K : Set α, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
+
+-- TODO: the T2Space hypothesis is here only to make compact sets closed. It could be removed if
+-- InnerRegular was about compact and closed sets, and not only compact sets.
+lemma tight_singleton [T2Space α] [OpensMeasurableSpace α]
+    (μ : Measure α) [IsFiniteMeasure μ] [μ.InnerRegular] :
+    Tight {μ} := by
+  cases eq_zero_or_neZero μ with
+  | inl hμ =>
+    rw [hμ]
+    refine fun _ _ ↦ ⟨∅, isCompact_empty, ?_⟩
+    simp
+  | inr hμ =>
+    let r := μ Set.univ
+    have hr : 0 < r := by simp [hμ.out]
+    intro ε hε
+    cases lt_or_ge ε r with
+    | inl hεr =>
+      have hεr' : r - ε < r := ENNReal.sub_lt_self (measure_ne_top μ _) hr.ne' hε.ne'
+      obtain ⟨K, _, hK_compact, hKμ⟩ :=
+        (MeasurableSet.univ : MeasurableSet (Set.univ : Set α)).exists_lt_isCompact hεr'
+      refine ⟨K, hK_compact, fun μ' hμ' ↦ ?_⟩
+      simp only [Set.mem_singleton_iff] at hμ'
+      rw [hμ', measure_compl hK_compact.isClosed.measurableSet (measure_ne_top μ _),
+        tsub_le_iff_right]
+      rw [ENNReal.sub_lt_iff_lt_right (ne_top_of_lt hεr) hεr.le, add_comm] at hKμ
+      exact hKμ.le
+    | inr hεr =>
+      refine ⟨∅, isCompact_empty, ?_⟩
+      intro μ' hμ'
+      simp only [Set.mem_singleton_iff] at hμ'
+      rw [hμ', Set.compl_empty]
+      exact hεr
+
+end MeasureTheory
diff --git a/blueprint/src/chapter/separating.tex b/blueprint/src/chapter/separating.tex
index 6c03098..235aca4 100644
--- a/blueprint/src/chapter/separating.tex
+++ b/blueprint/src/chapter/separating.tex
@@ -6,6 +6,7 @@ \chapter{Separating subalgebras}
 \end{definition}
 
 \begin{definition}\label{def:separating}
+\lean{MeasureTheory.Separating} \leanok
 A set $\mathcal F$ of functions $E \to F$ is separating in $\mathcal P(E)$ if for all probability measures $\mu, \nu$ on $E$ with $\mu \ne \nu$, there exists $f \in \mathcal F$ with $\mu[f] \ne \nu[f]$.
 \end{definition}
 
@@ -93,6 +94,7 @@ \chapter{Separating subalgebras}
 \end{proof}
 
 \begin{lemma}\label{lem:Cb_eq_of_separating}
+\uses{def:separates_points}
 Let $\mathcal A$ be a subalgebra of $C_b(E, \mathbb{C})$ that separates points. Let $\mu, \nu$ be two probability measures. If for all $f \in \mathcal A$, $\mu[f] = \nu[f]$, then for all $g \in C_b(E, \mathbb{C})$, $\mu[g] = \nu[g]$.
 \end{lemma}
 
@@ -115,7 +117,6 @@ \chapter{Separating subalgebras}
 \end{proof}
 
 \begin{theorem}[Subalgebras separating points]\label{thm:separating_starSubalgebra}
-\uses{def:separates_points}
 Let $E$ be a complete separable pseudo-metric space. Let $\mathcal A \subseteq C_b(E, \mathbb{C})$ be a star-subalgebra that separates points. Then $\mathcal A$ is separating in $\mathcal P(E)$.
 \end{theorem}
 
diff --git a/blueprint/src/chapter/tight.tex b/blueprint/src/chapter/tight.tex
index f64fb82..47330a7 100644
--- a/blueprint/src/chapter/tight.tex
+++ b/blueprint/src/chapter/tight.tex
@@ -1,7 +1,8 @@
 \chapter{Tight families of measures}
 
 \begin{definition}\label{def:tight}
-A set $S$ of measures on $\Omega$ is tight if for all $\varepsilon > 0$ there exists a compact set $K$ such that for all $\mu \in S$, $\mu(\Omega \setminus K) \le \varepsilon$.
+\lean{MeasureTheory.Tight} \leanok
+A set $S$ of measures on $\Omega$ is tight if for all $\varepsilon > 0$ there exists a compact set $K$ such that for all $\mu \in S$, $\mu(K^c) \le \varepsilon$.
 \end{definition}
 
 \begin{lemma}\label{lem:tight_of_cvg}