OAI/Analysis/CircleDomains/Probability/FiniteTupleLevelLaws.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The single-level conclusions pass to each finite prior union, with its actual product Haar law and the sum of the expected counts.

  1. theorem OAI.CircleDomainRigidity.pathImageCount_iUnion_le_sum line 22
  2. theorem OAI.CircleDomainRigidity.ae_finite_tuple_level_law line 31