OAI/NumberTheory/DukePrimeDegree/Geometry/RootPrefixStationaryImages.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Transferring local stationarity through actual quotient boxes

The image restriction is the pushforward of the coordinate restriction. Consequently a local integral identity for one ambient Markov kernel gives a stationary restriction of the original ambient measure.

  1. theorem OAI.DukePrimeDegree.RootPrefixBox.measurableSet_param_image line 26
  2. theorem OAI.DukePrimeDegree.RootPrefixBox.stationary_image_of_local_integrals line 42
  3. theorem OAI.DukePrimeDegree.RootPrefixBox.stationary_image_of_local_event line 66