OAI/Probability/InvariantIsing/Spectral/SpectralPathLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

L1 approximation of the trial path preserves the finite spectral interaction functional, as required when removing a finite partition.

  1. lemma OAI.InvariantIsing.finiteTemperatureFunctional_tendsto_of_L1 line 14