OAI/Combinatorics/SumProduct/Alignment/AllLevel13.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.RationalLattice.ImageGeometry line 29
  2. theorem OAI.RationalLattice.imageGeometry_nonempty line 46
  3. lemma OAI.RationalLattice.ImageGeometry.level_compact_reps line 65
  4. lemma OAI.RationalLattice.ImageGeometry.quotient_compactSpace line 74
  5. lemma OAI.RationalLattice.ImageGeometry.covered_level_compact_reps line 98
  6. lemma OAI.RationalLattice.ImageGeometry.covered_quotient_compactSpace line 107
  7. lemma OAI.ProbabilityMixtures.empirical_map line 134
  8. lemma OAI.ProbabilityMixtures.empirical_preimage line 156
  9. def OAI.AllLevelFactorization.Factorization.coveredPointMixture line 188
  10. def OAI.AllLevelFactorization.Factorization.coveredEmpiricalPointLaw line 191
  11. lemma OAI.AllLevelFactorization.Factorization.coveredEmpiricalPointLaw_eq line 196
  12. theorem OAI.AllLevelFactorization.Factorization.covered_weak_point_law line 209
  13. lemma OAI.AllLevelFactorization.Factorization.coveredPointMixture_integral line 219
  14. def OAI.AllLevelFactorization.actualPointMixture line 270
  15. lemma OAI.AllLevelFactorization.actual_weak_point_law line 275
  16. lemma OAI.AllLevelFactorization.actual_weak_point_law_map line 283
  17. lemma OAI.AllLevelFactorization.actualPointMixture_integral line 298
  18. theorem OAI.AllLevelFactorization.actual_point_law_exists line 315