Merge pull request #3 from RemyDegenne/tight

Add def of Separating

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

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

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}