RetainedMainProbability.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Baseline tuple reciprocals and the retained padding event pay every main prime exactly once.

theorem OAI.TwoPointCorrelations.tuple_weight_mul_retained_main_probability_le line 12