OAI/Probability/FreeIsing/Trees/OrbitAverage.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.TreeOrbitAverage.Extension line 14
  2. instance OAI.Problem367.TreeOrbitAverage.extensionFinite line 17
  3. instance OAI.Problem367.TreeOrbitAverage.extensionFintype line 23
  4. def OAI.Problem367.TreeOrbitAverage.extensionEquivReducedTail line 26
  5. theorem OAI.Problem367.TreeOrbitAverage.card_extension line 39
  6. def OAI.Problem367.TreeOrbitAverage.extensionNilEquivTreeShell line 44
  7. theorem OAI.Problem367.TreeOrbitAverage.card_extension_nil_zero line 55
  8. theorem OAI.Problem367.TreeOrbitAverage.card_extension_nil_succ line 59
  9. def OAI.Problem367.TreeOrbitAverage.endpoint line 63
  10. def OAI.Problem367.TreeOrbitAverage.FixesStemBall line 66
  11. theorem OAI.Problem367.TreeOrbitAverage.exists_extension_map line 69
  12. theorem OAI.Problem367.TreeOrbitAverage.integral_weight_mul_extension_average line 78
  13. theorem OAI.Problem367.TreeOrbitAverage.integral_weight_mul_le_extension_average line 111