OAI/Probability/FreeIsing/Trees/RadialEnergy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem367.treeShell_radial_succ line 11
  2. theorem OAI.Problem367.summable_of_tree_radial_le line 17
  3. theorem OAI.Problem367.tsum_le_of_tree_radial_le line 22
  4. theorem OAI.Problem367.summable_of_attenuated_tree_bound line 32
  5. theorem OAI.Problem367.tsum_treeShell_radial_tail line 43
  6. lemma OAI.Problem367.tsum_treeShell_radial_cutoff line 59
  7. theorem OAI.Problem367.tsum_tree_radial_cutoff line 85
  8. theorem OAI.Problem367.tsum_cutoff_le_of_tree_radial_le line 103
  9. theorem OAI.Problem367.ae_summable_sq_of_tree_radial_bound line 125
  10. theorem OAI.Problem367.integral_tsum_sq_eq_of_tree_radial_bound line 145
  11. theorem OAI.Problem367.integral_tsum_sq_le_of_tree_radial_bound line 157
  12. theorem OAI.Problem367.integral_tsum_sq_cutoff_le_of_tree_radial_bound line 169