Documentation
Atlas
.
BooleanFunctions
.
code
.
PBiased
Search
return to top
source
Imports
Init
Mathlib.MeasureTheory.Constructions.Pi
Mathlib.Probability.ProbabilityMassFunction.Constructions
Imported by
BooleanFourier
.
pBiasedBit
BooleanFourier
.
pBiasedBit
.
instIsProbabilityMeasure
BooleanFourier
.
pBiasedMeasure
BooleanFourier
.
pBiasedMeasure
.
instIsProbabilityMeasure
source
noncomputable def
BooleanFourier
.
pBiasedBit
(
p
:
NNReal
)
(
hp
:
p
≤
1
)
:
MeasureTheory.Measure
Bool
Instances For
source
instance
BooleanFourier
.
pBiasedBit
.
instIsProbabilityMeasure
(
p
:
NNReal
)
(
hp
:
p
≤
1
)
:
MeasureTheory.IsProbabilityMeasure
(
pBiasedBit
p
hp
)
source
noncomputable def
BooleanFourier
.
pBiasedMeasure
(
n
:
ℕ
)
(
p
:
NNReal
)
(
hp
:
p
≤
1
)
:
MeasureTheory.Measure
(
Fin
n
→
Bool
)
Instances For
source
instance
BooleanFourier
.
pBiasedMeasure
.
instIsProbabilityMeasure
(
n
:
ℕ
)
(
p
:
NNReal
)
(
hp
:
p
≤
1
)
:
MeasureTheory.IsProbabilityMeasure
(
pBiasedMeasure
n
p
hp
)