OAI/Probability/InvariantIsing/Arrays/NSpinComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Haar-direction comparison for the actual enriched Ising recursion.

  1. theorem OAI.InvariantIsing.vectorCascade_terminal_comparison line 15
  2. theorem OAI.InvariantIsing.abs_rotatedCascadeValue_sub_rotation_le line 55
  3. theorem OAI.InvariantIsing.abs_rotatedEnrichedPressure_sub_rotation_le line 73