OAI/Analysis/MarkovType/FiniteMarcinkiewicz.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.finiteMoment line 17
  2. def OAI.MarkovSuperreflexivity.finiteTail line 20
  3. def OAI.MarkovSuperreflexivity.largeCut line 23
  4. def OAI.MarkovSuperreflexivity.smallCut line 26
  5. theorem OAI.MarkovSuperreflexivity.largeCut_add_smallCut line 30
  6. theorem OAI.MarkovSuperreflexivity.finiteTail_add_le line 36
  7. def OAI.MarkovSuperreflexivity.FiniteWeakType line 70
  8. theorem OAI.MarkovSuperreflexivity.finiteTail_split_weak line 75
  9. def OAI.MarkovSuperreflexivity.largeMomentKernel line 90
  10. def OAI.MarkovSuperreflexivity.smallMomentKernel line 93
  11. theorem OAI.MarkovSuperreflexivity.integrable_largeMomentKernel line 96
  12. theorem OAI.MarkovSuperreflexivity.integral_largeMomentKernel line 100
  13. theorem OAI.MarkovSuperreflexivity.integrable_smallMomentKernel line 111
  14. theorem OAI.MarkovSuperreflexivity.integral_smallMomentKernel line 124
  15. def OAI.MarkovSuperreflexivity.finiteLayerKernel line 137
  16. theorem OAI.MarkovSuperreflexivity.integrable_finiteLayerKernel line 140
  17. theorem OAI.MarkovSuperreflexivity.integral_finiteLayerKernel line 145
  18. theorem OAI.MarkovSuperreflexivity.finiteLayerKernel_eq_of_pos line 157
  19. def OAI.MarkovSuperreflexivity.finiteLargeKernel line 167
  20. def OAI.MarkovSuperreflexivity.finiteSmallKernel line 170
  21. theorem OAI.MarkovSuperreflexivity.integrable_finiteLargeKernel line 173
  22. theorem OAI.MarkovSuperreflexivity.integrable_finiteSmallKernel line 178
  23. theorem OAI.MarkovSuperreflexivity.integral_finiteLargeKernel line 183
  24. theorem OAI.MarkovSuperreflexivity.integral_finiteSmallKernel line 194
  25. theorem OAI.MarkovSuperreflexivity.weakThresholdFactor line 205
  26. theorem OAI.MarkovSuperreflexivity.largeCut_weighted_kernel line 211
  27. theorem OAI.MarkovSuperreflexivity.smallCut_weighted_kernel line 232
  28. theorem OAI.MarkovSuperreflexivity.finiteLayerKernel_le line 257
  29. theorem OAI.MarkovSuperreflexivity.finite_marcinkiewicz line 287