OAI/Probability/InvariantIsing/Spectral/PositiveResolventBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform trace and quadratic bounds for positive resolvents.

  1. lemma OAI.InvariantIsing.positiveResolvent_trace_le line 11
  2. lemma OAI.InvariantIsing.positiveResolvent_quadratic_le line 21
  3. lemma OAI.InvariantIsing.positiveResolvent_quadratic_nonneg line 34
  4. lemma OAI.InvariantIsing.positiveResolvent_normalized_abs_bound line 42