OAI/Combinatorics/SumProduct/Alignment/MicrocellFibers01.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MicrocellConditional.eventMass line 27
  2. lemma OAI.MicrocellConditional.law_apply_units line 29
  3. lemma OAI.MicrocellConditional.subset_event_sum line 39
  4. theorem OAI.MicrocellConditional.conditional_ratio line 57
  5. lemma OAI.MicrocellConditional.cell_real_law line 69
  6. theorem OAI.MicrocellConditional.conditional_event_error line 89
  7. theorem OAI.MicrocellConditional.conditional_success line 111
  8. def OAI.MicrocellFibers.fiber line 143
  9. def OAI.MicrocellFibers.point line 146
  10. lemma OAI.MicrocellFibers.point_mem line 148
  11. lemma OAI.MicrocellFibers.point_injective line 160
  12. lemma OAI.MicrocellFibers.represent line 165
  13. def OAI.MicrocellFibers.parametrization line 180
  14. lemma OAI.MicrocellFibers.fiber_card line 190
  15. lemma OAI.MicrocellFibers.fiber_nonempty line 195
  16. lemma OAI.MicrocellFibers.fiber_subset_units line 200
  17. lemma OAI.MicrocellFibers.uniform_fiber line 217
  18. theorem OAI.MicrocellFibers.raw_fiber_success line 233