OAI/Probability/FreeIsing/Trees/ResponseRowEnergy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.ResponseRows.summable_weighted_tree_profile line 11
  2. theorem OAI.Problem367.ResponseRows.tsum_weighted_tree_profile line 23
  3. def OAI.Problem367.ResponseRows.shellProfile line 41
  4. theorem OAI.Problem367.ResponseRows.shellProfile_zero line 45
  5. theorem OAI.Problem367.ResponseRows.shellProfile_succ line 48
  6. theorem OAI.Problem367.ResponseRows.summable_and_tsum_le_shell_budget line 51
  7. theorem OAI.Problem367.ResponseRows.weighted_energy_shell_bound line 79
  8. theorem OAI.Problem367.ResponseRows.pathNoiseEnergy_empty line 103
  9. theorem OAI.Problem367.ResponseRows.pathLinearEnergy_empty line 107
  10. theorem OAI.Problem367.ResponseRows.pathNoiseEnergy_nonneg line 111
  11. theorem OAI.Problem367.ResponseRows.pathLinearEnergy_nonneg line 115
  12. theorem OAI.Problem367.ResponseRows.integral_tree_density_le_shell_energies line 119