OAI/Probability/SKSupport/Control/ValueDifference.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ZeroTemperatureSK.coefficientDistance line 15
2. lemma OAI.ZeroTemperatureSK.coefficientDistance_nonneg line 18
3. lemma OAI.ZeroTemperatureSK.value_difference_bound line 21
4. def OAI.ZeroTemperatureSK.compactDifference line 29
5. def OAI.ZeroTemperatureSK.compactDifferenceRate line 32
6. lemma OAI.ZeroTemperatureSK.compactDifference_continuous line 35
7. lemma OAI.ZeroTemperatureSK.compactDifference_deriv line 46
8. lemma OAI.ZeroTemperatureSK.compactDifference_family line 54
9. lemma OAI.ZeroTemperatureSK.compactDifferenceRate_family line 76
10. def OAI.ZeroTemperatureSK.differenceField line 83