OAI/Probability/FreeIsing/Trees/RootedBroadcast.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.RootedBroadcast.spinMul line 14
  2. lemma OAI.Problem367.RootedBroadcast.spinMul_pos line 17
  3. lemma OAI.Problem367.RootedBroadcast.pos_spinMul line 19
  4. lemma OAI.Problem367.RootedBroadcast.spinMul_self line 21
  5. lemma OAI.Problem367.RootedBroadcast.spinMul_comm line 23
  6. lemma OAI.Problem367.RootedBroadcast.spinMul_assoc line 25
  7. lemma OAI.Problem367.RootedBroadcast.spinMul_cancel line 27
  8. lemma OAI.Problem367.RootedBroadcast.measurable_spinMul line 30
  9. def OAI.Problem367.RootedBroadcast.biasedSpin line 33
  10. lemma OAI.Problem367.RootedBroadcast.measurable_biasedSpin line 36
  11. lemma OAI.Problem367.RootedBroadcast.biasedSpin_pos_mass line 39
  12. lemma OAI.Problem367.RootedBroadcast.biasedSpin_neg_mass line 51
  13. abbrev OAI.Problem367.RootedBroadcast.parent line 63
  14. def OAI.Problem367.RootedBroadcast.ofNoise line 65
  15. lemma OAI.Problem367.RootedBroadcast.ofNoise_root line 74
  16. lemma OAI.Problem367.RootedBroadcast.ofNoise_nonroot line 79
  17. lemma OAI.Problem367.RootedBroadcast.ofNoise_append line 84
  18. lemma OAI.Problem367.RootedBroadcast.measurable_ofNoise_apply line 94
  19. lemma OAI.Problem367.RootedBroadcast.measurable_ofNoise line 123
  20. def OAI.Problem367.RootedBroadcast.noiseFromSpins line 126
  21. lemma OAI.Problem367.RootedBroadcast.measurable_noiseFromSpins line 129
  22. lemma OAI.Problem367.RootedBroadcast.noiseFromSpins_ofNoise line 137
  23. lemma OAI.Problem367.RootedBroadcast.ofNoise_noiseFromSpins line 146
  24. def OAI.Problem367.RootedBroadcast.measurableEquiv line 166
  25. def OAI.Problem367.RootedBroadcast.edgeNoise line 174
  26. lemma OAI.Problem367.RootedBroadcast.measurable_edgeNoise line 176
  27. lemma OAI.Problem367.RootedBroadcast.edgeNoise_mass line 179
  28. def OAI.Problem367.RootedBroadcast.inputNoise line 191
  29. lemma OAI.Problem367.RootedBroadcast.measurable_inputNoise line 194
  30. def OAI.Problem367.RootedBroadcast.factor line 201
  31. lemma OAI.Problem367.RootedBroadcast.measurable_factor line 204
  32. lemma OAI.Problem367.RootedBroadcast.factor_append line 207
  33. def OAI.Problem367.RootedBroadcast.noiseWeight line 213
  34. lemma OAI.Problem367.RootedBroadcast.inputNoise_cylinder line 217