OAI/Analysis/MarkovType/FiniteSeparation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.finiteL1 line 18
  2. theorem OAI.MarkovSuperreflexivity.finiteL1_nonneg line 20
  3. theorem OAI.MarkovSuperreflexivity.finiteL1_zero line 23
  4. theorem OAI.MarkovSuperreflexivity.finiteL1_single line 26
  5. theorem OAI.MarkovSuperreflexivity.continuous_finiteL1 line 35
  6. theorem OAI.MarkovSuperreflexivity.convex_finiteL1_lt line 39
  7. def OAI.MarkovSuperreflexivity.finiteMixtures line 58
  8. theorem OAI.MarkovSuperreflexivity.mem_finiteMixtures line 63
  9. theorem OAI.MarkovSuperreflexivity.convex_finiteMixtures line 75
  10. theorem OAI.MarkovSuperreflexivity.continuousLinearMap_pi_expansion line 85
  11. theorem OAI.MarkovSuperreflexivity.exists_finite_mixture_l1_lt line 100