OAI/Dynamics/ConditionalShuffle/CycleEnergy.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Thorp.Conditional.mean_fintype_irrel line 9
  2. lemma OAI.Thorp.Conditional.rawPermute_mass line 15
  3. lemma OAI.Thorp.Conditional.rawPermute_support line 18
  4. lemma OAI.Thorp.Conditional.rawPermute_count line 23
  5. lemma OAI.Thorp.Conditional.rawIterate_mass line 26
  6. lemma OAI.Thorp.Conditional.rawIterate_support line 32
  7. lemma OAI.Thorp.Conditional.rawIterate_count line 39
  8. abbrev OAI.Thorp.Conditional.OverlayEnergy.Bits line 48
  9. abbrev OAI.Thorp.Conditional.OverlayEnergy.Prep9 line 49
  10. abbrev OAI.Thorp.Conditional.OverlayEnergy.Prep200 line 50
  11. abbrev OAI.Thorp.Conditional.OverlayEnergy.Active line 51
  12. abbrev OAI.Thorp.Conditional.OverlayEnergy.CycleCoins line 52
  13. def OAI.Thorp.Conditional.OverlayEnergy.cycle line 54
  14. def OAI.Thorp.Conditional.OverlayEnergy.cyclePerm line 59
  15. lemma OAI.Thorp.Conditional.OverlayEnergy.cycle_free line 62
  16. lemma OAI.Thorp.Conditional.OverlayEnergy.cycle_count line 68
  17. lemma OAI.Thorp.Conditional.OverlayEnergy.cycle_mass line 73
  18. lemma OAI.Thorp.Conditional.OverlayEnergy.cycle_support line 78
  19. lemma OAI.Thorp.Conditional.OverlayEnergy.cycle_energy_le line 83
  20. def OAI.Thorp.Conditional.OverlayEnergy.coefficient line 88
  21. lemma OAI.Thorp.Conditional.OverlayEnergy.coefficient_nonneg line 92
  22. lemma OAI.Thorp.Conditional.OverlayEnergy.cycle_expected_energy line 94