add charFun docstring

RemyDegenne · Dec 28, 2023 · 08c92f5 · 08c92f5
1 parent faa9014
commit 08c92f5
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Clt/CharFun.lean b/Clt/CharFun.lean
@@ -69,6 +69,7 @@ namespace ProbabilityTheory
 
 variable {E : Type*} [MeasurableSpace E]
 
+/-- The characteristic function of a measure. -/
 noncomputable
 def charFun [Inner ℝ E] (μ : Measure E) (t : E) : ℂ := ∫ x, exp (⟪t, x⟫ • I) ∂μ