OAI/Computability/MaxCut/Games/UniformPartition.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Exact finite uniform conditioning and total expectation, including empty fibres.

  1. def OAI.MaxCutGames.Soundness.UniformPartition.mean line 12
  2. theorem OAI.MaxCutGames.Soundness.UniformPartition.mean_equiv line 15
  3. def OAI.MaxCutGames.Soundness.UniformPartition.fiberSum line 20
  4. def OAI.MaxCutGames.Soundness.UniformPartition.fiberSize line 24
  5. theorem OAI.MaxCutGames.Soundness.UniformPartition.fiberSize_eq_card line 27
  6. theorem OAI.MaxCutGames.Soundness.UniformPartition.sum_fiberSum line 35
  7. theorem OAI.MaxCutGames.Soundness.UniformPartition.fiberSize_mul line 44
  8. theorem OAI.MaxCutGames.Soundness.UniformPartition.fiberSize_pos line 53
  9. theorem OAI.MaxCutGames.Soundness.UniformPartition.fiberSize_mul_conditional line 62
  10. theorem OAI.MaxCutGames.Soundness.UniformPartition.total_mean line 72
  11. theorem OAI.MaxCutGames.Soundness.UniformPartition.mean_mono line 91
  12. theorem OAI.MaxCutGames.Soundness.UniformPartition.mean_le_partition_bound line 95
  13. theorem OAI.MaxCutGames.Soundness.UniformPartition.fiber_conditional_eq_subtype_mean line 105