OAI/Probability/SKSupport/Parabolic/ForwardRegularity.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroTemperatureSK.Heat.forwardCorrection_smooth line 15
  2. lemma OAI.ZeroTemperatureSK.Heat.forwardCorrection_deriv line 21
  3. lemma OAI.ZeroTemperatureSK.Heat.forwardGradient_family line 31
  4. lemma OAI.ZeroTemperatureSK.Heat.forwardCorrection_regular line 44
  5. lemma OAI.ZeroTemperatureSK.Heat.forwardCorrection_jet line 49
  6. lemma OAI.ZeroTemperatureSK.Heat.forwardCorrection_continuous line 61
  7. lemma OAI.ZeroTemperatureSK.Heat.forwardGradient_continuous line 70
  8. lemma OAI.ZeroTemperatureSK.Heat.forwardCorrection_even line 80
  9. def OAI.ZeroTemperatureSK.Heat.forwardCorrectionRate line 91
  10. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_forwardCorrection line 97
  11. def OAI.ZeroTemperatureSK.Heat.AffineSmoothFamily line 119
  12. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.continuous_iteratedDeriv line 124
  13. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.affine line 130
  14. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.affine_id_mul line 138
  15. lemma OAI.ZeroTemperatureSK.Heat.AffineSmoothFamily.add line 146
  16. lemma OAI.ZeroTemperatureSK.Heat.AffineSmoothFamily.const_mul line 156
  17. lemma OAI.ZeroTemperatureSK.Heat.AffineSmoothFamily.continuous line 164
  18. lemma OAI.ZeroTemperatureSK.Heat.AffineSmoothFamily.smooth line 169
  19. lemma OAI.ZeroTemperatureSK.Heat.AffineSmoothFamily.deriv line 174
  20. lemma OAI.ZeroTemperatureSK.Heat.AffineSmoothFamily.iteratedDeriv line 188
  21. lemma OAI.ZeroTemperatureSK.Heat.AffineSmoothFamily.bound line 195
  22. lemma OAI.ZeroTemperatureSK.Heat.AffineSmoothFamily.intervalIntegrable line 206
  23. lemma OAI.ZeroTemperatureSK.Heat.AffineSmoothFamily.hasDerivAt_integral line 211
  24. lemma OAI.ZeroTemperatureSK.Heat.AffineSmoothFamily.iteratedDeriv_integral line 233