OAI/Analysis/MarkovType/ChartTransport.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.FiniteCoupling.eventMass line 23
  2. theorem OAI.MarkovSuperreflexivity.FiniteCoupling.eventMass_nonneg line 26
  3. theorem OAI.MarkovSuperreflexivity.FiniteCoupling.eventMass_compl line 36
  4. theorem OAI.MarkovSuperreflexivity.FiniteCoupling.eventMass_average line 52
  5. theorem OAI.MarkovSuperreflexivity.FiniteCoupling.eventMass_transpose line 62
  6. def OAI.MarkovSuperreflexivity.symmetrizeFiniteCouplings line 75
  7. theorem OAI.MarkovSuperreflexivity.symmetrizeFiniteCouplings_reverse line 80
  8. theorem OAI.MarkovSuperreflexivity.symmetrizeFiniteCouplings_good line 88
  9. def OAI.MarkovSuperreflexivity.chartTransportDomain line 97
  10. def OAI.MarkovSuperreflexivity.chartTransportDomainSource line 100
  11. def OAI.MarkovSuperreflexivity.chartTransportDomainTarget line 111
  12. def OAI.MarkovSuperreflexivity.chartTransportSourceTuple line 119
  13. def OAI.MarkovSuperreflexivity.chartTransportTargetTuple line 124
  14. theorem OAI.MarkovSuperreflexivity.chart_good_iff_transport_tuple line 129
  15. def OAI.MarkovSuperreflexivity.preliminaryChartCoupling line 153
  16. theorem OAI.MarkovSuperreflexivity.preliminaryChartCoupling_good_mass line 161
  17. abbrev OAI.MarkovSuperreflexivity.PositiveMassSupport line 172
  18. theorem OAI.MarkovSuperreflexivity.mass_zero_outside_positive_support line 175
  19. theorem OAI.MarkovSuperreflexivity.sum_positive_support line 179
  20. def OAI.MarkovSuperreflexivity.positiveSupportLaw line 185
  21. def OAI.MarkovSuperreflexivity.restrictPositiveCoupling line 193
  22. theorem OAI.MarkovSuperreflexivity.restrictPositiveCoupling_eventMass line 207
  23. abbrev OAI.MarkovSuperreflexivity.UniformCouplingEdge line 227
  24. def OAI.MarkovSuperreflexivity.uniformCouplingChain line 229
  25. theorem OAI.MarkovSuperreflexivity.uniformCouplingChain_edge_mass line 264
  26. theorem OAI.MarkovSuperreflexivity.uniformCouplingChain_letter_mass line 278
  27. theorem OAI.MarkovSuperreflexivity.uniformCouplingChain_marked_letter_mass line 291
  28. theorem OAI.MarkovSuperreflexivity.uniformCouplingChain_good_mass line 311
  29. def OAI.MarkovSuperreflexivity.reversibleChartCoupling line 337
  30. theorem OAI.MarkovSuperreflexivity.reversibleChartCoupling_good line 342
  31. def OAI.MarkovSuperreflexivity.chartTransportChain line 359
  32. theorem OAI.MarkovSuperreflexivity.chartTransportChain_good_mass line 368
  33. theorem OAI.MarkovSuperreflexivity.chartTransportChain_marked_letter_mass line 388
  34. theorem OAI.MarkovSuperreflexivity.chartTransportChain_reverse_ne line 406