OAI/Probability/InvariantIsing/Gaussian/GaussianPatternNorms.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact finite Gaussian norm and minimum identities.

  1. def OAI.InvariantIsing.gaussianPatternColumn line 14

    Also declared: ComparatorChallenges/InvariantIsing.lean:274 (same declaration text).

  2. lemma OAI.InvariantIsing.gaussianPatternSum_eq_sum line 17
  3. def OAI.InvariantIsing.gaussianPatternOperator line 23

    Also declared: ComparatorChallenges/InvariantIsing.lean:277 (same declaration text).

  4. def OAI.InvariantIsing.gaussianPatternTransposeOperator line 28
  5. lemma OAI.InvariantIsing.gaussianPattern_transpose_norm line 34
  6. lemma OAI.InvariantIsing.gaussianPatternOperator_spin line 43
  7. lemma OAI.InvariantIsing.gaussianPatternOperator_norm line 46
  8. lemma OAI.InvariantIsing.gaussianPattern_max_sqrt line 50
  9. lemma OAI.InvariantIsing.gaussianPattern_min_sqrt line 61