OAI/Probability/InvariantIsing/Spectral/SpectralComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Monotonicity and scalar shifts for the pointwise and mean pressures. These are the finite-volume squeeze estimates used in spectral discretization.

  1. lemma OAI.InvariantIsing.rotatedEnergy_mono line 14
  2. lemma OAI.InvariantIsing.rotatedPressure_mono line 21
  3. lemma OAI.InvariantIsing.rotatedEnergy_add_scalar line 31
  4. lemma OAI.InvariantIsing.rotatedPressure_add_scalar line 38
  5. lemma OAI.InvariantIsing.meanPressure_add_scalar line 51
  6. lemma OAI.InvariantIsing.meanPressure_squeeze line 60