OAI/NumberTheory/DukePrimeDegree/Entropy/ConditionalInformationLowerBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Whole-future conditional information is bounded by metric entropy

Finite present clips have their own, smaller future sigma algebra. Conditioning on the full countable future and further transverse data only decreases their entropy. Passing to the proved clipping limit gives the bound without a finite Shannon entropy assumption on the countable observation.

  1. lemma OAI.DukePrimeDegree.clipped_future_sigma_le line 24
  2. theorem OAI.DukePrimeDegree.conditionalInformation_integral_le_metricEntropy line 47