OAI/Probability/FreeIsing/Estimates/PairCorrelation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.reducedWordDistance line 11
  2. theorem OAI.Problem367.reducedWordDistance_nil_left line 16
  3. theorem OAI.Problem367.reducedWordDistance_nil_right line 19
  4. theorem OAI.Problem367.reducedWordDistance_cons_same line 22
  5. theorem OAI.Problem367.reducedWordDistance_cons_ne line 27
  6. theorem OAI.Problem367.reducedWordDistance_symm line 32
  7. theorem OAI.Problem367.reducedWordDistance_self line 45
  8. theorem OAI.Problem367.reducedWordDistance_move_head line 51
  9. theorem OAI.Problem367.freeLaw_correlation_lists line 64
  10. theorem OAI.Problem367.HasFreeIsingLaw.pair_correlation line 107