OAI/Analysis/MarkovType/FiniteTruncationTail.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MarkovSuperreflexivity.FiniteLaw.prob_nonneg line 21

    Distinct definitions of this name: OAI/Analysis/MarkovType/DyadicWeakAmplification.lean:19 (different declaration text). Qualify references as OAI.MarkovSuperreflexivity.FiniteLaw.prob_nonneg@path.

  2. theorem OAI.MarkovSuperreflexivity.FiniteLaw.prob_le_one line 28

    Distinct definitions of this name: OAI/Analysis/MarkovType/DyadicWeakAmplification.lean:35 (different declaration text). Qualify references as OAI.MarkovSuperreflexivity.FiniteLaw.prob_le_one@path.

  3. theorem OAI.MarkovSuperreflexivity.FiniteLaw.prob_le_add_of_imp_or line 38
  4. theorem OAI.MarkovSuperreflexivity.finite_budget_maximal_prob_le line 60
  5. theorem OAI.MarkovSuperreflexivity.finite_budget_truncation_tail line 105