OAI/Analysis/CircleDomains/Probability/LevelLawQuantifiers.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite expected counts make the free-avoidance statement available with the independent level chosen first. This uses Borel count inequalities and does not assume measurability of the raw free-incidence event.

  1. theorem OAI.CircleDomainRigidity.ae_level_parameter_free_avoidance line 20