OAI/Probability/FreeIsing/Critical/NoisePathConstants.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.half_path_cut_admissible line 9
  2. def OAI.Problem367.criticalNoiseEta line 25
  3. def OAI.Problem367.criticalNoiseLengthConstant line 29
  4. def OAI.Problem367.criticalNoiseTailBase line 32
  5. theorem OAI.Problem367.criticalNoise_constants_positive line 34
  6. theorem OAI.Problem367.criticalNoise_length_admissible line 54
  7. theorem OAI.Problem367.criticalNoise_threshold_eq line 76
  8. theorem OAI.Problem367.criticalNoise_tail_eq line 80