OAI/NumberTheory/DukePrimeDegree/Entropy/WholeFutureSelfConditional.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Self-consistency of the global root-future kernel

Local self-consistency on a countable atlas passes to the actual ambient kernel. Together with stationarity this identifies its conditional law.

  1. theorem OAI.DukePrimeDegree.RootPrefixCoordinates.wholeFutureKernel_self_constant line 25