OAI/Analysis/CircleDomains/Probability/DelayedTupleMeasure.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Delaying tags scales their weighted tuple measure, allowing every finite tuple cost of a fixed allowed path to become arbitrarily small.

  1. theorem OAI.CircleDomainRigidity.slotWeight_add line 15
  2. theorem OAI.CircleDomainRigidity.weightedTupleMeasure_delay line 18
  3. theorem OAI.CircleDomainRigidity.lintegral_weightedTupleMeasure_delay line 42
  4. theorem OAI.CircleDomainRigidity.tendsto_delayedTupleCost line 48