Merge pull request #1 from RemyDegenne/PR_test

Add charFun docstring
RemyDegenne · Dec 28, 2023 · 1c9802b · 1c9802b
2 parents a1bdad6 + bfb095f
commit 1c9802b
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) ∂μ