OAI/NumberTheory/DukePrimeDegree/Geometry/RootPrefixAmbientStationarity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local stationarity of the ambient whole-future law

On a future-measurable event whose complete future fibers fit in the box, the actual normalized intrinsic law on the ambient root orbit recovers every ambient measurable event. This retains the local event needed for gluing and makes no global stationarity assumption.

  1. theorem OAI.DukePrimeDegree.RootPrefixBox.setIntegral_ambient_wholeFuture_probability line 29