OAI/NumberTheory/DukePrimeDegree/Entropy/RootPrefixFiniteEntropy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite future conditioning in actual root boxes

After recording a finite observation as well as the transverse coordinate, the entropy is computed by the actual intrinsic product at the sampled point, restricted and normalized on its observed fiber.

  1. theorem OAI.DukePrimeDegree.RootPrefixBox.conditionalEntropy_transverse_label_intrinsicProduct line 26