OAI/Analysis/CircleDomains/Selection/TupleReference.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The tuple reference measure is a positive weighted sum of Lebesgue measures on the finite tuple tori, indexed by label type rather than slot.

  1. abbrev OAI.CircleDomainRigidity.TupleType line 15
  2. def OAI.CircleDomainRigidity.tupleFiber line 17
  3. theorem OAI.CircleDomainRigidity.continuous_tupleFiber line 20
  4. theorem OAI.CircleDomainRigidity.measurable_tupleFiber line 23
  5. def OAI.CircleDomainRigidity.tupleReference line 27
  6. theorem OAI.CircleDomainRigidity.tupleReference_apply line 30
  7. theorem OAI.CircleDomainRigidity.tupleReference_univ line 36
  8. theorem OAI.CircleDomainRigidity.finite_tupleReference line 47
  9. theorem OAI.CircleDomainRigidity.lintegral_tupleReference line 50
  10. theorem OAI.CircleDomainRigidity.tupleReference_fiber_null line 58
  11. theorem OAI.CircleDomainRigidity.null_tupleInfiniteExclusions line 65