OAI/Probability/InvariantIsing/Spectral/MeasureMagneticTransport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The field transportation bound extends from finite spectral laws to every compact spectral law by uniform transform approximation.

  1. theorem OAI.InvariantIsing.measureMagnetic_transport_le line 13