OAI/Probability/InvariantIsing/Pressure/PressureLipschitz.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Frobenius continuity of Haar pressure

The Lipschitz constant is independent of dimension and of a deterministic magnetic field. This is the finite-volume estimate required to apply the published SO(N) concentration input.

  1. lemma OAI.InvariantIsing.specialRotation_spin_dist_sq_le line 20
  2. lemma OAI.InvariantIsing.abs_rotatedEnergy_sub_rotation_le line 41
  3. lemma OAI.InvariantIsing.abs_rotatedPressure_sub_rotation_le line 99