OAI/Analysis/CircleDomains/Probability/TupleProductNull.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Null events on every pair of finite level-torus fibers are null for the actual positive weighted tuple reference measure.

  1. theorem OAI.CircleDomainRigidity.tupleReference_product_null line 14