OAI/Probability/FreeIsing/Spectral/NoisyLawSpectral.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem367.NoisyLawSpectral.law line 12
2. theorem OAI.Problem367.NoisyLawSpectral.local_koopman_far_decay line 16
3. theorem OAI.Problem367.NoisyLawSpectral.localCriticalDecay line 66
4. theorem OAI.Problem367.NoisyLawSpectral.centeredAverage_norm_le_critical line 79