OAI/Analysis/MarkovType/DyadicWeakType.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MarkovSuperreflexivity.finiteMoment_nonneg line 14
  2. theorem OAI.MarkovSuperreflexivity.finiteMoment_smul line 18
  3. theorem OAI.MarkovSuperreflexivity.dyadicInputWeight_pos line 29
  4. theorem OAI.MarkovSuperreflexivity.dyadic_eq_zero_of_inputMoment_eq_zero line 39
  5. def OAI.MarkovSuperreflexivity.dyadicCenter line 56
  6. theorem OAI.MarkovSuperreflexivity.dyadicRoot_center line 61
  7. theorem OAI.MarkovSuperreflexivity.dyadicCoefficient_center line 65
  8. theorem OAI.MarkovSuperreflexivity.dyadicInputMoment_center line 69
  9. theorem OAI.MarkovSuperreflexivity.dyadicProcess_center line 77
  10. theorem OAI.MarkovSuperreflexivity.dyadicSynthesis_center line 88
  11. theorem OAI.MarkovSuperreflexivity.dyadic_zero_tail line 93
  12. def OAI.MarkovSuperreflexivity.dyadicWeakConstant line 136
  13. def OAI.MarkovSuperreflexivity.dyadicWeakNorm line 138
  14. theorem OAI.MarkovSuperreflexivity.dyadicWeakConstant_pos line 140
  15. theorem OAI.MarkovSuperreflexivity.dyadicWeakNorm_pos line 145
  16. theorem OAI.MarkovSuperreflexivity.dyadicWeakNorm_power line 148
  17. theorem OAI.MarkovSuperreflexivity.dyadic_tail line 153
  18. theorem OAI.MarkovSuperreflexivity.dyadic_weak_type line 216