OAI/Probability/FreeIsing/Trees/FinitePathGibbs.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.FinitePathGibbs.rawKernel line 12
  2. theorem OAI.Problem367.FinitePathGibbs.rawKernel_pos line 15
  3. def OAI.Problem367.FinitePathGibbs.tailPartition line 18
  4. theorem OAI.Problem367.FinitePathGibbs.tailPartition_zero line 21
  5. theorem OAI.Problem367.FinitePathGibbs.tailPartition_pos line 25
  6. theorem OAI.Problem367.FinitePathGibbs.tailPartition_succ line 33
  7. def OAI.Problem367.FinitePathGibbs.backwardField line 42
  8. theorem OAI.Problem367.FinitePathGibbs.normalize_binary line 49
  9. theorem OAI.Problem367.FinitePathGibbs.normalized_head line 59
  10. theorem OAI.Problem367.FinitePathGibbs.normalized_path line 81
  11. theorem OAI.Problem367.FinitePathGibbs.half_log_transmitted line 105
  12. theorem OAI.Problem367.FinitePathGibbs.tailPartition_half_log line 133
  13. theorem OAI.Problem367.FinitePathGibbs.backwardField_cavity line 160
  14. def OAI.Problem367.FinitePathGibbs.partition line 168
  15. theorem OAI.Problem367.FinitePathGibbs.partition_pos line 171
  16. def OAI.Problem367.FinitePathGibbs.rootLaw line 177
  17. theorem OAI.Problem367.FinitePathGibbs.rootLaw_pos line 180
  18. theorem OAI.Problem367.FinitePathGibbs.sum_rootLaw line 185
  19. def OAI.Problem367.FinitePathGibbs.mass line 190
  20. theorem OAI.Problem367.FinitePathGibbs.mass_eq_jointWeight line 195
  21. def OAI.Problem367.FinitePathGibbs.energy line 207
  22. theorem OAI.Problem367.FinitePathGibbs.mass_eq_exp_energy line 212
  23. theorem OAI.Problem367.FinitePathGibbs.mass_nonneg line 219
  24. theorem OAI.Problem367.FinitePathGibbs.sum_mass line 224
  25. theorem OAI.Problem367.FinitePathGibbs.partition_eq_sum_exp line 231
  26. def OAI.Problem367.FinitePathGibbs.mean line 239
  27. theorem OAI.Problem367.FinitePathGibbs.mean_endpoints line 243
  28. theorem OAI.Problem367.FinitePathGibbs.mean_first line 253
  29. theorem OAI.Problem367.FinitePathGibbs.mean_last line 262
  30. def OAI.Problem367.FinitePathGibbs.endpointCovariance line 270
  31. theorem OAI.Problem367.FinitePathGibbs.endpointCovariance_eq line 275
  32. def OAI.Problem367.FinitePathGibbs.rootField line 285
  33. theorem OAI.Problem367.FinitePathGibbs.rootField_zero line 289
  34. theorem OAI.Problem367.FinitePathGibbs.rootField_succ line 293
  35. theorem OAI.Problem367.FinitePathGibbs.rootLaw_eq_tanh line 298
  36. theorem OAI.Problem367.FinitePathGibbs.mean_first_eq_tanh line 316
  37. theorem OAI.Problem367.FinitePathGibbs.artanh_mean_first line 323
  38. theorem OAI.Problem367.FinitePathGibbs.rootField_sub_bound line 328
  39. theorem OAI.Problem367.FinitePathGibbs.artanh_mean_first_sub_bound line 337
  40. theorem OAI.Problem367.FinitePathGibbs.endpointCovariance_mem_Icc line 343