OAI/Probability/FreeIsing/Trees/WeightedShellSummation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.regularPathWeight_le_closed_threshold line 9
  2. theorem OAI.Problem367.summable_and_tsum_shell_le_path line 16
  3. theorem OAI.Problem367.shell_noise_drift_le_path_sums line 40