OAI/NumberTheory/DukePrimeDegree/Geometry/NestedRectangleRestriction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The real marginal after restricting an independent physical window

  1. theorem OAI.DukePrimeDegree.independent_restrict_real_marginal line 15