OAI/Combinatorics/SumProduct/Alignment/AllLevel11.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompactUniformComposition.compose line 28
  2. lemma OAI.CompactUniformComposition.floor_normalized_close line 44
  3. lemma OAI.AllLevelFactorization.Factorization.smooth_composed_uniform line 77
  4. lemma OAI.AllLevelFactorization.Factorization.smooth_floor_tests line 95
  5. def OAI.AllLevelFactorization.Factorization.natResidue line 145
  6. def OAI.AllLevelFactorization.Factorization.pointStructured line 146
  7. def OAI.AllLevelFactorization.Factorization.leftTest line 149
  8. lemma OAI.AllLevelFactorization.Factorization.leftTest_continuous line 152
  9. def OAI.AllLevelFactorization.Factorization.limitTest line 157
  10. lemma OAI.AllLevelFactorization.Factorization.limitTest_continuous line 159
  11. lemma OAI.AllLevelFactorization.Factorization.point_realization line 162
  12. lemma OAI.AllLevelFactorization.Factorization.pointStructured_local line 180
  13. lemma OAI.AllLevelFactorization.Factorization.empirical_eq_expect line 198
  14. theorem OAI.AllLevelFactorization.Factorization.global_point_law line 206
  15. def OAI.ProbabilityMixtures.finiteAverage line 256
  16. lemma OAI.ProbabilityMixtures.finiteAverage_integral line 263
  17. def OAI.ProbabilityMixtures.unitTime line 271
  18. instance OAI.ProbabilityMixtures.unitTime_probability line 272
  19. def OAI.ProbabilityMixtures.intervalPush line 279
  20. lemma OAI.ProbabilityMixtures.intervalPush_integral line 282
  21. def OAI.ProbabilityMixtures.empirical line 296
  22. lemma OAI.ProbabilityMixtures.empirical_integral line 302