OAI/Probability/InvariantIsing/Spectral/MeasureWeakResolvent.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Resolvent continuity under weak convergence and convergence of upper edges. Bounded continuous test functions avoid the pole outside the supports.

  1. theorem OAI.InvariantIsing.measureResolvent_tendsto_weak line 14
  2. theorem OAI.InvariantIsing.measureInverse_tendsto_weak line 55