OAI/Probability/FreeIsing/Estimates/NonbacktrackingOperator.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.summable_norm_of_affine_geometric_bound line 7
  2. def OAI.Problem367.diagonalOperator line 23
  3. def OAI.Problem367.nonbacktrackingOperator line 25
  4. theorem OAI.Problem367.diagonalOperator_apply line 31
  5. theorem OAI.Problem367.nonbacktrackingOperator_apply line 36
  6. theorem OAI.Problem367.nonbacktrackingOperator_quadratic line 42
  7. def OAI.Problem367.diagonalOperatorAlgHom line 61
  8. theorem OAI.Problem367.aeval_diagonalOperator line 87
  9. theorem OAI.Problem367.norm_diagonalOperator_le line 93
  10. theorem OAI.Problem367.norm_nonbacktrackingOperator_le line 105
  11. theorem OAI.Problem367.norm_nonbacktrackingOperator_pow_le line 127
  12. theorem OAI.Problem367.norm_nonbacktrackingOperator_pow_le_of_selfAdjoint line 147
  13. theorem OAI.Problem367.norm_nonbacktrackingOperator_scalar_pow_le line 156
  14. theorem OAI.Problem367.norm_nonbacktrackingOperator_scalar_le line 167
  15. theorem OAI.Problem367.norm_scaled_nonbacktrackingOperator_pow_le line 182
  16. theorem OAI.Problem367.summable_norm_scaled_nonbacktrackingOperator_pow line 215