OAI/NumberTheory/DukePrimeDegree/Entropy/ConditionalRectangleProducts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normalized conditional products on actual rectangles

  1. lemma OAI.DukePrimeDegree.probability_eq_prod_marginals_of_prod line 14
  2. theorem OAI.DukePrimeDegree.conditional_restrict_rectangle_product line 24
  3. theorem OAI.DukePrimeDegree.exists_remainingRoot_independent_box line 57