OAI/Probability/InvariantIsing/Arrays/TensorAmplitudeComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A continuous covariance modulus in the actual Gaussian perturbation amplitudes.

  1. lemma OAI.InvariantIsing.spinTensorFeature_mixed_amplitude_covariance line 14
  2. lemma OAI.InvariantIsing.tensorPath_amplitude_increment_cross_le line 43
  3. def OAI.InvariantIsing.tensorAmplitudeModulus line 101
  4. lemma OAI.InvariantIsing.tensorPathLogMean_amplitude_comparison line 104
  5. lemma OAI.InvariantIsing.tensorPathPressure_amplitude_comparison line 130