OAI/NumberTheory/TwoPoint/Walks/SegmentedWitnessDecay.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Include every main/witness segment record in the singleton decay estimate.

  1. theorem OAI.TwoPointCorrelations.eventually_segmented_witness_decay line 13