Documentation
Atlas
.
BooleanFunctions
.
code
.
SpectralSample
Search
return to top
source
Imports
Init
Atlas.BooleanFunctions.code.FourierExpansion
Mathlib.Probability.ProbabilityMassFunction.Constructions
Imported by
BooleanFourier
.
fourierWeight
BooleanFourier
.
spectralDist
source
noncomputable def
BooleanFourier
.
fourierWeight
{
n
:
ℕ
}
(
f
:
(
Fin
n
→
Bool
)
→
ℝ
)
(
S
:
Finset
(
Fin
n
)
)
:
ENNReal
Instances For
source
noncomputable def
BooleanFourier
.
spectralDist
{
n
:
ℕ
}
(
f
:
(
Fin
n
→
Bool
)
→
ℝ
)
(
hf
:
∑
S
:
Finset
(
Fin
n
)
,
fourierCoeff
f
S
^
2
=
1
)
:
PMF
(
Finset
(
Fin
n
)
)
Instances For