OAI/Combinatorics/BalancedRyser/Probability/FiniteKernelPotential.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.FiniteKernelPotential.advance line 14
  2. def OAI.Balanced.FiniteKernelPotential.weights line 17
  3. theorem OAI.Balanced.FiniteKernelPotential.weights_zero line 21
  4. theorem OAI.Balanced.FiniteKernelPotential.weights_succ line 24
  5. theorem OAI.Balanced.FiniteKernelPotential.advance_nonneg line 27
  6. theorem OAI.Balanced.FiniteKernelPotential.weights_nonneg line 34
  7. theorem OAI.Balanced.FiniteKernelPotential.advance_pairing line 43
  8. theorem OAI.Balanced.FiniteKernelPotential.advance_potential_le line 48
  9. theorem OAI.Balanced.FiniteKernelPotential.expected_potential_le line 57
  10. theorem OAI.Balanced.FiniteKernelPotential.payoff_le line 69
  11. def OAI.Balanced.FiniteKernelPotential.pointMass line 82
  12. theorem OAI.Balanced.FiniteKernelPotential.pointMass_nonneg line 85
  13. theorem OAI.Balanced.FiniteKernelPotential.pointMass_pairing line 88
  14. theorem OAI.Balanced.FiniteKernelPotential.pointMass_potential_le line 91
  15. theorem OAI.Balanced.FiniteKernelPotential.pointMass_payoff_le line 99
  16. theorem OAI.Balanced.FiniteKernelPotential.weights_eq_of_recurrence line 108
  17. theorem OAI.Balanced.FiniteKernelPotential.evolution_payoff_le line 118
  18. theorem OAI.Balanced.FiniteKernelPotential.pointMass_event_le line 128