OAI/Combinatorics/UniformKServer/PiIntegrate.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Fubini for an arbitrary function on the same finite independent tape. The one-coordinate ledger may depend on every other coordinate.

  1. theorem OAI.UniformKServer.FiniteProbability.Law.expect_pi_split line 18
  2. theorem OAI.UniformKServer.FiniteProbability.Law.expect_pi_fiber_le line 48
  3. theorem OAI.UniformKServer.FiniteProbability.Law.expect_prod_reverse line 60
  4. theorem OAI.UniformKServer.FiniteProbability.Law.expect_pair line 73
  5. theorem OAI.UniformKServer.FiniteProbability.Law.expect_pair_reverse line 76