OAI/NumberTheory/DukePrimeDegree/Entropy/FutureRestrictionNull.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing a box restriction with only a null-set exception

For future-kernel gluing it suffices that the future measure outside a box vanishes. Literal containment of every point in the fiber is stronger than necessary.

  1. theorem OAI.DukePrimeDegree.normalized_restriction_of_null_diff line 19