Documentation
Atlas
.
BooleanFunctions
.
code
.
NoiseSemigroup
Search
return to top
source
Imports
Init
Atlas.BooleanFunctions.code.Stability
Imported by
BooleanFourier
.
fourierCoeff_noiseOperator
BooleanFourier
.
noiseOperator_comp
source
theorem
BooleanFourier
.
fourierCoeff_noiseOperator
{
n
:
ℕ
}
(
ρ
:
ℝ
)
(
f
:
(
Fin
n
→
Bool
)
→
ℝ
)
(
S
:
Finset
(
Fin
n
)
)
:
fourierCoeff
(
noiseOperator
ρ
f
)
S
=
ρ
^
S
.
card
*
fourierCoeff
f
S
source
theorem
BooleanFourier
.
noiseOperator_comp
{
n
:
ℕ
}
(
ρ
σ
:
ℝ
)
(
f
:
(
Fin
n
→
Bool
)
→
ℝ
)
:
noiseOperator
ρ
(
noiseOperator
σ
f
)
=
noiseOperator
(
ρ
*
σ
)
f