OAI/NumberTheory/TwoPoint/Bounds/DeletionNormalization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Normalize the three deletion costs by the exact padding and tuple masses. The rare-site term uses only S*V ≥ 1.

  1. lemma OAI.TwoPointCorrelations.normalize_three_deletion_costs line 11
  2. lemma OAI.TwoPointCorrelations.normalize_endpoint_deletion_costs line 28