OAI/NumberTheory/DukePrimeDegree/Entropy/RootPrefixTubeInformation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Diagonal-tube information in actual conditional leaves

The local-to-ambient integral below keeps the restriction to the box range. In particular, it does not replace a restricted integral by a global mean without a further argument.

  1. def OAI.DukePrimeDegree.RootPrefixBox.leafBackwardTubeInformation line 26
  2. theorem OAI.DukePrimeDegree.RootPrefixBox.ae_leafBackwardTubeInformation_eq line 33
  3. theorem OAI.DukePrimeDegree.RootPrefixBox.integrable_leafBackwardTubeInformation line 45
  4. theorem OAI.DukePrimeDegree.RootPrefixBox.integral_leafBackwardTubeInformation line 60