OAI/Probability/FreeIsing/Estimates/RadialSummability.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.treeShellSigmaEquiv line 9
  2. theorem OAI.Problem367.tsum_treeShell_radial line 12
  3. theorem OAI.Problem367.summable_radial_iff line 20
  4. theorem OAI.Problem367.tsum_radial line 31
  5. theorem OAI.Problem367.summable_geometric_radial line 43
  6. theorem OAI.Problem367.tsum_geometric_radial line 55
  7. theorem OAI.Problem367.summable_geometric_radial_iff line 73
  8. theorem OAI.Problem367.not_summable_geometric_radial_of_critical line 100
  9. theorem OAI.Problem367.summable_norm_sq_of_radial_bound line 106
  10. theorem OAI.Problem367.tsum_norm_sq_le_of_radial_bound line 117
  11. theorem OAI.Problem367.memℓp_two_of_radial_bound line 130