OAI/Analysis/MarkovType/FiniteChains.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MarkovSuperreflexivity.FiniteReversibleChain line 14

    Also declared: ComparatorChallenges/MarkovType.lean:11 (same declaration text).

  2. abbrev OAI.MarkovSuperreflexivity.StatePath line 23

    Also declared: ComparatorChallenges/MarkovType.lean:20 (same declaration text).

  3. def OAI.MarkovSuperreflexivity.pathWeight line 25

    Also declared: ComparatorChallenges/MarkovType.lean:22 (same declaration text).

  4. def OAI.MarkovSuperreflexivity.stateCost line 29

    Also declared: ComparatorChallenges/MarkovType.lean:26 (same declaration text).

  5. def OAI.MarkovSuperreflexivity.MarkovTypeWith line 34

    Also declared: ComparatorChallenges/MarkovType.lean:31 (same declaration text).

  6. def OAI.MarkovSuperreflexivity.HasMarkovType line 39

    Also declared: ComparatorChallenges/MarkovType.lean:36 (same declaration text).

  7. def OAI.MarkovSuperreflexivity.HasNontrivialMarkovType line 42

    Also declared: ComparatorChallenges/MarkovType.lean:39 (same declaration text).

  8. theorem OAI.MarkovSuperreflexivity.pathWeight_nonneg line 45
  9. theorem OAI.MarkovSuperreflexivity.stateCost_nonneg line 50