OAI/Combinatorics/SumProduct/Alignment/AlignmentMass01.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OwnTerminal.project_pow line 22
  2. lemma OAI.OwnTerminal.project_inv line 29
  3. lemma OAI.OwnTerminal.project_zpow line 35
  4. lemma OAI.OwnTerminal.project_list line 44
  5. lemma OAI.OwnTerminal.terminal_projection line 58
  6. theorem OAI.AlignmentMass.finite_closed_mass line 92
  7. theorem OAI.AlignmentMass.cover_sum line 123
  8. def OAI.AlignmentMass.ClosedGood line 143
  9. def OAI.AlignmentMass.OpenGood line 147
  10. def OAI.AlignmentMass.Success line 151
  11. lemma OAI.AlignmentMass.isClosed_closedGood line 155
  12. lemma OAI.AlignmentMass.isOpen_openGood line 163
  13. lemma OAI.AlignmentMass.closed_subset_open line 171
  14. lemma OAI.AlignmentMass.open_subset_success line 179
  15. theorem OAI.AlignmentMass.mixture_lower line 194
  16. theorem OAI.AlignmentMass.eventually_success_mass line 208
  17. theorem OAI.AlignmentMass.conditional_mass line 233
  18. theorem OAI.AlignmentMass.conditional_mass_mixture line 260