OAI/Probability/SKSupport/Diffusion/FiniteFeedback.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.uniform_lipschitz line 14
  2. def OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.toDrift line 20
  3. def OAI.ZeroTemperatureSK.rightCoeff line 28
  4. lemma OAI.ZeroTemperatureSK.rightCoeff_measurable line 32
  5. lemma OAI.ZeroTemperatureSK.rightCoeff_bounds line 39
  6. lemma OAI.ZeroTemperatureSK.rightCoeff_family line 51
  7. def OAI.ZeroTemperatureSK.finiteFeedbackFun line 57
  8. lemma OAI.ZeroTemperatureSK.finiteFeedback_family line 60
  9. def OAI.ZeroTemperatureSK.finiteFeedback line 64
  10. lemma OAI.ZeroTemperatureSK.finiteValue_shift line 68
  11. lemma OAI.ZeroTemperatureSK.rightCoeff_shift line 83
  12. lemma OAI.ZeroTemperatureSK.finiteFeedback_step line 98