OAI/Analysis/CircleDomains/Probability/NullLevelTuples.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Null sets of scalar levels induce null sets of finite tagged tuples. This also supplies a Borel description when the null sets are envelopes.

  1. theorem OAI.CircleDomainRigidity.measurableEmbedding_tupleFiber line 14
  2. theorem OAI.CircleDomainRigidity.levelTuple_eq_iUnion_fibers line 22
  3. theorem OAI.CircleDomainRigidity.measurableSet_levelTuple_of_fibers line 33
  4. def OAI.CircleDomainRigidity.tuplesWithBadLevel line 38
  5. theorem OAI.CircleDomainRigidity.measurableSet_tuplesWithBadLevel line 41
  6. theorem OAI.CircleDomainRigidity.tupleReference_badLevel_null line 49
  7. theorem OAI.CircleDomainRigidity.ae_slots_zero_on_null_tuples line 71
  8. theorem OAI.CircleDomainRigidity.no_tag_level_in_null_set line 83