`BookProof.ChapterSolovayCoordinates.finiteCoordinateMarginal` (I : Finset ℕ) : Measure.map I.restrict coordinateTailMeasure = Measure.pi (fun _ : I => standardGaussian)

Initializing...

`BookProof.ChapterSolovayCoordinates.finiteCoordinateMarginal` (I : Finset ℕ) : Measure.map I.restrict coordinateTailMeasure = Measure.pi (fun _ : I => standardGaussian) · Prove2Me