OAI/Probability/InvariantIsing/Spectral/CompactResolventTests.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Positive resolvents as a separating family for compact nonnegative spectral laws.

  1. def OAI.InvariantIsing.compactResolventTest line 11
  2. lemma OAI.InvariantIsing.compactResolventTests_separate line 16
  3. theorem OAI.InvariantIsing.compact_resolvent_tendstoInMeasure line 37