OAI/Probability/InvariantIsing/Gaussian/GaussianPatternEuclideanNorm.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The Euclidean operator norm of the physical Gaussian array is 1-Lipschitz.

  1. def OAI.InvariantIsing.gaussianPatternEuclideanOperator line 11
  2. lemma OAI.InvariantIsing.gaussianPattern_frobenius line 16
  3. lemma OAI.InvariantIsing.gaussianPatternEuclideanOperator_bound line 23
  4. lemma OAI.InvariantIsing.gaussianPatternEuclideanOperator_norm_le line 32
  5. lemma OAI.InvariantIsing.gaussianPatternEuclideanOperator_sub line 37
  6. def OAI.InvariantIsing.gaussianPatternSingularMax line 45
  7. theorem OAI.InvariantIsing.gaussianPatternSingularMax_lipschitz line 48