OAI/Probability/InvariantIsing/Core/UnitBilinearNorm.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The Euclidean operator norm as the supremum of unit bilinear tests.

  1. abbrev OAI.InvariantIsing.UnitVector line 12
  2. lemma OAI.InvariantIsing.unitVector_nonempty line 14
  3. lemma OAI.InvariantIsing.unitBilinear_le_norm line 19
  4. theorem OAI.InvariantIsing.norm_eq_iSup_unitBilinear line 28
  5. lemma OAI.InvariantIsing.gaussianPattern_unitBilinear line 58