OAI/Probability/InvariantIsing/Spectral/FiniteSpectralMeasure.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The general measure transform agrees with the finite-alphabet transform. Positive masses ensure that the upper edge is an atom and the inverse is uncapped.

  1. def OAI.InvariantIsing.finiteSpectralMeasure line 16

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:123 (different declaration text). Qualify references as OAI.InvariantIsing.finiteSpectralMeasure@path.

  2. theorem OAI.InvariantIsing.finiteSpectralMeasure_probability line 19

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:126 (different declaration text). Qualify references as OAI.InvariantIsing.finiteSpectralMeasure_probability@path.

  3. theorem OAI.InvariantIsing.integral_finiteSpectralMeasure line 25
  4. theorem OAI.InvariantIsing.ae_finiteSpectralMeasure line 34
  5. theorem OAI.InvariantIsing.measureResolvent_finiteSpectralMeasure line 42
  6. theorem OAI.InvariantIsing.measureR_finiteSpectralMeasure line 47