OAI/Combinatorics/SumProduct/Alignment/CompactConvex01.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompactConvexFixedPoint.average line 26
  2. lemma OAI.CompactConvexFixedPoint.average_mem line 30
  3. lemma OAI.CompactConvexFixedPoint.average_difference line 43
  4. theorem OAI.CompactConvexFixedPoint.exists_fixed line 55
  5. theorem OAI.CompactConvexFixedPoint.exists_common_fixed line 89
  6. def OAI.CompactConvexFixedPoint.fixedSet line 135
  7. lemma OAI.CompactConvexFixedPoint.fixedSet_compact line 139
  8. lemma OAI.CompactConvexFixedPoint.fixedSet_convex line 149
  9. lemma OAI.CompactConvexFixedPoint.fixedSet_invariant line 157
  10. lemma OAI.CompactConvexFixedPoint.fixedSet_step line 170
  11. theorem OAI.CompactConvexFixedPoint.exists_solvable_fixed line 196
  12. def OAI.SolvableInvariantMeasure.evaluations line 228
  13. lemma OAI.SolvableInvariantMeasure.continuous_evaluations line 232
  14. lemma OAI.SolvableInvariantMeasure.compact_evaluations line 237
  15. lemma OAI.SolvableInvariantMeasure.convex_evaluations line 241
  16. def OAI.SolvableInvariantMeasure.pushRep line 266
  17. lemma OAI.SolvableInvariantMeasure.pushRep_evaluations line 285
  18. theorem OAI.SolvableInvariantMeasure.exists_invariant_integrals line 295
  19. theorem OAI.SolvableInvariantMeasure.exists_invariant_measure line 313
  20. theorem OAI.SolvableInvariantMeasure.exists_invariant_fullSupport line 333