OAI/Analysis/MarkovType/SmoothnessBounds.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.SymmetricPowerSmooth line 21
  2. def OAI.MarkovSuperreflexivity.PowerSmooth line 25
  3. def OAI.MarkovSuperreflexivity.smoothnessDeviations line 29
  4. def OAI.MarkovSuperreflexivity.smoothnessModulus line 33
  5. theorem OAI.MarkovSuperreflexivity.mean_le_root_le_one_add line 36
  6. theorem OAI.MarkovSuperreflexivity.SymmetricPowerSmooth.powerSmooth line 60
  7. theorem OAI.MarkovSuperreflexivity.seminorm_le_symmetric_average line 73
  8. theorem OAI.MarkovSuperreflexivity.smoothnessDeviation_nonneg line 83
  9. theorem OAI.MarkovSuperreflexivity.smoothnessDeviation_le_abs line 90
  10. theorem OAI.MarkovSuperreflexivity.smoothnessDeviations_bddAbove line 100
  11. theorem OAI.MarkovSuperreflexivity.smoothnessDeviations_insert_bddAbove line 106
  12. theorem OAI.MarkovSuperreflexivity.smoothnessModulus_nonneg line 115
  13. theorem OAI.MarkovSuperreflexivity.smoothnessModulus_le line 120
  14. theorem OAI.MarkovSuperreflexivity.smoothnessModulus_le_abs line 132
  15. theorem OAI.MarkovSuperreflexivity.smoothnessModulus_zero line 137
  16. theorem OAI.MarkovSuperreflexivity.smoothnessDeviation_le_modulus line 143
  17. theorem OAI.MarkovSuperreflexivity.PowerSmooth.smoothnessModulus_le line 149
  18. theorem OAI.MarkovSuperreflexivity.powerSmooth_iff_smoothnessModulus_le line 157
  19. theorem OAI.MarkovSuperreflexivity.SymmetricPowerSmooth.smoothnessModulus_le line 167
  20. theorem OAI.MarkovSuperreflexivity.smoothnessModulus_eq_standard_of_exists_unit line 173
  21. theorem OAI.MarkovSuperreflexivity.exists_seminorm_unit_of_pos line 189
  22. theorem OAI.MarkovSuperreflexivity.exists_seminorm_unit_of_definite line 195
  23. theorem OAI.MarkovSuperreflexivity.smoothnessModulus_eq_standard_of_definite line 204
  24. theorem OAI.MarkovSuperreflexivity.smoothnessModulus_eq_zero_of_no_unit line 212
  25. theorem OAI.MarkovSuperreflexivity.smoothnessModulus_eq_zero_of_subsingleton line 219
  26. theorem OAI.MarkovSuperreflexivity.PowerSmooth.uniformSmooth line 229
  27. theorem OAI.MarkovSuperreflexivity.SymmetricPowerSmooth.uniformSmooth line 256
  28. theorem OAI.MarkovSuperreflexivity.EquivalentNorm.smoothnessModulus_eq_standard line 260