OAI/NumberTheory/TwoPoint/Walks/CanonicalRareDeletion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Canonical prohibited-site deletion with all prime-family, circuit, and rare-event hypotheses supplied by the actual bands and bin family.

  1. def OAI.TwoPointCorrelations.canonicalPairPadding line 14
  2. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_canonical_rare_deletion line 18