Skip to content

Commit ba28b6a

Browse files
LLaurancebryangingechen
authored andcommitted
chore(Probability): remove TODO on characteristic functions (leanprover-community#40595)
mathlib4 now has Fourier transforms and the characteristic function is defined at [`MeasureTheory.charFun`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/CharacteristicFunction/Basic.html#MeasureTheory.charFun).
1 parent 8ff09d9 commit ba28b6a

1 file changed

Lines changed: 0 additions & 6 deletions

File tree

Mathlib/Probability/Density.lean

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -43,12 +43,6 @@ random variables with this distribution.
4343
* `MeasureTheory.pdf.IsUniform.integral_eq` : If `X` follows the uniform distribution with
4444
its pdf having support `s`, then `X` has expectation `(λ s)⁻¹ * ∫ x in s, x dx` where `λ`
4545
is the Lebesgue measure.
46-
47-
## TODO
48-
49-
Ultimately, we would also like to define characteristic functions to describe distributions as
50-
it exists for all random variables. However, to define this, we will need Fourier transforms
51-
which we currently do not have.
5246
-/
5347

5448
@[expose] public section

0 commit comments

Comments
 (0)