OAI/Probability/FreeIsing/Estimates/Osgood.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.osgoodTransform line 12
  2. lemma OAI.Problem367.osgoodInner_pos line 14
  3. lemma OAI.Problem367.hasDerivAt_osgoodTransform line 20
  4. lemma OAI.Problem367.continuousOn_criticalLogPrimitive line 32
  5. lemma OAI.Problem367.hasDerivAt_criticalLogPrimitive line 47
  6. lemma OAI.Problem367.criticalLogCoefficient_integrable line 56
  7. lemma OAI.Problem367.criticalLogCoefficient_integral line 65
  8. lemma OAI.Problem367.tendsto_osgoodTransform_nhdsGT_zero line 77
  9. lemma OAI.Problem367.criticalCoefficient_integrable line 87
  10. lemma OAI.Problem367.not_bounded_osgoodTransform_of_tendsto_zero line 96
  11. def OAI.Problem367.osgoodModulus line 108
  12. lemma OAI.Problem367.osgoodModulus_pos line 110
  13. lemma OAI.Problem367.osgoodModulus_mono line 113
  14. lemma OAI.Problem367.osgoodModulus_mono_nonneg line 132
  15. lemma OAI.Problem367.osgood_regularized_deriv_bound line 139
  16. lemma OAI.Problem367.osgoodTransform_antitone line 159
  17. def OAI.Problem367.criticalTimeCoefficient line 168
  18. lemma OAI.Problem367.criticalTimeCoefficient_integrable line 173
  19. lemma OAI.Problem367.criticalTimeCoefficient_intervalIntegrable line 190
  20. lemma OAI.Problem367.criticalTimeCoefficient_nonneg line 196
  21. lemma OAI.Problem367.criticalPowerCoefficient_integral line 201
  22. lemma OAI.Problem367.criticalCoefficient_integral line 207