OAI/Analysis/CircleDomains/Probability/ParametricNullTuples.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Borel scalar-level envelopes remain Borel after forming finite tuples and active slots, also when they depend on an earlier sampled path.

  1. def OAI.CircleDomainRigidity.badTupleGraph line 16
  2. theorem OAI.CircleDomainRigidity.measurableSet_badTupleGraph line 19
  3. def OAI.CircleDomainRigidity.badSlotGraph line 43
  4. theorem OAI.CircleDomainRigidity.measurableSet_badSlotGraph line 46