OAI/NumberTheory/DukePrimeDegree/Entropy/FutureKernelCovariance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Covariance of the actual normalized future measures

  1. lemma OAI.DukePrimeDegree.normalized_restriction_after_normalize_map line 16
  2. theorem OAI.DukePrimeDegree.EliminationChain.ae_normalizedFuture_diagonal line 31
  3. def OAI.DukePrimeDegree.EliminationChain.ambientFutureMeasure line 62
  4. theorem OAI.DukePrimeDegree.EliminationChain.ae_ambientFuture_diagonal line 73
  5. def OAI.DukePrimeDegree.delayedFutureKernel line 100
  6. instance OAI.DukePrimeDegree.delayedFutureKernel_markov line 106
  7. theorem OAI.DukePrimeDegree.delayedFutureKernel_spec line 115