OAI/Probability/InvariantIsing/Spectral/MeasureRBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compact-support estimates for the general spectral transform.

  1. lemma OAI.InvariantIsing.integrable_spectralCoordinate line 13
  2. theorem OAI.InvariantIsing.measureR_bounds_all line 23
  3. theorem OAI.InvariantIsing.measureInverse_uncapped_small line 37
  4. theorem OAI.InvariantIsing.measureR_sub_mean_identity line 52
  5. theorem OAI.InvariantIsing.measureR_sub_mean_bound line 90
  6. theorem OAI.InvariantIsing.continuousAt_measureR_zero line 133
  7. theorem OAI.InvariantIsing.continuous_measureR line 152