@[reducible, inline]

abbrev CommunicationComplexity.CoinTape (n : ℕ) : Type

Equations

• CommunicationComplexity.CoinTape n = (Fin n → Bool)

noncomputable instance CommunicationComplexity.coinTapeMeasure (n : ℕ) : MeasureTheory.MeasureSpace (CoinTape n)

The uniform probability measure on CoinTape n. Every outcome of n independent fair coin flips is equally likely.

Equations

• CommunicationComplexity.coinTapeMeasure n = { toMeasurableSpace := MeasurableSpace.pi, volume := ProbabilityTheory.uniformOn Set.univ }

instance CommunicationComplexity.coinTapeIsProbabilityMeasure (n : ℕ) : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

noncomputable instance CommunicationComplexity.coinTapeFiniteProbabilitySpace (n : ℕ) : FiniteProbabilitySpace (CoinTape n)

Equations

• CommunicationComplexity.coinTapeFiniteProbabilitySpace n = CommunicationComplexity.FiniteProbabilitySpace.of (CommunicationComplexity.CoinTape n)