OAI/Analysis/MarkovType/DyadicWeakAmplification.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

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

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

  2. theorem OAI.MarkovSuperreflexivity.FiniteLaw.prob_mono line 24
  3. theorem OAI.MarkovSuperreflexivity.FiniteLaw.prob_le_one line 35

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

  4. def OAI.MarkovSuperreflexivity.dyadicAmplificationThreshold line 40
  5. def OAI.MarkovSuperreflexivity.dyadicAmplificationRadius line 41
  6. def OAI.MarkovSuperreflexivity.dyadicZeroWeakConstant line 42
  7. theorem OAI.MarkovSuperreflexivity.dyadicAmplificationThreshold_pos line 44
  8. theorem OAI.MarkovSuperreflexivity.dyadicAmplificationRadius_pos line 48
  9. theorem OAI.MarkovSuperreflexivity.dyadicAmplificationThreshold_power line 52
  10. theorem OAI.MarkovSuperreflexivity.dyadicZeroWeakConstant_ge_one line 58
  11. theorem OAI.MarkovSuperreflexivity.dyadic_half_power_scale line 69
  12. theorem OAI.MarkovSuperreflexivity.dyadic_normalized_zero_tail line 123