OAI/Probability/SKSupport/Foundations/FiniteValue.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroTemperatureSK.Heat.continuousOn_moving_heat_from line 19
  2. lemma OAI.ZeroTemperatureSK.Heat.backward_heat_dual line 49
  3. def OAI.ZeroTemperatureSK.Heat.finiteValue line 73
  4. def OAI.ZeroTemperatureSK.Heat.finiteCoeff line 79
  5. lemma OAI.ZeroTemperatureSK.Heat.finiteValue_regular line 83
  6. lemma OAI.ZeroTemperatureSK.Heat.finiteValue_lipschitz line 100
  7. lemma OAI.ZeroTemperatureSK.Heat.finiteValue_head line 116
  8. lemma OAI.ZeroTemperatureSK.Heat.finiteValue_tail line 120
  9. lemma OAI.ZeroTemperatureSK.Heat.finiteValue_zero line 124
  10. lemma OAI.ZeroTemperatureSK.Heat.measurable_finiteValue line 134
  11. lemma OAI.ZeroTemperatureSK.Heat.measurable_finiteCoeff line 144
  12. lemma OAI.ZeroTemperatureSK.Heat.finiteCoeff_bounds line 152
  13. lemma OAI.ZeroTemperatureSK.Heat.finiteValue_uniform_derivative_bounds line 168