OAI/Analysis/CircleDomains/Probability/CountableSquareLawBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Countably prescribed visit bounds define a Borel family of laws and are preserved under probability mixtures.

  1. def OAI.CircleDomainRigidity.CountableSquareLawBounds line 17
  2. theorem OAI.CircleDomainRigidity.measurableSet_countableSquareLawBounds line 21
  3. theorem OAI.CircleDomainRigidity.CountableSquareLawBounds.mixture line 31