OAI/Probability/SKSupport/Control/FiniteContinuity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ZeroTemperatureSK.Heat.finiteValue_time_bound line 12
2. lemma OAI.ZeroTemperatureSK.Heat.finiteValue_joint_bound line 70
3. lemma OAI.ZeroTemperatureSK.Heat.finiteValue_continuousOn line 84
4. def OAI.ZeroTemperatureSK.Heat.finiteRate line 101
5. lemma OAI.ZeroTemperatureSK.Heat.measurable_finiteRate line 104
6. lemma OAI.ZeroTemperatureSK.Heat.finiteRate_bounded line 110
7. lemma OAI.ZeroTemperatureSK.Heat.intervalIntegrable_finiteRate line 124
8. lemma OAI.ZeroTemperatureSK.Heat.finiteRate_head line 133
9. lemma OAI.ZeroTemperatureSK.Heat.finiteRate_tail line 144
10. lemma OAI.ZeroTemperatureSK.Heat.integral_finiteRate_tail line 150
11. lemma OAI.ZeroTemperatureSK.Heat.backward_integral_rate line 160
12. theorem OAI.ZeroTemperatureSK.Heat.finiteValue_integral_rate line 178