OAI/Probability/StrongRayleigh/CantorProjective.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336AdditiveD139.CantorProjective.sites line 14
  2. lemma OAI.Problem336AdditiveD139.CantorProjective.mem_sites line 18
  3. lemma OAI.Problem336AdditiveD139.CantorProjective.sites_mono line 22
  4. def OAI.Problem336AdditiveD139.CantorProjective.extract line 26
  5. lemma OAI.Problem336AdditiveD139.CantorProjective.measurable_extract line 30
  6. def OAI.Problem336AdditiveD139.CantorProjective.bitFamily line 37
  7. instance OAI.Problem336AdditiveD139.CantorProjective.bitFamily_isProbabilityMeasure line 41
  8. lemma OAI.Problem336AdditiveD139.CantorProjective.bitFamily_projective line 46
  9. theorem OAI.Problem336AdditiveD139.CantorProjective.exists_bit_limit line 58
  10. def OAI.Problem336AdditiveD139.CantorProjective.extractFrom line 65
  11. lemma OAI.Problem336AdditiveD139.CantorProjective.measurable_extractFrom line 69
  12. lemma OAI.Problem336AdditiveD139.CantorProjective.bitFamily_eq_map_of_sites_subset line 76
  13. theorem OAI.Problem336AdditiveD139.CantorProjective.map_finite_observations line 86
  14. def OAI.Problem336AdditiveD139.CantorProjective.encodeEquiv line 116
  15. theorem OAI.Problem336AdditiveD139.CantorProjective.encoded_marginal line 129
  16. theorem OAI.Problem336AdditiveD139.CantorProjective.decoded_isProjectiveLimit line 150
  17. theorem OAI.Problem336AdditiveD139.CantorProjective.projective_exists_of_cantor_equiv line 169
  18. theorem OAI.Problem336AdditiveD139.CantorProjective.real_projective_exists line 178