OAI/Probability/SKSupport/Backward/BackwardJointBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ZeroTemperatureSK.Heat.backward_joint_bound line 18
2. lemma OAI.ZeroTemperatureSK.Heat.deriv_varianceLogHeat_tilted line 36
3. lemma OAI.ZeroTemperatureSK.Heat.backward_gradient_joint_bound line 54
4. lemma OAI.ZeroTemperatureSK.Heat.continuousOn_of_joint_bound line 67
5. lemma OAI.ZeroTemperatureSK.Heat.continuousOn_moving_heat line 86
6. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_backward_curve line 120
7. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_moving_backward_heat line 133