OAI/Probability/InvariantIsing/Spectral/MeasureResolvent.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The resolvent and the edge-capped inverse for a general spectral law. The upper edge is an explicit parameter; the hypotheses below say that the law is supported below it. No inverse is assumed to exist at the edge.

  1. def OAI.InvariantIsing.measureResolvent line 15

    Also declared: ComparatorChallenges/InvariantIsing.lean:115 (same declaration text).

  2. def OAI.InvariantIsing.measureInverse line 17

    Also declared: ComparatorChallenges/InvariantIsing.lean:117 (same declaration text).

  3. def OAI.InvariantIsing.measureR line 20

    Also declared: ComparatorChallenges/InvariantIsing.lean:120 (same declaration text).

  4. lemma OAI.InvariantIsing.measurable_resolventKernel line 23
  5. lemma OAI.InvariantIsing.resolventKernel_bound line 26
  6. lemma OAI.InvariantIsing.integrable_resolventKernel line 31
  7. lemma OAI.InvariantIsing.measureResolvent_le line 38
  8. lemma OAI.InvariantIsing.le_measureResolvent line 46
  9. theorem OAI.InvariantIsing.measureResolvent_strictAnti line 56
  10. theorem OAI.InvariantIsing.continuousAt_measureResolvent line 70
  11. theorem OAI.InvariantIsing.exists_measureResolvent_solution line 88
  12. theorem OAI.InvariantIsing.measureInverse_eq_of_solution line 103
  13. theorem OAI.InvariantIsing.measureInverse_bounds line 116
  14. theorem OAI.InvariantIsing.measureR_bounds line 131