OAI/Probability/InvariantIsing/Cavity/CavityCanonicalHaarLog.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual canonical fresh-group logarithmic observable and its finite-volume measurability and boundedness.

  1. lemma OAI.InvariantIsing.cavity_canonical_group_projection_bound line 16
  2. def OAI.InvariantIsing.cavityCanonicalHaarLog line 30
  3. lemma OAI.InvariantIsing.measurable_cavityCanonicalHaarLog line 45
  4. lemma OAI.InvariantIsing.cavityCanonicalHaarLog_bound line 54