OAI/Probability/InvariantIsing/Spectral/MeasureSpectralContinuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Spectral-transform continuity for compactly supported laws, including the zero argument and the upper-edge branch.

  1. theorem OAI.InvariantIsing.spectralMean_tendsto_weak line 14
  2. theorem OAI.InvariantIsing.measureR_tendsto_weak_pos line 40
  3. theorem OAI.InvariantIsing.measureR_tendsto_weak_zero line 60