OAI/NumberTheory/JointDickman/Probability/RemainingSplitRegularity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Regularity loss under the actual conditional fair-split law

  1. theorem OAI.JointDickman.fair_selected_remaining_regularity_loss line 13