OAI/Probability/InvariantIsing/Gaussian/GaussianConeCutoff.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Compact scalar cutoffs preserving the exact Lipschitz constant.

  1. def OAI.InvariantIsing.gaussianCone line 11
  2. def OAI.InvariantIsing.gaussianConeCutoff line 14
  3. lemma OAI.InvariantIsing.gaussianCone_nonneg line 18
  4. lemma OAI.InvariantIsing.gaussianCone_lipschitz line 21
  5. lemma OAI.InvariantIsing.gaussianConeCutoff_lipschitz line 34
  6. lemma OAI.InvariantIsing.gaussianConeCutoff_zero line 41
  7. lemma OAI.InvariantIsing.gaussianConeCutoff_compact line 48
  8. lemma OAI.InvariantIsing.gaussianConeCutoff_norm_le line 56
  9. lemma OAI.InvariantIsing.gaussianConeCutoff_eq line 71