OAI/Probability/FreeIsing/Estimates/NonbacktrackingDecay.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.NonbacktrackingComplement.vertexRate line 18
  2. theorem OAI.Problem367.NonbacktrackingComplement.vertexRate_nonneg line 20
  3. theorem OAI.Problem367.NonbacktrackingComplement.vertexRate_lt_one line 24
  4. def OAI.Problem367.NonbacktrackingComplement.normalizedVertex line 30
  5. def OAI.Problem367.NonbacktrackingComplement.normalizedCompanion line 33
  6. def OAI.Problem367.NonbacktrackingComplement.companion line 37
  7. theorem OAI.Problem367.NonbacktrackingComplement.normalizedVertex_selfAdjoint line 40
  8. theorem OAI.Problem367.NonbacktrackingComplement.norm_normalizedVertex_le_one line 52
  9. theorem OAI.Problem367.NonbacktrackingComplement.companion_apply line 63
  10. theorem OAI.Problem367.NonbacktrackingComplement.norm_normalizedCompanion_pow_le_of_chebyshev_bound line 75
  11. theorem OAI.Problem367.NonbacktrackingComplement.norm_companion_pow_le_of_chebyshev_bound line 100
  12. theorem OAI.Problem367.NonbacktrackingComplement.exists_norm_edgeOperator_pow_bound_of_chebyshev_bound line 120
  13. theorem OAI.Problem367.NonbacktrackingComplement.summable_norm_edgeOperator_pow_of_chebyshev_bound line 164
  14. theorem OAI.Problem367.NonbacktrackingComplement.normalizedVertex_chebyshev_bound line 189
  15. theorem OAI.Problem367.NonbacktrackingComplement.norm_normalizedCompanion_pow_le line 201
  16. theorem OAI.Problem367.NonbacktrackingComplement.norm_companion_pow_le line 208
  17. theorem OAI.Problem367.NonbacktrackingComplement.exists_norm_edgeOperator_pow_bound line 216
  18. theorem OAI.Problem367.NonbacktrackingComplement.summable_norm_edgeOperator_pow line 228
  19. theorem OAI.Problem367.NonbacktrackingComplement.normalizedVertex_chebyshev_bound_real line 244
  20. theorem OAI.Problem367.NonbacktrackingComplement.exists_norm_edgeOperator_pow_bound_real line 251
  21. theorem OAI.Problem367.NonbacktrackingComplement.summable_norm_edgeOperator_pow_real line 263