OAI/Analysis/CircleDomains/Probability/RandomShifts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Independent uniform grid shifts

The shifts have normalized interval distribution. Any two distinct labels have product law, so the two-shift integral equals their expected wedge cost.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.shiftLaw line 22
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.shiftLaw_eq line 24
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.shiftLaw_isProbabilityMeasure line 28
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_shiftLaw_pair line 34
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.measurePreserving_grid_pair line 46
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_grid_pair line 58