OAI/Probability/FreeIsing/Ising/CopyShellEnergies.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.nonnegativeShellSup line 12
  2. theorem OAI.Problem367.nonnegativeShellSup_nonneg line 17
  3. theorem OAI.Problem367.le_nonnegativeShellSup line 23
  4. theorem OAI.Problem367.nonnegativeShellSup_le line 29
  5. def OAI.Problem367.IsingCopyResponseRowPaths.noiseShellEnergy line 46
  6. def OAI.Problem367.IsingCopyResponseRowPaths.linearShellEnergy line 49
  7. theorem OAI.Problem367.IsingCopyResponseRowPaths.pathCavityProduct_eq_pathProduct line 52
  8. theorem OAI.Problem367.IsingCopyResponseRowPaths.pathCavityLogSum_eq_pathLogDiff line 61
  9. theorem OAI.Problem367.IsingCopyResponseRowPaths.linearEnergy_le_siteVariance line 75
  10. theorem OAI.Problem367.IsingCopyResponseRowPaths.exists_short_shell_energy_bounds line 88