PriorPerturbationVariance.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform concentration of the actual finite perturbation for a fixed constrained prior. No full-cube symmetry is used in this estimate.