OAI/GroupTheory/SimpleAmenable/RandomFields/SignalCutoff.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.scaledSiteConjugate_displacement line 15
2. theorem OAI.SimpleAmenable.flagSignalDifference_ne_zero_near line 29
3. theorem OAI.SimpleAmenable.flagSignalDifference_cutoff line 50
4. theorem OAI.SimpleAmenable.compactSignal_amplitude line 68
5. theorem OAI.SimpleAmenable.flagAveragingMatrix_row_sum line 90
6. theorem OAI.SimpleAmenable.flagAveragingMatrix_row_sum_uniform line 113
7. theorem OAI.SimpleAmenable.flagAveragingMatrix_crude_error line 126